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
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 +
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,
"""
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
return assertions
def getInfo(self, str flag):
- """Get info from the solver.
+ """
+ Get info from the solver.
SMT-LIB:
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.
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.
"""
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
with pytest.raises(RuntimeError):
solver.blockModel()
+
def test_block_model4(solver):
solver.setOption("produce-models", "true")
solver.setOption("block-models", "literals")
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")
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")
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)
+
+
projects / cvc5.git / commitdiff