-from collections import defaultdict
+from collections import defaultdict, Set
from fractions import Fraction
+from functools import wraps
import sys
from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
+from libc.stddef cimport wchar_t
from libcpp.pair cimport pair
-from libcpp.set cimport set
+from libcpp.set cimport set as c_set
from libcpp.string cimport string
from libcpp.vector cimport vector
from cvc5 cimport DatatypeSelector as c_DatatypeSelector
from cvc5 cimport Result as c_Result
from cvc5 cimport RoundingMode as c_RoundingMode
+from cvc5 cimport UnknownExplanation as c_UnknownExplanation
from cvc5 cimport Op as c_Op
from cvc5 cimport Solver as c_Solver
from cvc5 cimport Grammar as c_Grammar
from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
+from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT
+from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED
+from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON
+from cvc5 cimport OTHER
from cvc5 cimport Term as c_Term
from cvc5 cimport hash as c_hash
-
+from cvc5 cimport wstring as c_wstring
+from cvc5 cimport tuple as c_tuple
+from cvc5 cimport get0, get1, get2
from cvc5kinds cimport Kind as c_Kind
+cdef extern from "Python.h":
+ wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
+ object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
+ void PyMem_Free(void*)
+
################################## DECORATORS #################################
def expand_list_arg(num_req_args=0):
- '''
+ """
Creates a decorator that looks at index num_req_args of the args,
if it's a list, it expands it before calling the function.
- '''
+ """
def decorator(func):
+ @wraps(func)
def wrapper(owner, *args):
if len(args) == num_req_args + 1 and \
isinstance(args[num_req_args], list):
cdef class Datatype:
- """Wrapper class for :cpp:class:`cvc5::api::Datatype`."""
+ """
+ A cvc5 datatype.
+ Wrapper class for :cpp:class:`cvc5::api::Datatype`.
+ """
cdef c_Datatype cd
cdef Solver solver
def __cinit__(self, Solver solver):
self.solver = solver
def __getitem__(self, index):
- """Return a constructor by index or by name."""
cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
if isinstance(index, int) and index >= 0:
dc.cdc = self.cd[(<int?> index)]
return dc
def getConstructor(self, str name):
- """Return a constructor by name."""
+ """
+ :param name: the name of the constructor.
+ :return: a constructor by name.
+ """
cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
dc.cdc = self.cd.getConstructor(name.encode())
return dc
def getConstructorTerm(self, str name):
- """:return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`)."""
+ """
+ :param name: the name of the constructor.
+ :return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`).
+ """
cdef Term term = Term(self.solver)
term.cterm = self.cd.getConstructorTerm(name.encode())
return term
def getSelector(self, str name):
- """Return a selector by name."""
+ """
+ :param name: the name of the selector..
+ :return: a selector by name.
+ """
cdef DatatypeSelector ds = DatatypeSelector(self.solver)
ds.cds = self.cd.getSelector(name.encode())
return ds
+ def getName(self):
+ """
+ :return: the name of the datatype.
+ """
+ return self.cd.getName().decode()
+
def getNumConstructors(self):
- """:return: number of constructors."""
+ """
+ :return: number of constructors in this datatype.
+ """
return self.cd.getNumConstructors()
def isParametric(self):
- """:return: whether this datatype is parametric."""
+ """:return: True if this datatype is parametric."""
return self.cd.isParametric()
def isCodatatype(self):
- """:return: whether this datatype corresponds to a co-datatype."""
+ """:return: True if this datatype corresponds to a co-datatype."""
return self.cd.isCodatatype()
def isTuple(self):
- """:return: whether this datatype corresponds to a tuple."""
+ """:return: True if this datatype corresponds to a tuple."""
return self.cd.isTuple()
def isRecord(self):
- """:return: whether this datatype corresponds to a record."""
+ """:return: True if this datatype corresponds to a record."""
return self.cd.isRecord()
def isFinite(self):
- """:return: whether this datatype is finite."""
+ """:return: True if this datatype is finite."""
return self.cd.isFinite()
def isWellFounded(self):
- """:return: whether this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
+ """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
return self.cd.isWellFounded()
def hasNestedRecursion(self):
- """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
+ """:return: True if this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
return self.cd.hasNestedRecursion()
+ def isNull(self):
+ """:return: True if this Datatype is a null object."""
+ return self.cd.isNull()
+
def __str__(self):
return self.cd.toString().decode()
cdef class DatatypeConstructor:
+ """
+ A cvc5 datatype constructor.
+ Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.
+ """
cdef c_DatatypeConstructor cdc
cdef Solver solver
def __cinit__(self, Solver solver):
if isinstance(index, int) and index >= 0:
ds.cds = self.cdc[(<int?> index)]
elif isinstance(index, str):
- ds.cds = self.cdc[(<const string &> name.encode())]
+ ds.cds = self.cdc[(<const string &> index.encode())]
else:
raise ValueError("Expecting a non-negative integer or string")
return ds
def getName(self):
+ """
+ :return: the name of the constructor.
+ """
return self.cdc.getName().decode()
def getConstructorTerm(self):
+ """
+ :return: the constructor operator as a term.
+ """
cdef Term term = Term(self.solver)
term.cterm = self.cdc.getConstructorTerm()
return term
+ def getSpecializedConstructorTerm(self, Sort retSort):
+ """
+ Specialized method for parametric datatypes (see :cpp:func:`DatatypeConstructor::getSpecializedConstructorTerm() <cvc5::api::DatatypeConstructor::getSpecializedConstructorTerm>`).
+
+ :param retSort: the desired return sort of the constructor
+ :return: the constructor operator as a term.
+ """
+ cdef Term term = Term(self.solver)
+ term.cterm = self.cdc.getSpecializedConstructorTerm(retSort.csort)
+ return term
+
def getTesterTerm(self):
+ """
+ :return: the tester operator that is related to this constructor, as a term.
+ """
cdef Term term = Term(self.solver)
term.cterm = self.cdc.getTesterTerm()
return term
def getNumSelectors(self):
+ """
+ :return: the number of selecters (so far) of this Datatype constructor.
+ """
return self.cdc.getNumSelectors()
def getSelector(self, str name):
+ """
+ :param name: the name of the datatype selector.
+ :return: the first datatype selector with the given name
+ """
cdef DatatypeSelector ds = DatatypeSelector(self.solver)
ds.cds = self.cdc.getSelector(name.encode())
return ds
def getSelectorTerm(self, str name):
+ """
+ :param name: the name of the datatype selector.
+ :return: a term representing the firstdatatype selector with the given name.
+ """
cdef Term term = Term(self.solver)
term.cterm = self.cdc.getSelectorTerm(name.encode())
return term
+ def isNull(self):
+ """:return: True if this DatatypeConstructor is a null object."""
+ return self.cdc.isNull()
+
def __str__(self):
return self.cdc.toString().decode()
cdef class DatatypeConstructorDecl:
+ """
+ A cvc5 datatype constructor declaration.
+ Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.
+ """
cdef c_DatatypeConstructorDecl cddc
cdef Solver solver
self.solver = solver
def addSelector(self, str name, Sort sort):
+ """
+ Add datatype selector declaration.
+
+ :param name: the name of the datatype selector declaration to add.
+ :param sort: the range sort of the datatype selector declaration to add.
+ """
self.cddc.addSelector(name.encode(), sort.csort)
def addSelectorSelf(self, str name):
+ """
+ Add datatype selector declaration whose range sort is the datatype itself.
+
+ :param name: the name of the datatype selector declaration to add.
+ """
self.cddc.addSelectorSelf(name.encode())
+ def isNull(self):
+ """:return: True if this DatatypeConstructorDecl is a null object."""
+ return self.cddc.isNull()
+
def __str__(self):
return self.cddc.toString().decode()
cdef class DatatypeDecl:
+ """
+ A cvc5 datatype declaration.
+ Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.
+ """
cdef c_DatatypeDecl cdd
cdef Solver solver
def __cinit__(self, Solver solver):
self.solver = solver
def addConstructor(self, DatatypeConstructorDecl ctor):
+ """
+ Add a datatype constructor declaration.
+
+ :param ctor: the datatype constructor declaration to add.
+ """
self.cdd.addConstructor(ctor.cddc)
def getNumConstructors(self):
+ """
+ :return: number of constructors (so far) for this datatype declaration.
+ """
return self.cdd.getNumConstructors()
def isParametric(self):
+ """
+ :return: is this datatype declaration parametric?
+ """
return self.cdd.isParametric()
+ def getName(self):
+ """
+ :return: the name of this datatype declaration.
+ """
+ return self.cdd.getName().decode()
+
+ def isNull(self):
+ """:return: True if this DatatypeDecl is a null object."""
+ return self.cdd.isNull()
+
def __str__(self):
return self.cdd.toString().decode()
cdef class DatatypeSelector:
+ """
+ A cvc5 datatype selector.
+ Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.
+ """
cdef c_DatatypeSelector cds
cdef Solver solver
def __cinit__(self, Solver solver):
self.solver = solver
def getName(self):
+ """
+ :return: the name of this datatype selector.
+ """
return self.cds.getName().decode()
def getSelectorTerm(self):
+ """
+ :return: the selector opeartor of this datatype selector as a term.
+ """
cdef Term term = Term(self.solver)
term.cterm = self.cds.getSelectorTerm()
return term
def getUpdaterTerm(self):
+ """
+ :return: the updater opeartor of this datatype selector as a term.
+ """
cdef Term term = Term(self.solver)
term.cterm = self.cds.getUpdaterTerm()
return term
def getRangeSort(self):
+ """
+ :return: the range sort of this selector.
+ """
cdef Sort sort = Sort(self.solver)
sort.csort = self.cds.getRangeSort()
return sort
+ def isNull(self):
+ """:return: True if this DatatypeSelector is a null object."""
+ return self.cds.isNull()
+
def __str__(self):
return self.cds.toString().decode()
cdef class Op:
+ """
+ A cvc5 operator.
+ An operator is a term that represents certain operators,
+ instantiated with its required parameters, e.g.,
+ a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`.
+ Wrapper class for :cpp:class:`cvc5::api::Op`.
+ """
cdef c_Op cop
cdef Solver solver
def __cinit__(self, Solver solver):
return cophash(self.cop)
def getKind(self):
+ """
+ :return: the kind of this operator.
+ """
return kind(<int> self.cop.getKind())
-
+
def isIndexed(self):
+ """
+ :return: True iff this operator is indexed.
+ """
return self.cop.isIndexed()
def isNull(self):
+ """
+ :return: True iff this operator is a null term.
+ """
return self.cop.isNull()
+ def getNumIndices(self):
+ """
+ :return: number of indices of this op.
+ """
+ return self.cop.getNumIndices()
+
def getIndices(self):
+ """
+ :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() <cvc5::api::Op::getIndices>`).
+ """
indices = None
try:
- indices = self.cop.getIndices[string]()
+ indices = self.cop.getIndices[string]().decode()
except:
pass
return indices
cdef class Grammar:
+ """
+ A Sygus Grammar.
+ Wrapper class for :cpp:class:`cvc5::api::Grammar`.
+ """
cdef c_Grammar cgrammar
cdef Solver solver
def __cinit__(self, Solver solver):
self.cgrammar = c_Grammar()
def addRule(self, Term ntSymbol, Term rule):
+ """
+ Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
+
+ :param ntSymbol: the non-terminal to which the rule is added.
+ :param rule: the rule to add.
+ """
self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
def addAnyConstant(self, Term ntSymbol):
+ """
+ Allow ``ntSymbol`` to be an arbitrary constant.
+
+ :param ntSymbol: the non-terminal allowed to be constant.
+ """
self.cgrammar.addAnyConstant(ntSymbol.cterm)
def addAnyVariable(self, Term ntSymbol):
+ """
+ Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``.
+
+ :param ntSymbol: the non-terminal allowed to be any input variable.
+ """
self.cgrammar.addAnyVariable(ntSymbol.cterm)
def addRules(self, Term ntSymbol, rules):
+ """
+ Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
+
+ :param ntSymbol: the non-terminal to which the rules are added.
+ :param rules: the rules to add.
+ """
cdef vector[c_Term] crules
for r in rules:
crules.push_back((<Term?> r).cterm)
self.cgrammar.addRules(ntSymbol.cterm, crules)
cdef class Result:
+ """
+ Encapsulation of a three-valued solver result, with explanations.
+ Wrapper class for :cpp:class:`cvc5::api::Result`.
+ """
cdef c_Result cr
def __cinit__(self):
# gets populated by solver
self.cr = c_Result()
def isNull(self):
+ """
+ :return: True if Result is empty, i.e., a nullary Result,
+ and not an actual result returned from a :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` (and friends) query.
+ """
return self.cr.isNull()
def isSat(self):
+ """
+ :return: True if query was a satisfiable :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query.
+ """
return self.cr.isSat()
def isUnsat(self):
+ """
+ :return: True if query was an usatisfiable :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query.
+ """
return self.cr.isUnsat()
def isSatUnknown(self):
+ """
+ :return: True if query was a :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query and cvc5 was not able to determine (un)satisfiability.
+ """
return self.cr.isSatUnknown()
def isEntailed(self):
+ """
+ :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query.
+ """
return self.cr.isEntailed()
def isNotEntailed(self):
+ """
+ :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query that is not entailed.
+ """
return self.cr.isNotEntailed()
def isEntailmentUnknown(self):
+ """
+ :return: True if query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query query and cvc5 was not able to determine if it is entailed.
+ """
return self.cr.isEntailmentUnknown()
+
+ def getUnknownExplanation(self):
+ """
+ :return: an explanation for an unknown query result.
+ """
+ return UnknownExplanation(<int> self.cr.getUnknownExplanation())
def __eq__(self, Result other):
return self.cr == other.cr
def __ne__(self, Result other):
return self.cr != other.cr
- def getUnknownExplanation(self):
- return self.cr.getUnknownExplanation().decode()
-
def __str__(self):
return self.cr.toString().decode()
cdef class RoundingMode:
+ """
+ Rounding modes for floating-point numbers.
+
+ For many floating-point operations, infinitely precise results may not be
+ representable with the number of available bits. Thus, the results are
+ rounded in a certain way to one of the representable floating-point numbers.
+
+ These rounding modes directly follow the SMT-LIB theory for floating-point
+ arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
+ The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
+ Standard 754.
+
+ Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`.
+ """
cdef c_RoundingMode crm
cdef str name
def __cinit__(self, int rm):
return self.name
+cdef class UnknownExplanation:
+ """
+ Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`.
+ """
+ cdef c_UnknownExplanation cue
+ cdef str name
+ def __cinit__(self, int ue):
+ # crm always assigned externally
+ self.cue = <c_UnknownExplanation> ue
+ self.name = __unknown_explanations[ue]
+
+ def __eq__(self, UnknownExplanation other):
+ return (<int> self.cue) == (<int> other.cue)
+
+ def __ne__(self, UnknownExplanation other):
+ return not self.__eq__(other)
+
+ def __hash__(self):
+ return hash((<int> self.crm, self.name))
+
+ def __str__(self):
+ return self.name
+
+ def __repr__(self):
+ return self.name
+
+
cdef class Solver:
+ """Wrapper class for :cpp:class:`cvc5::api::Solver`."""
cdef c_Solver* csolver
def __cinit__(self):
- self.csolver = new c_Solver(NULL)
+ self.csolver = new c_Solver()
def __dealloc__(self):
del self.csolver
- def supportsFloatingPoint(self):
- return self.csolver.supportsFloatingPoint()
-
def getBooleanSort(self):
+ """:return: sort Boolean
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.getBooleanSort()
return sort
def getIntegerSort(self):
+ """:return: sort Integer
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.getIntegerSort()
return sort
+ def getNullSort(self):
+ """:return: sort null
+ """
+ cdef Sort sort = Sort(self)
+ sort.csort = self.csolver.getNullSort()
+ return sort
+
def getRealSort(self):
+ """:return: sort Real
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.getRealSort()
return sort
def getRegExpSort(self):
+ """:return: sort of RegExp
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.getRegExpSort()
return sort
def getRoundingModeSort(self):
+ """:return: sort RoundingMode
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.getRoundingModeSort()
return sort
def getStringSort(self):
+ """:return: sort String
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.getStringSort()
return sort
def mkArraySort(self, Sort indexSort, Sort elemSort):
+ """Create an array sort.
+
+ :param indexSort: the array index sort
+ :param elemSort: the array element sort
+ :return: the array sort
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
return sort
def mkBitVectorSort(self, uint32_t size):
+ """Create a bit-vector sort.
+
+ :param size: the bit-width of the bit-vector sort
+ :return: the bit-vector sort
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkBitVectorSort(size)
return sort
def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
+ """Create a floating-point sort.
+
+ :param exp: the bit-width of the exponent of the floating-point sort.
+ :param sig: the bit-width of the significand of the floating-point sort.
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
return sort
def mkDatatypeSort(self, DatatypeDecl dtypedecl):
+ """Create a datatype sort.
+
+ :param dtypedecl: the datatype declaration from which the sort is created
+ :return: the datatype sort
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
return sort
- def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts):
- sorts = []
+ def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
+ """
+ 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
+ built using "unresolved" sorts.
+
+ We associate each sort in unresolvedSorts with exacly one datatype from
+ dtypedecls. In particular, it must have the same name as exactly one
+ datatype declaration in dtypedecls.
+
+ When constructing datatypes, unresolved sorts are replaced by the datatype
+ sort constructed for the datatype declaration it is associated with.
+
+ :param dtypedecls: the datatype declarations from which the sort is created
+ :param unresolvedSorts: the list of unresolved sorts
+ :return: the datatype sorts
+ """
+ if unresolvedSorts == None:
+ unresolvedSorts = set([])
+ else:
+ assert isinstance(unresolvedSorts, Set)
+ sorts = []
cdef vector[c_DatatypeDecl] decls
for decl in dtypedecls:
decls.push_back((<DatatypeDecl?> decl).cdd)
- cdef set[c_Sort] usorts
+ cdef c_set[c_Sort] usorts
for usort in unresolvedSorts:
usorts.insert((<Sort?> usort).csort)
csorts = self.csolver.mkDatatypeSorts(
- <const vector[c_DatatypeDecl]&> decls, <const set[c_Sort]&> usorts)
+ <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
for csort in csorts:
sort = Sort(self)
sort.csort = csort
return sorts
def mkFunctionSort(self, sorts, Sort codomain):
+ """ Create function sort.
+
+ :param sorts: the sort of the function arguments
+ :param codomain: the sort of the function return value
+ :return: the function sort
+ """
cdef Sort sort = Sort(self)
# populate a vector with dereferenced c_Sorts
return sort
def mkParamSort(self, symbolname):
+ """ Create a sort parameter.
+
+ :param symbol: the name of the sort
+ :return: the sort parameter
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkParamSort(symbolname.encode())
return sort
@expand_list_arg(num_req_args=0)
def mkPredicateSort(self, *sorts):
- '''
- Supports the following arguments:
- Sort mkPredicateSort(List[Sort] sorts)
+ """Create a predicate sort.
- where sorts can also be comma-separated arguments of
- type Sort
- '''
+ :param sorts: the list of sorts of the predicate, as a list or as distinct arguments.
+ :return: the predicate sort
+ """
cdef Sort sort = Sort(self)
cdef vector[c_Sort] v
for s in sorts:
@expand_list_arg(num_req_args=0)
def mkRecordSort(self, *fields):
- '''
- Supports the following arguments:
- Sort mkRecordSort(List[Tuple[str, Sort]] fields)
+ """Create a record sort
- where fields can also be comma-separated arguments of
- type Tuple[str, Sort]
- '''
+ :param fields: the list of fields of the record, as a list or as distinct arguments
+ :return: the record sort
+ """
cdef Sort sort = Sort(self)
cdef vector[pair[string, c_Sort]] v
cdef pair[string, c_Sort] p
return sort
def mkSetSort(self, Sort elemSort):
+ """Create a set sort.
+
+ :param elemSort: the sort of the set elements
+ :return: the set sort
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkSetSort(elemSort.csort)
return sort
def mkBagSort(self, Sort elemSort):
+ """Create a bag sort.
+
+ :param elemSort: the sort of the bag elements
+ :return: the bag sort
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkBagSort(elemSort.csort)
return sort
def mkSequenceSort(self, Sort elemSort):
+ """Create a sequence sort.
+
+ :param elemSort: the sort of the sequence elements
+ :return: the sequence sort
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
return sort
def mkUninterpretedSort(self, str name):
+ """Create an uninterpreted sort.
+
+ :param symbol: the name of the sort
+ :return: the uninterpreted sort
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.mkUninterpretedSort(name.encode())
return sort
def mkSortConstructorSort(self, str symbol, size_t arity):
+ """Create a sort constructor sort.
+
+ :param symbol: the symbol of the sort
+ :param arity: the arity of the sort
+ :return: the sort constructor sort
+ """
cdef Sort sort = Sort(self)
sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
return sort
@expand_list_arg(num_req_args=0)
def mkTupleSort(self, *sorts):
- '''
- Supports the following arguments:
- Sort mkTupleSort(List[Sort] sorts)
+ """Create a tuple sort.
- where sorts can also be comma-separated arguments of
- type Sort
- '''
+ :param sorts: of the elements of the tuple, as a list or as distinct arguments
+ :return: the tuple sort
+ """
cdef Sort sort = Sort(self)
cdef vector[c_Sort] v
for s in sorts:
@expand_list_arg(num_req_args=1)
def mkTerm(self, kind_or_op, *args):
- '''
- Supports the following arguments:
- Term mkTerm(Kind kind)
- Term mkTerm(Kind kind, Op child1, List[Term] children)
- Term mkTerm(Kind kind, List[Term] children)
-
- where List[Term] can also be comma-separated arguments
- '''
+ """
+ Supports the following arguments:
+
+ - ``Term mkTerm(Kind kind)``
+ - ``Term mkTerm(Kind kind, Op child1, List[Term] children)``
+ - ``Term mkTerm(Kind kind, List[Term] children)``
+
+ where ``List[Term]`` can also be comma-separated arguments
+ """
cdef Term term = Term(self)
cdef vector[c_Term] v
term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
return term
- def mkOp(self, kind k, arg0=None, arg1 = None):
- '''
+ def mkTuple(self, sorts, terms):
+ """Create a tuple term. Terms are automatically converted if sorts are compatible.
+
+ :param sorts: The sorts of the elements in the tuple
+ :param terms: The elements in the tuple
+ :return: the tuple Term
+ """
+ cdef vector[c_Sort] csorts
+ cdef vector[c_Term] cterms
+
+ for s in sorts:
+ csorts.push_back((<Sort?> s).csort)
+ for s in terms:
+ cterms.push_back((<Term?> s).cterm)
+ cdef Term result = Term(self)
+ result.cterm = self.csolver.mkTuple(csorts, cterms)
+ return result
+
+ @expand_list_arg(num_req_args=0)
+ def mkOp(self, kind k, *args):
+ """
Supports the following uses:
- Op mkOp(Kind kind)
- Op mkOp(Kind kind, Kind k)
- Op mkOp(Kind kind, const string& arg)
- Op mkOp(Kind kind, uint32_t arg)
- Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)
- '''
+
+ - ``Op mkOp(Kind kind)``
+ - ``Op mkOp(Kind kind, Kind k)``
+ - ``Op mkOp(Kind kind, const string& arg)``
+ - ``Op mkOp(Kind kind, uint32_t arg)``
+ - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
+ - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind)
+ """
cdef Op op = Op(self)
+ cdef vector[uint32_t] v
- if arg0 is None:
+ if len(args) == 0:
op.cop = self.csolver.mkOp(k.k)
- elif arg1 is None:
- if isinstance(arg0, kind):
- op.cop = self.csolver.mkOp(k.k, (<kind?> arg0).k)
- elif isinstance(arg0, str):
+ elif len(args) == 1:
+ if isinstance(args[0], str):
op.cop = self.csolver.mkOp(k.k,
<const string &>
- arg0.encode())
- elif isinstance(arg0, int):
- op.cop = self.csolver.mkOp(k.k, <int?> arg0)
+ args[0].encode())
+ elif isinstance(args[0], int):
+ op.cop = self.csolver.mkOp(k.k, <int?> args[0])
+ elif isinstance(args[0], list):
+ for a in args[0]:
+ if a < 0 or a >= 2 ** 31:
+ raise ValueError("Argument {} must fit in a uint32_t".format(a))
+
+ v.push_back((<uint32_t?> a))
+ op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v)
else:
raise ValueError("Unsupported signature"
- " mkOp: {}".format(" X ".join([str(k), str(arg0)])))
- else:
- if isinstance(arg0, int) and isinstance(arg1, int):
- op.cop = self.csolver.mkOp(k.k, <int> arg0,
- <int> arg1)
+ " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
+ elif len(args) == 2:
+ if isinstance(args[0], int) and isinstance(args[1], int):
+ op.cop = self.csolver.mkOp(k.k, <int> args[0], <int> args[1])
else:
raise ValueError("Unsupported signature"
- " mkOp: {}".format(" X ".join([k, arg0, arg1])))
+ " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
return op
def mkTrue(self):
+ """Create a Boolean true constant.
+
+ :return: the true constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkTrue()
return term
def mkFalse(self):
+ """Create a Boolean false constant.
+
+ :return: the false constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkFalse()
return term
def mkBoolean(self, bint val):
+ """Create a Boolean constant.
+
+ :return: the Boolean constant
+ :param val: the value of the constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkBoolean(val)
return term
def mkPi(self):
+ """Create a constant representing the number Pi.
+
+ :return: a constant representing Pi
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkPi()
return term
def mkInteger(self, val):
+ """Create an integer constant.
+
+ :param val: representation of the constant: either a string or integer
+ :return: a constant of sort Integer
+ """
cdef Term term = Term(self)
if isinstance(val, str):
term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
return term
def mkReal(self, val, den=None):
+ """Create a real constant.
+
+ :param: `val` the value of the term. Can be an integer, float, or string. It will be formatted as a string before the term is built.
+ :param: `den` if not None, the value is `val`/`den`
+ :return: a real term with literal value
+
+ Can be used in various forms:
+
+ - Given a string ``"N/D"`` constructs the corresponding rational.
+ - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
+ - Given a float ``f``, constructs the rational matching ``f``'s string representation. This means that ``mkReal(0.3)`` gives ``3/10`` and not the IEEE-754 approximation of ``3/10``.
+ - Given a string ``"W"`` or an integer, constructs that integer.
+ - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``.
+ """
cdef Term term = Term(self)
if den is None:
term.cterm = self.csolver.mkReal(str(val).encode())
return term
def mkRegexpEmpty(self):
+ """Create a regular expression empty term.
+
+ :return: the empty term
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkRegexpEmpty()
return term
def mkRegexpSigma(self):
+ """Create a regular expression sigma term.
+
+ :return: the sigma term
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkRegexpSigma()
return term
def mkEmptySet(self, Sort s):
+ """Create a constant representing an empty set of the given sort.
+
+ :param sort: the sort of the set elements.
+ :return: the empty set constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkEmptySet(s.csort)
return term
+ def mkEmptyBag(self, Sort s):
+ """Create a constant representing an empty bag of the given sort.
+
+ :param sort: the sort of the bag elements.
+ :return: the empty bag constant
+ """
+ cdef Term term = Term(self)
+ term.cterm = self.csolver.mkEmptyBag(s.csort)
+ return term
def mkSepNil(self, Sort sort):
+ """Create a separation logic nil term.
+
+ :param sort: the sort of the nil term
+ :return: the separation logic nil term
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkSepNil(sort.csort)
return term
- def mkString(self, str_or_vec):
+ def mkString(self, str s, useEscSequences = None):
+ """
+ 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
+ :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character
+ :return: the String constant
+ """
cdef Term term = Term(self)
- cdef vector[unsigned] v
- if isinstance(str_or_vec, str):
- for u in str_or_vec:
- v.push_back(<unsigned> ord(u))
- term.cterm = self.csolver.mkString(<const vector[unsigned]&> v)
- elif isinstance(str_or_vec, list):
- for u in str_or_vec:
- if not isinstance(u, int):
- raise ValueError("List should contain ints but got: {}"
- .format(str_or_vec))
- v.push_back(<unsigned> u)
- term.cterm = self.csolver.mkString(<const vector[unsigned]&> v)
+ cdef Py_ssize_t size
+ cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
+ if isinstance(useEscSequences, bool):
+ term.cterm = self.csolver.mkString(
+ s.encode(), <bint> useEscSequences)
else:
- raise ValueError("Expected string or vector of ASCII codes"
- " but got: {}".format(str_or_vec))
+ term.cterm = self.csolver.mkString(c_wstring(tmp, size))
+ PyMem_Free(tmp)
return term
def mkEmptySequence(self, Sort sort):
+ """Create an empty sequence of the given element sort.
+
+ :param sort: The element sort of the sequence.
+ :return: the empty sequence with given element sort.
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkEmptySequence(sort.csort)
return term
def mkUniverseSet(self, Sort sort):
+ """Create a universe set of the given sort.
+
+ :param sort: the sort of the set elements
+ :return: the universe set constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkUniverseSet(sort.csort)
return term
- def mkBitVector(self, size_or_str, val = None):
+ @expand_list_arg(num_req_args=0)
+ def mkBitVector(self, *args):
+ """
+ Supports the following arguments:
+
+ - ``Term mkBitVector(int size, int val=0)``
+ - ``Term mkBitVector(int size, string val, int base)``
+
+ :return: a bit-vector literal term
+ :param: `size` an integer size.
+ :param: `val` an integer representating the value, in the first form. In the second form, a string representing the value.
+ :param: `base` the base of the string representation (second form only)
+ """
cdef Term term = Term(self)
- if isinstance(size_or_str, int):
- if val is None:
- term.cterm = self.csolver.mkBitVector(<uint32_t> size_or_str)
- else:
- term.cterm = self.csolver.mkBitVector(<uint32_t> size_or_str,
- <const string &> str(val).encode(),
- 10)
- elif isinstance(size_or_str, str):
- # handle default value
- if val is None:
- term.cterm = self.csolver.mkBitVector(
- <const string &> size_or_str.encode())
- else:
- term.cterm = self.csolver.mkBitVector(
- <const string &> size_or_str.encode(), <uint32_t> val)
+ if len(args) == 0:
+ raise ValueError("Missing arguments to mkBitVector")
+ size = args[0]
+ if not isinstance(size, int):
+ raise ValueError(
+ "Invalid first argument to mkBitVector '{}', "
+ "expected bit-vector size".format(size))
+ if len(args) == 1:
+ term.cterm = self.csolver.mkBitVector(<uint32_t> size)
+ elif len(args) == 2:
+ val = args[1]
+ if not isinstance(val, int):
+ raise ValueError(
+ "Invalid second argument to mkBitVector '{}', "
+ "expected integer value".format(size))
+ term.cterm = self.csolver.mkBitVector(
+ <uint32_t> size, <uint32_t> val)
+ elif len(args) == 3:
+ val = args[1]
+ base = args[2]
+ if not isinstance(val, str):
+ raise ValueError(
+ "Invalid second argument to mkBitVector '{}', "
+ "expected value string".format(size))
+ if not isinstance(base, int):
+ raise ValueError(
+ "Invalid third argument to mkBitVector '{}', "
+ "expected base given as integer".format(size))
+ term.cterm = self.csolver.mkBitVector(
+ <uint32_t> size,
+ <const string&> str(val).encode(),
+ <uint32_t> base)
else:
- raise ValueError("Unexpected inputs {} to"
- " mkBitVector".format((size_or_str, val)))
+ raise ValueError("Unexpected inputs to mkBitVector")
return term
def mkConstArray(self, Sort sort, Term val):
+ """
+ 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)
+ :param val: the constant value to store (must match the sort's element sort)
+ :return: the constant array term
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
return term
def mkPosInf(self, int exp, int sig):
+ """Create a positive infinity floating-point constant.
+
+ :param exp: Number of bits in the exponent
+ :param sig: Number of bits in the significand
+ :return: the floating-point constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkPosInf(exp, sig)
return term
def mkNegInf(self, int exp, int sig):
+ """Create a negative infinity floating-point constant.
+
+ :param exp: Number of bits in the exponent
+ :param sig: Number of bits in the significand
+ :return: the floating-point constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkNegInf(exp, sig)
return term
def mkNaN(self, int exp, int sig):
+ """Create a not-a-number (NaN) floating-point constant.
+
+ :param exp: Number of bits in the exponent
+ :param sig: Number of bits in the significand
+ :return: the floating-point constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkNaN(exp, sig)
return term
def mkPosZero(self, int exp, int sig):
+ """Create a positive zero (+0.0) floating-point constant.
+
+ :param exp: Number of bits in the exponent
+ :param sig: Number of bits in the significand
+ :return: the floating-point constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkPosZero(exp, sig)
return term
def mkNegZero(self, int exp, int sig):
+ """Create a negative zero (+0.0) floating-point constant.
+
+ :param exp: Number of bits in the exponent
+ :param sig: Number of bits in the significand
+ :return: the floating-point constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkNegZero(exp, sig)
return term
def mkRoundingMode(self, RoundingMode rm):
+ """Create a roundingmode constant.
+
+ :param rm: the floating point rounding mode this constant represents
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
return term
def mkUninterpretedConst(self, Sort sort, int index):
+ """Create uninterpreted constant.
+
+ :param sort: Sort of the constant
+ :param index: Index of the constant
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index)
return term
def mkAbstractValue(self, index):
+ """
+ Create an abstract value constant.
+ The given index needs to be positive.
+
+ :param index: Index of the abstract value
+ """
cdef Term term = Term(self)
try:
term.cterm = self.csolver.mkAbstractValue(str(index).encode())
except:
- raise ValueError("mkAbstractValue expects a str representing a number"
- " or an int, but got{}".format(index))
+ raise ValueError(
+ "mkAbstractValue expects a str representing a number"
+ " or an int, but got{}".format(index))
return term
def mkFloatingPoint(self, int exp, int sig, Term val):
+ """Create a floating-point constant.
+
+ :param exp: Size of the exponent
+ :param sig: Size of the significand
+ :param val: Value of the floating-point constant as a bit-vector term
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
return term
def mkConst(self, Sort sort, symbol=None):
+ """
+ Create (first-order) constant (0-arity function symbol).
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( declare-const <symbol> <sort> )
+ ( declare-fun <symbol> ( ) <sort> )
+
+ :param sort: the sort of the constant
+ :param symbol: the name of the constant. If None, a default symbol is used.
+ :return: the first-order constant
+ """
cdef Term term = Term(self)
if symbol is None:
term.cterm = self.csolver.mkConst(sort.csort)
return term
def mkVar(self, Sort sort, symbol=None):
+ """
+ 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
+ :param symbol: the name of the variable
+ :return: the variable
+ """
cdef Term term = Term(self)
if symbol is None:
term.cterm = self.csolver.mkVar(sort.csort)
return term
def mkDatatypeConstructorDecl(self, str name):
+ """
+ :return: a datatype constructor declaration
+ :param: `name` the constructor's name
+ """
cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
return ddc
def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
+ """Create a datatype declaration.
+
+ :param name: the name of the datatype
+ :param isCoDatatype: true if a codatatype is to be constructed
+ :return: the DatatypeDecl
+ """
cdef DatatypeDecl dd = DatatypeDecl(self)
cdef vector[c_Sort] v
return dd
def simplify(self, Term t):
+ """
+ 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.
+
+ :param t: the formula to simplify
+ :return: the simplified formula
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.simplify(t.cterm)
return term
def assertFormula(self, Term term):
+ """ Assert a formula
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( assert <term> )
+
+ :param term: the formula to assert
+ """
self.csolver.assertFormula(term.cterm)
def checkSat(self):
+ """
+ Check satisfiability.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( check-sat )
+
+ :return: the result of the satisfiability check.
+ """
cdef Result r = Result()
r.cr = self.csolver.checkSat()
return r
def mkSygusGrammar(self, boundVars, ntSymbols):
+ """
+ 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
+ :param ntSymbols: the pre-declaration of the non-terminal symbols
+ :return: the grammar
+ """
cdef Grammar grammar = Grammar(self)
cdef vector[c_Term] bvc
cdef vector[c_Term] ntc
return grammar
def mkSygusVar(self, Sort sort, str symbol=""):
+ """Append symbol to the current list of universal variables.
+
+ SyGuS v2:
+
+ .. code-block:: smtlib
+
+ ( declare-var <symbol> <sort> )
+
+ :param sort: the sort of the universal variable
+ :param symbol: the name of the universal variable
+ :return: the universal variable
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode())
return term
def addSygusConstraint(self, Term t):
+ """
+ Add a formula to the set of SyGuS constraints.
+
+ SyGuS v2:
+
+ .. code-block:: smtlib
+
+ ( constraint <term> )
+
+ :param term: the formula to add as a constraint
+ """
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
+ invariant synthesis problem.
+
+ SyGuS v2:
+
+ .. code-block:: smtlib
+
+ ( inv-constraint <inv> <pre> <trans> <post> )
+
+ :param inv: the function-to-synthesize
+ :param pre: the pre-condition
+ :param trans: the transition relation
+ :param post: the post-condition
+ """
self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
+ """
+ Synthesize n-ary function following specified syntactic constraints.
+
+ SyGuS v2:
+
+ .. code-block:: smtlib
+
+ ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
+
+ :param symbol: the name of the function
+ :param boundVars: the parameters to this function
+ :param sort: the sort of the return value of this function
+ :param grammar: the syntactic constraints
+ :return: the function
+ """
cdef Term term = Term(self)
cdef vector[c_Term] v
for bv in bound_vars:
return term
def checkSynth(self):
+ """
+ Try to find a solution for the synthesis conjecture corresponding to the
+ current list of functions-to-synthesize, universal variables and
+ constraints.
+
+ SyGuS v2:
+
+ .. code-block:: smtlib
+
+ ( check-synth )
+
+ :return: the result of the synthesis conjecture.
+ """
cdef Result r = Result()
r.cr = self.csolver.checkSynth()
return r
def getSynthSolution(self, Term term):
+ """
+ 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: the synthesis solution of the given term
+ """
cdef Term t = Term(self)
t.cterm = self.csolver.getSynthSolution(term.cterm)
return t
+ def getSynthSolutions(self, list terms):
+ """
+ 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: the synthesis solutions of the given terms
+ """
+ result = []
+ cdef vector[c_Term] vec
+ for t in terms:
+ vec.push_back((<Term?> t).cterm)
+ cresult = self.csolver.getSynthSolutions(vec)
+ for s in cresult:
+ term = Term(self)
+ term.cterm = s
+ result.append(term)
+ return result
+
+
def synthInv(self, symbol, bound_vars, Grammar grammar=None):
+ """
+ Synthesize invariant.
+
+ SyGuS v2:
+
+ .. code-block:: smtlib
+
+ ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
+
+ :param symbol: the name of the invariant
+ :param boundVars: the parameters to this invariant
+ :param grammar: the syntactic constraints
+ :return: the invariant
+ """
cdef Term term = Term(self)
cdef vector[c_Term] v
for bv in bound_vars:
term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
return term
- def printSynthSolution(self):
- self.csolver.printSynthSolution(cout)
-
@expand_list_arg(num_req_args=0)
def checkSatAssuming(self, *assumptions):
- '''
- Supports the following arguments:
- Result checkSatAssuming(List[Term] assumptions)
+ """ Check satisfiability assuming the given formula.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
- where assumptions can also be comma-separated arguments of
- type (boolean) Term
- '''
+ ( check-sat-assuming ( <prop_literal> ) )
+
+ :param assumptions: the formulas to assume, as a list or as distinct arguments
+ :return: the result of the satisfiability check.
+ """
cdef Result r = Result()
# used if assumptions is a list of terms
cdef vector[c_Term] v
@expand_list_arg(num_req_args=0)
def checkEntailed(self, *assumptions):
- '''
- Supports the following arguments:
- Result checkEntailed(List[Term] assumptions)
+ """Check entailment of the given formula w.r.t. the current set of assertions.
- where assumptions can also be comma-separated arguments of
- type (boolean) Term
- '''
+ :param terms: the formulas to check entailment for, as a list or as distinct arguments
+ :return: the result of the entailment check.
+ """
cdef Result r = Result()
# used if assumptions is a list of terms
cdef vector[c_Term] v
@expand_list_arg(num_req_args=1)
def declareDatatype(self, str symbol, *ctors):
- '''
- Supports the following arguments:
- Sort declareDatatype(str symbol, List[Term] ctors)
+ """
+ Create datatype sort.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
- where ctors can also be comma-separated arguments of
- type DatatypeConstructorDecl
- '''
+ ( declare-datatype <symbol> <datatype_decl> )
+
+ :param symbol: the name of the datatype sort
+ :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
+ :return: the datatype sort
+ """
cdef Sort sort = Sort(self)
cdef vector[c_DatatypeConstructorDecl] v
return sort
def declareFun(self, str symbol, list sorts, Sort sort):
+ """Declare n-ary function symbol.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( declare-fun <symbol> ( <sort>* ) <sort> )
+
+ :param symbol: the name of the function
+ :param sorts: the sorts of the parameters to this function
+ :param sort: the sort of the return value of this function
+ :return: the function
+ """
cdef Term term = Term(self)
cdef vector[c_Sort] v
for s in sorts:
return term
def declareSort(self, str symbol, int arity):
+ """Declare uninterpreted sort.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( declare-sort <symbol> <numeral> )
+
+ :param symbol: the name of the sort
+ :param arity: the arity of the sort
+ :return: the sort
+ """
cdef Sort sort = Sort(self)
sort.csort = self.csolver.declareSort(symbol.encode(), arity)
return sort
def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
- '''
+ """
+ Define n-ary function.
Supports two uses:
- Term defineFun(str symbol, List[Term] bound_vars,
- Sort sort, Term term, bool glbl)
- Term defineFun(Term fun, List[Term] bound_vars,
- Term term, bool glbl)
- '''
+
+ - ``Term defineFun(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
+ - ``Term defineFun(Term fun, List[Term] bound_vars, Term term, bool glbl)``
+
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( define-fun <function_def> )
+
+ :param symbol: the name of the function
+ :param bound_vars: the parameters to this function
+ :param sort: the sort of the return value of this function
+ :param term: the function body
+ :param global: determines whether this definition is global (i.e. persists when popping the context)
+ :return: the function
+ """
cdef Term term = Term(self)
cdef vector[c_Term] v
for bv in bound_vars:
return term
def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
- '''
+ """Define recursive functions.
+
Supports two uses:
- Term defineFunRec(str symbol, List[Term] bound_vars,
- Sort sort, Term term, bool glbl)
- Term defineFunRec(Term fun, List[Term] bound_vars,
- Term term, bool glbl)
- '''
+
+ - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
+ - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
+
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
+
+ Create elements of parameter ``funs`` with mkConst().
+
+ :param funs: the sorted functions
+ :param bound_vars: the list of parameters to the functions
+ :param terms: the list of function bodies of the functions
+ :param global: determines whether this definition is global (i.e. persists when popping the context)
+ :return: the function
+ """
cdef Term term = Term(self)
cdef vector[c_Term] v
for bv in bound_vars:
return term
def defineFunsRec(self, funs, bound_vars, terms):
+ """Define recursive functions.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
+
+ Create elements of parameter ``funs`` with mkConst().
+
+ :param funs: the sorted functions
+ :param bound_vars: the list of parameters to the functions
+ :param terms: the list of function bodies of the functions
+ :param global: determines whether this definition is global (i.e. persists when popping the context)
+ :return: the function
+ """
cdef vector[c_Term] vf
cdef vector[vector[c_Term]] vbv
cdef vector[c_Term] vt
vf.push_back((<Term?> t).cterm)
def getAssertions(self):
+ """Get the list of asserted formulas.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-assertions )
+
+ :return: the list of asserted formulas
+ """
assertions = []
for a in self.csolver.getAssertions():
term = Term(self)
return assertions
def getInfo(self, str flag):
+ """Get info from the solver.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-info <info_flag> )
+
+ :param flag: the info flag
+ :return: the info
+ """
return self.csolver.getInfo(flag.encode())
def getOption(self, str option):
+ """Get the value of a given option.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-option <keyword> )
+
+ :param option: the option for which the value is queried
+ :return: a string representation of the option value
+ """
return self.csolver.getOption(option.encode())
def getUnsatAssumptions(self):
+ """
+ Get the set of unsat ("failed") assumptions.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-unsat-assumptions )
+
+ Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
+
+ :return: the set of unsat assumptions.
+ """
assumptions = []
for a in self.csolver.getUnsatAssumptions():
term = Term(self)
return assumptions
def getUnsatCore(self):
+ """Get the unsatisfiable core.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-unsat-core )
+
+ Requires to enable option :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
+
+ :return: a set of terms representing the unsatisfiable core
+ """
core = []
for a in self.csolver.getUnsatCore():
term = Term(self)
return core
def getValue(self, Term t):
+ """Get the value of the given term in the current model.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-value ( <term> ) )
+
+ :param term: the term for which the value is queried
+ :return: the value of the given term
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.getValue(t.cterm)
return term
+ def getModelDomainElements(self, Sort s):
+ """
+ Get the domain elements of uninterpreted sort s in the current model. The
+ current model interprets s as the finite sort whose domain elements are
+ given in the return value of this method.
+
+ :param s: The uninterpreted sort in question
+ :return: the domain elements of s in the current model
+ """
+ result = []
+ cresult = self.csolver.getModelDomainElements(s.csort)
+ for e in cresult:
+ term = Term(self)
+ term.cterm = e
+ result.append(term)
+ return result
+
+ def isModelCoreSymbol(self, Term v):
+ """
+ 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.
+
+ :param v: The term in question
+ :return: true if v is a model core symbol
+ """
+ return self.csolver.isModelCoreSymbol(v.cterm)
+
def getSeparationHeap(self):
+ """When using separation logic, obtain the term for the heap.
+
+ :return: The term for the heap
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.getSeparationHeap()
return term
- def declareSeparationHeap(self, Sort locType, Sort dataType):
- self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
-
def getSeparationNilTerm(self):
+ """When using separation logic, obtain the term for nil.
+
+ :return: The term for nil
+ """
cdef Term term = Term(self)
term.cterm = self.csolver.getSeparationNilTerm()
return term
+ def declareSeparationHeap(self, Sort locType, Sort dataType):
+ """
+ When using separation logic, this sets the location sort and the
+ datatype sort to the given ones. This method should be invoked exactly
+ once, before any separation logic constraints are provided.
+
+ :param locSort: The location sort of the heap
+ :param dataSort: The data sort of the heap
+ """
+ self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
+
def declarePool(self, str symbol, Sort sort, initValue):
+ """Declare a symbolic pool of terms with the given initial value.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( declare-pool <symbol> <sort> ( <term>* ) )
+
+ :param symbol: The name of the pool
+ :param sort: The sort of the elements of the pool.
+ :param initValue: The initial value of the pool
+ """
cdef Term term = Term(self)
cdef vector[c_Term] niv
for v in initValue:
return term
def pop(self, nscopes=1):
+ """Pop ``nscopes`` level(s) from the assertion stack.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( pop <numeral> )
+
+ :param nscopes: the number of levels to pop
+ """
self.csolver.pop(nscopes)
def push(self, nscopes=1):
+ """ Push ``nscopes`` level(s) to the assertion stack.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( push <numeral> )
+
+ :param nscopes: the number of levels to push
+ """
self.csolver.push(nscopes)
def resetAssertions(self):
+ """
+ Remove all assertions.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( reset-assertions )
+
+ """
self.csolver.resetAssertions()
def setInfo(self, str keyword, str value):
+ """Set info.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( set-info <attribute> )
+
+ :param keyword: the info flag
+ :param value: the value of the info flag
+ """
self.csolver.setInfo(keyword.encode(), value.encode())
def setLogic(self, str logic):
+ """Set logic.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( set-logic <symbol> )
+
+ :param logic: the logic to set
+ """
self.csolver.setLogic(logic.encode())
def setOption(self, str option, str value):
+ """Set option.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( set-option <option> )
+
+ :param option: the option name
+ :param value: the option value
+ """
self.csolver.setOption(option.encode(), value.encode())
def __hash__(self):
return csorthash(self.csort)
+ def isNull(self):
+ return self.csort.isNull()
+
def isBoolean(self):
return self.csort.isBoolean()
def isTester(self):
return self.csort.isTester()
+ def isUpdater(self):
+ return self.csort.isUpdater()
+
def isFunction(self):
return self.csort.isFunction()
def isBag(self):
return self.csort.isBag()
-
+
def isSequence(self):
return self.csort.isSequence()
cdef Sort sort = Sort(self.solver)
sort.csort = self.csort.getTesterCodomainSort()
return sort
-
+
def getFunctionArity(self):
return self.csort.getFunctionArity()
def getSortConstructorArity(self):
return self.csort.getSortConstructorArity()
- def getBVSize(self):
- return self.csort.getBVSize()
+ def getBitVectorSize(self):
+ return self.csort.getBitVectorSize()
- def getFPExponentSize(self):
- return self.csort.getFPExponentSize()
+ def getFloatingPointExponentSize(self):
+ return self.csort.getFloatingPointExponentSize()
- def getFPSignificandSize(self):
- return self.csort.getFPSignificandSize()
+ def getFloatingPointSignificandSize(self):
+ return self.csort.getFloatingPointSignificandSize()
def getDatatypeParamSorts(self):
param_sorts = []
# lists for substitutions
cdef vector[c_Term] ces
cdef vector[c_Term] creplacements
-
+
# normalize the input parameters to be lists
if isinstance(term_or_list_1, list):
assert isinstance(term_or_list_2, list)
# add the single elements to the vectors
ces.push_back((<Term?> term_or_list_1).cterm)
creplacements.push_back((<Term?> term_or_list_2).cterm)
-
+
# call the API substitute method with lists
term.cterm = self.cterm.substitute(ces, creplacements)
return term
def isNull(self):
return self.cterm.isNull()
- def getConstArrayBase(self):
- cdef Term term = Term(self.solver)
- term.cterm = self.cterm.getConstArrayBase()
- return term
-
- def getConstSequenceElements(self):
- elems = []
- for e in self.cterm.getConstSequenceElements():
- term = Term(self.solver)
- term.cterm = e
- elems.append(term)
- return elems
-
def notTerm(self):
cdef Term term = Term(self.solver)
term.cterm = self.cterm.notTerm()
term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
return term
- def isInteger(self):
- return self.cterm.isInteger()
-
+ def isConstArray(self):
+ return self.cterm.isConstArray()
+
+ def getConstArrayBase(self):
+ cdef Term term = Term(self.solver)
+ term.cterm = self.cterm.getConstArrayBase()
+ return term
+
+ def isBooleanValue(self):
+ return self.cterm.isBooleanValue()
+
+ def getBooleanValue(self):
+ return self.cterm.getBooleanValue()
+
+ def isStringValue(self):
+ return self.cterm.isStringValue()
+
+ def getStringValue(self):
+ cdef Py_ssize_t size
+ cdef c_wstring s = self.cterm.getStringValue()
+ return PyUnicode_FromWideChar(s.data(), s.size())
+
+ def isIntegerValue(self):
+ return self.cterm.isIntegerValue()
+ def isAbstractValue(self):
+ return self.cterm.isAbstractValue()
+
+ def getAbstractValue(self):
+ return self.cterm.getAbstractValue().decode()
+
+ def isFloatingPointPosZero(self):
+ return self.cterm.isFloatingPointPosZero()
+
+ def isFloatingPointNegZero(self):
+ return self.cterm.isFloatingPointNegZero()
+
+ def isFloatingPointPosInf(self):
+ return self.cterm.isFloatingPointPosInf()
+
+ def isFloatingPointNegInf(self):
+ return self.cterm.isFloatingPointNegInf()
+
+ def isFloatingPointNaN(self):
+ return self.cterm.isFloatingPointNaN()
+
+ def isFloatingPointValue(self):
+ return self.cterm.isFloatingPointValue()
+
+ def getFloatingPointValue(self):
+ cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
+ cdef Term term = Term(self.solver)
+ term.cterm = get2(t)
+ return (get0(t), get1(t), term)
+
+ def isSetValue(self):
+ return self.cterm.isSetValue()
+
+ def getSetValue(self):
+ elems = set()
+ for e in self.cterm.getSetValue():
+ term = Term(self.solver)
+ term.cterm = e
+ elems.add(term)
+ return elems
+
+ def isSequenceValue(self):
+ return self.cterm.isSequenceValue()
+
+ def getSequenceValue(self):
+ elems = []
+ for e in self.cterm.getSequenceValue():
+ term = Term(self.solver)
+ term.cterm = e
+ elems.append(term)
+ return elems
+
+ def isUninterpretedValue(self):
+ return self.cterm.isUninterpretedValue()
+
+ def getUninterpretedValue(self):
+ cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue()
+ cdef Sort sort = Sort(self.solver)
+ sort.csort = p.first
+ i = p.second
+ return (sort, i)
+
+ def isTupleValue(self):
+ return self.cterm.isTupleValue()
+
+ def getTupleValue(self):
+ elems = []
+ for e in self.cterm.getTupleValue():
+ term = Term(self.solver)
+ term.cterm = e
+ elems.append(term)
+ return elems
+
+ def getIntegerValue(self):
+ return int(self.cterm.getIntegerValue().decode())
+
+ def isRealValue(self):
+ return self.cterm.isRealValue()
+
+ def getRealValue(self):
+ """Returns the value of a real term as a Fraction"""
+ return Fraction(self.cterm.getRealValue().decode())
+
+ def isBitVectorValue(self):
+ return self.cterm.isBitVectorValue()
+
+ def getBitVectorValue(self, base = 2):
+ """Returns the value of a bit-vector term as a 0/1 string"""
+ return self.cterm.getBitVectorValue(base).decode()
+
def toPythonObj(self):
- '''
+ """
Converts a constant value Term to a Python object.
Currently supports:
Int -- returns a Python int
Real -- returns a Python Fraction
BV -- returns a Python int (treats BV as unsigned)
+ String -- returns a Python Unicode string
Array -- returns a Python dict mapping indices to values
-- the constant base is returned as the default value
- String -- returns a Python Unicode string
- '''
-
- string_repr = self.cterm.toString().decode()
- assert string_repr
- sort = self.getSort()
- res = None
- if sort.isBoolean():
- if string_repr == "true":
- res = True
- else:
- assert string_repr == "false"
- res = False
-
- elif sort.isInteger():
- updated_string_repr = string_repr.strip('()').replace(' ', '')
- try:
- res = int(updated_string_repr)
- except:
- raise ValueError("Failed to convert"
- " {} to an int".format(string_repr))
-
- elif sort.isReal():
- updated_string_repr = string_repr
- try:
- # rational format (/ a b) most likely
- # note: a or b could be negated: (- a)
- splits = [s.strip('()/')
- for s in updated_string_repr.strip('()/') \
- .replace('(- ', '(-').split()]
- assert len(splits) == 2
- num = int(splits[0])
- den = int(splits[1])
- res = Fraction(num, den)
- except:
- try:
- # could be exact: e.g., 1.0
- res = Fraction(updated_string_repr)
- except:
- raise ValueError("Failed to convert "
- "{} to a Fraction".format(string_repr))
-
- elif sort.isBitVector():
- # expecting format #b<bits>
- assert string_repr[:2] == "#b"
- python_bin_repr = "0" + string_repr[1:]
- try:
- res = int(python_bin_repr, 2)
- except:
- raise ValueError("Failed to convert bitvector "
- "{} to an int".format(string_repr))
-
- elif sort.isArray():
+ """
+
+ if self.isBooleanValue():
+ return self.getBooleanValue()
+ elif self.isIntegerValue():
+ return self.getIntegerValue()
+ elif self.isRealValue():
+ return self.getRealValue()
+ elif self.isBitVectorValue():
+ return int(self.getBitVectorValue(), 2)
+ elif self.isStringValue():
+ return self.getStringValue()
+ elif self.getSort().isArray():
+ res = None
keys = []
values = []
base_value = None
for k, v in zip(keys, values):
res[k] = v
- elif sort.isString():
- # Strip leading and trailing double quotes and replace double
- # double quotes by single quotes
- string_repr = string_repr[1:-1].replace('""', '"')
-
- # Convert escape sequences
- res = ''
- escape_prefix = '\\u{'
- i = 0
- while True:
- prev_i = i
- i = string_repr.find(escape_prefix, i)
- if i == -1:
- res += string_repr[prev_i:]
- break
-
- res += string_repr[prev_i:i]
- val = string_repr[i + len(escape_prefix):string_repr.find('}', i)]
- res += chr(int(val, 16))
- i += len(escape_prefix) + len(val) + 1
- else:
- raise ValueError("Cannot convert term {}"
- " of sort {} to Python object".format(string_repr,
- sort))
-
- assert res is not None
- return res
+ return res
# Generate rounding modes
del r
del rm_int
del name
+
+
+# Generate unknown explanations
+cdef __unknown_explanations = {
+ <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
+ <int> INCOMPLETE: "Incomplete",
+ <int> TIMEOUT: "Timeout",
+ <int> RESOURCEOUT: "Resourceout",
+ <int> MEMOUT: "Memout",
+ <int> INTERRUPTED: "Interrupted",
+ <int> NO_STATUS: "NoStatus",
+ <int> UNSUPPORTED: "Unsupported",
+ <int> OTHER: "Other",
+ <int> UNKNOWN_REASON: "UnknownReason"
+}
+
+for ue_int, name in __unknown_explanations.items():
+ u = UnknownExplanation(ue_int)
+
+ if name in dir(mod_ref):
+ raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
+
+ setattr(mod_ref, name, u)
+
+del u
+del ue_int
+del name
projects / cvc5.git / blobdiff