From 58ac4c2b5a13137edf707f7bbc812066d300c11a Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 8 Aug 2018 12:11:49 -0700 Subject: [PATCH] Fixing the hexiom bug for UNARY encoding --- hexiom/csolverHexiom.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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) -- 2.34.1