Performance improvement ...

[Benchmarks_CSolver.git] / hexiom / csolverHexiom.py

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 30a93b30d0a92b458fa2e64a3a8889afd971a09b..ee7f2020c24f6695ed5a163215a2fde1b4267ddf 100755 (executable)
--- 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])