From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 30 Mar 2022 06:05:49 +0000 (+0300)
Subject: Adding some missing python API methods and tests (#8441)
X-Git-Tag: cvc5-1.0.0~127
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=92844d783c7ea7caef74862e751a9e326f8dee6b;p=cvc5.git

Adding some missing python API methods and tests (#8441)

This PR adds methods to the python API, as well as tests for the new methods and other tests for existing methods, translated from solver_black.cpp.
---

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index ae92c4a82..5cc6f1c65 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -6,6 +6,7 @@ from libcpp.map cimport map as c_map
 from libcpp.set cimport set
 from libcpp.string cimport string
 from libcpp.vector cimport vector
+from libcpp.map cimport map
 from libcpp.pair cimport pair
 from cvc5kinds cimport Kind
 from cvc5types cimport RoundingMode
@@ -245,6 +246,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Term declareSygusVar(Sort sort, const string& symbol) except +
         Term declareSygusVar(Sort sort) except +
         void addSygusConstraint(Term term) except +
+        void addSygusAssume(Term term) except +
         void addSygusInvConstraint(Term inv_f, Term pre_f, Term trans_f, Term post_f) except +
         Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort) except +
         Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort, Grammar grammar) except +
@@ -327,8 +329,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         OptionInfo getOptionInfo(const string& option) except +
         vector[Term] getUnsatAssumptions() except +
         vector[Term] getUnsatCore() except +
+        map[Term,Term] getDifficulty() except +
         Term getValue(Term term) except +
         vector[Term] getValue(const vector[Term]& terms) except +
+        Term getQuantifierElimination(const Term& q) except +
+        Term getQuantifierEliminationDisjunct(const Term& q) except +
         vector[Term] getModelDomainElements(Sort sort) except +
         bint isModelCoreSymbol(Term v) except +
         string getModel(const vector[Sort]& sorts,
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index a4c85a768..81809b564 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1602,6 +1602,20 @@ cdef class Solver:
         """
         self.csolver.addSygusConstraint(t.cterm)
 
+    def addSygusAssume(self, Term t):
+        """
+        Add a formula to the set of Sygus assumptions.
+
+        SyGuS v2:
+
+        .. code-block:: smtlib
+
+            ( assume <term> )
+
+        :param term: the formuula to add as an assumption
+        """
+        self.csolver.addSygusAssume(t.cterm)
+
     def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
         """
         Add a set of SyGuS constraints to the current state that correspond to an
@@ -1999,7 +2013,8 @@ cdef class Solver:
         return assertions
 
     def getInfo(self, str flag):
-        """Get info from the solver.
+        """
+        Get info from the solver.
 
         SMT-LIB:
 
@@ -2104,6 +2119,15 @@ cdef class Solver:
             res['modes'] = [s.decode() for s in mi.modes]
         return res
 
+    def getOptionNames(self):
+       """Get all option names that can be used with `setOption`, `getOption` and `getOptionInfo`.
+       :return: all option names
+       """
+       result = []
+       for n in self.csolver.getOptionNames():
+           result += [n.decode()]
+       return result
+
     def getUnsatAssumptions(self):
         """
         Get the set of unsat ("failed") assumptions.
@@ -2152,6 +2176,30 @@ cdef class Solver:
             core.append(term)
         return core
 
+    def getDifficulty(self):
+        """
+            Get a difficulty estimate for an asserted formula. This method is intended to be called immediately after 
+            any response to a checkSat.
+
+            .. warning:: This method is experimental and may change in future
+                         versions.
+
+            :return: a map from (a subset of) the input assertions to a real value that is an estimate of how difficult each assertion was to solver. Unmentioned assertions can be assumed to have zero difficulty.
+        """
+        diffi = {}
+        for p in self.csolver.getDifficulty():
+            k = p.first
+            v = p.second
+
+            termk = Term(self)
+            termk.cterm = k
+
+            termv = Term(self)
+            termv.cterm = v
+
+            diffi[termk] = termv
+        return diffi
+
     def getValue(self, Term t):
         """Get the value of the given term in the current model.
 
@@ -2200,6 +2248,88 @@ cdef class Solver:
         """
         return self.csolver.isModelCoreSymbol(v.cterm)
 
+    def getQuantifierElimination(self, Term term):
+        """Do quantifier elimination.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-qe <q> )
+
+        Requires a logic that supports quantifier elimination.
+        Currently, the only logics supported by quantifier elimination
+        are LRA and LIA.
+
+        .. warning:: This method is experimental and may change in future
+                         versions.
+
+        :param q: a quantified formula of the form
+                :math:`Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)'
+                where
+                :math:'Q\bar{x}' is a set of quantified variables of the form
+                :math:'Q x_1...x_k' and
+                :math:'P( x_1...x_i, y_1...y_j )' is a quantifier-free formula
+        :return: a formula :math:'\phi'  such that, given the current set of formulas
+               :math:'A asserted to this solver:
+               - :math:'(A \wedge q)' :math:'(A \wedge \phi)' are equivalent
+               - :math:'\phi' is quantifier-free formula containing only free
+                 variables in :math:'y_1...y_n'.
+        """
+        cdef Term result = Term(self)
+        result.cterm = self.csolver.getQuantifierElimination(term.cterm)
+        return result
+
+    def getQuantifierEliminationDisjunct(self, Term term):
+        """Do partial quantifier elimination, which can be used for incrementally computing
+        the result of a quantifier elimination.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-qe-disjunct <q> )
+
+        Requires a logic that supports quantifier elimination.
+        Currently, the only logics supported by quantifier elimination
+        are LRA and LIA.
+            
+	.. warning:: This method is experimental and may change in future
+                         versions.
+        
+           :param q: a quantified formula of the form
+                   @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
+                   where
+                   @f$Q\bar{x}@f$ is a set of quantified variables of the form
+                   @f$Q x_1...x_k@f$ and
+                   @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
+           :return: a formula @f$\phi@f$ such that, given the current set of formulas
+                  @f$A@f$ asserted to this solver:
+                  - @f$(A \wedge q \implies A \wedge \phi)@f$ if @f$Q@f$ is
+                    @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if
+                    @f$Q@f$ is @f$\exists@f$
+                  - @f$\phi@f$ is quantifier-free formula containing only free
+                    variables in @f$y_1...y_n@f$
+                  - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the
+                    formula
+                    @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge
+                    \neg (\phi \wedge Q_n))@f$
+                    where for each @f$i = 1...n@f$,
+                    formula @f$(\phi \wedge Q_i)@f$ is the result of calling
+                    Solver::getQuantifierEliminationDisjunct() for @f$q@f$ with the
+                    set of assertions @f$(A \wedge Q_{i-1})@f$.
+                    Similarly, if @f$Q@f$ is @f$\forall@f$, then let
+                    @f$(A \wedge Q_n)@f$ be
+                    @f$(A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge
+                    Q_n))@f$
+                    where @f$(\phi \wedge Q_i)@f$ is the same as above.
+                    In either case, we have that @f$(\phi \wedge Q_j)@f$ will
+                    eventually be true or false, for some finite j.
+        """
+        cdef Term result = Term(self)
+        result.cterm = self.csolver.getQuantifierEliminationDisjunct(term.cterm)
+        return result
+    
     def getModel(self, sorts, consts):
         """Get the model
 
diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 9ba032f0a..f07aa8e74 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1600,6 +1600,7 @@ def test_block_model3(solver):
     with pytest.raises(RuntimeError):
         solver.blockModel()
 
+
 def test_block_model4(solver):
     solver.setOption("produce-models", "true")
     solver.setOption("block-models", "literals")
@@ -1966,6 +1967,20 @@ def test_add_sygus_constraint(solver):
     with pytest.raises(RuntimeError):
         slv.addSygusConstraint(boolTerm)
 
+def test_add_sygus_assume(solver):
+    solver.setOption("sygus", "true")
+    nullTerm = cvc5.Term(solver)
+    boolTerm = solver.mkBoolean(False)
+    intTerm = solver.mkInteger(1)
+    solver.addSygusAssume(boolTerm)
+    with pytest.raises(RuntimeError):
+        solver.addSygusAssume(nullTerm)
+    with pytest.raises(RuntimeError):
+        solver.addSygusAssume(intTerm)
+    slv = cvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.addSygusAssume(boolTerm)
+
 
 def test_add_sygus_inv_constraint(solver):
     solver.setOption("sygus", "true")
@@ -2265,6 +2280,20 @@ def test_get_model_domain_elements(solver):
     with pytest.raises(RuntimeError):
         solver.getModelDomainElements(intSort)
 
+def test_get_model_domain_elements2(solver):
+    solver.setOption("produce-models", "true")
+    solver.setOption("finite-model-find", "true")
+    uSort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(uSort, "x")
+    y = solver.mkVar(uSort, "y")
+    eq = solver.mkTerm(Kind.Equal, x, y)
+    bvl = solver.mkTerm(Kind.VariableList, x, y)
+    f = solver.mkTerm(Kind.Forall, bvl, eq)
+    solver.assertFormula(f)
+    solver.checkSat()
+    solver.getModelDomainElements(uSort)
+    assert len(solver.getModelDomainElements(uSort)) == 1
+
 
 def test_get_synth_solutions(solver):
     solver.setOption("sygus", "true")
@@ -2587,3 +2616,102 @@ def test_tuple_project(solver):
 
         assert "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str(
             projection)
+
+
+
+def test_get_data_type_arity(solver):
+  ctor1 = solver.mkDatatypeConstructorDecl("_x21");
+  ctor2 = solver.mkDatatypeConstructorDecl("_x31");
+  s3 = solver.declareDatatype("_x17", [ctor1, ctor2]);
+  assert s3.getDatatypeArity() == 0
+
+
+def test_get_difficulty(solver):
+  solver.setOption("produce-difficulty", "true")
+  # cannot ask before a check sat
+  with pytest.raises(RuntimeError):
+      solver.getDifficulty()
+  solver.checkSat()
+  solver.getDifficulty()
+
+def test_get_difficulty2(solver):
+  solver.checkSat()
+  with pytest.raises(RuntimeError):
+  # option is not set
+      solver.getDifficulty()
+
+def test_get_difficulty3(solver):
+  solver.setOption("produce-difficulty", "true")
+  intSort = solver.getIntegerSort()
+  x = solver.mkConst(intSort, "x")
+  zero = solver.mkInteger(0)
+  ten = solver.mkInteger(10)
+  f0 = solver.mkTerm(Kind.Geq, x, ten)
+  f1 = solver.mkTerm(Kind.Geq, zero, x)
+  solver.checkSat()
+  dmap = solver.getDifficulty()
+  # difficulty should map assertions to integer values
+  for key, value in dmap.items():
+    assert key == f0 or key == f1
+    assert value.getKind() == Kind.CONST_RATIONAL
+
+def test_get_model(solver):
+    solver.setOption("produce-models", "true")
+    uSort = solver.mkUninterpretedSort("u")
+    x = solver.mkConst(uSort, "x")
+    y = solver.mkConst(uSort, "y")
+    z = solver.mkConst(uSort, "z")
+    f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y));
+    solver.assertFormula(f)
+    solver.checkSat()
+    sorts = [uSort]
+    terms = [x, y]
+    solver.getModel(sorts, terms)
+    null = cvc5.Term(solver)
+    terms += [null]
+    with pytest.raises(RuntimeError):
+        solver.getModel(sorts, terms)
+
+def test_get_model2(solver):
+    solver.setOption("produce-models", "true")
+    sorts = []
+    terms = []
+    with pytest.raises(RuntimeError):
+        solver.getModel(sorts, terms)
+
+def test_get_model_3(solver):
+    solver.setOption("produce-models", "true")
+    sorts = []
+    terms = []
+    solver.checkSat()
+    solver.getModel(sorts, terms)
+    integer = solver.getIntegerSort()
+    sorts += [integer]
+    with pytest.raises(RuntimeError):
+        solver.getModel(sorts, terms)
+
+def test_get_option_names(solver):
+    names = solver.getOptionNames()
+    assert len(names) > 100
+    assert "verbose" in names
+    assert "foobar" not in names
+
+def test_get_quantifier_elimination(solver):
+    x = solver.mkVar(solver.getBooleanSort(), "x")
+    forall = solver.mkTerm(Kind.Forall, solver.mkTerm(Kind.VariableList, x), solver.mkTerm(Kind.Or, x, solver.mkTerm(Kind.Not, x)))
+    with pytest.raises(RuntimeError):
+        solver.getQuantifierElimination(cvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.getQuantifierElimination(cvc5.Solver().mkBoolean(False))
+    solver.getQuantifierElimination(forall)
+
+def test_get_quantifier_elimination_disjunct(solver):
+    x = solver.mkVar(solver.getBooleanSort(), "x")
+    forall = solver.mkTerm(Kind.Forall, solver.mkTerm(Kind.VariableList, x), solver.mkTerm(Kind.Or, x, solver.mkTerm(Kind.Not, x)))
+    with pytest.raises(RuntimeError):
+        solver.getQuantifierEliminationDisjunct(cvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.getQuantifierEliminationDisjunct(cvc5.Solver().mkBoolean(False))
+    solver.getQuantifierEliminationDisjunct(forall)
+    
+