return sort
def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
- """Create a vector of datatype sorts using unresolved sorts. The names of
+ """
+ Create a vector of datatype sorts using unresolved sorts. The names of
the datatype declarations in dtypedecls must be distinct.
This method is called when the DatatypeDecl objects dtypedecls have been
return term
def mkString(self, str s, useEscSequences = None):
- """Create a String constant from a `str` which may contain SMT-LIB
+ """
+ Create a String constant from a `str` which may contain SMT-LIB
compatible escape sequences like ``\\u1234`` to encode unicode characters.
:param s: the string this constant represents
return term
def mkConstArray(self, Sort sort, Term val):
- """ Create a constant array with the provided constant value stored at every
+ """
+ Create a constant array with the provided constant value stored at every
index
:param sort: the sort of the constant array (must be an array sort)
return term
def mkAbstractValue(self, index):
- """Create an abstract value constant.
+ """
+ Create an abstract value constant.
The given index needs to be positive.
:param index: Index of the abstract value
return term
def mkVar(self, Sort sort, symbol=None):
- """Create a bound variable to be used in a binder (i.e. a quantifier, a
+ """
+ Create a bound variable to be used in a binder (i.e. a quantifier, a
lambda, or a witness binder).
:param sort: the sort of the variable
return term
def mkDatatypeConstructorDecl(self, str name):
- """ :return: a datatype constructor declaration
+ """
+ :return: a datatype constructor declaration
:param: `name` the constructor's name
"""
cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
return dd
def simplify(self, Term t):
- """Simplify a formula without doing "much" work. Does not involve the
+ """
+ Simplify a formula without doing "much" work. Does not involve the
SAT Engine in the simplification, but uses the current definitions,
assertions, and the current partial model, if one has been constructed.
It also involves theory normalization.
return r
def mkSygusGrammar(self, boundVars, ntSymbols):
- """Create a SyGuS grammar. The first non-terminal is treated as the
+ """
+ Create a SyGuS grammar. The first non-terminal is treated as the
starting non-terminal, so the order of non-terminals matters.
:param boundVars: the parameters to corresponding synth-fun/synth-inv
self.csolver.addSygusConstraint(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
+ """
+ Add a set of SyGuS constraints to the current state that correspond to an
invariant synthesis problem.
SyGuS v2:
return r
def getSynthSolution(self, Term term):
- """Get the synthesis solution of the given term. This method should be
+ """
+ Get the synthesis solution of the given term. This method should be
called immediately after the solver answers unsat for sygus input.
:param term: the term for which the synthesis solution is queried
return t
def getSynthSolutions(self, list terms):
- """Get the synthesis solutions of the given terms. This method should be
+ """
+ Get the synthesis solutions of the given terms. This method should be
called immediately after the solver answers unsat for sygus input.
:param terms: the terms for which the synthesis solutions is queried
return result
def isModelCoreSymbol(self, Term v):
- """This returns false if the model value of free constant v was not
+ """
+ This returns false if the model value of free constant v was not
essential for showing the satisfiability of the last call to checkSat
using the current model. This method will only return false (for any v)
if the model-cores option has been set.
projects / cvc5.git / commitdiff