1 from collections import defaultdict
2 from fractions import Fraction
3 from functools import wraps
6 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
7 from libc.stddef cimport wchar_t
9 from libcpp.pair cimport pair
10 from libcpp.set cimport set as c_set
11 from libcpp.string cimport string
12 from libcpp.vector cimport vector
14 from cvc5 cimport cout
15 from cvc5 cimport Datatype as c_Datatype
16 from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
17 from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
18 from cvc5 cimport DatatypeDecl as c_DatatypeDecl
19 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
20 from cvc5 cimport Result as c_Result
21 from cvc5 cimport RoundingMode as c_RoundingMode
22 from cvc5 cimport UnknownExplanation as c_UnknownExplanation
23 from cvc5 cimport Op as c_Op
24 from cvc5 cimport Solver as c_Solver
25 from cvc5 cimport Grammar as c_Grammar
26 from cvc5 cimport Sort as c_Sort
27 from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
28 from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
29 from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
30 from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT
31 from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED
32 from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON
33 from cvc5 cimport OTHER
34 from cvc5 cimport Term as c_Term
35 from cvc5 cimport hash as c_hash
36 from cvc5 cimport wstring as c_wstring
37 from cvc5 cimport tuple as c_tuple
38 from cvc5 cimport get0, get1, get2
39 from cvc5kinds cimport Kind as c_Kind
41 cdef extern from "Python.h":
42 wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
43 object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
44 void PyMem_Free(void*)
46 ################################## DECORATORS #################################
47 def expand_list_arg(num_req_args=0):
49 Creates a decorator that looks at index num_req_args of the args,
50 if it's a list, it expands it before calling the function.
54 def wrapper(owner, *args):
55 if len(args) == num_req_args + 1 and \
56 isinstance(args[num_req_args], list):
57 args = list(args[:num_req_args]) + args[num_req_args]
58 return func(owner, *args)
61 ###############################################################################
64 ### Using PEP-8 spacing recommendations
65 ### Limit linewidth to 79 characters
66 ### Break before binary operators
67 ### surround top level functions and classes with two spaces
68 ### separate methods by one space
69 ### use spaces in functions sparingly to separate logical blocks
70 ### can omit spaces between unrelated oneliners
71 ### always use c++ default arguments
72 #### only use default args of None at python level
74 # References and pointers
75 # The Solver object holds a pointer to a c_Solver.
76 # This is because the assignment operator is deleted in the C++ API for solvers.
77 # Cython has a limitation where you can't stack allocate objects
78 # that have constructors with arguments:
79 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
80 # To get around that you can either have a nullary constructor and assignment
81 # or, use a pointer (which is what we chose).
82 # An additional complication of this is that to free up resources, you must
83 # know when to delete the object.
84 # Python will not follow the same scoping rules as in C++, so it must be
85 # able to reference count. To do this correctly, the solver must be a
86 # reference in the Python class for any class that keeps a pointer to
87 # the solver in C++ (to ensure the solver is not deleted before something
88 # that depends on it).
91 ## Objects for hashing
92 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
93 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
94 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
100 Wrapper class for :cpp:class:`cvc5::api::Datatype`.
104 def __cinit__(self, Solver solver):
107 def __getitem__(self, index):
108 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
109 if isinstance(index, int) and index >= 0:
110 dc.cdc = self.cd[(<int?> index)]
111 elif isinstance(index, str):
112 dc.cdc = self.cd[(<const string &> index.encode())]
114 raise ValueError("Expecting a non-negative integer or string")
117 def getConstructor(self, str name):
119 :param name: the name of the constructor.
120 :return: a constructor by name.
122 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
123 dc.cdc = self.cd.getConstructor(name.encode())
126 def getConstructorTerm(self, str name):
128 :param name: the name of the constructor.
129 :return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`).
131 cdef Term term = Term(self.solver)
132 term.cterm = self.cd.getConstructorTerm(name.encode())
135 def getSelector(self, str name):
137 :param name: the name of the selector..
138 :return: a selector by name.
140 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
141 ds.cds = self.cd.getSelector(name.encode())
146 :return: the name of the datatype.
148 return self.cd.getName().decode()
150 def getNumConstructors(self):
152 :return: number of constructors in this datatype.
154 return self.cd.getNumConstructors()
156 def getParameters(self):
158 :return: the parameters of this datatype, if it is parametric. An exception is thrown if this datatype is not parametric.
161 for s in self.cd.getParameters():
162 sort = Sort(self.solver)
164 param_sorts.append(sort)
167 def isParametric(self):
168 """:return: True if this datatype is parametric."""
169 return self.cd.isParametric()
171 def isCodatatype(self):
172 """:return: True if this datatype corresponds to a co-datatype."""
173 return self.cd.isCodatatype()
176 """:return: True if this datatype corresponds to a tuple."""
177 return self.cd.isTuple()
180 """:return: True if this datatype corresponds to a record."""
181 return self.cd.isRecord()
184 """:return: True if this datatype is finite."""
185 return self.cd.isFinite()
187 def isWellFounded(self):
188 """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
189 return self.cd.isWellFounded()
192 """:return: True if this Datatype is a null object."""
193 return self.cd.isNull()
196 return self.cd.toString().decode()
199 return self.cd.toString().decode()
203 dc = DatatypeConstructor(self.solver)
208 cdef class DatatypeConstructor:
210 A cvc5 datatype constructor.
211 Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.
213 cdef c_DatatypeConstructor cdc
215 def __cinit__(self, Solver solver):
216 self.cdc = c_DatatypeConstructor()
219 def __getitem__(self, index):
220 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
221 if isinstance(index, int) and index >= 0:
222 ds.cds = self.cdc[(<int?> index)]
223 elif isinstance(index, str):
224 ds.cds = self.cdc[(<const string &> index.encode())]
226 raise ValueError("Expecting a non-negative integer or string")
231 :return: the name of the constructor.
233 return self.cdc.getName().decode()
235 def getConstructorTerm(self):
237 :return: the constructor operator as a term.
239 cdef Term term = Term(self.solver)
240 term.cterm = self.cdc.getConstructorTerm()
243 def getInstantiatedConstructorTerm(self, Sort retSort):
245 Specialized method for parametric datatypes (see
246 :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm()
247 <cvc5::api::DatatypeConstructor::getInstantiatedConstructorTerm>`).
249 :param retSort: the desired return sort of the constructor
250 :return: the constructor operator as a term.
252 cdef Term term = Term(self.solver)
253 term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort)
256 def getTesterTerm(self):
258 :return: the tester operator that is related to this constructor, as a term.
260 cdef Term term = Term(self.solver)
261 term.cterm = self.cdc.getTesterTerm()
264 def getNumSelectors(self):
266 :return: the number of selecters (so far) of this Datatype constructor.
268 return self.cdc.getNumSelectors()
270 def getSelector(self, str name):
272 :param name: the name of the datatype selector.
273 :return: the first datatype selector with the given name
275 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
276 ds.cds = self.cdc.getSelector(name.encode())
279 def getSelectorTerm(self, str name):
281 :param name: the name of the datatype selector.
282 :return: a term representing the firstdatatype selector with the given name.
284 cdef Term term = Term(self.solver)
285 term.cterm = self.cdc.getSelectorTerm(name.encode())
289 """:return: True if this DatatypeConstructor is a null object."""
290 return self.cdc.isNull()
293 return self.cdc.toString().decode()
296 return self.cdc.toString().decode()
300 ds = DatatypeSelector(self.solver)
305 cdef class DatatypeConstructorDecl:
307 A cvc5 datatype constructor declaration.
308 Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.
310 cdef c_DatatypeConstructorDecl cddc
313 def __cinit__(self, Solver solver):
316 def addSelector(self, str name, Sort sort):
318 Add datatype selector declaration.
320 :param name: the name of the datatype selector declaration to add.
321 :param sort: the codomain sort of the datatype selector declaration
324 self.cddc.addSelector(name.encode(), sort.csort)
326 def addSelectorSelf(self, str name):
328 Add datatype selector declaration whose codomain sort is the
331 :param name: the name of the datatype selector declaration to add.
333 self.cddc.addSelectorSelf(name.encode())
336 """:return: True if this DatatypeConstructorDecl is a null object."""
337 return self.cddc.isNull()
340 return self.cddc.toString().decode()
343 return self.cddc.toString().decode()
346 cdef class DatatypeDecl:
348 A cvc5 datatype declaration.
349 Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.
351 cdef c_DatatypeDecl cdd
353 def __cinit__(self, Solver solver):
356 def addConstructor(self, DatatypeConstructorDecl ctor):
358 Add a datatype constructor declaration.
360 :param ctor: the datatype constructor declaration to add.
362 self.cdd.addConstructor(ctor.cddc)
364 def getNumConstructors(self):
366 :return: number of constructors (so far) for this datatype declaration.
368 return self.cdd.getNumConstructors()
370 def isParametric(self):
372 :return: is this datatype declaration parametric?
374 return self.cdd.isParametric()
378 :return: the name of this datatype declaration.
380 return self.cdd.getName().decode()
383 """:return: True if this DatatypeDecl is a null object."""
384 return self.cdd.isNull()
387 return self.cdd.toString().decode()
390 return self.cdd.toString().decode()
393 cdef class DatatypeSelector:
395 A cvc5 datatype selector.
396 Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.
398 cdef c_DatatypeSelector cds
400 def __cinit__(self, Solver solver):
401 self.cds = c_DatatypeSelector()
406 :return: the name of this datatype selector.
408 return self.cds.getName().decode()
410 def getSelectorTerm(self):
412 :return: the selector opeartor of this datatype selector as a term.
414 cdef Term term = Term(self.solver)
415 term.cterm = self.cds.getSelectorTerm()
418 def getUpdaterTerm(self):
420 :return: the updater opeartor of this datatype selector as a term.
422 cdef Term term = Term(self.solver)
423 term.cterm = self.cds.getUpdaterTerm()
426 def getCodomainSort(self):
428 :return: the codomain sort of this selector.
430 cdef Sort sort = Sort(self.solver)
431 sort.csort = self.cds.getCodomainSort()
435 """:return: True if this DatatypeSelector is a null object."""
436 return self.cds.isNull()
439 return self.cds.toString().decode()
442 return self.cds.toString().decode()
448 An operator is a term that represents certain operators,
449 instantiated with its required parameters, e.g.,
450 a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`.
451 Wrapper class for :cpp:class:`cvc5::api::Op`.
455 def __cinit__(self, Solver solver):
459 def __eq__(self, Op other):
460 return self.cop == other.cop
462 def __ne__(self, Op other):
463 return self.cop != other.cop
466 return self.cop.toString().decode()
469 return self.cop.toString().decode()
472 return cophash(self.cop)
476 :return: the kind of this operator.
478 return Kind(<int> self.cop.getKind())
482 :return: True iff this operator is indexed.
484 return self.cop.isIndexed()
488 :return: True iff this operator is a null term.
490 return self.cop.isNull()
492 def getNumIndices(self):
494 :return: number of indices of this op.
496 return self.cop.getNumIndices()
498 def getIndices(self):
500 :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() <cvc5::api::Op::getIndices>`).
504 indices = self.cop.getIndices[string]().decode()
509 indices = self.cop.getIndices[uint32_t]()
514 indices = self.cop.getIndices[pair[uint32_t, uint32_t]]()
519 raise RuntimeError("Unable to retrieve indices from {}".format(self))
526 Wrapper class for :cpp:class:`cvc5::api::Grammar`.
528 cdef c_Grammar cgrammar
530 def __cinit__(self, Solver solver):
532 self.cgrammar = c_Grammar()
534 def addRule(self, Term ntSymbol, Term rule):
536 Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
538 :param ntSymbol: the non-terminal to which the rule is added.
539 :param rule: the rule to add.
541 self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
543 def addAnyConstant(self, Term ntSymbol):
545 Allow ``ntSymbol`` to be an arbitrary constant.
547 :param ntSymbol: the non-terminal allowed to be constant.
549 self.cgrammar.addAnyConstant(ntSymbol.cterm)
551 def addAnyVariable(self, Term ntSymbol):
553 Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``.
555 :param ntSymbol: the non-terminal allowed to be any input variable.
557 self.cgrammar.addAnyVariable(ntSymbol.cterm)
559 def addRules(self, Term ntSymbol, rules):
561 Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
563 :param ntSymbol: the non-terminal to which the rules are added.
564 :param rules: the rules to add.
566 cdef vector[c_Term] crules
568 crules.push_back((<Term?> r).cterm)
569 self.cgrammar.addRules(ntSymbol.cterm, crules)
573 Encapsulation of a three-valued solver result, with explanations.
574 Wrapper class for :cpp:class:`cvc5::api::Result`.
578 # gets populated by solver
583 :return: True if Result is empty, i.e., a nullary Result, and not an actual result returned from a
584 :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` (and friends) query.
586 return self.cr.isNull()
590 :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.
592 return self.cr.isSat()
596 :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.
598 return self.cr.isUnsat()
600 def isSatUnknown(self):
602 :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.
604 return self.cr.isSatUnknown()
606 def isEntailed(self):
608 :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query.
610 return self.cr.isEntailed()
612 def isNotEntailed(self):
614 :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query that is not entailed.
616 return self.cr.isNotEntailed()
618 def isEntailmentUnknown(self):
620 :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.
622 return self.cr.isEntailmentUnknown()
624 def getUnknownExplanation(self):
626 :return: an explanation for an unknown query result.
628 return UnknownExplanation(<int> self.cr.getUnknownExplanation())
630 def __eq__(self, Result other):
631 return self.cr == other.cr
633 def __ne__(self, Result other):
634 return self.cr != other.cr
637 return self.cr.toString().decode()
640 return self.cr.toString().decode()
643 cdef class RoundingMode:
645 Rounding modes for floating-point numbers.
647 For many floating-point operations, infinitely precise results may not be
648 representable with the number of available bits. Thus, the results are
649 rounded in a certain way to one of the representable floating-point numbers.
651 These rounding modes directly follow the SMT-LIB theory for floating-point
652 arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
653 The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
656 Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`.
658 cdef c_RoundingMode crm
660 def __cinit__(self, int rm):
661 # crm always assigned externally
662 self.crm = <c_RoundingMode> rm
663 self.name = __rounding_modes[rm]
665 def __eq__(self, RoundingMode other):
666 return (<int> self.crm) == (<int> other.crm)
668 def __ne__(self, RoundingMode other):
669 return not self.__eq__(other)
672 return hash((<int> self.crm, self.name))
681 cdef class UnknownExplanation:
683 Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`.
685 cdef c_UnknownExplanation cue
687 def __cinit__(self, int ue):
688 # crm always assigned externally
689 self.cue = <c_UnknownExplanation> ue
690 self.name = __unknown_explanations[ue]
692 def __eq__(self, UnknownExplanation other):
693 return (<int> self.cue) == (<int> other.cue)
695 def __ne__(self, UnknownExplanation other):
696 return not self.__eq__(other)
699 return hash((<int> self.crm, self.name))
709 """Wrapper class for :cpp:class:`cvc5::api::Solver`."""
710 cdef c_Solver* csolver
713 self.csolver = new c_Solver()
715 def __dealloc__(self):
718 def getBooleanSort(self):
719 """:return: sort Boolean
721 cdef Sort sort = Sort(self)
722 sort.csort = self.csolver.getBooleanSort()
725 def getIntegerSort(self):
726 """:return: sort Integer
728 cdef Sort sort = Sort(self)
729 sort.csort = self.csolver.getIntegerSort()
732 def getNullSort(self):
733 """:return: sort null
735 cdef Sort sort = Sort(self)
736 sort.csort = self.csolver.getNullSort()
739 def getRealSort(self):
740 """:return: sort Real
742 cdef Sort sort = Sort(self)
743 sort.csort = self.csolver.getRealSort()
746 def getRegExpSort(self):
747 """:return: sort of RegExp
749 cdef Sort sort = Sort(self)
750 sort.csort = self.csolver.getRegExpSort()
753 def getRoundingModeSort(self):
754 """:return: sort RoundingMode
756 cdef Sort sort = Sort(self)
757 sort.csort = self.csolver.getRoundingModeSort()
760 def getStringSort(self):
761 """:return: sort String
763 cdef Sort sort = Sort(self)
764 sort.csort = self.csolver.getStringSort()
767 def mkArraySort(self, Sort indexSort, Sort elemSort):
768 """Create an array sort.
770 :param indexSort: the array index sort
771 :param elemSort: the array element sort
772 :return: the array sort
774 cdef Sort sort = Sort(self)
775 sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
778 def mkBitVectorSort(self, uint32_t size):
779 """Create a bit-vector sort.
781 :param size: the bit-width of the bit-vector sort
782 :return: the bit-vector sort
784 cdef Sort sort = Sort(self)
785 sort.csort = self.csolver.mkBitVectorSort(size)
788 def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
789 """Create a floating-point sort.
791 :param exp: the bit-width of the exponent of the floating-point sort.
792 :param sig: the bit-width of the significand of the floating-point sort.
794 cdef Sort sort = Sort(self)
795 sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
798 def mkDatatypeSort(self, DatatypeDecl dtypedecl):
799 """Create a datatype sort.
801 :param dtypedecl: the datatype declaration from which the sort is created
802 :return: the datatype sort
804 cdef Sort sort = Sort(self)
805 sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
808 def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
810 Create a vector of datatype sorts using unresolved sorts. The names of
811 the datatype declarations in dtypedecls must be distinct.
813 This method is called when the DatatypeDecl objects dtypedecls have been
814 built using "unresolved" sorts.
816 We associate each sort in unresolvedSorts with exacly one datatype from
817 dtypedecls. In particular, it must have the same name as exactly one
818 datatype declaration in dtypedecls.
820 When constructing datatypes, unresolved sorts are replaced by the datatype
821 sort constructed for the datatype declaration it is associated with.
823 :param dtypedecls: the datatype declarations from which the sort is created
824 :param unresolvedSorts: the list of unresolved sorts
825 :return: the datatype sorts
827 if unresolvedSorts == None:
828 unresolvedSorts = set([])
830 assert isinstance(unresolvedSorts, set)
833 cdef vector[c_DatatypeDecl] decls
834 for decl in dtypedecls:
835 decls.push_back((<DatatypeDecl?> decl).cdd)
837 cdef c_set[c_Sort] usorts
838 for usort in unresolvedSorts:
839 usorts.insert((<Sort?> usort).csort)
841 csorts = self.csolver.mkDatatypeSorts(
842 <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
850 def mkFunctionSort(self, sorts, Sort codomain):
851 """ Create function sort.
853 :param sorts: the sort of the function arguments
854 :param codomain: the sort of the function return value
855 :return: the function sort
858 cdef Sort sort = Sort(self)
859 # populate a vector with dereferenced c_Sorts
860 cdef vector[c_Sort] v
862 if isinstance(sorts, Sort):
863 sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
865 elif isinstance(sorts, list):
867 v.push_back((<Sort?>s).csort)
869 sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
873 def mkParamSort(self, symbolname):
874 """ Create a sort parameter.
876 :param symbol: the name of the sort
877 :return: the sort parameter
879 cdef Sort sort = Sort(self)
880 sort.csort = self.csolver.mkParamSort(symbolname.encode())
883 @expand_list_arg(num_req_args=0)
884 def mkPredicateSort(self, *sorts):
885 """Create a predicate sort.
887 :param sorts: the list of sorts of the predicate, as a list or as distinct arguments.
888 :return: the predicate sort
890 cdef Sort sort = Sort(self)
891 cdef vector[c_Sort] v
893 v.push_back((<Sort?> s).csort)
894 sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
897 @expand_list_arg(num_req_args=0)
898 def mkRecordSort(self, *fields):
899 """Create a record sort
901 :param fields: the list of fields of the record, as a list or as distinct arguments
902 :return: the record sort
904 cdef Sort sort = Sort(self)
905 cdef vector[pair[string, c_Sort]] v
906 cdef pair[string, c_Sort] p
910 p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
912 sort.csort = self.csolver.mkRecordSort(
913 <const vector[pair[string, c_Sort]] &> v)
916 def mkSetSort(self, Sort elemSort):
917 """Create a set sort.
919 :param elemSort: the sort of the set elements
920 :return: the set sort
922 cdef Sort sort = Sort(self)
923 sort.csort = self.csolver.mkSetSort(elemSort.csort)
926 def mkBagSort(self, Sort elemSort):
927 """Create a bag sort.
929 :param elemSort: the sort of the bag elements
930 :return: the bag sort
932 cdef Sort sort = Sort(self)
933 sort.csort = self.csolver.mkBagSort(elemSort.csort)
936 def mkSequenceSort(self, Sort elemSort):
937 """Create a sequence sort.
939 :param elemSort: the sort of the sequence elements
940 :return: the sequence sort
942 cdef Sort sort = Sort(self)
943 sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
946 def mkUninterpretedSort(self, str name):
947 """Create an uninterpreted sort.
949 :param symbol: the name of the sort
950 :return: the uninterpreted sort
952 cdef Sort sort = Sort(self)
953 sort.csort = self.csolver.mkUninterpretedSort(name.encode())
956 def mkUnresolvedSort(self, str name, size_t arity = 0):
957 """Create an unresolved sort.
959 This is for creating yet unresolved sort placeholders for mutually
962 :param symbol: the name of the sort
963 :param arity: the number of sort parameters of the sort
964 :return: the unresolved sort
966 cdef Sort sort = Sort(self)
967 sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity)
970 def mkSortConstructorSort(self, str symbol, size_t arity):
971 """Create a sort constructor sort.
973 :param symbol: the symbol of the sort
974 :param arity: the arity of the sort
975 :return: the sort constructor sort
977 cdef Sort sort = Sort(self)
978 sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
981 @expand_list_arg(num_req_args=0)
982 def mkTupleSort(self, *sorts):
983 """Create a tuple sort.
985 :param sorts: of the elements of the tuple, as a list or as distinct arguments
986 :return: the tuple sort
988 cdef Sort sort = Sort(self)
989 cdef vector[c_Sort] v
991 v.push_back((<Sort?> s).csort)
992 sort.csort = self.csolver.mkTupleSort(v)
995 @expand_list_arg(num_req_args=1)
996 def mkTerm(self, kind_or_op, *args):
998 Supports the following arguments:
1000 - ``Term mkTerm(Kind kind)``
1001 - ``Term mkTerm(Kind kind, Op child1, List[Term] children)``
1002 - ``Term mkTerm(Kind kind, List[Term] children)``
1004 where ``List[Term]`` can also be comma-separated arguments
1006 cdef Term term = Term(self)
1007 cdef vector[c_Term] v
1010 if isinstance(kind_or_op, Kind):
1011 op = self.mkOp(kind_or_op)
1014 term.cterm = self.csolver.mkTerm((<Op?> op).cop)
1017 v.push_back((<Term?> a).cterm)
1018 term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
1021 def mkTuple(self, sorts, terms):
1022 """Create a tuple term. Terms are automatically converted if sorts are compatible.
1024 :param sorts: The sorts of the elements in the tuple
1025 :param terms: The elements in the tuple
1026 :return: the tuple Term
1028 cdef vector[c_Sort] csorts
1029 cdef vector[c_Term] cterms
1032 csorts.push_back((<Sort?> s).csort)
1034 cterms.push_back((<Term?> s).cterm)
1035 cdef Term result = Term(self)
1036 result.cterm = self.csolver.mkTuple(csorts, cterms)
1039 @expand_list_arg(num_req_args=0)
1040 def mkOp(self, k, *args):
1042 Supports the following uses:
1044 - ``Op mkOp(Kind kind)``
1045 - ``Op mkOp(Kind kind, Kind k)``
1046 - ``Op mkOp(Kind kind, const string& arg)``
1047 - ``Op mkOp(Kind kind, uint32_t arg)``
1048 - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
1049 - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind)
1051 cdef Op op = Op(self)
1052 cdef vector[uint32_t] v
1055 op.cop = self.csolver.mkOp(<c_Kind> k.value)
1056 elif len(args) == 1:
1057 if isinstance(args[0], str):
1058 op.cop = self.csolver.mkOp(<c_Kind> k.value,
1061 elif isinstance(args[0], int):
1062 op.cop = self.csolver.mkOp(<c_Kind> k.value, <int?> args[0])
1063 elif isinstance(args[0], list):
1065 if a < 0 or a >= 2 ** 31:
1066 raise ValueError("Argument {} must fit in a uint32_t".format(a))
1068 v.push_back((<uint32_t?> a))
1069 op.cop = self.csolver.mkOp(<c_Kind> k.value, <const vector[uint32_t]&> v)
1071 raise ValueError("Unsupported signature"
1072 " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
1073 elif len(args) == 2:
1074 if isinstance(args[0], int) and isinstance(args[1], int):
1075 op.cop = self.csolver.mkOp(<c_Kind> k.value, <int> args[0], <int> args[1])
1077 raise ValueError("Unsupported signature"
1078 " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
1082 """Create a Boolean true constant.
1084 :return: the true constant
1086 cdef Term term = Term(self)
1087 term.cterm = self.csolver.mkTrue()
1091 """Create a Boolean false constant.
1093 :return: the false constant
1095 cdef Term term = Term(self)
1096 term.cterm = self.csolver.mkFalse()
1099 def mkBoolean(self, bint val):
1100 """Create a Boolean constant.
1102 :return: the Boolean constant
1103 :param val: the value of the constant
1105 cdef Term term = Term(self)
1106 term.cterm = self.csolver.mkBoolean(val)
1110 """Create a constant representing the number Pi.
1112 :return: a constant representing Pi
1114 cdef Term term = Term(self)
1115 term.cterm = self.csolver.mkPi()
1118 def mkInteger(self, val):
1119 """Create an integer constant.
1121 :param val: representation of the constant: either a string or integer
1122 :return: a constant of sort Integer
1124 cdef Term term = Term(self)
1125 if isinstance(val, str):
1126 term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
1128 assert(isinstance(val, int))
1129 term.cterm = self.csolver.mkInteger((<int?> val))
1132 def mkReal(self, val, den=None):
1133 """Create a real constant.
1135 :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.
1136 :param den: if not None, the value is `val`/`den`
1137 :return: a real term with literal value
1139 Can be used in various forms:
1141 - Given a string ``"N/D"`` constructs the corresponding rational.
1142 - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
1143 - 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``.
1144 - Given a string ``"W"`` or an integer, constructs that integer.
1145 - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``.
1147 cdef Term term = Term(self)
1149 term.cterm = self.csolver.mkReal(str(val).encode())
1151 if not isinstance(val, int) or not isinstance(den, int):
1152 raise ValueError("Expecting integers when"
1153 " constructing a rational"
1154 " but got: {}".format((val, den)))
1155 term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
1158 def mkRegexpAll(self):
1159 """Create a regular expression all (re.all) term.
1161 :return: the all term
1163 cdef Term term = Term(self)
1164 term.cterm = self.csolver.mkRegexpAll()
1167 def mkRegexpAllchar(self):
1168 """Create a regular expression allchar (re.allchar) term.
1170 :return: the allchar term
1172 cdef Term term = Term(self)
1173 term.cterm = self.csolver.mkRegexpAllchar()
1176 def mkRegexpNone(self):
1177 """Create a regular expression none (re.none) term.
1179 :return: the none term
1181 cdef Term term = Term(self)
1182 term.cterm = self.csolver.mkRegexpNone()
1185 def mkEmptySet(self, Sort s):
1186 """Create a constant representing an empty set of the given sort.
1188 :param sort: the sort of the set elements.
1189 :return: the empty set constant
1191 cdef Term term = Term(self)
1192 term.cterm = self.csolver.mkEmptySet(s.csort)
1195 def mkEmptyBag(self, Sort s):
1196 """Create a constant representing an empty bag of the given sort.
1198 :param sort: the sort of the bag elements.
1199 :return: the empty bag constant
1201 cdef Term term = Term(self)
1202 term.cterm = self.csolver.mkEmptyBag(s.csort)
1206 """Create a separation logic empty term.
1208 :return: the separation logic empty term
1210 cdef Term term = Term(self)
1211 term.cterm = self.csolver.mkSepEmp()
1214 def mkSepNil(self, Sort sort):
1215 """Create a separation logic nil term.
1217 :param sort: the sort of the nil term
1218 :return: the separation logic nil term
1220 cdef Term term = Term(self)
1221 term.cterm = self.csolver.mkSepNil(sort.csort)
1224 def mkString(self, str s, useEscSequences = None):
1226 Create a String constant from a `str` which may contain SMT-LIB
1227 compatible escape sequences like ``\\u1234`` to encode unicode characters.
1229 :param s: the string this constant represents
1230 :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character
1231 :return: the String constant
1233 cdef Term term = Term(self)
1234 cdef Py_ssize_t size
1235 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1236 if isinstance(useEscSequences, bool):
1237 term.cterm = self.csolver.mkString(
1238 s.encode(), <bint> useEscSequences)
1240 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1244 def mkEmptySequence(self, Sort sort):
1245 """Create an empty sequence of the given element sort.
1247 :param sort: The element sort of the sequence.
1248 :return: the empty sequence with given element sort.
1250 cdef Term term = Term(self)
1251 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1254 def mkUniverseSet(self, Sort sort):
1255 """Create a universe set of the given sort.
1257 :param sort: the sort of the set elements
1258 :return: the universe set constant
1260 cdef Term term = Term(self)
1261 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1264 @expand_list_arg(num_req_args=0)
1265 def mkBitVector(self, *args):
1267 Supports the following arguments:
1269 - ``Term mkBitVector(int size, int val=0)``
1270 - ``Term mkBitVector(int size, string val, int base)``
1272 :return: a bit-vector literal term
1273 :param size: an integer size.
1274 :param val: an integer representating the value, in the first form. In the second form, a string representing the value.
1275 :param base: the base of the string representation (second form only)
1277 cdef Term term = Term(self)
1279 raise ValueError("Missing arguments to mkBitVector")
1281 if not isinstance(size, int):
1283 "Invalid first argument to mkBitVector '{}', "
1284 "expected bit-vector size".format(size))
1286 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1287 elif len(args) == 2:
1289 if not isinstance(val, int):
1291 "Invalid second argument to mkBitVector '{}', "
1292 "expected integer value".format(size))
1293 term.cterm = self.csolver.mkBitVector(
1294 <uint32_t> size, <uint32_t> val)
1295 elif len(args) == 3:
1298 if not isinstance(val, str):
1300 "Invalid second argument to mkBitVector '{}', "
1301 "expected value string".format(size))
1302 if not isinstance(base, int):
1304 "Invalid third argument to mkBitVector '{}', "
1305 "expected base given as integer".format(size))
1306 term.cterm = self.csolver.mkBitVector(
1308 <const string&> str(val).encode(),
1311 raise ValueError("Unexpected inputs to mkBitVector")
1314 def mkConstArray(self, Sort sort, Term val):
1316 Create a constant array with the provided constant value stored at every
1319 :param sort: the sort of the constant array (must be an array sort)
1320 :param val: the constant value to store (must match the sort's element sort)
1321 :return: the constant array term
1323 cdef Term term = Term(self)
1324 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1327 def mkFloatingPointPosInf(self, int exp, int sig):
1328 """Create a positive infinity floating-point constant.
1330 :param exp: Number of bits in the exponent
1331 :param sig: Number of bits in the significand
1332 :return: the floating-point constant
1334 cdef Term term = Term(self)
1335 term.cterm = self.csolver.mkFloatingPointPosInf(exp, sig)
1338 def mkFloatingPointNegInf(self, int exp, int sig):
1339 """Create a negative infinity floating-point constant.
1341 :param exp: Number of bits in the exponent
1342 :param sig: Number of bits in the significand
1343 :return: the floating-point constant
1345 cdef Term term = Term(self)
1346 term.cterm = self.csolver.mkFloatingPointNegInf(exp, sig)
1349 def mkFloatingPointNaN(self, int exp, int sig):
1350 """Create a not-a-number (NaN) floating-point constant.
1352 :param exp: Number of bits in the exponent
1353 :param sig: Number of bits in the significand
1354 :return: the floating-point constant
1356 cdef Term term = Term(self)
1357 term.cterm = self.csolver.mkFloatingPointNaN(exp, sig)
1360 def mkFloatingPointPosZero(self, int exp, int sig):
1361 """Create a positive zero (+0.0) floating-point constant.
1363 :param exp: Number of bits in the exponent
1364 :param sig: Number of bits in the significand
1365 :return: the floating-point constant
1367 cdef Term term = Term(self)
1368 term.cterm = self.csolver.mkFloatingPointPosZero(exp, sig)
1371 def mkFloatingPointNegZero(self, int exp, int sig):
1372 """Create a negative zero (+0.0) floating-point constant.
1374 :param exp: Number of bits in the exponent
1375 :param sig: Number of bits in the significand
1376 :return: the floating-point constant
1378 cdef Term term = Term(self)
1379 term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig)
1382 def mkRoundingMode(self, RoundingMode rm):
1383 """Create a roundingmode constant.
1385 :param rm: the floating point rounding mode this constant represents
1387 cdef Term term = Term(self)
1388 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
1391 def mkFloatingPoint(self, int exp, int sig, Term val):
1392 """Create a floating-point constant.
1394 :param exp: Size of the exponent
1395 :param sig: Size of the significand
1396 :param val: Value of the floating-point constant as a bit-vector term
1398 cdef Term term = Term(self)
1399 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1402 def mkCardinalityConstraint(self, Sort sort, int index):
1403 """Create cardinality constraint.
1405 :param sort: Sort of the constraint
1406 :param index: The upper bound for the cardinality of the sort
1408 cdef Term term = Term(self)
1409 term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
1412 def mkConst(self, Sort sort, symbol=None):
1414 Create (first-order) constant (0-arity function symbol).
1418 .. code-block:: smtlib
1420 ( declare-const <symbol> <sort> )
1421 ( declare-fun <symbol> ( ) <sort> )
1423 :param sort: the sort of the constant
1424 :param symbol: the name of the constant. If None, a default symbol is used.
1425 :return: the first-order constant
1427 cdef Term term = Term(self)
1429 term.cterm = self.csolver.mkConst(sort.csort)
1431 term.cterm = self.csolver.mkConst(sort.csort,
1432 (<str?> symbol).encode())
1435 def mkVar(self, Sort sort, symbol=None):
1437 Create a bound variable to be used in a binder (i.e. a quantifier, a
1438 lambda, or a witness binder).
1440 :param sort: the sort of the variable
1441 :param symbol: the name of the variable
1442 :return: the variable
1444 cdef Term term = Term(self)
1446 term.cterm = self.csolver.mkVar(sort.csort)
1448 term.cterm = self.csolver.mkVar(sort.csort,
1449 (<str?> symbol).encode())
1452 def mkDatatypeConstructorDecl(self, str name):
1454 :return: a datatype constructor declaration
1455 :param name: the constructor's name
1457 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1458 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1461 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1462 """Create a datatype declaration.
1464 :param name: the name of the datatype
1465 :param isCoDatatype: true if a codatatype is to be constructed
1466 :return: the DatatypeDecl
1468 cdef DatatypeDecl dd = DatatypeDecl(self)
1469 cdef vector[c_Sort] v
1472 if sorts_or_bool is None and isCoDatatype is None:
1473 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1474 elif sorts_or_bool is not None and isCoDatatype is None:
1475 if isinstance(sorts_or_bool, bool):
1476 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1477 <bint> sorts_or_bool)
1478 elif isinstance(sorts_or_bool, Sort):
1479 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1480 (<Sort> sorts_or_bool).csort)
1481 elif isinstance(sorts_or_bool, list):
1482 for s in sorts_or_bool:
1483 v.push_back((<Sort?> s).csort)
1484 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1485 <const vector[c_Sort]&> v)
1487 raise ValueError("Unhandled second argument type {}"
1488 .format(type(sorts_or_bool)))
1489 elif sorts_or_bool is not None and isCoDatatype is not None:
1490 if isinstance(sorts_or_bool, Sort):
1491 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1492 (<Sort> sorts_or_bool).csort,
1493 <bint> isCoDatatype)
1494 elif isinstance(sorts_or_bool, list):
1495 for s in sorts_or_bool:
1496 v.push_back((<Sort?> s).csort)
1497 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1498 <const vector[c_Sort]&> v,
1499 <bint> isCoDatatype)
1501 raise ValueError("Unhandled second argument type {}"
1502 .format(type(sorts_or_bool)))
1504 raise ValueError("Can't create DatatypeDecl with {}".format([type(a)
1511 def simplify(self, Term t):
1513 Simplify a formula without doing "much" work. Does not involve the
1514 SAT Engine in the simplification, but uses the current definitions,
1515 assertions, and the current partial model, if one has been constructed.
1516 It also involves theory normalization.
1518 :param t: the formula to simplify
1519 :return: the simplified formula
1521 cdef Term term = Term(self)
1522 term.cterm = self.csolver.simplify(t.cterm)
1525 def assertFormula(self, Term term):
1526 """ Assert a formula
1530 .. code-block:: smtlib
1534 :param term: the formula to assert
1536 self.csolver.assertFormula(term.cterm)
1540 Check satisfiability.
1544 .. code-block:: smtlib
1548 :return: the result of the satisfiability check.
1550 cdef Result r = Result()
1551 r.cr = self.csolver.checkSat()
1554 def mkSygusGrammar(self, boundVars, ntSymbols):
1556 Create a SyGuS grammar. The first non-terminal is treated as the
1557 starting non-terminal, so the order of non-terminals matters.
1559 :param boundVars: the parameters to corresponding synth-fun/synth-inv
1560 :param ntSymbols: the pre-declaration of the non-terminal symbols
1561 :return: the grammar
1563 cdef Grammar grammar = Grammar(self)
1564 cdef vector[c_Term] bvc
1565 cdef vector[c_Term] ntc
1566 for bv in boundVars:
1567 bvc.push_back((<Term?> bv).cterm)
1568 for nt in ntSymbols:
1569 ntc.push_back((<Term?> nt).cterm)
1570 grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1573 def mkSygusVar(self, Sort sort, str symbol=""):
1574 """Append symbol to the current list of universal variables.
1578 .. code-block:: smtlib
1580 ( declare-var <symbol> <sort> )
1582 :param sort: the sort of the universal variable
1583 :param symbol: the name of the universal variable
1584 :return: the universal variable
1586 cdef Term term = Term(self)
1587 term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode())
1590 def addSygusConstraint(self, Term t):
1592 Add a formula to the set of SyGuS constraints.
1596 .. code-block:: smtlib
1598 ( constraint <term> )
1600 :param term: the formula to add as a constraint
1602 self.csolver.addSygusConstraint(t.cterm)
1604 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1606 Add a set of SyGuS constraints to the current state that correspond to an
1607 invariant synthesis problem.
1611 .. code-block:: smtlib
1613 ( inv-constraint <inv> <pre> <trans> <post> )
1615 :param inv: the function-to-synthesize
1616 :param pre: the pre-condition
1617 :param trans: the transition relation
1618 :param post: the post-condition
1620 self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1622 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1624 Synthesize n-ary function following specified syntactic constraints.
1628 .. code-block:: smtlib
1630 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1632 :param symbol: the name of the function
1633 :param boundVars: the parameters to this function
1634 :param sort: the sort of the return value of this function
1635 :param grammar: the syntactic constraints
1636 :return: the function
1638 cdef Term term = Term(self)
1639 cdef vector[c_Term] v
1640 for bv in bound_vars:
1641 v.push_back((<Term?> bv).cterm)
1643 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1645 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1648 def checkSynth(self):
1650 Try to find a solution for the synthesis conjecture corresponding to the
1651 current list of functions-to-synthesize, universal variables and
1656 .. code-block:: smtlib
1660 :return: the result of the synthesis conjecture.
1662 cdef Result r = Result()
1663 r.cr = self.csolver.checkSynth()
1666 def checkSynthNext(self):
1668 Try to find a next solution for the synthesis conjecture corresponding
1669 to the current list of functions-to-synthesize, universal variables and
1670 constraints. Must be called immediately after a successful call to
1671 check-synth or check-synth-next. Requires incremental mode.
1675 .. code-block:: smtlib
1679 :return: the result of the check, which is unsat if the check succeeded,
1680 in which case solutions are available via getSynthSolutions.
1682 cdef Result r = Result()
1683 r.cr = self.csolver.checkSynthNext()
1686 def getSynthSolution(self, Term term):
1688 Get the synthesis solution of the given term. This method should be
1689 called immediately after the solver answers unsat for sygus input.
1691 :param term: the term for which the synthesis solution is queried
1692 :return: the synthesis solution of the given term
1694 cdef Term t = Term(self)
1695 t.cterm = self.csolver.getSynthSolution(term.cterm)
1698 def getSynthSolutions(self, list terms):
1700 Get the synthesis solutions of the given terms. This method should be
1701 called immediately after the solver answers unsat for sygus input.
1703 :param terms: the terms for which the synthesis solutions is queried
1704 :return: the synthesis solutions of the given terms
1707 cdef vector[c_Term] vec
1709 vec.push_back((<Term?> t).cterm)
1710 cresult = self.csolver.getSynthSolutions(vec)
1718 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1720 Synthesize invariant.
1724 .. code-block:: smtlib
1726 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1728 :param symbol: the name of the invariant
1729 :param boundVars: the parameters to this invariant
1730 :param grammar: the syntactic constraints
1731 :return: the invariant
1733 cdef Term term = Term(self)
1734 cdef vector[c_Term] v
1735 for bv in bound_vars:
1736 v.push_back((<Term?> bv).cterm)
1738 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
1740 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
1743 @expand_list_arg(num_req_args=0)
1744 def checkSatAssuming(self, *assumptions):
1745 """ Check satisfiability assuming the given formula.
1749 .. code-block:: smtlib
1751 ( check-sat-assuming ( <prop_literal> ) )
1753 :param assumptions: the formulas to assume, as a list or as distinct arguments
1754 :return: the result of the satisfiability check.
1756 cdef Result r = Result()
1757 # used if assumptions is a list of terms
1758 cdef vector[c_Term] v
1759 for a in assumptions:
1760 v.push_back((<Term?> a).cterm)
1761 r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
1764 @expand_list_arg(num_req_args=0)
1765 def checkEntailed(self, *assumptions):
1766 """Check entailment of the given formula w.r.t. the current set of assertions.
1768 :param terms: the formulas to check entailment for, as a list or as distinct arguments
1769 :return: the result of the entailment check.
1771 cdef Result r = Result()
1772 # used if assumptions is a list of terms
1773 cdef vector[c_Term] v
1774 for a in assumptions:
1775 v.push_back((<Term?> a).cterm)
1776 r.cr = self.csolver.checkEntailed(<const vector[c_Term]&> v)
1779 @expand_list_arg(num_req_args=1)
1780 def declareDatatype(self, str symbol, *ctors):
1782 Create datatype sort.
1786 .. code-block:: smtlib
1788 ( declare-datatype <symbol> <datatype_decl> )
1790 :param symbol: the name of the datatype sort
1791 :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
1792 :return: the datatype sort
1794 cdef Sort sort = Sort(self)
1795 cdef vector[c_DatatypeConstructorDecl] v
1798 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1799 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1802 def declareFun(self, str symbol, list sorts, Sort sort):
1803 """Declare n-ary function symbol.
1807 .. code-block:: smtlib
1809 ( declare-fun <symbol> ( <sort>* ) <sort> )
1811 :param symbol: the name of the function
1812 :param sorts: the sorts of the parameters to this function
1813 :param sort: the sort of the return value of this function
1814 :return: the function
1816 cdef Term term = Term(self)
1817 cdef vector[c_Sort] v
1819 v.push_back((<Sort?> s).csort)
1820 term.cterm = self.csolver.declareFun(symbol.encode(),
1821 <const vector[c_Sort]&> v,
1825 def declareSort(self, str symbol, int arity):
1826 """Declare uninterpreted sort.
1830 .. code-block:: smtlib
1832 ( declare-sort <symbol> <numeral> )
1834 :param symbol: the name of the sort
1835 :param arity: the arity of the sort
1838 cdef Sort sort = Sort(self)
1839 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
1842 def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
1843 """Define n-ary function.
1847 .. code-block:: smtlib
1849 ( define-fun <function_def> )
1851 :param symbol: the name of the function
1852 :param bound_vars: the parameters to this function
1853 :param sort: the sort of the return value of this function
1854 :param term: the function body
1855 :param glbl: determines whether this definition is global (i.e. persists when popping the context)
1856 :return: the function
1858 cdef Term fun = Term(self)
1859 cdef vector[c_Term] v
1860 for bv in bound_vars:
1861 v.push_back((<Term?> bv).cterm)
1863 fun.cterm = self.csolver.defineFun(symbol.encode(),
1864 <const vector[c_Term] &> v,
1870 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1871 """Define recursive functions.
1875 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1876 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1881 .. code-block:: smtlib
1883 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1885 Create elements of parameter ``funs`` with mkConst().
1887 :param funs: the sorted functions
1888 :param bound_vars: the list of parameters to the functions
1889 :param terms: the list of function bodies of the functions
1890 :param global: determines whether this definition is global (i.e. persists when popping the context)
1891 :return: the function
1893 cdef Term term = Term(self)
1894 cdef vector[c_Term] v
1895 for bv in bound_vars:
1896 v.push_back((<Term?> bv).cterm)
1899 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
1900 <const vector[c_Term] &> v,
1901 (<Sort?> sort_or_term).csort,
1905 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
1906 <const vector[c_Term]&> v,
1907 (<Term?> sort_or_term).cterm,
1912 def defineFunsRec(self, funs, bound_vars, terms):
1913 """Define recursive functions.
1917 .. code-block:: smtlib
1919 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1921 Create elements of parameter ``funs`` with mkConst().
1923 :param funs: the sorted functions
1924 :param bound_vars: the list of parameters to the functions
1925 :param terms: the list of function bodies of the functions
1926 :param global: determines whether this definition is global (i.e. persists when popping the context)
1927 :return: the function
1929 cdef vector[c_Term] vf
1930 cdef vector[vector[c_Term]] vbv
1931 cdef vector[c_Term] vt
1934 vf.push_back((<Term?> f).cterm)
1936 cdef vector[c_Term] temp
1937 for v in bound_vars:
1939 temp.push_back((<Term?> t).cterm)
1944 vf.push_back((<Term?> t).cterm)
1947 """Get the refutation proof
1951 .. code-block:: smtlib
1955 Requires to enable option
1956 :ref:`produce-proofs <lbl-option-produce-proofs>`.
1958 :return: a string representing the proof, according to the value of
1961 return self.csolver.getProof()
1963 def getLearnedLiterals(self):
1964 """Get a list of literals that are entailed by the current set of assertions
1968 .. code-block:: smtlib
1970 ( get-learned-literals )
1972 :return: the list of literals
1975 for a in self.csolver.getLearnedLiterals():
1981 def getAssertions(self):
1982 """Get the list of asserted formulas.
1986 .. code-block:: smtlib
1990 :return: the list of asserted formulas
1993 for a in self.csolver.getAssertions():
1996 assertions.append(term)
1999 def getInfo(self, str flag):
2000 """Get info from the solver.
2004 .. code-block:: smtlib
2006 ( get-info <info_flag> )
2008 :param flag: the info flag
2011 return self.csolver.getInfo(flag.encode())
2013 def getOption(self, str option):
2014 """Get the value of a given option.
2018 .. code-block:: smtlib
2020 ( get-option <keyword> )
2022 :param option: the option for which the value is queried
2023 :return: a string representation of the option value
2025 return self.csolver.getOption(option.encode())
2027 def getUnsatAssumptions(self):
2029 Get the set of unsat ("failed") assumptions.
2033 .. code-block:: smtlib
2035 ( get-unsat-assumptions )
2037 Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
2039 :return: the set of unsat assumptions.
2042 for a in self.csolver.getUnsatAssumptions():
2045 assumptions.append(term)
2048 def getUnsatCore(self):
2049 """Get the unsatisfiable core.
2053 .. code-block:: smtlib
2057 Requires to enable option :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
2060 In contrast to SMT-LIB, the API does not distinguish between named and
2061 unnamed assertions when producing an unsatisfiable core. Additionally,
2062 the API allows this option to be called after a check with assumptions.
2063 A subset of those assumptions may be included in the unsatisfiable core
2064 returned by this method.
2066 :return: a set of terms representing the unsatisfiable core
2069 for a in self.csolver.getUnsatCore():
2075 def getValue(self, Term t):
2076 """Get the value of the given term in the current model.
2080 .. code-block:: smtlib
2082 ( get-value ( <term> ) )
2084 :param term: the term for which the value is queried
2085 :return: the value of the given term
2087 cdef Term term = Term(self)
2088 term.cterm = self.csolver.getValue(t.cterm)
2091 def getModelDomainElements(self, Sort s):
2093 Get the domain elements of uninterpreted sort s in the current model. The
2094 current model interprets s as the finite sort whose domain elements are
2095 given in the return value of this method.
2097 :param s: The uninterpreted sort in question
2098 :return: the domain elements of s in the current model
2101 cresult = self.csolver.getModelDomainElements(s.csort)
2108 def isModelCoreSymbol(self, Term v):
2110 This returns false if the model value of free constant v was not
2111 essential for showing the satisfiability of the last call to checkSat
2112 using the current model. This method will only return false (for any v)
2113 if the model-cores option has been set.
2115 :param v: The term in question
2116 :return: true if v is a model core symbol
2118 return self.csolver.isModelCoreSymbol(v.cterm)
2120 def getValueSepHeap(self):
2121 """When using separation logic, obtain the term for the heap.
2123 :return: The term for the heap
2125 cdef Term term = Term(self)
2126 term.cterm = self.csolver.getValueSepHeap()
2129 def getValueSepNil(self):
2130 """When using separation logic, obtain the term for nil.
2132 :return: The term for nil
2134 cdef Term term = Term(self)
2135 term.cterm = self.csolver.getValueSepNil()
2138 def declareSepHeap(self, Sort locType, Sort dataType):
2140 When using separation logic, this sets the location sort and the
2141 datatype sort to the given ones. This method should be invoked exactly
2142 once, before any separation logic constraints are provided.
2144 :param locSort: The location sort of the heap
2145 :param dataSort: The data sort of the heap
2147 self.csolver.declareSepHeap(locType.csort, dataType.csort)
2149 def declarePool(self, str symbol, Sort sort, initValue):
2150 """Declare a symbolic pool of terms with the given initial value.
2154 .. code-block:: smtlib
2156 ( declare-pool <symbol> <sort> ( <term>* ) )
2158 :param symbol: The name of the pool
2159 :param sort: The sort of the elements of the pool.
2160 :param initValue: The initial value of the pool
2162 cdef Term term = Term(self)
2163 cdef vector[c_Term] niv
2165 niv.push_back((<Term?> v).cterm)
2166 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
2169 def pop(self, nscopes=1):
2170 """Pop ``nscopes`` level(s) from the assertion stack.
2174 .. code-block:: smtlib
2178 :param nscopes: the number of levels to pop
2180 self.csolver.pop(nscopes)
2182 def push(self, nscopes=1):
2183 """ Push ``nscopes`` level(s) to the assertion stack.
2187 .. code-block:: smtlib
2191 :param nscopes: the number of levels to push
2193 self.csolver.push(nscopes)
2195 def resetAssertions(self):
2197 Remove all assertions.
2201 .. code-block:: smtlib
2203 ( reset-assertions )
2206 self.csolver.resetAssertions()
2208 def setInfo(self, str keyword, str value):
2213 .. code-block:: smtlib
2215 ( set-info <attribute> )
2217 :param keyword: the info flag
2218 :param value: the value of the info flag
2220 self.csolver.setInfo(keyword.encode(), value.encode())
2222 def setLogic(self, str logic):
2227 .. code-block:: smtlib
2229 ( set-logic <symbol> )
2231 :param logic: the logic to set
2233 self.csolver.setLogic(logic.encode())
2235 def setOption(self, str option, str value):
2240 .. code-block:: smtlib
2242 ( set-option <option> )
2244 :param option: the option name
2245 :param value: the option value
2247 self.csolver.setOption(option.encode(), value.encode())
2249 def getInterpolant(self, Term conj, *args):
2250 """Get an interpolant.
2254 .. code-block:: smtlib
2256 ( get-interpol <conj> )
2257 ( get-interpol <conj> <grammar> )
2259 Requires option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
2261 Supports the following variants:
2263 - ``bool getInteprolant(Term conj, Term output)``
2264 - ``bool getInteprolant(Term conj, Grammar grammar, Term output)``
2266 :param conj: the conjecture term
2267 :param output: the term where the result will be stored
2268 :param grammar: a grammar for the inteprolant
2269 :return: True iff an interpolant was found
2273 assert isinstance(args[0], Term)
2274 result = self.csolver.getInterpolant(conj.cterm, (<Term ?> args[0]).cterm)
2276 assert len(args) == 2
2277 assert isinstance(args[0], Grammar)
2278 assert isinstance(args[1], Term)
2279 result = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
2283 def getInterpolantNext(self, Term output):
2285 Get the next interpolant. Can only be called immediately after
2286 a succesful call to get-interpol or get-interpol-next.
2287 Is guaranteed to produce a syntactically different interpolant wrt the
2288 last returned interpolant if successful.
2292 .. code-block:: smtlib
2294 ( get-interpol-next )
2296 Requires to enable incremental mode, and
2297 option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
2299 :param output: the term where the result will be stored
2300 :return: True iff an interpolant was found
2302 result = self.csolver.getInterpolantNext(output.cterm)
2305 def getAbduct(self, Term conj, *args):
2310 .. code-block:: smtlib
2312 ( get-abduct <conj> )
2313 ( get-abduct <conj> <grammar> )
2315 Requires to enable option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2317 Supports the following variants:
2319 - ``bool getAbduct(Term conj, Term output)``
2320 - ``bool getAbduct(Term conj, Grammar grammar, Term output)``
2322 :param conj: the conjecture term
2323 :param output: the term where the result will be stored
2324 :param grammar: a grammar for the abduct
2325 :return: True iff an abduct was found
2329 assert isinstance(args[0], Term)
2330 result = self.csolver.getAbduct(conj.cterm, (<Term ?> args[0]).cterm)
2332 assert len(args) == 2
2333 assert isinstance(args[0], Grammar)
2334 assert isinstance(args[1], Term)
2335 result = self.csolver.getAbduct(conj.cterm, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
2338 def getAbductNext(self, Term output):
2340 Get the next abduct. Can only be called immediately after
2341 a succesful call to get-abduct or get-abduct-next.
2342 Is guaranteed to produce a syntactically different abduct wrt the
2343 last returned abduct if successful.
2347 .. code-block:: smtlib
2351 Requires to enable incremental mode, and
2352 option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2353 :param output: the term where the result will be stored
2354 :return: True iff an abduct was found
2356 result = self.csolver.getAbductNext(output.cterm)
2359 def blockModel(self):
2361 Block the current model. Can be called only if immediately preceded by a
2362 SAT or INVALID query.
2366 .. code-block:: smtlib
2370 Requires enabling option
2371 :ref:`produce-models <lbl-option-produce-models>`
2373 :ref:`block-models <lbl-option-block-models>`
2374 to a mode other than ``none``.
2376 self.csolver.blockModel()
2378 def blockModelValues(self, terms):
2380 Block the current model values of (at least) the values in terms. Can be
2381 called only if immediately preceded by a SAT or NOT_ENTAILED query.
2385 .. code-block:: smtlib
2387 (block-model-values ( <terms>+ ))
2389 Requires enabling option
2390 :ref:`produce-models <lbl-option-produce-models>`.
2392 cdef vector[c_Term] nts
2394 nts.push_back((<Term?> t).cterm)
2395 self.csolver.blockModelValues(nts)
2400 The sort of a cvc5 term.
2404 def __cinit__(self, Solver solver):
2405 # csort always set by Solver
2406 self.solver = solver
2408 def __eq__(self, Sort other):
2409 return self.csort == other.csort
2411 def __ne__(self, Sort other):
2412 return self.csort != other.csort
2414 def __lt__(self, Sort other):
2415 return self.csort < other.csort
2417 def __gt__(self, Sort other):
2418 return self.csort > other.csort
2420 def __le__(self, Sort other):
2421 return self.csort <= other.csort
2423 def __ge__(self, Sort other):
2424 return self.csort >= other.csort
2427 return self.csort.toString().decode()
2430 return self.csort.toString().decode()
2433 return csorthash(self.csort)
2435 def hasSymbol(self):
2436 """:return: True iff this sort has a symbol."""
2437 return self.csort.hasSymbol()
2439 def getSymbol(self):
2441 Asserts :py:meth:`hasSymbol()`.
2443 :return: the raw symbol of the sort.
2445 return self.csort.getSymbol().decode()
2448 """:return: True if this Sort is a null sort."""
2449 return self.csort.isNull()
2451 def isBoolean(self):
2453 Is this a Boolean sort?
2455 :return: True if the sort is the Boolean sort.
2457 return self.csort.isBoolean()
2459 def isInteger(self):
2461 Is this an integer sort?
2463 :return: True if the sort is the integer sort.
2465 return self.csort.isInteger()
2469 Is this a real sort?
2471 :return: True if the sort is the real sort.
2473 return self.csort.isReal()
2477 Is this a string sort?
2479 :return: True if the sort is the string sort.
2481 return self.csort.isString()
2485 Is this a regexp sort?
2487 :return: True if the sort is the regexp sort.
2489 return self.csort.isRegExp()
2491 def isRoundingMode(self):
2493 Is this a rounding mode sort?
2495 :return: True if the sort is the rounding mode sort.
2497 return self.csort.isRoundingMode()
2499 def isBitVector(self):
2501 Is this a bit-vector sort?
2503 :return: True if the sort is a bit-vector sort.
2505 return self.csort.isBitVector()
2507 def isFloatingPoint(self):
2509 Is this a floating-point sort?
2511 :return: True if the sort is a bit-vector sort.
2513 return self.csort.isFloatingPoint()
2515 def isDatatype(self):
2517 Is this a datatype sort?
2519 :return: True if the sort is a datatype sort.
2521 return self.csort.isDatatype()
2523 def isParametricDatatype(self):
2525 Is this a parametric datatype sort?
2527 :return: True if the sort is a parametric datatype sort.
2529 return self.csort.isParametricDatatype()
2531 def isConstructor(self):
2533 Is this a constructor sort?
2535 :return: True if the sort is a constructor sort.
2537 return self.csort.isConstructor()
2539 def isSelector(self):
2541 Is this a selector sort?
2543 :return: True if the sort is a selector sort.
2545 return self.csort.isSelector()
2549 Is this a tester sort?
2551 :return: True if the sort is a selector sort.
2553 return self.csort.isTester()
2555 def isUpdater(self):
2557 Is this a datatype updater sort?
2559 :return: True if the sort is a datatype updater sort.
2561 return self.csort.isUpdater()
2563 def isFunction(self):
2565 Is this a function sort?
2567 :return: True if the sort is a function sort.
2569 return self.csort.isFunction()
2571 def isPredicate(self):
2573 Is this a predicate sort?
2574 That is, is this a function sort mapping to Boolean? All predicate
2575 sorts are also function sorts.
2577 :return: True if the sort is a predicate sort.
2579 return self.csort.isPredicate()
2583 Is this a tuple sort?
2585 :return: True if the sort is a tuple sort.
2587 return self.csort.isTuple()
2591 Is this a record sort?
2593 :return: True if the sort is a record sort.
2595 return self.csort.isRecord()
2599 Is this an array sort?
2601 :return: True if the sort is an array sort.
2603 return self.csort.isArray()
2609 :return: True if the sort is a set sort.
2611 return self.csort.isSet()
2617 :return: True if the sort is a bag sort.
2619 return self.csort.isBag()
2621 def isSequence(self):
2623 Is this a sequence sort?
2625 :return: True if the sort is a sequence sort.
2627 return self.csort.isSequence()
2629 def isUninterpretedSort(self):
2631 Is this a sort uninterpreted?
2633 :return: True if the sort is uninterpreted.
2635 return self.csort.isUninterpretedSort()
2637 def isSortConstructor(self):
2639 Is this a sort constructor kind?
2641 :return: True if this a sort constructor kind.
2643 return self.csort.isSortConstructor()
2645 def isFirstClass(self):
2647 Is this a first-class sort?
2648 First-class sorts are sorts for which:
2650 1. we handle equalities between terms of that type, and
2651 2. they are allowed to be parameters of parametric sorts
2652 (e.g. index or element sorts of arrays).
2654 Examples of sorts that are not first-class include sort constructor
2655 sorts and regular expression sorts.
2657 :return: True if the sort is a first-class sort.
2659 return self.csort.isFirstClass()
2661 def isFunctionLike(self):
2663 Is this a function-LIKE sort?
2665 Anything function-like except arrays (e.g., datatype selectors) is
2666 considered a function here. Function-like terms can not be the argument
2667 or return value for any term that is function-like.
2668 This is mainly to avoid higher order.
2670 .. note:: Arrays are explicitly not considered function-like here.
2672 :return: True if this is a function-like sort
2674 return self.csort.isFunctionLike()
2676 def isSubsortOf(self, Sort sort):
2678 Is this sort a subsort of the given sort?
2680 :return: True if this sort is a subsort of s
2682 return self.csort.isSubsortOf(sort.csort)
2684 def getDatatype(self):
2686 :return: the underlying datatype of a datatype sort
2688 cdef Datatype d = Datatype(self.solver)
2689 d.cd = self.csort.getDatatype()
2692 def instantiate(self, params):
2694 Instantiate a parameterized datatype/sort sort.
2695 Create sorts parameter with :py:meth:`Solver.mkParamSort()`
2697 :param params: the list of sort parameters to instantiate with
2699 cdef Sort sort = Sort(self.solver)
2700 cdef vector[c_Sort] v
2702 v.push_back((<Sort?> s).csort)
2703 sort.csort = self.csort.instantiate(v)
2706 def substitute(self, sort_or_list_1, sort_or_list_2):
2708 Substitution of Sorts.
2710 :param sort_or_list_1: the subsort or subsorts to be substituted within this sort.
2711 :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort.
2713 Note that this replacement is applied during a pre-order traversal and
2714 only once to the sort. It is not run until fix point. In the case that
2715 sort_or_list_1 contains duplicates, the replacement earliest in the list
2719 ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])`` will
2720 return ``(Array (Array C D) B)``.
2723 # The resulting sort after substitution
2724 cdef Sort sort = Sort(self.solver)
2725 # lists for substitutions
2726 cdef vector[c_Sort] ces
2727 cdef vector[c_Sort] creplacements
2729 # normalize the input parameters to be lists
2730 if isinstance(sort_or_list_1, list):
2731 assert isinstance(sort_or_list_2, list)
2733 replacements = sort_or_list_2
2734 if len(es) != len(replacements):
2735 raise RuntimeError("Expecting list inputs to substitute to "
2736 "have the same length but got: "
2737 "{} and {}".format(len(es), len(replacements)))
2739 for e, r in zip(es, replacements):
2740 ces.push_back((<Sort?> e).csort)
2741 creplacements.push_back((<Sort?> r).csort)
2744 # add the single elements to the vectors
2745 ces.push_back((<Sort?> sort_or_list_1).csort)
2746 creplacements.push_back((<Sort?> sort_or_list_2).csort)
2748 # call the API substitute method with lists
2749 sort.csort = self.csort.substitute(ces, creplacements)
2753 def getConstructorArity(self):
2755 :return: the arity of a constructor sort.
2757 return self.csort.getConstructorArity()
2759 def getConstructorDomainSorts(self):
2761 :return: the domain sorts of a constructor sort
2764 for s in self.csort.getConstructorDomainSorts():
2765 sort = Sort(self.solver)
2767 domain_sorts.append(sort)
2770 def getConstructorCodomainSort(self):
2772 :return: the codomain sort of a constructor sort
2774 cdef Sort sort = Sort(self.solver)
2775 sort.csort = self.csort.getConstructorCodomainSort()
2778 def getSelectorDomainSort(self):
2780 :return: the domain sort of a selector sort
2782 cdef Sort sort = Sort(self.solver)
2783 sort.csort = self.csort.getSelectorDomainSort()
2786 def getSelectorCodomainSort(self):
2788 :return: the codomain sort of a selector sort
2790 cdef Sort sort = Sort(self.solver)
2791 sort.csort = self.csort.getSelectorCodomainSort()
2794 def getTesterDomainSort(self):
2796 :return: the domain sort of a tester sort
2798 cdef Sort sort = Sort(self.solver)
2799 sort.csort = self.csort.getTesterDomainSort()
2802 def getTesterCodomainSort(self):
2804 :return: the codomain sort of a tester sort, which is the Boolean sort
2806 cdef Sort sort = Sort(self.solver)
2807 sort.csort = self.csort.getTesterCodomainSort()
2810 def getFunctionArity(self):
2812 :return: the arity of a function sort
2814 return self.csort.getFunctionArity()
2816 def getFunctionDomainSorts(self):
2818 :return: the domain sorts of a function sort
2821 for s in self.csort.getFunctionDomainSorts():
2822 sort = Sort(self.solver)
2824 domain_sorts.append(sort)
2827 def getFunctionCodomainSort(self):
2829 :return: the codomain sort of a function sort
2831 cdef Sort sort = Sort(self.solver)
2832 sort.csort = self.csort.getFunctionCodomainSort()
2835 def getArrayIndexSort(self):
2837 :return: the array index sort of an array sort
2839 cdef Sort sort = Sort(self.solver)
2840 sort.csort = self.csort.getArrayIndexSort()
2843 def getArrayElementSort(self):
2845 :return: the array element sort of an array sort
2847 cdef Sort sort = Sort(self.solver)
2848 sort.csort = self.csort.getArrayElementSort()
2851 def getSetElementSort(self):
2853 :return: the element sort of a set sort
2855 cdef Sort sort = Sort(self.solver)
2856 sort.csort = self.csort.getSetElementSort()
2859 def getBagElementSort(self):
2861 :return: the element sort of a bag sort
2863 cdef Sort sort = Sort(self.solver)
2864 sort.csort = self.csort.getBagElementSort()
2867 def getSequenceElementSort(self):
2869 :return: the element sort of a sequence sort
2871 cdef Sort sort = Sort(self.solver)
2872 sort.csort = self.csort.getSequenceElementSort()
2875 def getUninterpretedSortName(self):
2877 :return: the name of an uninterpreted sort
2879 return self.csort.getUninterpretedSortName().decode()
2881 def isUninterpretedSortParameterized(self):
2883 :return: True if an uninterpreted sort is parameterized
2885 return self.csort.isUninterpretedSortParameterized()
2887 def getUninterpretedSortParamSorts(self):
2889 :return: the parameter sorts of an uninterpreted sort
2892 for s in self.csort.getUninterpretedSortParamSorts():
2893 sort = Sort(self.solver)
2895 param_sorts.append(sort)
2898 def getSortConstructorName(self):
2900 :return: the name of a sort constructor sort
2902 return self.csort.getSortConstructorName().decode()
2904 def getSortConstructorArity(self):
2906 :return: the arity of a sort constructor sort
2908 return self.csort.getSortConstructorArity()
2910 def getBitVectorSize(self):
2912 :return: the bit-width of the bit-vector sort
2914 return self.csort.getBitVectorSize()
2916 def getFloatingPointExponentSize(self):
2918 :return: the bit-width of the exponent of the floating-point sort
2920 return self.csort.getFloatingPointExponentSize()
2922 def getFloatingPointSignificandSize(self):
2924 :return: the width of the significand of the floating-point sort
2926 return self.csort.getFloatingPointSignificandSize()
2928 def getDatatypeParamSorts(self):
2930 Return the parameters of a parametric datatype sort. If this sort
2931 is a non-instantiated parametric datatype, this returns the
2932 parameter sorts of the underlying datatype. If this sort is an
2933 instantiated parametric datatype, then this returns the sort
2934 parameters that were used to construct the sort via
2935 :py:meth:`instantiate()`.
2937 :return: the parameter sorts of a parametric datatype sort
2940 for s in self.csort.getDatatypeParamSorts():
2941 sort = Sort(self.solver)
2943 param_sorts.append(sort)
2946 def getDatatypeArity(self):
2948 :return: the arity of a datatype sort
2950 return self.csort.getDatatypeArity()
2952 def getTupleLength(self):
2954 :return: the length of a tuple sort
2956 return self.csort.getTupleLength()
2958 def getTupleSorts(self):
2960 :return: the element sorts of a tuple sort
2963 for s in self.csort.getTupleSorts():
2964 sort = Sort(self.solver)
2966 tuple_sorts.append(sort)
2973 Wrapper class for :cpp:class:`cvc5::api::Term`.
2977 def __cinit__(self, Solver solver):
2978 # cterm always set in the Solver object
2979 self.solver = solver
2981 def __eq__(self, Term other):
2982 return self.cterm == other.cterm
2984 def __ne__(self, Term other):
2985 return self.cterm != other.cterm
2987 def __lt__(self, Term other):
2988 return self.cterm < other.cterm
2990 def __gt__(self, Term other):
2991 return self.cterm > other.cterm
2993 def __le__(self, Term other):
2994 return self.cterm <= other.cterm
2996 def __ge__(self, Term other):
2997 return self.cterm >= other.cterm
2999 def __getitem__(self, int index):
3000 cdef Term term = Term(self.solver)
3002 term.cterm = self.cterm[index]
3004 raise ValueError("Expecting a non-negative integer or string")
3008 return self.cterm.toString().decode()
3011 return self.cterm.toString().decode()
3014 for ci in self.cterm:
3015 term = Term(self.solver)
3020 return ctermhash(self.cterm)
3022 def getNumChildren(self):
3023 """:return: the number of children of this term."""
3024 return self.cterm.getNumChildren()
3027 """:return: the id of this term."""
3028 return self.cterm.getId()
3031 """:return: the :py:class:`cvc5.Kind` of this term."""
3032 return Kind(<int> self.cterm.getKind())
3035 """:return: the :py:class:`cvc5.Sort` of this term."""
3036 cdef Sort sort = Sort(self.solver)
3037 sort.csort = self.cterm.getSort()
3040 def substitute(self, term_or_list_1, term_or_list_2):
3042 :return: the result of simultaneously replacing the term(s) stored in ``term_or_list_1`` by the term(s) stored in ``term_or_list_2`` in this term.
3044 Note that this replacement is applied during a pre-order traversal and
3045 only once to the term. It is not run until fix point. In the case that
3046 terms contains duplicates, the replacement earliest in the list takes
3047 priority. For example, calling substitute on ``f(x,y)`` with
3051 term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ]
3053 results in the term ``f(g(z),y)``.
3055 # The resulting term after substitution
3056 cdef Term term = Term(self.solver)
3057 # lists for substitutions
3058 cdef vector[c_Term] ces
3059 cdef vector[c_Term] creplacements
3061 # normalize the input parameters to be lists
3062 if isinstance(term_or_list_1, list):
3063 assert isinstance(term_or_list_2, list)
3065 replacements = term_or_list_2
3066 if len(es) != len(replacements):
3067 raise RuntimeError("Expecting list inputs to substitute to "
3068 "have the same length but got: "
3069 "{} and {}".format(len(es), len(replacements)))
3071 for e, r in zip(es, replacements):
3072 ces.push_back((<Term?> e).cterm)
3073 creplacements.push_back((<Term?> r).cterm)
3076 # add the single elements to the vectors
3077 ces.push_back((<Term?> term_or_list_1).cterm)
3078 creplacements.push_back((<Term?> term_or_list_2).cterm)
3080 # call the API substitute method with lists
3081 term.cterm = self.cterm.substitute(ces, creplacements)
3085 """:return: True iff this term has an operator."""
3086 return self.cterm.hasOp()
3090 .. note:: This is safe to call when :py:meth:`hasOp()` returns True.
3092 :return: the :py:class:`cvc5.Op` used to create this Term.
3094 cdef Op op = Op(self.solver)
3095 op.cop = self.cterm.getOp()
3098 def hasSymbol(self):
3099 """:return: True iff this term has a symbol."""
3100 return self.cterm.hasSymbol()
3102 def getSymbol(self):
3104 Asserts :py:meth:`hasSymbol()`.
3106 :return: the raw symbol of the term.
3108 return self.cterm.getSymbol().decode()
3111 """:return: True iff this term is a null term."""
3112 return self.cterm.isNull()
3118 :return: the Boolean negation of this term.
3120 cdef Term term = Term(self.solver)
3121 term.cterm = self.cterm.notTerm()
3124 def andTerm(self, Term t):
3128 :param t: a Boolean term
3129 :return: the conjunction of this term and the given term
3131 cdef Term term = Term(self.solver)
3132 term.cterm = self.cterm.andTerm((<Term> t).cterm)
3135 def orTerm(self, Term t):
3139 :param t: a Boolean term
3140 :return: the disjunction of this term and the given term
3142 cdef Term term = Term(self.solver)
3143 term.cterm = self.cterm.orTerm(t.cterm)
3146 def xorTerm(self, Term t):
3148 Boolean exclusive or.
3150 :param t: a Boolean term
3151 :return: the exclusive disjunction of this term and the given term
3153 cdef Term term = Term(self.solver)
3154 term.cterm = self.cterm.xorTerm(t.cterm)
3157 def eqTerm(self, Term t):
3161 :param t: a Boolean term
3162 :return: the Boolean equivalence of this term and the given term
3164 cdef Term term = Term(self.solver)
3165 term.cterm = self.cterm.eqTerm(t.cterm)
3168 def impTerm(self, Term t):
3170 Boolean Implication.
3172 :param t: a Boolean term
3173 :return: the implication of this term and the given term
3175 cdef Term term = Term(self.solver)
3176 term.cterm = self.cterm.impTerm(t.cterm)
3179 def iteTerm(self, Term then_t, Term else_t):
3181 If-then-else with this term as the Boolean condition.
3183 :param then_t: the `then` term
3184 :param else_t: the `else` term
3185 :return: the if-then-else term with this term as the Boolean condition
3187 cdef Term term = Term(self.solver)
3188 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
3191 def isConstArray(self):
3192 """:return: True iff this term is a constant array."""
3193 return self.cterm.isConstArray()
3195 def getConstArrayBase(self):
3197 Asserts :py:meth:`isConstArray()`.
3199 :return: the base (element stored at all indicies) of this constant array
3201 cdef Term term = Term(self.solver)
3202 term.cterm = self.cterm.getConstArrayBase()
3205 def isBooleanValue(self):
3206 """:return: True iff this term is a Boolean value."""
3207 return self.cterm.isBooleanValue()
3209 def getBooleanValue(self):
3211 Asserts :py:meth:`isBooleanValue()`
3213 :return: the representation of a Boolean value as a native Boolean value.
3215 return self.cterm.getBooleanValue()
3217 def isStringValue(self):
3218 """:return: True iff this term is a string value."""
3219 return self.cterm.isStringValue()
3221 def getStringValue(self):
3223 Asserts :py:meth:`isStringValue()`.
3226 This method is not to be confused with :py:meth:`__str__()` which
3227 returns the term in some string representation, whatever data it
3230 :return: the string term as a native string value.
3232 cdef Py_ssize_t size
3233 cdef c_wstring s = self.cterm.getStringValue()
3234 return PyUnicode_FromWideChar(s.data(), s.size())
3236 def getRealOrIntegerValueSign(self):
3238 Get integer or real value sign. Must be called on integer or real values,
3239 or otherwise an exception is thrown.
3241 :return: 0 if this term is zero, -1 if this term is a negative real or
3242 integer value, 1 if this term is a positive real or integer
3245 return self.cterm.getRealOrIntegerValueSign()
3247 def isIntegerValue(self):
3248 """:return: True iff this term is an integer value."""
3249 return self.cterm.isIntegerValue()
3251 def getIntegerValue(self):
3253 Asserts :py:meth:`isIntegerValue()`.
3255 :return: the integer term as a native python integer.
3257 return int(self.cterm.getIntegerValue().decode())
3259 def isFloatingPointPosZero(self):
3260 """:return: True iff the term is the floating-point value for positive zero."""
3261 return self.cterm.isFloatingPointPosZero()
3263 def isFloatingPointNegZero(self):
3264 """:return: True iff the term is the floating-point value for negative zero."""
3265 return self.cterm.isFloatingPointNegZero()
3267 def isFloatingPointPosInf(self):
3268 """:return: True iff the term is the floating-point value for positive infinity."""
3269 return self.cterm.isFloatingPointPosInf()
3271 def isFloatingPointNegInf(self):
3272 """:return: True iff the term is the floating-point value for negative infinity."""
3273 return self.cterm.isFloatingPointNegInf()
3275 def isFloatingPointNaN(self):
3276 """:return: True iff the term is the floating-point value for not a number."""
3277 return self.cterm.isFloatingPointNaN()
3279 def isFloatingPointValue(self):
3280 """:return: True iff this term is a floating-point value."""
3281 return self.cterm.isFloatingPointValue()
3283 def getFloatingPointValue(self):
3285 Asserts :py:meth:`isFloatingPointValue()`.
3287 :return: the representation of a floating-point value as a tuple of the exponent width, the significand width and a bit-vector value.
3289 cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
3290 cdef Term term = Term(self.solver)
3291 term.cterm = get2(t)
3292 return (get0(t), get1(t), term)
3294 def isSetValue(self):
3296 A term is a set value if it is considered to be a (canonical) constant
3297 set value. A canonical set value is one whose AST is:
3302 (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
3304 where ``c1 ... cn`` are values ordered by id such that
3305 ``c1 > ... > cn`` (see also :cpp:func:`cvc5::api::Term::operator>()`).
3308 A universe set term ``(kind SET_UNIVERSE)`` is not considered to be
3311 :return: True if the term is a set value.
3313 return self.cterm.isSetValue()
3315 def getSetValue(self):
3317 Asserts :py:meth:`isSetValue()`.
3319 :return: the representation of a set value as a set of terms.
3322 for e in self.cterm.getSetValue():
3323 term = Term(self.solver)
3328 def isSequenceValue(self):
3329 """:return: True iff this term is a sequence value."""
3330 return self.cterm.isSequenceValue()
3332 def getSequenceValue(self):
3334 Asserts :py:meth:`isSequenceValue()`.
3337 It is usually necessary for sequences to call
3338 :py:meth:`Solver.simplify()` to turn a sequence that is constructed
3339 by, e.g., concatenation of unit sequences, into a sequence value.
3341 :return: the representation of a sequence value as a vector of terms.
3344 for e in self.cterm.getSequenceValue():
3345 term = Term(self.solver)
3350 def isUninterpretedSortValue(self):
3351 """:return: True iff this term is a value from an uninterpreted sort."""
3352 return self.cterm.isUninterpretedSortValue()
3354 def getUninterpretedSortValue(self):
3356 Asserts :py:meth:`isUninterpretedSortValue()`.
3358 :return: the representation of an uninterpreted value as a pair of its sort and its index.
3360 return self.cterm.getUninterpretedSortValue()
3362 def isTupleValue(self):
3363 """:return: True iff this term is a tuple value."""
3364 return self.cterm.isTupleValue()
3366 def getTupleValue(self):
3368 Asserts :py:meth:`isTupleValue()`.
3370 :return: the representation of a tuple value as a vector of terms.
3373 for e in self.cterm.getTupleValue():
3374 term = Term(self.solver)
3379 def isRealValue(self):
3381 .. note:: A term of kind PI is not considered to be a real value.
3383 :return: True iff this term is a rational value.
3385 return self.cterm.isRealValue()
3387 def getRealValue(self):
3389 Asserts :py:meth:`isRealValue()`.
3391 :return: the representation of a rational value as a python Fraction.
3393 return Fraction(self.cterm.getRealValue().decode())
3395 def isBitVectorValue(self):
3396 """:return: True iff this term is a bit-vector value."""
3397 return self.cterm.isBitVectorValue()
3399 def getBitVectorValue(self, base = 2):
3401 Asserts :py:meth:`isBitVectorValue()`.
3402 Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexdecimal string).
3404 :return: the representation of a bit-vector value in string representation.
3406 return self.cterm.getBitVectorValue(base).decode()
3408 def toPythonObj(self):
3410 Converts a constant value Term to a Python object.
3414 - Boolean -- returns a Python bool
3415 - Int -- returns a Python int
3416 - Real -- returns a Python Fraction
3417 - BV -- returns a Python int (treats BV as unsigned)
3418 - String -- returns a Python Unicode string
3419 - Array -- returns a Python dict mapping indices to values. the constant base is returned as the default value
3423 if self.isBooleanValue():
3424 return self.getBooleanValue()
3425 elif self.isIntegerValue():
3426 return self.getIntegerValue()
3427 elif self.isRealValue():
3428 return self.getRealValue()
3429 elif self.isBitVectorValue():
3430 return int(self.getBitVectorValue(), 2)
3431 elif self.isStringValue():
3432 return self.getStringValue()
3433 elif self.getSort().isArray():
3439 # Array models are represented as a series of store operations
3440 # on a constant array
3443 if t.getKind().value == c_Kind.STORE:
3445 keys.append(t[1].toPythonObj())
3446 values.append(t[2].toPythonObj())
3447 to_visit.append(t[0])
3449 assert t.getKind().value == c_Kind.CONST_ARRAY
3450 base_value = t.getConstArrayBase().toPythonObj()
3452 assert len(keys) == len(values)
3453 assert base_value is not None
3455 # put everything in a dictionary with the constant
3456 # base as the result for any index not included in the stores
3457 res = defaultdict(lambda : base_value)
3458 for k, v in zip(keys, values):
3464 # Generate rounding modes
3465 cdef __rounding_modes = {
3466 <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
3467 <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
3468 <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
3469 <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
3470 <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway"
3473 mod_ref = sys.modules[__name__]
3474 for rm_int, name in __rounding_modes.items():
3475 r = RoundingMode(rm_int)
3477 if name in dir(mod_ref):
3478 raise RuntimeError("Redefinition of Python RoundingMode %s."%name)
3480 setattr(mod_ref, name, r)
3487 # Generate unknown explanations
3488 cdef __unknown_explanations = {
3489 <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
3490 <int> INCOMPLETE: "Incomplete",
3491 <int> TIMEOUT: "Timeout",
3492 <int> RESOURCEOUT: "Resourceout",
3493 <int> MEMOUT: "Memout",
3494 <int> INTERRUPTED: "Interrupted",
3495 <int> NO_STATUS: "NoStatus",
3496 <int> UNSUPPORTED: "Unsupported",
3497 <int> OTHER: "Other",
3498 <int> UNKNOWN_REASON: "UnknownReason"
3501 for ue_int, name in __unknown_explanations.items():
3502 u = UnknownExplanation(ue_int)
3504 if name in dir(mod_ref):
3505 raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
3507 setattr(mod_ref, name, u)