projects
/
Benchmarks_CSolver.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
8606a2c
)
Making occupation constraint part of the element
author
Hamed Gorjiara
<hgorjiar@uci.edu>
Wed, 1 Aug 2018 08:01:17 +0000
(
01:01
-0700)
committer
Hamed Gorjiara
<hgorjiar@uci.edu>
Wed, 1 Aug 2018 08:01:17 +0000
(
01:01
-0700)
hexiom/csolverHexiom.py
patch
|
blob
|
history
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.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):
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
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
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):
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)
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]
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)
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?
# 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 = []
# (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:
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,
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()
).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,
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,
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())
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,
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())
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:
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
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
ruleset = formulation.ruleset
topology = formulation.topology
elems = formulation.elems
- O = ruleset.get_varset_by_name('O')
layout = [None for p in topology.ps]
layout = [None for p in topology.ps]
- for i,
bool in enumerate(O.csvar
s):
- if csolverlb.getBooleanValue(csolver, bool):
- e = elems[i]
- layout[i]=
csolverlb.getElementValue(csolver, e)
+ for i,
e in enumerate(elem
s):
+ elem= csolverlb.getElementValue(csolver, e)
+ if elem != 0:
+ layout[i]=
elem
print '=== Initial input: ==='
formulation.board_input.print_to_stdout()
print '=== Initial input: ==='
formulation.board_input.print_to_stdout()