Making occupation constraint part of the element

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 1b1fad69dd4f6ef3c2610a4e7a572ab4293bff74..653905886bc0755c798b5904be5628198c8a13af 100755 (executable)
--- a/hexiom/csolverHexiom.py
+++ b/hexiom/csolverHexiom.py
@@ -73,7 +73,6 @@ class RuleSet(object):
         self.vsets_by_name = {}
         self.csolver = csolver
         self.csolverlb= csolverlb
-        self.next_free_variable = 1
 
     class VariableSet(object):
         def __init__(self, ruleset, name, csolverlb, csolver, dims):
@@ -93,9 +92,6 @@ class RuleSet(object):
                 raise Exception('repeated name %s'%name)
             ruleset.vsets_by_name[name] = self
             
-            self.first_variable = self.ruleset.next_free_variable
-            self.ruleset.next_free_variable += self.size
-            
             self.csvars = [csolverlb.getBooleanVar(csolver, c_uint(getType(name))) for i in range(self.size)]
             self.csolverlb = csolverlb
             self.csolver = csolver
@@ -509,17 +505,26 @@ def read_input(fil):
 def generateElements(csolverlb, csolver, slot_range, value_range):
     elems = []
     for slot in range(slot_range[0], slot_range[-1]+1):
-        s1 = [ i for i in range(value_range[0],value_range[-1]+1)]
+        s1 = [ i for i in range(value_range[0],value_range[-1]+2)]
         set1 = (c_long* len(s1))(*s1)
         s1 = csolverlb.createSet(csolver, c_uint(11), set1, c_uint(len(s1)))
         e1 = csolverlb.getElementVar(csolver,s1)
-#         csolverlb.mustHaveValue(csolver, e1)
+        csolverlb.mustHaveValue(csolver, e1)
         elems.append(e1)
     return elems
 
 def Placement(csolverlb, csolver, elems, m, n):
     e1 = elems[m]
-    e2 = csolverlb.getElementConst(csolver, c_uint(12), n)
+    e2 = csolverlb.getElementConst(csolver, c_uint(12), n+1)
+    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 Occupied(csolverlb, csolver, elems, m):
+    e1 = elems[m]
+    e2 = csolverlb.getElementConst(csolver, c_uint(12), 0)
     equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS))
     inp = [e1,e2]
     inputs = (c_void_p*len(inp))(*inp)
@@ -556,7 +561,7 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
 #     Placement = ruleset.VarSet('P', [slot_range, value_range])
     elems = generateElements(csolverlb, csolver, slot_range, value_range)
     # (m) = is the m-th tile occupied?
-    Occupied = ruleset.VarSet('O', csolverlb, csolver, [slot_range])
+#     Occupied = ruleset.VarSet('O', csolverlb, csolver, [slot_range])
 
     # (m)(k,i) = m-th slot has k occupied slots among its first i neighbours
     NeighbourPartialSum = []
@@ -579,13 +584,13 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
         replaceWithElemConst(csolverlb, csolver, elems, m, n) 
           
     for m in board_input.blocked_positions:
-        csolverlb.addConstraint(csolver, (-Occupied(m)).getConstraint() )
+        csolverlb.addConstraint(csolver, (-Occupied(csolverlb, csolver, elems, m)).getConstraint() )
 
     print 'Creating tile placement rules...'
     rules =[]
     for m in topology.ps:
         csolverlb.addConstraint(csolver, BruteForceOnlyOne(csolverlb, csolver,
-            [-Occupied(m)] + [+Placement(csolverlb, csolver, elems,m,n) for n in range(7)]
+            [-Occupied(csolverlb, csolver, elems, m)] + [+Placement(csolverlb, csolver, elems,m,n) for n in range(7)]
         ).getConstraint())
 
     adj_graph = topology.pos_adjacency_graph()
@@ -606,13 +611,13 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
 
         csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver,
             NPSum, NSum,
-            [+Occupied(v) for v in adj_graph[m]],
+            [+Occupied(csolverlb, csolver, elems, v) for v in adj_graph[m]],
             None
         ).getConstraint())
 
         for n in range(0, nvs+1):
             csolverlb.addConstraint(csolver, Implies(csolverlb, csolver,
-                Occupied(m),
+                Occupied(csolverlb, csolver, elems, m),
                 Equivalent(csolverlb, csolver, +Placement(csolverlb, csolver, elems,m,n), +NSum(n) )
             ).getConstraint())
         
@@ -633,7 +638,7 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
 
     csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver,
         EmptyPartialSum, EmptySum,
-        [ -Occupied(m) for m in topology.ps ],
+        [ -Occupied(csolverlb, csolver, elems, m) for m in topology.ps ],
         empty_count + 1
     ).getConstraint())
 
@@ -675,7 +680,7 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
     def vars_from_sim(ms):
         vs = []
         for m in ms:
-            vs.append( +Occupied(m) )
+            vs.append( +Occupied(csolverlb, csolver, elems, m) )
             vs.extend([ +Placement(csolverlb, csolver, elems,m,n) for n in range(0, 7) ])
         return vs
 
@@ -707,14 +712,13 @@ def print_board_from_assignments(csolverlb, csolver, formulation):
     ruleset = formulation.ruleset
     topology = formulation.topology
     elems = formulation.elems
-    O = ruleset.get_varset_by_name('O')
 
     layout = [None for p in topology.ps]
     
-    for i, bool in enumerate(O.csvars):
-        if csolverlb.getBooleanValue(csolver, bool):
-            e = elems[i]
-            layout[i]= csolverlb.getElementValue(csolver, e)
+    for i, e in enumerate(elems):
+        elem= csolverlb.getElementValue(csolver, e)
+        if elem != 0:
+            layout[i]= elem 
 
     print '=== Initial input: ==='
     formulation.board_input.print_to_stdout()