9
9
import sys
10
10
import copy
11
11
from cpmpy import *
12
- from cpmpy .solver_interfaces .ortools import CPMpyORTools
13
- from cpmpy .model_tools .get_variables import vars_expr
14
- from cpmpy .model_tools .flatten_model import flatten_constraint
12
+ from cpmpy .solvers .ortools import CPM_ortools
13
+ from cpmpy .transformations .get_variables import get_variables
14
+ from cpmpy .transformations .flatten_model import flatten_constraint
15
15
16
16
def main ():
17
- x , y = IntVar (- 9 ,9 , shape = 2 )
18
- m = Model ([
17
+ x , y = intvar (- 9 ,9 , shape = 2 )
18
+ m = Model (
19
19
x < 0 ,
20
20
x < 1 ,
21
21
x > 2 ,
22
22
(x + y > 0 ) | (y < 0 ),
23
23
(y >= 0 ) | (x >= 0 ),
24
24
(y < 0 ) | (x < 0 ),
25
25
(y > 0 ) | (x < 0 ),
26
- alldifferent ([ x ,y ] ) # invalid for musx_assum
27
- ] )
26
+ AllDifferent ( x ,y ) # invalid for musx_assum
27
+ )
28
28
assert (m .solve () is False )
29
29
30
30
mus = musx (m .constraints , [], verbose = True )
@@ -49,7 +49,7 @@ def musx(soft_constraints, hard_constraints=[], verbose=False):
49
49
# see if solver supports reification of 'con'
50
50
try :
51
51
m = Model ([BoolVar ().implies (con )])
52
- CPMpyORTools (m ).solve ()
52
+ CPM_ortools (m ).solve ()
53
53
# it did
54
54
soft_assum .append (con )
55
55
except :
@@ -82,7 +82,7 @@ def musx_pure(soft_constraints, hard_constraints=[], verbose=False):
82
82
# this will favor MUS with few variables per constraint,
83
83
# and will remove large constraints earlier which may speed it up
84
84
# TODO: count nr of subexpressions? (generalisation of nr of vars)
85
- soft_constraints = sorted (soft_constraints , key = lambda c : - len (vars_expr (c )))
85
+ soft_constraints = sorted (soft_constraints , key = lambda c : - len (get_variables (c )))
86
86
87
87
# small optimisation: pre-flatten all constraints once
88
88
# so it needs not be done over-and-over in solving
@@ -97,12 +97,12 @@ def musx_pure(soft_constraints, hard_constraints=[], verbose=False):
97
97
mus_idx = [] # index into 'soft_constraints' that belong to the MUS
98
98
99
99
# init solver with hard constraints
100
- #s_base = CPMpyORTools (Model(hard))
100
+ #s_base = CPM_ortools (Model(hard))
101
101
m_base = Model (hard )
102
102
for i in range (len (soft_constraints )):
103
103
#s_without_i = copy.deepcopy(s_base) # deep copy solver state
104
104
# add all other remaining (flattened) constraints
105
- s_without_i = CPMpyORTools (m_base )
105
+ s_without_i = CPM_ortools (m_base )
106
106
s_without_i += soft [i + 1 :]
107
107
108
108
if s_without_i .solve ():
@@ -148,7 +148,7 @@ def musx_assum(soft_constraints, hard_constraints=[], verbose=False):
148
148
indmap = dict ((v ,i ) for (i ,v ) in enumerate (ind ))
149
149
150
150
# make solver once, check that it is unsat and start from core
151
- assum_solver = CPMpyORTools (assum_model )
151
+ assum_solver = CPM_ortools (assum_model )
152
152
if assum_solver .solve (assumptions = ind ):
153
153
if verbose :
154
154
print ("Unexpectedly, the model is SAT" )
0 commit comments