From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Wed, 8 Aug 2018 19:11:49 +0000 (-0700)
Subject: Fixing the hexiom bug for UNARY encoding
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=58ac4c2b5a13137edf707f7bbc812066d300c11a;p=Benchmarks_CSolver.git

Fixing the hexiom bug for UNARY encoding
---

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 1ebec590..30a93b30 100755
--- a/hexiom/csolverHexiom.py
+++ b/hexiom/csolverHexiom.py
@@ -530,11 +530,11 @@ 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
 
@@ -609,7 +609,7 @@ 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( m)).getConstraint() )
 
     print 'Creating tile placement rules...'
     rules =[]
@@ -780,7 +780,8 @@ def main():
    
     print '=== Done! Calling CSolver solver now ==='
     if len(sys.argv) > 2 and sys.argv[-1] == "--dump":
-        csolverlb.serialize(csolver)
+         csolverlb.serialize(csolver)
+#     csolverlb.printConstraints(csolver)
     if csolverlb.solve(csolver) != 1:
         print '*** Got UNSAT result! ***'
         sys.exit(1)