cvc5 SMT solver

cpmpy/solvers/__init__.py

@@ -36,6 +36,7 @@
         gurobi
         exact
         z3
+        cvc5
         pysat
         pysdd
         pindakaas

cpmpy/solvers/utils.py

@@ -32,6 +32,7 @@
 from .cplex import CPM_cplex
 from .pindakaas import CPM_pindakaas
 from .hexaly import CPM_hexaly
+from .cvc5 import CPM_cvc5
 
 def param_combinations(all_params, remaining_keys=None, cur_params=None):
     """
@@ -87,7 +88,8 @@ def base_solvers(cls):
                 ("cpo", CPM_cpo),
                 ("cplex", CPM_cplex),
                 ("pindakaas", CPM_pindakaas),
-                ("hexaly", CPM_hexaly)
+                ("hexaly", CPM_hexaly),
+                ("cvc5", CPM_cvc5)
                ]
 
     @classmethod

docs/api/solvers/cvc5.rst

@@ -0,0 +1,7 @@
+CPMpy cvc5 interface (:mod:`cpmpy.solvers.cvc5`)
+=====================================================
+
+.. automodule:: cpmpy.solvers.cvc5
+    :members:
+    :undoc-members:
+    :inherited-members:

docs/index.rst

@@ -60,6 +60,11 @@ Supported solvers
      - SAT ASAT ISAT - OPT IOPT
      - pip
      - 
+   * - :doc:`cvc5 <api/solvers/cvc5>`
+     - SMT
+     - SAT
+     - pip
+     - 
    * - :doc:`Gurobi <api/solvers/gurobi>`
      - ILP
      - SAT - OPT IOPT - PAR

gbd_tst.py

@@ -0,0 +1,41 @@
+import cpmpy as cp
+from cpmpy.tools.dataset.problem.jsplib import JSPLibDataset
+from cpmpy.tools.jsplib.parser import read_jsplib, _parse_jsplib, _model_jsplib
+from cpmpy.tools.dimacs import write_dimacs
+import tqdm
+
+from cpmpy.transformations.int2bool import int2bool
+from cpmpy.transformations.decompose_global import decompose_in_tree
+from cpmpy.transformations.flatten_model import flatten_constraint, flatten_model
+from cpmpy.transformations.linearize import linearize_constraint, only_positive_bv, only_positive_coefficients
+from cpmpy.transformations.normalize import simplify_boolean, toplevel_list
+from cpmpy.transformations.reification import only_bv_reifies, only_implies
+
+if __name__ == "__main__":
+
+    dataset = JSPLibDataset(root=".", download=True)
+    for instance, metadata in tqdm.tqdm(dataset):
+        model = read_jsplib(instance)
+
+        cnf_model = cp.Model()
+        csemap = {}
+        encoding = "auto"
+        ivarmap = dict()
+        for cpm_expr in model.constraints:
+            cpm_cons = toplevel_list(cpm_expr)
+            cpm_cons = decompose_in_tree(cpm_cons, csemap=csemap)
+            cpm_cons = simplify_boolean(cpm_cons)
+            cpm_cons = flatten_constraint(cpm_cons, csemap=csemap)  # flat normal form
+            cpm_cons = only_bv_reifies(cpm_cons, csemap=csemap)
+            cpm_cons = only_implies(cpm_cons, csemap=csemap)
+            cpm_cons = linearize_constraint(cpm_cons, csemap=csemap)  # the core of the MIP-linearization
+            cpm_cons = int2bool(cpm_cons, ivarmap, encoding=encoding)
+            cpm_cons = only_positive_coefficients(cpm_cons)
+            cpm_cons = only_positive_bv(cpm_cons, csemap=csemap)
+            cnf_model += (cpm_cons)
+
+        cnf_model = flatten_model(cnf_model)
+
+        fname = instance + ".dimacs.cnf"
+        write_dimacs(cnf_model, fname)
+

setup.py

@@ -33,6 +33,7 @@ def get_version(rel_path):
     "pumpkin": ["pumpkin-solver>=0.2.1"],
     "pindakaas": ["pindakaas>=0.2.1"],
     "cplex": ["docplex", "cplex"],
+    "cvc5": ["cvc5"],
 }
 solver_dependencies["all"] = list({pkg for group in solver_dependencies.values() for pkg in group}) 
 

tests/test_solverinterface.py

@@ -142,6 +142,9 @@ def test_minimize(solver_name):
 
     ivar = intvar(1, 10)
 
+    if solver_name == "cvc5":
+        return # TODO: should be skipped instead, need to rework pytest decorators / markers
+
     try:
         solver.minimize(ivar)
     except NotImplementedError:
@@ -157,7 +160,7 @@ def test_minimize(solver_name):
 def test_maximize(solver_name):
     """Test maximize functionality"""
     solver_class = SolverLookup.lookup(solver_name)
-    if solver_name == "z3":
+    if solver_name == "cvc5":
         return
     solver = solver_class() if solver_name != "z3" else solver_class(subsolver="opt")
 
@@ -303,6 +306,9 @@ def test_has_objective(solver_name):
     except NotImplementedError:
         # Solver doesn't support objectives
         assert not solver.has_objective()
+    except NotSupportedError:
+        # Solver doesn't support objectives
+        assert not solver.has_objective()
 
 @pytest.mark.parametrize("solver_name", SOLVERNAMES)
 @skip_on_missing_pblib(skip_on_exception_only=True)

tests/test_solvers.py

@@ -13,6 +13,7 @@
 from cpmpy.solvers.pindakaas import CPM_pindakaas
 from cpmpy.solvers.solver_interface import ExitStatus
 from cpmpy.solvers.z3 import CPM_z3
+from cpmpy.solvers.cvc5 import CPM_cvc5
 from cpmpy.solvers.minizinc import CPM_minizinc
 from cpmpy.solvers.gurobi import CPM_gurobi
 from cpmpy.solvers.exact import CPM_exact
@@ -493,6 +494,38 @@ def test_z3(self):
         s = cp.SolverLookup.get("z3", m)
         self.assertFalse(s.solve()) # upgrade z3 with pip install --upgrade z3-solver
 
+    @pytest.mark.skipif(not CPM_cvc5.supported(),
+                    reason="cvc5 not installed")
+    def test_cvc5(self):
+        bv = cp.boolvar(shape=3)
+        iv = cp.intvar(0, 9, shape=3)
+        # circular 'bigger then', UNSAT
+        m = cp.Model([
+            bv[0].implies(iv[0] > iv[1]),
+            bv[1].implies(iv[1] > iv[2]),
+            bv[2].implies(iv[2] > iv[0])
+        ])
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertFalse(s.solve(assumptions=bv))
+
+        m = cp.Model(~(iv[0] != iv[1]))
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertTrue(s.solve())
+
+        m = cp.Model((iv[0] == 0) & ((iv[0] != iv[1]) == 0))
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertTrue(s.solve())
+
+        m = cp.Model([~bv, ~((iv[0] + abs(iv[1])) == sum(iv))])
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertTrue(s.solve())
+
+        x = cp.intvar(0, 1)
+        m = cp.Model((x >= 0.1) & (x != 1))
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertFalse(s.solve()) # TODO: same bug as z3?
+
+
     def test_pow(self):
         iv1 = cp.intvar(2,9)
         for i in [0,1,2]:
@@ -956,8 +989,8 @@ def test_incremental_assumptions(self, solver):
         if "assumptions" not in inspect.signature((s.solve)).parameters:
             return # solver does not support solving under assumptions
 
-        if solver == "pysdd":
-            return # not implemented in pysdd
+        if solver == "pysdd" or solver == "cvc5":
+            return # not implemented in pysdd or cvc5
 
         s += x | y
         assert s.solve(assumptions=[x])