From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Wed, 8 Aug 2018 20:24:19 +0000 (-0700)
Subject: Performance improvement ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=60449ef6b77f5398bf4449e033a138579de77bf2;p=Benchmarks_CSolver.git

Performance improvement ...
---

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 30a93b30..ee7f2020 100755
--- a/hexiom/csolverHexiom.py
+++ b/hexiom/csolverHexiom.py
@@ -538,6 +538,15 @@ def generateElements(csolverlb, csolver, slot_range, value_range):
         elems.append(e1)
     return elems
 
+def lessThanValue(csolverlb, csolver, elems, m, n):
+    e1 = elems[m]
+    e2 = csolverlb.getElementConst(csolver, c_uint(12), n)
+    equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_LT))
+    inp = [e1,e2]
+    inputs = (c_void_p*len(inp))(*inp)
+    b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2))
+    return CSConstraint(csolverlb, csolver, b)
+
 def Placement(csolverlb, csolver, elems, m, n):
     e1 = elems[m]
     e2 = csolverlb.getElementConst(csolver, c_uint(12), n)
@@ -547,14 +556,14 @@ def Placement(csolverlb, csolver, elems, m, n):
     b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2))
     return CSConstraint(csolverlb, csolver, b)
 
-# def Occupied(csolverlb, csolver, elems, m):
-#     e1 = elems[m]
-#     e2 = csolverlb.getElementConst(csolver, c_uint(12), 7)
-#     equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS))
-#     inp = [e1,e2]
-#     inputs = (c_void_p*len(inp))(*inp)
-#     b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2))
-#     return CSConstraint(csolverlb, csolver, b)
+def emptyValue(csolverlb, csolver, elems, m):
+    e1 = elems[m]
+    e2 = csolverlb.getElementConst(csolver, c_uint(12), 7)
+    equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS))
+    inp = [e1,e2]
+    inputs = (c_void_p*len(inp))(*inp)
+    b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2))
+    return CSConstraint(csolverlb, csolver, b)
     
 def replaceWithElemConst(csolverlb, solver, elems, m, n):
     elems[m] = csolverlb.getElementConst(solver, c_uint(10), n)
@@ -646,9 +655,10 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
                 Equivalent(csolverlb, csolver, +Placement(csolverlb, csolver, elems,m,n), +NSum(n) )
             ).getConstraint())
         
-        for n in range(nvs+1, 7):
-            csolverlb.addConstraint(csolver, (-Placement(csolverlb, csolver, elems,m,n)).getConstraint() )
-
+#         for n in range(nvs+1, 7):
+#             csolverlb.addConstraint(csolver, (-Placement(csolverlb, csolver, elems,m,n)).getConstraint() )
+        constr =[lessThanValue(csolverlb, csolver, elems, m, nvs+1), emptyValue(csolverlb, csolver, elems, m)]
+        csolverlb.addConstraint(csolver, Or(csolverlb, csolver, constr).getConstraint())
     print 'Creating constraints for the number of empty cell...'
 
     empty_count = len(topology.ps) - sum([c for (_,c) in board_input.counts])