Merge branch 'master' into remove-unused-parts

# Conflicts:
#	cpmpy/transformations/linearize.py

cpmpy/solvers/exact.py

@@ -33,10 +33,12 @@
 from ..transformations.get_variables import get_variables
 from ..transformations.decompose_global import decompose_in_tree
 from ..transformations.linearize import linearize_constraint, only_positive_bv
-from ..transformations.reification import only_bv_implies, reify_rewrite
+from ..transformations.reification import only_implies, reify_rewrite, only_bv_reifies
 from ..transformations.normalize import toplevel_list
 from ..expressions.globalconstraints import DirectConstraint
 from ..exceptions import NotSupportedError
+from ..expressions.utils import flatlist
+
 import numpy as np
 import numbers
 
@@ -407,7 +409,8 @@ def transform(self, cpm_expr):
         cpm_cons = flatten_constraint(cpm_cons)  # flat normal form
         cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum']))  # constraints that support reification
         cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum"]))  # supports >, <, !=
-        cpm_cons = only_bv_implies(cpm_cons)  # anything that can create full reif should go above...
+        cpm_cons = only_bv_reifies(cpm_cons)
+        cpm_cons = only_implies(cpm_cons)  # anything that can create full reif should go above...
         cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum"}))  # the core of the MIP-linearization
         cpm_cons = only_positive_bv(cpm_cons)  # after linearisation, rewrite ~bv into 1-bv
         return cpm_cons
@@ -481,7 +484,7 @@ def __add__(self, cpm_expr_orig):
 
         # transform and post the constraints
         for cpm_expr in self.transform(cpm_expr_orig):
-            # Comparisons: only numeric ones as 'only_bv_implies()' has removed the '==' reification for Boolean expressions
+            # Comparisons: only numeric ones as 'only_implies()' has removed the '==' reification for Boolean expressions
             # numexpr `comp` bvar|const
             if isinstance(cpm_expr, Comparison):
                 lhs, rhs = cpm_expr.args
@@ -588,6 +591,10 @@ def solution_hint(self, cpm_vars, vals):
         :param cpm_vars: list of CPMpy variables
         :param vals: list of (corresponding) values for the variables
         """
+
+        cpm_vars = flatlist(cpm_vars)
+        vals = flatlist(vals)
+        assert (len(cpm_vars) == len(vals)), "Variables and values must have the same size for hinting"
         try:
             pkg_resources.require("exact>=1.1.5")
             self.xct_solver.setSolutionHints(self.solver_vars(cpm_vars), vals)

cpmpy/solvers/gurobi.py

@@ -36,7 +36,7 @@
 from ..transformations.get_variables import get_variables
 from ..transformations.linearize import linearize_constraint, only_positive_bv
 from ..transformations.normalize import toplevel_list
-from ..transformations.reification import only_bv_implies, reify_rewrite
+from ..transformations.reification import only_implies, reify_rewrite, only_bv_reifies
 
 try:
     import gurobipy as gp
@@ -273,7 +273,8 @@ def transform(self, cpm_expr):
         cpm_cons = flatten_constraint(cpm_cons)  # flat normal form
         cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum']))  # constraints that support reification
         cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"]))  # supports >, <, !=
-        cpm_cons = only_bv_implies(cpm_cons)  # anything that can create full reif should go above...
+        cpm_cons = only_bv_reifies(cpm_cons)
+        cpm_cons = only_implies(cpm_cons)  # anything that can create full reif should go above...
         cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","sub","min","max","mul","abs","pow","div"}))  # the core of the MIP-linearization
         cpm_cons = only_positive_bv(cpm_cons)  # after linearization, rewrite ~bv into 1-bv
         return cpm_cons
@@ -304,7 +305,7 @@ def __add__(self, cpm_expr_orig):
       # transform and post the constraints
       for cpm_expr in self.transform(cpm_expr_orig):
 
-        # Comparisons: only numeric ones as 'only_bv_implies()' has removed the '==' reification for Boolean expressions
+        # Comparisons: only numeric ones as 'only_implies()' has removed the '==' reification for Boolean expressions
         # numexpr `comp` bvar|const
         if isinstance(cpm_expr, Comparison):
             lhs, rhs = cpm_expr.args

cpmpy/solvers/minizinc.py

@@ -391,9 +391,8 @@ def transform(self, cpm_expr):
         cpm_cons = toplevel_list(cpm_expr)
         supported = {"min", "max", "abs", "element", "count", "alldifferent", "alldifferent_except0", "allequal",
                      "inverse", "ite" "xor", "table", "cumulative", "circuit", "gcc"}
-        cpm_cons = decompose_in_tree(cpm_cons, supported)
+        return decompose_in_tree(cpm_cons, supported)
 
-        return simplify_boolean(cpm_cons)
 
     def __add__(self, cpm_expr):
         """

cpmpy/solvers/ortools.py

@@ -32,12 +32,12 @@
 from ..expressions.globalconstraints import DirectConstraint
 from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, boolvar
 from ..expressions.globalconstraints import GlobalConstraint
-from ..expressions.utils import is_num, is_any_list, eval_comparison
+from ..expressions.utils import is_num, is_any_list, eval_comparison, flatlist
 from ..transformations.decompose_global import decompose_in_tree
 from ..transformations.get_variables import get_variables
 from ..transformations.flatten_model import flatten_constraint, flatten_objective
 from ..transformations.normalize import toplevel_list
-from ..transformations.reification import only_bv_implies, reify_rewrite
+from ..transformations.reification import only_implies, reify_rewrite, only_bv_reifies
 from ..transformations.comparison import only_numexpr_equality
 
 class CPM_ortools(SolverInterface):
@@ -334,7 +334,8 @@ def transform(self, cpm_expr):
         cpm_cons = flatten_constraint(cpm_cons)  # flat normal form
         cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum']))  # constraints that support reification
         cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"]))  # supports >, <, !=
-        cpm_cons = only_bv_implies(cpm_cons) # everything that can create
+        cpm_cons = only_bv_reifies(cpm_cons)
+        cpm_cons = only_implies(cpm_cons)  # everything that can create
                                              # reified expr must go before this
         return cpm_cons
 
@@ -408,7 +409,7 @@ def _post_constraint(self, cpm_expr, reifiable=False):
                 raise NotImplementedError("Not a known supported ORTools Operator '{}' {}".format(
                         cpm_expr.name, cpm_expr))
 
-        # Comparisons: only numeric ones as the `only_bv_implies()` transformation
+        # Comparisons: only numeric ones as the `only_implies()` transformation
         # has removed the '==' reification for Boolean expressions
         # numexpr `comp` bvar|const
         elif isinstance(cpm_expr, Comparison):
@@ -520,6 +521,10 @@ def solution_hint(self, cpm_vars, vals):
         :param vals: list of (corresponding) values for the variables
         """
         self.ort_model.ClearHints() # because add just appends
+
+        cpm_vars = flatlist(cpm_vars)
+        vals = flatlist(vals)
+        assert (len(cpm_vars) == len(vals)), "Variables and values must have the same size for hinting"
         for (cpm_var, val) in zip(cpm_vars, vals):
             self.ort_model.AddHint(self.solver_var(cpm_var), val)
 

cpmpy/solvers/pysat.py

@@ -34,12 +34,13 @@
 from ..expressions.core import Expression, Comparison, Operator, BoolVal
 from ..expressions.variables import _BoolVarImpl, NegBoolView, boolvar
 from ..expressions.globalconstraints import DirectConstraint
-from ..expressions.utils import is_any_list, is_int
+from ..expressions.utils import is_int, flatlist
 from ..transformations.decompose_global import decompose_in_tree
 from ..transformations.get_variables import get_variables
 from ..transformations.flatten_model import flatten_constraint
 from ..transformations.normalize import toplevel_list
-from ..transformations.reification import only_bv_implies
+from ..transformations.reification import only_implies, only_bv_reifies
+
 
 class CPM_pysat(SolverInterface):
     """
@@ -230,7 +231,8 @@ def transform(self, cpm_expr):
         cpm_cons = toplevel_list(cpm_expr)
         cpm_cons = decompose_in_tree(cpm_cons)
         cpm_cons = flatten_constraint(cpm_cons)
-        cpm_cons = only_bv_implies(cpm_cons)
+        cpm_cons = only_bv_reifies(cpm_cons)
+        cpm_cons = only_implies(cpm_cons)
         return cpm_cons
 
     def __add__(self, cpm_expr_orig):
@@ -258,7 +260,7 @@ def __add__(self, cpm_expr_orig):
         if cpm_expr.name == 'or':
             self.pysat_solver.add_clause(self.solver_vars(cpm_expr.args))
 
-        elif cpm_expr.name == '->':  # BV -> BE only thanks to only_bv_implies
+        elif cpm_expr.name == '->':  # BV -> BE only thanks to only_bv_reifies
             a0,a1 = cpm_expr.args
 
             # BoolVar() -> BoolVar()
@@ -314,6 +316,11 @@ def solution_hint(self, cpm_vars, vals):
         :param cpm_vars: list of CPMpy variables
         :param vals: list of (corresponding) values for the variables
         """
+
+        cpm_vars = flatlist(cpm_vars)
+        vals = flatlist(vals)
+        assert (len(cpm_vars) == len(vals)), "Variables and values must have the same size for hinting"
+
         literals = []
         for (cpm_var, val) in zip(cpm_vars, vals):
             lit = self.solver_var(cpm_var)

cpmpy/solvers/z3.py

@@ -250,7 +250,6 @@ def transform(self, cpm_expr):
         cpm_cons = toplevel_list(cpm_expr)
         supported = {"alldifferent", "xor", "ite"}  # z3 accepts these reified too
         cpm_cons = decompose_in_tree(cpm_cons, supported, supported)
-        cpm_cons = simplify_boolean(cpm_cons)
         return cpm_cons
 
     def __add__(self, cpm_expr):

cpmpy/transformations/linearize.py

@@ -39,6 +39,7 @@
 """
 import copy
 import numpy as np
+from cpmpy.transformations.normalize import toplevel_list
 
 from .flatten_model import flatten_constraint, get_or_make_var
 from .get_variables import get_variables
@@ -108,48 +109,22 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False):
             if lhs.name == "sub":
                 # convert to wsum
                 lhs = sum([1 * lhs.args[0] + -1 * lhs.args[1]])
+                cpm_expr = eval_comparison(cpm_expr.name, lhs, rhs)
 
             # linearize unsupported operators
             elif isinstance(lhs, Operator) and lhs.name not in supported: # TODO: add mul, (abs?), (mod?), (pow?)
 
                 if lhs.name == "mul" and is_num(lhs.args[0]):
                     lhs = Operator("wsum",[[lhs.args[0]], [lhs.args[1]]])
+                    cpm_expr = eval_comparison(cpm_expr.name, lhs, rhs)
                 else:
                     raise TransformationNotImplementedError(f"lhs of constraint {cpm_expr} cannot be linearized, should be any of {supported | set(['sub'])} but is {lhs}. Please report on github")
 
             elif isinstance(lhs, GlobalConstraint) and lhs.name not in supported:
                 raise ValueError("Linearization of `lhs` not supported, run `cpmpy.transformations.decompose_global.decompose_global() first")
 
-            if is_num(lhs) or isinstance(lhs, _NumVarImpl) or (isinstance(lhs, Operator) and lhs.name in {"sum","wsum"}):
-                # bring all vars to lhs
-                if isinstance(rhs, _NumVarImpl):
-                    if isinstance(lhs, Operator) and lhs.name == "sum":
-                        lhs, rhs = sum([1 * a for a in lhs.args]+[-1 * rhs]), 0
-                    elif isinstance(lhs, _NumVarImpl) or (isinstance(lhs, Operator) and lhs.name == "wsum"):
-                        lhs, rhs = lhs + -1*rhs, 0
-                    else:
-                        raise ValueError(f"unexpected expression on lhs of expression, should be sum,wsum or intvar but got {lhs}")
-
-                assert not is_num(lhs), "lhs cannot be an integer at this point!"
-                # bring all const to rhs
-                if lhs.name == "sum":
-                    new_args = []
-                    for i, arg in enumerate(lhs.args):
-                        if is_num(arg):
-                            rhs -= arg
-                        else:
-                            new_args.append(arg)
-                    lhs = Operator("sum", new_args)
-
-                elif lhs.name == "wsum":
-                    new_weights, new_args = [],[]
-                    for i, (w, arg) in enumerate(zip(*lhs.args)):
-                        if is_num(arg):
-                            rhs -= w * arg
-                        else:
-                            new_weights.append(w)
-                            new_args.append(arg)
-                    lhs = Operator("wsum",[new_weights, new_args])
+            [cpm_expr] = canonical_comparison([cpm_expr])  # just transforms the constraint, not introducing new ones
+            lhs, rhs = cpm_expr.args
 
             # now fix the comparisons themselves
             if cpm_expr.name == "<":
@@ -213,7 +188,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False):
 
             newlist += constraints
 
-        elif isinstance(cpm_expr, DirectConstraint):
+        elif isinstance(cpm_expr, (DirectConstraint, BoolVal)):
             newlist.append(cpm_expr)
 
         elif isinstance(cpm_expr, GlobalConstraint) and cpm_expr.name not in supported:
@@ -277,4 +252,74 @@ def only_positive_bv(lst_of_expr):
         else:
             raise Exception(f"{cpm_expr} is not linear or is not supported. Please report on github")
 
-    return newlist
+    return newlist
+
+def canonical_comparison(lst_of_expr):
+
+    lst_of_expr = toplevel_list(lst_of_expr)               # ensure it is a list
+
+    newlist = []
+    for cpm_expr in lst_of_expr:
+
+        if isinstance(cpm_expr, Operator) and cpm_expr.name == '->':    # half reification of comparison
+            lhs, rhs = cpm_expr.args
+            if isinstance(rhs, Comparison):
+                rhs = canonical_comparison(rhs)[0]
+                newlist.append(lhs.implies(rhs))
+            elif isinstance(lhs, Comparison):
+                lhs = canonical_comparison(lhs)[0]
+                newlist.append(lhs.implies(rhs))
+
+        if isinstance(cpm_expr, Comparison):
+            lhs, rhs = cpm_expr.args
+            if isinstance(lhs, Comparison) and cpm_expr.name == "==":  # reification of comparison
+                lhs = canonical_comparison(lhs)[0]
+            elif is_num(lhs) or isinstance(lhs, _NumVarImpl) or (isinstance(lhs, Operator) and lhs.name in {"sum", "wsum"}):
+                # bring all vars to lhs
+                lhs2 = []
+                if isinstance(rhs, _NumVarImpl):
+                    lhs2, rhs = [-1 * rhs], 0
+                elif isinstance(rhs, Operator) and rhs.name == "sum":
+                    lhs2, rhs = [-1 * b if isinstance(b, _NumVarImpl) else 1 * b.args[0] for b in rhs.args
+                                 if isinstance(b, _NumVarImpl) or isinstance(b, Operator)], \
+                                 sum(b for b in rhs.args if is_num(b))
+                elif isinstance(rhs, Operator) and rhs.name == "wsum":
+                    lhs2, rhs = [-a * b for a, b in zip(rhs.args[0], rhs.args[1])
+                                    if isinstance(b, _NumVarImpl)], \
+                                    sum(-a * b for a, b in zip(rhs.args[0], rhs.args[1])
+                                    if not isinstance(b, _NumVarImpl))
+                if isinstance(lhs, Operator) and lhs.name == "sum":
+                    lhs, rhs = sum([1 * a for a in lhs.args] + lhs2), rhs
+                elif isinstance(lhs, _NumVarImpl) or (isinstance(lhs, Operator) and lhs.name == "wsum"):
+                    lhs, rhs = lhs + lhs2, rhs
+                else:
+                    raise ValueError(
+                        f"unexpected expression on lhs of expression, should be sum,wsum or intvar but got {lhs}")
+
+                assert not is_num(lhs), "lhs cannot be an integer at this point!"
+
+                # bring all const to rhs
+                if lhs.name == "sum":
+                    new_args = []
+                    for i, arg in enumerate(lhs.args):
+                        if is_num(arg):
+                            rhs -= arg
+                        else:
+                            new_args.append(arg)
+                    lhs = Operator("sum", new_args)
+
+                elif lhs.name == "wsum":
+                    new_weights, new_args = [], []
+                    for i, (w, arg) in enumerate(zip(*lhs.args)):
+                        if is_num(arg):
+                            rhs -= w * arg
+                        else:
+                            new_weights.append(w)
+                            new_args.append(arg)
+                    lhs = Operator("wsum", [new_weights, new_args])
+
+            newlist.append(eval_comparison(cpm_expr.name, lhs, rhs))
+        else:   # rest of expressions
+            newlist.append(cpm_expr)
+
+    return newlist