1 from collections import defaultdict
2 from fractions import Fraction
3 from functools import wraps
6 from cython.operator cimport dereference, preincrement
8 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
9 from libc.stddef cimport wchar_t
11 from libcpp cimport bool as c_bool
12 from libcpp.pair cimport pair
13 from libcpp.set cimport set as c_set
14 from libcpp.string cimport string
15 from libcpp.vector cimport vector
17 from cvc5 cimport cout
18 from cvc5 cimport Datatype as c_Datatype
19 from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
20 from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
21 from cvc5 cimport DatatypeDecl as c_DatatypeDecl
22 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
23 from cvc5 cimport Result as c_Result
24 from cvc5 cimport SynthResult as c_SynthResult
25 from cvc5 cimport RoundingMode as c_RoundingMode
26 from cvc5 cimport UnknownExplanation as c_UnknownExplanation
27 from cvc5 cimport Op as c_Op
28 from cvc5 cimport OptionInfo as c_OptionInfo
29 from cvc5 cimport holds as c_holds
30 from cvc5 cimport getVariant as c_getVariant
31 from cvc5 cimport Solver as c_Solver
32 from cvc5 cimport Statistics as c_Statistics
33 from cvc5 cimport Stat as c_Stat
34 from cvc5 cimport Grammar as c_Grammar
35 from cvc5 cimport Sort as c_Sort
36 from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
37 from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
38 from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
39 from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT
40 from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED
41 from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON
42 from cvc5 cimport OTHER
43 from cvc5 cimport Term as c_Term
44 from cvc5 cimport hash as c_hash
45 from cvc5 cimport wstring as c_wstring
46 from cvc5 cimport tuple as c_tuple
47 from cvc5 cimport get0, get1, get2
48 from cvc5kinds cimport Kind as c_Kind
50 cdef extern from "Python.h":
51 wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
52 object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
53 void PyMem_Free(void*)
55 ################################## DECORATORS #################################
56 def expand_list_arg(num_req_args=0):
58 Creates a decorator that looks at index num_req_args of the args,
59 if it's a list, it expands it before calling the function.
63 def wrapper(owner, *args):
64 if len(args) == num_req_args + 1 and \
65 isinstance(args[num_req_args], list):
66 args = list(args[:num_req_args]) + args[num_req_args]
67 return func(owner, *args)
70 ###############################################################################
73 ### Using PEP-8 spacing recommendations
74 ### Limit linewidth to 79 characters
75 ### Break before binary operators
76 ### surround top level functions and classes with two spaces
77 ### separate methods by one space
78 ### use spaces in functions sparingly to separate logical blocks
79 ### can omit spaces between unrelated oneliners
80 ### always use c++ default arguments
81 #### only use default args of None at python level
83 # References and pointers
84 # The Solver object holds a pointer to a c_Solver.
85 # This is because the assignment operator is deleted in the C++ API for solvers.
86 # Cython has a limitation where you can't stack allocate objects
87 # that have constructors with arguments:
88 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
89 # To get around that you can either have a nullary constructor and assignment
90 # or, use a pointer (which is what we chose).
91 # An additional complication of this is that to free up resources, you must
92 # know when to delete the object.
93 # Python will not follow the same scoping rules as in C++, so it must be
94 # able to reference count. To do this correctly, the solver must be a
95 # reference in the Python class for any class that keeps a pointer to
96 # the solver in C++ (to ensure the solver is not deleted before something
97 # that depends on it).
100 ## Objects for hashing
101 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
102 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
103 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
109 Wrapper class for :cpp:class:`cvc5::api::Datatype`.
113 def __cinit__(self, Solver solver):
116 def __getitem__(self, index):
117 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
118 if isinstance(index, int) and index >= 0:
119 dc.cdc = self.cd[(<int?> index)]
120 elif isinstance(index, str):
121 dc.cdc = self.cd[(<const string &> index.encode())]
123 raise ValueError("Expecting a non-negative integer or string")
126 def getConstructor(self, str name):
128 :param name: the name of the constructor.
129 :return: a constructor by name.
131 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
132 dc.cdc = self.cd.getConstructor(name.encode())
135 def getConstructorTerm(self, str name):
137 :param name: the name of the constructor.
138 :return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`).
140 cdef Term term = Term(self.solver)
141 term.cterm = self.cd.getConstructorTerm(name.encode())
144 def getSelector(self, str name):
146 :param name: the name of the selector..
147 :return: a selector by name.
149 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
150 ds.cds = self.cd.getSelector(name.encode())
155 :return: the name of the datatype.
157 return self.cd.getName().decode()
159 def getNumConstructors(self):
161 :return: number of constructors in this datatype.
163 return self.cd.getNumConstructors()
165 def getParameters(self):
167 :return: the parameters of this datatype, if it is parametric. An exception is thrown if this datatype is not parametric.
170 for s in self.cd.getParameters():
171 sort = Sort(self.solver)
173 param_sorts.append(sort)
176 def isParametric(self):
177 """:return: True if this datatype is parametric."""
178 return self.cd.isParametric()
180 def isCodatatype(self):
181 """:return: True if this datatype corresponds to a co-datatype."""
182 return self.cd.isCodatatype()
185 """:return: True if this datatype corresponds to a tuple."""
186 return self.cd.isTuple()
189 """:return: True if this datatype corresponds to a record."""
190 return self.cd.isRecord()
193 """:return: True if this datatype is finite."""
194 return self.cd.isFinite()
196 def isWellFounded(self):
197 """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
198 return self.cd.isWellFounded()
201 """:return: True if this Datatype is a null object."""
202 return self.cd.isNull()
205 return self.cd.toString().decode()
208 return self.cd.toString().decode()
212 dc = DatatypeConstructor(self.solver)
217 cdef class DatatypeConstructor:
219 A cvc5 datatype constructor.
220 Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.
222 cdef c_DatatypeConstructor cdc
224 def __cinit__(self, Solver solver):
225 self.cdc = c_DatatypeConstructor()
228 def __getitem__(self, index):
229 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
230 if isinstance(index, int) and index >= 0:
231 ds.cds = self.cdc[(<int?> index)]
232 elif isinstance(index, str):
233 ds.cds = self.cdc[(<const string &> index.encode())]
235 raise ValueError("Expecting a non-negative integer or string")
240 :return: the name of the constructor.
242 return self.cdc.getName().decode()
244 def getConstructorTerm(self):
246 :return: the constructor operator as a term.
248 cdef Term term = Term(self.solver)
249 term.cterm = self.cdc.getConstructorTerm()
252 def getInstantiatedConstructorTerm(self, Sort retSort):
254 Specialized method for parametric datatypes (see
255 :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm()
256 <cvc5::api::DatatypeConstructor::getInstantiatedConstructorTerm>`).
258 :param retSort: the desired return sort of the constructor
259 :return: the constructor operator as a term.
261 cdef Term term = Term(self.solver)
262 term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort)
265 def getTesterTerm(self):
267 :return: the tester operator that is related to this constructor, as a term.
269 cdef Term term = Term(self.solver)
270 term.cterm = self.cdc.getTesterTerm()
273 def getNumSelectors(self):
275 :return: the number of selecters (so far) of this Datatype constructor.
277 return self.cdc.getNumSelectors()
279 def getSelector(self, str name):
281 :param name: the name of the datatype selector.
282 :return: the first datatype selector with the given name
284 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
285 ds.cds = self.cdc.getSelector(name.encode())
288 def getSelectorTerm(self, str name):
290 :param name: the name of the datatype selector.
291 :return: a term representing the firstdatatype selector with the given name.
293 cdef Term term = Term(self.solver)
294 term.cterm = self.cdc.getSelectorTerm(name.encode())
298 """:return: True if this DatatypeConstructor is a null object."""
299 return self.cdc.isNull()
302 return self.cdc.toString().decode()
305 return self.cdc.toString().decode()
309 ds = DatatypeSelector(self.solver)
314 cdef class DatatypeConstructorDecl:
316 A cvc5 datatype constructor declaration.
317 Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.
319 cdef c_DatatypeConstructorDecl cddc
322 def __cinit__(self, Solver solver):
325 def addSelector(self, str name, Sort sort):
327 Add datatype selector declaration.
329 :param name: the name of the datatype selector declaration to add.
330 :param sort: the codomain sort of the datatype selector declaration
333 self.cddc.addSelector(name.encode(), sort.csort)
335 def addSelectorSelf(self, str name):
337 Add datatype selector declaration whose codomain sort is the
340 :param name: the name of the datatype selector declaration to add.
342 self.cddc.addSelectorSelf(name.encode())
345 """:return: True if this DatatypeConstructorDecl is a null object."""
346 return self.cddc.isNull()
349 return self.cddc.toString().decode()
352 return self.cddc.toString().decode()
355 cdef class DatatypeDecl:
357 A cvc5 datatype declaration.
358 Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.
360 cdef c_DatatypeDecl cdd
362 def __cinit__(self, Solver solver):
365 def addConstructor(self, DatatypeConstructorDecl ctor):
367 Add a datatype constructor declaration.
369 :param ctor: the datatype constructor declaration to add.
371 self.cdd.addConstructor(ctor.cddc)
373 def getNumConstructors(self):
375 :return: number of constructors (so far) for this datatype declaration.
377 return self.cdd.getNumConstructors()
379 def isParametric(self):
381 :return: is this datatype declaration parametric?
383 return self.cdd.isParametric()
387 :return: the name of this datatype declaration.
389 return self.cdd.getName().decode()
392 """:return: True if this DatatypeDecl is a null object."""
393 return self.cdd.isNull()
396 return self.cdd.toString().decode()
399 return self.cdd.toString().decode()
402 cdef class DatatypeSelector:
404 A cvc5 datatype selector.
405 Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.
407 cdef c_DatatypeSelector cds
409 def __cinit__(self, Solver solver):
410 self.cds = c_DatatypeSelector()
415 :return: the name of this datatype selector.
417 return self.cds.getName().decode()
419 def getSelectorTerm(self):
421 :return: the selector opeartor of this datatype selector as a term.
423 cdef Term term = Term(self.solver)
424 term.cterm = self.cds.getSelectorTerm()
427 def getUpdaterTerm(self):
429 :return: the updater opeartor of this datatype selector as a term.
431 cdef Term term = Term(self.solver)
432 term.cterm = self.cds.getUpdaterTerm()
435 def getCodomainSort(self):
437 :return: the codomain sort of this selector.
439 cdef Sort sort = Sort(self.solver)
440 sort.csort = self.cds.getCodomainSort()
444 """:return: True if this DatatypeSelector is a null object."""
445 return self.cds.isNull()
448 return self.cds.toString().decode()
451 return self.cds.toString().decode()
457 An operator is a term that represents certain operators,
458 instantiated with its required parameters, e.g.,
459 a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`.
460 Wrapper class for :cpp:class:`cvc5::api::Op`.
464 def __cinit__(self, Solver solver):
468 def __eq__(self, Op other):
469 return self.cop == other.cop
471 def __ne__(self, Op other):
472 return self.cop != other.cop
475 return self.cop.toString().decode()
478 return self.cop.toString().decode()
481 return cophash(self.cop)
485 :return: the kind of this operator.
487 return Kind(<int> self.cop.getKind())
491 :return: True iff this operator is indexed.
493 return self.cop.isIndexed()
497 :return: True iff this operator is a null term.
499 return self.cop.isNull()
501 def getNumIndices(self):
503 :return: number of indices of this op.
505 return self.cop.getNumIndices()
507 def __getitem__(self, i):
509 Get the index at position i.
510 :param i: the position of the index to return
511 :return: the index at position i
513 cdef Term term = Term(self.solver)
514 term.cterm = self.cop[i]
521 Wrapper class for :cpp:class:`cvc5::api::Grammar`.
523 cdef c_Grammar cgrammar
525 def __cinit__(self, Solver solver):
527 self.cgrammar = c_Grammar()
529 def addRule(self, Term ntSymbol, Term rule):
531 Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
533 :param ntSymbol: the non-terminal to which the rule is added.
534 :param rule: the rule to add.
536 self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
538 def addAnyConstant(self, Term ntSymbol):
540 Allow ``ntSymbol`` to be an arbitrary constant.
542 :param ntSymbol: the non-terminal allowed to be constant.
544 self.cgrammar.addAnyConstant(ntSymbol.cterm)
546 def addAnyVariable(self, Term ntSymbol):
548 Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``.
550 :param ntSymbol: the non-terminal allowed to be any input variable.
552 self.cgrammar.addAnyVariable(ntSymbol.cterm)
554 def addRules(self, Term ntSymbol, rules):
556 Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
558 :param ntSymbol: the non-terminal to which the rules are added.
559 :param rules: the rules to add.
561 cdef vector[c_Term] crules
563 crules.push_back((<Term?> r).cterm)
564 self.cgrammar.addRules(ntSymbol.cterm, crules)
568 Encapsulation of a three-valued solver result, with explanations.
569 Wrapper class for :cpp:class:`cvc5::api::Result`.
573 # gets populated by solver
578 :return: True if Result is empty, i.e., a nullary Result, and not an actual result returned from a
579 :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` (and friends) query.
581 return self.cr.isNull()
585 :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.
587 return self.cr.isSat()
591 :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.
593 return self.cr.isUnsat()
597 :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.
599 return self.cr.isUnknown()
601 def getUnknownExplanation(self):
603 :return: an explanation for an unknown query result.
605 return UnknownExplanation(<int> self.cr.getUnknownExplanation())
607 def __eq__(self, Result other):
608 return self.cr == other.cr
610 def __ne__(self, Result other):
611 return self.cr != other.cr
614 return self.cr.toString().decode()
617 return self.cr.toString().decode()
619 cdef class SynthResult:
621 Encapsulation of a solver synth result. This is the return value of the
623 - :py:meth:`Solver.checkSynth()`
624 - :py:meth:`Solver.checkSynthNext()`
625 which we call synthesis queries. This class indicates whether the
626 synthesis query has a solution, has no solution, or is unknown.
628 cdef c_SynthResult cr
630 # gets populated by solver
631 self.cr = c_SynthResult()
635 :return: True if SynthResult is null, i.e. not a SynthResult returned from a synthesis query.
637 return self.cr.isNull()
639 def hasSolution(self):
641 :return: True if the synthesis query has a solution.
643 return self.cr.hasSolution()
645 def hasNoSolution(self):
647 :return: True if the synthesis query has no solution.
648 In this case, then it was determined there was no solution.
650 return self.cr.hasNoSolution()
654 :return: True if the result of the synthesis query could not be determined.
656 return self.cr.isUnknown()
659 return self.cr.toString().decode()
662 return self.cr.toString().decode()
664 cdef class RoundingMode:
666 Rounding modes for floating-point numbers.
668 For many floating-point operations, infinitely precise results may not be
669 representable with the number of available bits. Thus, the results are
670 rounded in a certain way to one of the representable floating-point numbers.
672 These rounding modes directly follow the SMT-LIB theory for floating-point
673 arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
674 The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
677 Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`.
679 cdef c_RoundingMode crm
681 def __cinit__(self, int rm):
682 # crm always assigned externally
683 self.crm = <c_RoundingMode> rm
684 self.name = __rounding_modes[rm]
686 def __eq__(self, RoundingMode other):
687 return (<int> self.crm) == (<int> other.crm)
689 def __ne__(self, RoundingMode other):
690 return not self.__eq__(other)
693 return hash((<int> self.crm, self.name))
702 cdef class UnknownExplanation:
704 Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`.
706 cdef c_UnknownExplanation cue
708 def __cinit__(self, int ue):
709 # crm always assigned externally
710 self.cue = <c_UnknownExplanation> ue
711 self.name = __unknown_explanations[ue]
713 def __eq__(self, UnknownExplanation other):
714 return (<int> self.cue) == (<int> other.cue)
716 def __ne__(self, UnknownExplanation other):
717 return not self.__eq__(other)
720 return hash((<int> self.crm, self.name))
730 """Wrapper class for :cpp:class:`cvc5::api::Solver`."""
731 cdef c_Solver* csolver
734 self.csolver = new c_Solver()
736 def __dealloc__(self):
739 def getBooleanSort(self):
740 """:return: sort Boolean
742 cdef Sort sort = Sort(self)
743 sort.csort = self.csolver.getBooleanSort()
746 def getIntegerSort(self):
747 """:return: sort Integer
749 cdef Sort sort = Sort(self)
750 sort.csort = self.csolver.getIntegerSort()
753 def getNullSort(self):
754 """:return: sort null
756 cdef Sort sort = Sort(self)
757 sort.csort = self.csolver.getNullSort()
760 def getRealSort(self):
761 """:return: sort Real
763 cdef Sort sort = Sort(self)
764 sort.csort = self.csolver.getRealSort()
767 def getRegExpSort(self):
768 """:return: sort of RegExp
770 cdef Sort sort = Sort(self)
771 sort.csort = self.csolver.getRegExpSort()
774 def getRoundingModeSort(self):
775 """:return: sort RoundingMode
777 cdef Sort sort = Sort(self)
778 sort.csort = self.csolver.getRoundingModeSort()
781 def getStringSort(self):
782 """:return: sort String
784 cdef Sort sort = Sort(self)
785 sort.csort = self.csolver.getStringSort()
788 def mkArraySort(self, Sort indexSort, Sort elemSort):
789 """Create an array sort.
791 :param indexSort: the array index sort
792 :param elemSort: the array element sort
793 :return: the array sort
795 cdef Sort sort = Sort(self)
796 sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
799 def mkBitVectorSort(self, uint32_t size):
800 """Create a bit-vector sort.
802 :param size: the bit-width of the bit-vector sort
803 :return: the bit-vector sort
805 cdef Sort sort = Sort(self)
806 sort.csort = self.csolver.mkBitVectorSort(size)
809 def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
810 """Create a floating-point sort.
812 :param exp: the bit-width of the exponent of the floating-point sort.
813 :param sig: the bit-width of the significand of the floating-point sort.
815 cdef Sort sort = Sort(self)
816 sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
819 def mkDatatypeSort(self, DatatypeDecl dtypedecl):
820 """Create a datatype sort.
822 :param dtypedecl: the datatype declaration from which the sort is created
823 :return: the datatype sort
825 cdef Sort sort = Sort(self)
826 sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
829 def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
831 Create a vector of datatype sorts using unresolved sorts. The names of
832 the datatype declarations in dtypedecls must be distinct.
834 This method is called when the DatatypeDecl objects dtypedecls have been
835 built using "unresolved" sorts.
837 We associate each sort in unresolvedSorts with exacly one datatype from
838 dtypedecls. In particular, it must have the same name as exactly one
839 datatype declaration in dtypedecls.
841 When constructing datatypes, unresolved sorts are replaced by the datatype
842 sort constructed for the datatype declaration it is associated with.
844 :param dtypedecls: the datatype declarations from which the sort is created
845 :param unresolvedSorts: the list of unresolved sorts
846 :return: the datatype sorts
848 if unresolvedSorts == None:
849 unresolvedSorts = set([])
851 assert isinstance(unresolvedSorts, set)
854 cdef vector[c_DatatypeDecl] decls
855 for decl in dtypedecls:
856 decls.push_back((<DatatypeDecl?> decl).cdd)
858 cdef c_set[c_Sort] usorts
859 for usort in unresolvedSorts:
860 usorts.insert((<Sort?> usort).csort)
862 csorts = self.csolver.mkDatatypeSorts(
863 <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
871 def mkFunctionSort(self, sorts, Sort codomain):
872 """ Create function sort.
874 :param sorts: the sort of the function arguments
875 :param codomain: the sort of the function return value
876 :return: the function sort
879 cdef Sort sort = Sort(self)
880 # populate a vector with dereferenced c_Sorts
881 cdef vector[c_Sort] v
883 if isinstance(sorts, Sort):
884 sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
886 elif isinstance(sorts, list):
888 v.push_back((<Sort?>s).csort)
890 sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
894 def mkParamSort(self, symbolname):
895 """ Create a sort parameter.
897 :param symbol: the name of the sort
898 :return: the sort parameter
900 cdef Sort sort = Sort(self)
901 sort.csort = self.csolver.mkParamSort(symbolname.encode())
904 @expand_list_arg(num_req_args=0)
905 def mkPredicateSort(self, *sorts):
906 """Create a predicate sort.
908 :param sorts: the list of sorts of the predicate, as a list or as distinct arguments.
909 :return: the predicate sort
911 cdef Sort sort = Sort(self)
912 cdef vector[c_Sort] v
914 v.push_back((<Sort?> s).csort)
915 sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
918 @expand_list_arg(num_req_args=0)
919 def mkRecordSort(self, *fields):
920 """Create a record sort
922 :param fields: the list of fields of the record, as a list or as distinct arguments
923 :return: the record sort
925 cdef Sort sort = Sort(self)
926 cdef vector[pair[string, c_Sort]] v
927 cdef pair[string, c_Sort] p
931 p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
933 sort.csort = self.csolver.mkRecordSort(
934 <const vector[pair[string, c_Sort]] &> v)
937 def mkSetSort(self, Sort elemSort):
938 """Create a set sort.
940 :param elemSort: the sort of the set elements
941 :return: the set sort
943 cdef Sort sort = Sort(self)
944 sort.csort = self.csolver.mkSetSort(elemSort.csort)
947 def mkBagSort(self, Sort elemSort):
948 """Create a bag sort.
950 :param elemSort: the sort of the bag elements
951 :return: the bag sort
953 cdef Sort sort = Sort(self)
954 sort.csort = self.csolver.mkBagSort(elemSort.csort)
957 def mkSequenceSort(self, Sort elemSort):
958 """Create a sequence sort.
960 :param elemSort: the sort of the sequence elements
961 :return: the sequence sort
963 cdef Sort sort = Sort(self)
964 sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
967 def mkUninterpretedSort(self, str name):
968 """Create an uninterpreted sort.
970 :param symbol: the name of the sort
971 :return: the uninterpreted sort
973 cdef Sort sort = Sort(self)
974 sort.csort = self.csolver.mkUninterpretedSort(name.encode())
977 def mkUnresolvedSort(self, str name, size_t arity = 0):
978 """Create an unresolved sort.
980 This is for creating yet unresolved sort placeholders for mutually
983 :param symbol: the name of the sort
984 :param arity: the number of sort parameters of the sort
985 :return: the unresolved sort
987 cdef Sort sort = Sort(self)
988 sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity)
991 def mkSortConstructorSort(self, str symbol, size_t arity):
992 """Create a sort constructor sort.
994 :param symbol: the symbol of the sort
995 :param arity: the arity of the sort
996 :return: the sort constructor sort
998 cdef Sort sort = Sort(self)
999 sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
1002 @expand_list_arg(num_req_args=0)
1003 def mkTupleSort(self, *sorts):
1004 """Create a tuple sort.
1006 :param sorts: of the elements of the tuple, as a list or as distinct arguments
1007 :return: the tuple sort
1009 cdef Sort sort = Sort(self)
1010 cdef vector[c_Sort] v
1012 v.push_back((<Sort?> s).csort)
1013 sort.csort = self.csolver.mkTupleSort(v)
1016 @expand_list_arg(num_req_args=1)
1017 def mkTerm(self, kind_or_op, *args):
1019 Supports the following arguments:
1021 - ``Term mkTerm(Kind kind)``
1022 - ``Term mkTerm(Kind kind, Op child1, List[Term] children)``
1023 - ``Term mkTerm(Kind kind, List[Term] children)``
1025 where ``List[Term]`` can also be comma-separated arguments
1027 cdef Term term = Term(self)
1028 cdef vector[c_Term] v
1031 if isinstance(kind_or_op, Kind):
1032 op = self.mkOp(kind_or_op)
1035 term.cterm = self.csolver.mkTerm((<Op?> op).cop)
1038 v.push_back((<Term?> a).cterm)
1039 term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
1042 def mkTuple(self, sorts, terms):
1043 """Create a tuple term. Terms are automatically converted if sorts are compatible.
1045 :param sorts: The sorts of the elements in the tuple
1046 :param terms: The elements in the tuple
1047 :return: the tuple Term
1049 cdef vector[c_Sort] csorts
1050 cdef vector[c_Term] cterms
1053 csorts.push_back((<Sort?> s).csort)
1055 cterms.push_back((<Term?> s).cterm)
1056 cdef Term result = Term(self)
1057 result.cterm = self.csolver.mkTuple(csorts, cterms)
1060 @expand_list_arg(num_req_args=0)
1061 def mkOp(self, k, *args):
1063 Supports the following uses:
1065 - ``Op mkOp(Kind kind)``
1066 - ``Op mkOp(Kind kind, const string& arg)``
1067 - ``Op mkOp(Kind kind, uint32_t arg0, ...)``
1069 cdef Op op = Op(self)
1070 cdef vector[uint32_t] v
1073 op.cop = self.csolver.mkOp(<c_Kind> k.value)
1074 elif len(args) == 1 and isinstance(args[0], str):
1075 op.cop = self.csolver.mkOp(<c_Kind> k.value,
1080 if not isinstance(a, int):
1082 "Expected uint32_t for argument {}".format(a))
1083 if a < 0 or a >= 2 ** 31:
1085 "Argument {} must fit in a uint32_t".format(a))
1086 v.push_back((<uint32_t?> a))
1087 op.cop = self.csolver.mkOp(<c_Kind> k.value, v)
1091 """Create a Boolean true constant.
1093 :return: the true constant
1095 cdef Term term = Term(self)
1096 term.cterm = self.csolver.mkTrue()
1100 """Create a Boolean false constant.
1102 :return: the false constant
1104 cdef Term term = Term(self)
1105 term.cterm = self.csolver.mkFalse()
1108 def mkBoolean(self, bint val):
1109 """Create a Boolean constant.
1111 :return: the Boolean constant
1112 :param val: the value of the constant
1114 cdef Term term = Term(self)
1115 term.cterm = self.csolver.mkBoolean(val)
1119 """Create a constant representing the number Pi.
1121 :return: a constant representing Pi
1123 cdef Term term = Term(self)
1124 term.cterm = self.csolver.mkPi()
1127 def mkInteger(self, val):
1128 """Create an integer constant.
1130 :param val: representation of the constant: either a string or integer
1131 :return: a constant of sort Integer
1133 cdef Term term = Term(self)
1134 if isinstance(val, str):
1135 term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
1137 assert(isinstance(val, int))
1138 term.cterm = self.csolver.mkInteger((<int?> val))
1141 def mkReal(self, val, den=None):
1142 """Create a real constant.
1144 :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.
1145 :param den: if not None, the value is `val`/`den`
1146 :return: a real term with literal value
1148 Can be used in various forms:
1150 - Given a string ``"N/D"`` constructs the corresponding rational.
1151 - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
1152 - 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``.
1153 - Given a string ``"W"`` or an integer, constructs that integer.
1154 - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``.
1156 cdef Term term = Term(self)
1158 term.cterm = self.csolver.mkReal(str(val).encode())
1160 if not isinstance(val, int) or not isinstance(den, int):
1161 raise ValueError("Expecting integers when"
1162 " constructing a rational"
1163 " but got: {}".format((val, den)))
1164 term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
1167 def mkRegexpAll(self):
1168 """Create a regular expression all (re.all) term.
1170 :return: the all term
1172 cdef Term term = Term(self)
1173 term.cterm = self.csolver.mkRegexpAll()
1176 def mkRegexpAllchar(self):
1177 """Create a regular expression allchar (re.allchar) term.
1179 :return: the allchar term
1181 cdef Term term = Term(self)
1182 term.cterm = self.csolver.mkRegexpAllchar()
1185 def mkRegexpNone(self):
1186 """Create a regular expression none (re.none) term.
1188 :return: the none term
1190 cdef Term term = Term(self)
1191 term.cterm = self.csolver.mkRegexpNone()
1194 def mkEmptySet(self, Sort s):
1195 """Create a constant representing an empty set of the given sort.
1197 :param sort: the sort of the set elements.
1198 :return: the empty set constant
1200 cdef Term term = Term(self)
1201 term.cterm = self.csolver.mkEmptySet(s.csort)
1204 def mkEmptyBag(self, Sort s):
1205 """Create a constant representing an empty bag of the given sort.
1207 :param sort: the sort of the bag elements.
1208 :return: the empty bag constant
1210 cdef Term term = Term(self)
1211 term.cterm = self.csolver.mkEmptyBag(s.csort)
1215 """Create a separation logic empty term.
1217 :return: the separation logic empty term
1219 cdef Term term = Term(self)
1220 term.cterm = self.csolver.mkSepEmp()
1223 def mkSepNil(self, Sort sort):
1224 """Create a separation logic nil term.
1226 :param sort: the sort of the nil term
1227 :return: the separation logic nil term
1229 cdef Term term = Term(self)
1230 term.cterm = self.csolver.mkSepNil(sort.csort)
1233 def mkString(self, str s, useEscSequences = None):
1235 Create a String constant from a `str` which may contain SMT-LIB
1236 compatible escape sequences like ``\\u1234`` to encode unicode characters.
1238 :param s: the string this constant represents
1239 :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character
1240 :return: the String constant
1242 cdef Term term = Term(self)
1243 cdef Py_ssize_t size
1244 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1245 if isinstance(useEscSequences, bool):
1246 term.cterm = self.csolver.mkString(
1247 s.encode(), <bint> useEscSequences)
1249 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1253 def mkEmptySequence(self, Sort sort):
1254 """Create an empty sequence of the given element sort.
1256 :param sort: The element sort of the sequence.
1257 :return: the empty sequence with given element sort.
1259 cdef Term term = Term(self)
1260 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1263 def mkUniverseSet(self, Sort sort):
1264 """Create a universe set of the given sort.
1266 :param sort: the sort of the set elements
1267 :return: the universe set constant
1269 cdef Term term = Term(self)
1270 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1273 @expand_list_arg(num_req_args=0)
1274 def mkBitVector(self, *args):
1276 Supports the following arguments:
1278 - ``Term mkBitVector(int size, int val=0)``
1279 - ``Term mkBitVector(int size, string val, int base)``
1281 :return: a bit-vector literal term
1282 :param size: an integer size.
1283 :param val: an integer representating the value, in the first form. In the second form, a string representing the value.
1284 :param base: the base of the string representation (second form only)
1286 cdef Term term = Term(self)
1288 raise ValueError("Missing arguments to mkBitVector")
1290 if not isinstance(size, int):
1292 "Invalid first argument to mkBitVector '{}', "
1293 "expected bit-vector size".format(size))
1295 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1296 elif len(args) == 2:
1298 if not isinstance(val, int):
1300 "Invalid second argument to mkBitVector '{}', "
1301 "expected integer value".format(size))
1302 term.cterm = self.csolver.mkBitVector(
1303 <uint32_t> size, <uint32_t> val)
1304 elif len(args) == 3:
1307 if not isinstance(val, str):
1309 "Invalid second argument to mkBitVector '{}', "
1310 "expected value string".format(size))
1311 if not isinstance(base, int):
1313 "Invalid third argument to mkBitVector '{}', "
1314 "expected base given as integer".format(size))
1315 term.cterm = self.csolver.mkBitVector(
1317 <const string&> str(val).encode(),
1320 raise ValueError("Unexpected inputs to mkBitVector")
1323 def mkConstArray(self, Sort sort, Term val):
1325 Create a constant array with the provided constant value stored at every
1328 :param sort: the sort of the constant array (must be an array sort)
1329 :param val: the constant value to store (must match the sort's element sort)
1330 :return: the constant array term
1332 cdef Term term = Term(self)
1333 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1336 def mkFloatingPointPosInf(self, int exp, int sig):
1337 """Create a positive infinity floating-point constant.
1339 :param exp: Number of bits in the exponent
1340 :param sig: Number of bits in the significand
1341 :return: the floating-point constant
1343 cdef Term term = Term(self)
1344 term.cterm = self.csolver.mkFloatingPointPosInf(exp, sig)
1347 def mkFloatingPointNegInf(self, int exp, int sig):
1348 """Create a negative infinity floating-point constant.
1350 :param exp: Number of bits in the exponent
1351 :param sig: Number of bits in the significand
1352 :return: the floating-point constant
1354 cdef Term term = Term(self)
1355 term.cterm = self.csolver.mkFloatingPointNegInf(exp, sig)
1358 def mkFloatingPointNaN(self, int exp, int sig):
1359 """Create a not-a-number (NaN) floating-point constant.
1361 :param exp: Number of bits in the exponent
1362 :param sig: Number of bits in the significand
1363 :return: the floating-point constant
1365 cdef Term term = Term(self)
1366 term.cterm = self.csolver.mkFloatingPointNaN(exp, sig)
1369 def mkFloatingPointPosZero(self, int exp, int sig):
1370 """Create a positive zero (+0.0) floating-point constant.
1372 :param exp: Number of bits in the exponent
1373 :param sig: Number of bits in the significand
1374 :return: the floating-point constant
1376 cdef Term term = Term(self)
1377 term.cterm = self.csolver.mkFloatingPointPosZero(exp, sig)
1380 def mkFloatingPointNegZero(self, int exp, int sig):
1381 """Create a negative zero (+0.0) floating-point constant.
1383 :param exp: Number of bits in the exponent
1384 :param sig: Number of bits in the significand
1385 :return: the floating-point constant
1387 cdef Term term = Term(self)
1388 term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig)
1391 def mkRoundingMode(self, RoundingMode rm):
1392 """Create a roundingmode constant.
1394 :param rm: the floating point rounding mode this constant represents
1396 cdef Term term = Term(self)
1397 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
1400 def mkFloatingPoint(self, int exp, int sig, Term val):
1401 """Create a floating-point constant.
1403 :param exp: Size of the exponent
1404 :param sig: Size of the significand
1405 :param val: Value of the floating-point constant as a bit-vector term
1407 cdef Term term = Term(self)
1408 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1411 def mkCardinalityConstraint(self, Sort sort, int index):
1412 """Create cardinality constraint.
1414 :param sort: Sort of the constraint
1415 :param index: The upper bound for the cardinality of the sort
1417 cdef Term term = Term(self)
1418 term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
1421 def mkConst(self, Sort sort, symbol=None):
1423 Create (first-order) constant (0-arity function symbol).
1427 .. code-block:: smtlib
1429 ( declare-const <symbol> <sort> )
1430 ( declare-fun <symbol> ( ) <sort> )
1432 :param sort: the sort of the constant
1433 :param symbol: the name of the constant. If None, a default symbol is used.
1434 :return: the first-order constant
1436 cdef Term term = Term(self)
1438 term.cterm = self.csolver.mkConst(sort.csort)
1440 term.cterm = self.csolver.mkConst(sort.csort,
1441 (<str?> symbol).encode())
1444 def mkVar(self, Sort sort, symbol=None):
1446 Create a bound variable to be used in a binder (i.e. a quantifier, a
1447 lambda, or a witness binder).
1449 :param sort: the sort of the variable
1450 :param symbol: the name of the variable
1451 :return: the variable
1453 cdef Term term = Term(self)
1455 term.cterm = self.csolver.mkVar(sort.csort)
1457 term.cterm = self.csolver.mkVar(sort.csort,
1458 (<str?> symbol).encode())
1461 def mkDatatypeConstructorDecl(self, str name):
1463 :return: a datatype constructor declaration
1464 :param name: the constructor's name
1466 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1467 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1470 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1471 """Create a datatype declaration.
1473 :param name: the name of the datatype
1474 :param isCoDatatype: true if a codatatype is to be constructed
1475 :return: the DatatypeDecl
1477 cdef DatatypeDecl dd = DatatypeDecl(self)
1478 cdef vector[c_Sort] v
1481 if sorts_or_bool is None and isCoDatatype is None:
1482 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1483 elif sorts_or_bool is not None and isCoDatatype is None:
1484 if isinstance(sorts_or_bool, bool):
1485 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1486 <bint> sorts_or_bool)
1487 elif isinstance(sorts_or_bool, Sort):
1488 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1489 (<Sort> sorts_or_bool).csort)
1490 elif isinstance(sorts_or_bool, list):
1491 for s in sorts_or_bool:
1492 v.push_back((<Sort?> s).csort)
1493 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1494 <const vector[c_Sort]&> v)
1496 raise ValueError("Unhandled second argument type {}"
1497 .format(type(sorts_or_bool)))
1498 elif sorts_or_bool is not None and isCoDatatype is not None:
1499 if isinstance(sorts_or_bool, Sort):
1500 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1501 (<Sort> sorts_or_bool).csort,
1502 <bint> isCoDatatype)
1503 elif isinstance(sorts_or_bool, list):
1504 for s in sorts_or_bool:
1505 v.push_back((<Sort?> s).csort)
1506 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1507 <const vector[c_Sort]&> v,
1508 <bint> isCoDatatype)
1510 raise ValueError("Unhandled second argument type {}"
1511 .format(type(sorts_or_bool)))
1513 raise ValueError("Can't create DatatypeDecl with {}".format([type(a)
1520 def simplify(self, Term t):
1522 Simplify a formula without doing "much" work. Does not involve the
1523 SAT Engine in the simplification, but uses the current definitions,
1524 assertions, and the current partial model, if one has been constructed.
1525 It also involves theory normalization.
1527 :param t: the formula to simplify
1528 :return: the simplified formula
1530 cdef Term term = Term(self)
1531 term.cterm = self.csolver.simplify(t.cterm)
1534 def assertFormula(self, Term term):
1535 """ Assert a formula
1539 .. code-block:: smtlib
1543 :param term: the formula to assert
1545 self.csolver.assertFormula(term.cterm)
1549 Check satisfiability.
1553 .. code-block:: smtlib
1557 :return: the result of the satisfiability check.
1559 cdef Result r = Result()
1560 r.cr = self.csolver.checkSat()
1563 def mkSygusGrammar(self, boundVars, ntSymbols):
1565 Create a SyGuS grammar. The first non-terminal is treated as the
1566 starting non-terminal, so the order of non-terminals matters.
1568 :param boundVars: the parameters to corresponding synth-fun/synth-inv
1569 :param ntSymbols: the pre-declaration of the non-terminal symbols
1570 :return: the grammar
1572 cdef Grammar grammar = Grammar(self)
1573 cdef vector[c_Term] bvc
1574 cdef vector[c_Term] ntc
1575 for bv in boundVars:
1576 bvc.push_back((<Term?> bv).cterm)
1577 for nt in ntSymbols:
1578 ntc.push_back((<Term?> nt).cterm)
1579 grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1582 def declareSygusVar(self, Sort sort, str symbol=""):
1583 """Append symbol to the current list of universal variables.
1587 .. code-block:: smtlib
1589 ( declare-var <symbol> <sort> )
1591 :param sort: the sort of the universal variable
1592 :param symbol: the name of the universal variable
1593 :return: the universal variable
1595 cdef Term term = Term(self)
1596 term.cterm = self.csolver.declareSygusVar(sort.csort, symbol.encode())
1599 def addSygusConstraint(self, Term t):
1601 Add a formula to the set of SyGuS constraints.
1605 .. code-block:: smtlib
1607 ( constraint <term> )
1609 :param term: the formula to add as a constraint
1611 self.csolver.addSygusConstraint(t.cterm)
1613 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1615 Add a set of SyGuS constraints to the current state that correspond to an
1616 invariant synthesis problem.
1620 .. code-block:: smtlib
1622 ( inv-constraint <inv> <pre> <trans> <post> )
1624 :param inv: the function-to-synthesize
1625 :param pre: the pre-condition
1626 :param trans: the transition relation
1627 :param post: the post-condition
1629 self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1631 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1633 Synthesize n-ary function following specified syntactic constraints.
1637 .. code-block:: smtlib
1639 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1641 :param symbol: the name of the function
1642 :param boundVars: the parameters to this function
1643 :param sort: the sort of the return value of this function
1644 :param grammar: the syntactic constraints
1645 :return: the function
1647 cdef Term term = Term(self)
1648 cdef vector[c_Term] v
1649 for bv in bound_vars:
1650 v.push_back((<Term?> bv).cterm)
1652 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1654 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1657 def checkSynth(self):
1659 Try to find a solution for the synthesis conjecture corresponding to the
1660 current list of functions-to-synthesize, universal variables and
1665 .. code-block:: smtlib
1669 :return: the result of the check, which is "solution" if the check
1670 found a solution in which case solutions are available via
1671 getSynthSolutions, "no solution" if it was determined there is
1672 no solution, or "unknown" otherwise.
1674 cdef SynthResult r = SynthResult()
1675 r.cr = self.csolver.checkSynth()
1678 def checkSynthNext(self):
1680 Try to find a next solution for the synthesis conjecture corresponding
1681 to the current list of functions-to-synthesize, universal variables and
1682 constraints. Must be called immediately after a successful call to
1683 check-synth or check-synth-next. Requires incremental mode.
1687 .. code-block:: smtlib
1691 :return: the result of the check, which is "solution" if the check
1692 found a solution in which case solutions are available via
1693 getSynthSolutions, "no solution" if it was determined there is
1694 no solution, or "unknown" otherwise.
1696 cdef SynthResult r = SynthResult()
1697 r.cr = self.csolver.checkSynthNext()
1700 def getSynthSolution(self, Term term):
1702 Get the synthesis solution of the given term. This method should be
1703 called immediately after the solver answers unsat for sygus input.
1705 :param term: the term for which the synthesis solution is queried
1706 :return: the synthesis solution of the given term
1708 cdef Term t = Term(self)
1709 t.cterm = self.csolver.getSynthSolution(term.cterm)
1712 def getSynthSolutions(self, list terms):
1714 Get the synthesis solutions of the given terms. This method should be
1715 called immediately after the solver answers unsat for sygus input.
1717 :param terms: the terms for which the synthesis solutions is queried
1718 :return: the synthesis solutions of the given terms
1721 cdef vector[c_Term] vec
1723 vec.push_back((<Term?> t).cterm)
1724 cresult = self.csolver.getSynthSolutions(vec)
1732 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1734 Synthesize invariant.
1738 .. code-block:: smtlib
1740 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1742 :param symbol: the name of the invariant
1743 :param boundVars: the parameters to this invariant
1744 :param grammar: the syntactic constraints
1745 :return: the invariant
1747 cdef Term term = Term(self)
1748 cdef vector[c_Term] v
1749 for bv in bound_vars:
1750 v.push_back((<Term?> bv).cterm)
1752 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
1754 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
1757 @expand_list_arg(num_req_args=0)
1758 def checkSatAssuming(self, *assumptions):
1759 """ Check satisfiability assuming the given formula.
1763 .. code-block:: smtlib
1765 ( check-sat-assuming ( <prop_literal> ) )
1767 :param assumptions: the formulas to assume, as a list or as distinct arguments
1768 :return: the result of the satisfiability check.
1770 cdef Result r = Result()
1771 # used if assumptions is a list of terms
1772 cdef vector[c_Term] v
1773 for a in assumptions:
1774 v.push_back((<Term?> a).cterm)
1775 r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
1778 @expand_list_arg(num_req_args=1)
1779 def declareDatatype(self, str symbol, *ctors):
1781 Create datatype sort.
1785 .. code-block:: smtlib
1787 ( declare-datatype <symbol> <datatype_decl> )
1789 :param symbol: the name of the datatype sort
1790 :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
1791 :return: the datatype sort
1793 cdef Sort sort = Sort(self)
1794 cdef vector[c_DatatypeConstructorDecl] v
1797 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1798 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1801 def declareFun(self, str symbol, list sorts, Sort sort):
1802 """Declare n-ary function symbol.
1806 .. code-block:: smtlib
1808 ( declare-fun <symbol> ( <sort>* ) <sort> )
1810 :param symbol: the name of the function
1811 :param sorts: the sorts of the parameters to this function
1812 :param sort: the sort of the return value of this function
1813 :return: the function
1815 cdef Term term = Term(self)
1816 cdef vector[c_Sort] v
1818 v.push_back((<Sort?> s).csort)
1819 term.cterm = self.csolver.declareFun(symbol.encode(),
1820 <const vector[c_Sort]&> v,
1824 def declareSort(self, str symbol, int arity):
1825 """Declare uninterpreted sort.
1829 .. code-block:: smtlib
1831 ( declare-sort <symbol> <numeral> )
1833 :param symbol: the name of the sort
1834 :param arity: the arity of the sort
1837 cdef Sort sort = Sort(self)
1838 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
1841 def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
1842 """Define n-ary function.
1846 .. code-block:: smtlib
1848 ( define-fun <function_def> )
1850 :param symbol: the name of the function
1851 :param bound_vars: the parameters to this function
1852 :param sort: the sort of the return value of this function
1853 :param term: the function body
1854 :param glbl: determines whether this definition is global (i.e. persists when popping the context)
1855 :return: the function
1857 cdef Term fun = Term(self)
1858 cdef vector[c_Term] v
1859 for bv in bound_vars:
1860 v.push_back((<Term?> bv).cterm)
1862 fun.cterm = self.csolver.defineFun(symbol.encode(),
1863 <const vector[c_Term] &> v,
1869 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1870 """Define recursive functions.
1874 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1875 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1880 .. code-block:: smtlib
1882 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1884 Create elements of parameter ``funs`` with mkConst().
1886 :param funs: the sorted functions
1887 :param bound_vars: the list of parameters to the functions
1888 :param terms: the list of function bodies of the functions
1889 :param global: determines whether this definition is global (i.e. persists when popping the context)
1890 :return: the function
1892 cdef Term term = Term(self)
1893 cdef vector[c_Term] v
1894 for bv in bound_vars:
1895 v.push_back((<Term?> bv).cterm)
1898 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
1899 <const vector[c_Term] &> v,
1900 (<Sort?> sort_or_term).csort,
1904 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
1905 <const vector[c_Term]&> v,
1906 (<Term?> sort_or_term).cterm,
1911 def defineFunsRec(self, funs, bound_vars, terms):
1912 """Define recursive functions.
1916 .. code-block:: smtlib
1918 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1920 Create elements of parameter ``funs`` with mkConst().
1922 :param funs: the sorted functions
1923 :param bound_vars: the list of parameters to the functions
1924 :param terms: the list of function bodies of the functions
1925 :param global: determines whether this definition is global (i.e. persists when popping the context)
1926 :return: the function
1928 cdef vector[c_Term] vf
1929 cdef vector[vector[c_Term]] vbv
1930 cdef vector[c_Term] vt
1933 vf.push_back((<Term?> f).cterm)
1935 cdef vector[c_Term] temp
1936 for v in bound_vars:
1938 temp.push_back((<Term?> t).cterm)
1943 vf.push_back((<Term?> t).cterm)
1946 """Get the refutation proof
1950 .. code-block:: smtlib
1954 Requires to enable option
1955 :ref:`produce-proofs <lbl-option-produce-proofs>`.
1957 :return: a string representing the proof, according to the value of
1960 return self.csolver.getProof()
1962 def getLearnedLiterals(self):
1963 """Get a list of literals that are entailed by the current set of assertions
1967 .. code-block:: smtlib
1969 ( get-learned-literals )
1971 :return: the list of literals
1974 for a in self.csolver.getLearnedLiterals():
1980 def getAssertions(self):
1981 """Get the list of asserted formulas.
1985 .. code-block:: smtlib
1989 :return: the list of asserted formulas
1992 for a in self.csolver.getAssertions():
1995 assertions.append(term)
1998 def getInfo(self, str flag):
1999 """Get info from the solver.
2003 .. code-block:: smtlib
2005 ( get-info <info_flag> )
2007 :param flag: the info flag
2010 return self.csolver.getInfo(flag.encode())
2012 def getOption(self, str option):
2013 """Get the value of a given option.
2017 .. code-block:: smtlib
2019 ( get-option <keyword> )
2021 :param option: the option for which the value is queried
2022 :return: a string representation of the option value
2024 return self.csolver.getOption(option.encode()).decode()
2026 def getOptionNames(self):
2027 """Get all option names that can be used with `setOption`, `getOption` and `getOptionInfo`.
2029 :return: all option names
2031 return [s.decode() for s in self.csolver.getOptionNames()]
2033 def getOptionInfo(self, str option):
2034 """Get some information about the given option. Check the `OptionInfo`
2035 class for more details on which information is available.
2037 :return: information about the given option
2039 # declare all the variables we may need later
2040 cdef c_OptionInfo.ValueInfo[c_bool] vib
2041 cdef c_OptionInfo.ValueInfo[string] vis
2042 cdef c_OptionInfo.NumberInfo[int64_t] nii
2043 cdef c_OptionInfo.NumberInfo[uint64_t] niu
2044 cdef c_OptionInfo.NumberInfo[double] nid
2045 cdef c_OptionInfo.ModeInfo mi
2047 oi = self.csolver.getOptionInfo(option.encode())
2048 # generic information
2050 'name': oi.name.decode(),
2051 'aliases': [s.decode() for s in oi.aliases],
2052 'setByUser': oi.setByUser,
2055 # now check which type is actually in the variant
2056 if c_holds[c_OptionInfo.VoidInfo](oi.valueInfo):
2059 elif c_holds[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo):
2062 vib = c_getVariant[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo)
2063 res['current'] = vib.currentValue
2064 res['default'] = vib.defaultValue
2065 elif c_holds[c_OptionInfo.ValueInfo[string]](oi.valueInfo):
2068 vis = c_getVariant[c_OptionInfo.ValueInfo[string]](oi.valueInfo)
2069 res['current'] = vis.currentValue.decode()
2070 res['default'] = vis.defaultValue.decode()
2071 elif c_holds[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo):
2074 nii = c_getVariant[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo)
2075 res['current'] = nii.currentValue
2076 res['default'] = nii.defaultValue
2077 res['minimum'] = nii.minimum.value() if nii.minimum.has_value() else None
2078 res['maximum'] = nii.maximum.value() if nii.maximum.has_value() else None
2079 elif c_holds[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo):
2082 niu = c_getVariant[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo)
2083 res['current'] = niu.currentValue
2084 res['default'] = niu.defaultValue
2085 res['minimum'] = niu.minimum.value() if niu.minimum.has_value() else None
2086 res['maximum'] = niu.maximum.value() if niu.maximum.has_value() else None
2087 elif c_holds[c_OptionInfo.NumberInfo[double]](oi.valueInfo):
2090 nid = c_getVariant[c_OptionInfo.NumberInfo[double]](oi.valueInfo)
2091 res['current'] = nid.currentValue
2092 res['default'] = nid.defaultValue
2093 res['minimum'] = nid.minimum.value() if nid.minimum.has_value() else None
2094 res['maximum'] = nid.maximum.value() if nid.maximum.has_value() else None
2095 elif c_holds[c_OptionInfo.ModeInfo](oi.valueInfo):
2097 res['type'] = 'mode'
2098 mi = c_getVariant[c_OptionInfo.ModeInfo](oi.valueInfo)
2099 res['current'] = mi.currentValue.decode()
2100 res['default'] = mi.defaultValue.decode()
2101 res['modes'] = [s.decode() for s in mi.modes]
2104 def getUnsatAssumptions(self):
2106 Get the set of unsat ("failed") assumptions.
2110 .. code-block:: smtlib
2112 ( get-unsat-assumptions )
2114 Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
2116 :return: the set of unsat assumptions.
2119 for a in self.csolver.getUnsatAssumptions():
2122 assumptions.append(term)
2125 def getUnsatCore(self):
2126 """Get the unsatisfiable core.
2130 .. code-block:: smtlib
2134 Requires to enable option :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
2137 In contrast to SMT-LIB, the API does not distinguish between named and
2138 unnamed assertions when producing an unsatisfiable core. Additionally,
2139 the API allows this option to be called after a check with assumptions.
2140 A subset of those assumptions may be included in the unsatisfiable core
2141 returned by this method.
2143 :return: a set of terms representing the unsatisfiable core
2146 for a in self.csolver.getUnsatCore():
2152 def getValue(self, Term t):
2153 """Get the value of the given term in the current model.
2157 .. code-block:: smtlib
2159 ( get-value ( <term> ) )
2161 :param term: the term for which the value is queried
2162 :return: the value of the given term
2164 cdef Term term = Term(self)
2165 term.cterm = self.csolver.getValue(t.cterm)
2168 def getModelDomainElements(self, Sort s):
2170 Get the domain elements of uninterpreted sort s in the current model. The
2171 current model interprets s as the finite sort whose domain elements are
2172 given in the return value of this method.
2174 :param s: The uninterpreted sort in question
2175 :return: the domain elements of s in the current model
2178 cresult = self.csolver.getModelDomainElements(s.csort)
2185 def isModelCoreSymbol(self, Term v):
2187 This returns false if the model value of free constant v was not
2188 essential for showing the satisfiability of the last call to checkSat
2189 using the current model. This method will only return false (for any v)
2190 if the model-cores option has been set.
2192 :param v: The term in question
2193 :return: true if v is a model core symbol
2195 return self.csolver.isModelCoreSymbol(v.cterm)
2197 def getModel(self, sorts, consts):
2206 Requires to enable option
2207 :ref:`produce-models <lbl-option-produce-models>`.
2209 :param sorts: The list of uninterpreted sorts that should be printed in
2211 :param vars: The list of free constants that should be printed in the
2212 model. A subset of these may be printed based on
2214 :return: a string representing the model.
2217 cdef vector[c_Sort] csorts
2219 csorts.push_back((<Sort?> sort).csort)
2221 cdef vector[c_Term] cconsts
2222 for const in consts:
2223 cconsts.push_back((<Term?> const).cterm)
2225 return self.csolver.getModel(csorts, cconsts)
2227 def getValueSepHeap(self):
2228 """When using separation logic, obtain the term for the heap.
2230 :return: The term for the heap
2232 cdef Term term = Term(self)
2233 term.cterm = self.csolver.getValueSepHeap()
2236 def getValueSepNil(self):
2237 """When using separation logic, obtain the term for nil.
2239 :return: The term for nil
2241 cdef Term term = Term(self)
2242 term.cterm = self.csolver.getValueSepNil()
2245 def declareSepHeap(self, Sort locType, Sort dataType):
2247 When using separation logic, this sets the location sort and the
2248 datatype sort to the given ones. This method should be invoked exactly
2249 once, before any separation logic constraints are provided.
2251 :param locSort: The location sort of the heap
2252 :param dataSort: The data sort of the heap
2254 self.csolver.declareSepHeap(locType.csort, dataType.csort)
2256 def declarePool(self, str symbol, Sort sort, initValue):
2257 """Declare a symbolic pool of terms with the given initial value.
2261 .. code-block:: smtlib
2263 ( declare-pool <symbol> <sort> ( <term>* ) )
2265 :param symbol: The name of the pool
2266 :param sort: The sort of the elements of the pool.
2267 :param initValue: The initial value of the pool
2269 cdef Term term = Term(self)
2270 cdef vector[c_Term] niv
2272 niv.push_back((<Term?> v).cterm)
2273 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
2276 def pop(self, nscopes=1):
2277 """Pop ``nscopes`` level(s) from the assertion stack.
2281 .. code-block:: smtlib
2285 :param nscopes: the number of levels to pop
2287 self.csolver.pop(nscopes)
2289 def push(self, nscopes=1):
2290 """ Push ``nscopes`` level(s) to the assertion stack.
2294 .. code-block:: smtlib
2298 :param nscopes: the number of levels to push
2300 self.csolver.push(nscopes)
2302 def resetAssertions(self):
2304 Remove all assertions.
2308 .. code-block:: smtlib
2310 ( reset-assertions )
2313 self.csolver.resetAssertions()
2315 def setInfo(self, str keyword, str value):
2320 .. code-block:: smtlib
2322 ( set-info <attribute> )
2324 :param keyword: the info flag
2325 :param value: the value of the info flag
2327 self.csolver.setInfo(keyword.encode(), value.encode())
2329 def setLogic(self, str logic):
2334 .. code-block:: smtlib
2336 ( set-logic <symbol> )
2338 :param logic: the logic to set
2340 self.csolver.setLogic(logic.encode())
2342 def setOption(self, str option, str value):
2347 .. code-block:: smtlib
2349 ( set-option <option> )
2351 :param option: the option name
2352 :param value: the option value
2354 self.csolver.setOption(option.encode(), value.encode())
2357 def getInterpolant(self, Term conj, *args):
2358 """Get an interpolant.
2362 .. code-block:: smtlib
2364 ( get-interpol <conj> )
2365 ( get-interpol <conj> <grammar> )
2367 Requires option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
2369 Supports the following variants:
2371 - ``Term getInteprolant(Term conj)``
2372 - ``Term getInteprolant(Term conj, Grammar grammar)``
2374 :param conj: the conjecture term
2375 :param output: the term where the result will be stored
2376 :param grammar: a grammar for the inteprolant
2377 :return: True iff an interpolant was found
2379 cdef Term result = Term(self)
2381 result.cterm = self.csolver.getInterpolant(conj.cterm)
2383 assert len(args) == 1
2384 assert isinstance(args[0], Grammar)
2385 result.cterm = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> args[0]).cgrammar)
2389 def getInterpolantNext(self):
2391 Get the next interpolant. Can only be called immediately after
2392 a succesful call to get-interpol or get-interpol-next.
2393 Is guaranteed to produce a syntactically different interpolant wrt the
2394 last returned interpolant if successful.
2398 .. code-block:: smtlib
2400 ( get-interpol-next )
2402 Requires to enable incremental mode, and
2403 option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
2405 :param output: the term where the result will be stored
2406 :return: True iff an interpolant was found
2408 cdef Term result = Term(self)
2409 result.cterm = self.csolver.getInterpolantNext()
2412 def getAbduct(self, Term conj, *args):
2417 .. code-block:: smtlib
2419 ( get-abduct <conj> )
2420 ( get-abduct <conj> <grammar> )
2422 Requires to enable option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2424 Supports the following variants:
2426 - ``Term getAbduct(Term conj)``
2427 - ``Term getAbduct(Term conj, Grammar grammar)``
2429 :param conj: the conjecture term
2430 :param output: the term where the result will be stored
2431 :param grammar: a grammar for the abduct
2432 :return: True iff an abduct was found
2434 cdef Term result = Term(self)
2436 result.cterm = self.csolver.getAbduct(conj.cterm)
2438 assert len(args) == 1
2439 assert isinstance(args[0], Grammar)
2440 result.cterm = self.csolver.getAbduct(conj.cterm, (<Grammar ?> args[0]).cgrammar)
2443 def getAbductNext(self):
2445 Get the next abduct. Can only be called immediately after
2446 a succesful call to get-abduct or get-abduct-next.
2447 Is guaranteed to produce a syntactically different abduct wrt the
2448 last returned abduct if successful.
2452 .. code-block:: smtlib
2456 Requires to enable incremental mode, and
2457 option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2458 :param output: the term where the result will be stored
2459 :return: True iff an abduct was found
2461 cdef Term result = Term(self)
2462 result.cterm = self.csolver.getAbductNext()
2465 def blockModel(self):
2467 Block the current model. Can be called only if immediately preceded by a
2468 SAT or INVALID query.
2472 .. code-block:: smtlib
2476 Requires enabling option
2477 :ref:`produce-models <lbl-option-produce-models>`
2479 :ref:`block-models <lbl-option-block-models>`
2480 to a mode other than ``none``.
2482 self.csolver.blockModel()
2484 def blockModelValues(self, terms):
2486 Block the current model values of (at least) the values in terms. Can be
2487 called only if immediately preceded by a SAT or NOT_ENTAILED query.
2491 .. code-block:: smtlib
2493 (block-model-values ( <terms>+ ))
2495 Requires enabling option
2496 :ref:`produce-models <lbl-option-produce-models>`.
2498 cdef vector[c_Term] nts
2500 nts.push_back((<Term?> t).cterm)
2501 self.csolver.blockModelValues(nts)
2503 def getInstantiations(self):
2505 Return a string that contains information about all instantiations made
2506 by the quantifiers module.
2508 return self.csolver.getInstantiations()
2510 def getStatistics(self):
2512 Returns a snapshot of the current state of the statistic values of this
2513 solver. The returned object is completely decoupled from the solver and
2514 will not change when the solver is used again.
2517 res.cstats = self.csolver.getStatistics()
2523 The sort of a cvc5 term.
2527 def __cinit__(self, Solver solver):
2528 # csort always set by Solver
2529 self.solver = solver
2531 def __eq__(self, Sort other):
2532 return self.csort == other.csort
2534 def __ne__(self, Sort other):
2535 return self.csort != other.csort
2537 def __lt__(self, Sort other):
2538 return self.csort < other.csort
2540 def __gt__(self, Sort other):
2541 return self.csort > other.csort
2543 def __le__(self, Sort other):
2544 return self.csort <= other.csort
2546 def __ge__(self, Sort other):
2547 return self.csort >= other.csort
2550 return self.csort.toString().decode()
2553 return self.csort.toString().decode()
2556 return csorthash(self.csort)
2558 def hasSymbol(self):
2559 """:return: True iff this sort has a symbol."""
2560 return self.csort.hasSymbol()
2562 def getSymbol(self):
2564 Asserts :py:meth:`hasSymbol()`.
2566 :return: the raw symbol of the sort.
2568 return self.csort.getSymbol().decode()
2571 """:return: True if this Sort is a null sort."""
2572 return self.csort.isNull()
2574 def isBoolean(self):
2576 Is this a Boolean sort?
2578 :return: True if the sort is the Boolean sort.
2580 return self.csort.isBoolean()
2582 def isInteger(self):
2584 Is this an integer sort?
2586 :return: True if the sort is the integer sort.
2588 return self.csort.isInteger()
2592 Is this a real sort?
2594 :return: True if the sort is the real sort.
2596 return self.csort.isReal()
2600 Is this a string sort?
2602 :return: True if the sort is the string sort.
2604 return self.csort.isString()
2608 Is this a regexp sort?
2610 :return: True if the sort is the regexp sort.
2612 return self.csort.isRegExp()
2614 def isRoundingMode(self):
2616 Is this a rounding mode sort?
2618 :return: True if the sort is the rounding mode sort.
2620 return self.csort.isRoundingMode()
2622 def isBitVector(self):
2624 Is this a bit-vector sort?
2626 :return: True if the sort is a bit-vector sort.
2628 return self.csort.isBitVector()
2630 def isFloatingPoint(self):
2632 Is this a floating-point sort?
2634 :return: True if the sort is a bit-vector sort.
2636 return self.csort.isFloatingPoint()
2638 def isDatatype(self):
2640 Is this a datatype sort?
2642 :return: True if the sort is a datatype sort.
2644 return self.csort.isDatatype()
2646 def isConstructor(self):
2648 Is this a constructor sort?
2650 :return: True if the sort is a constructor sort.
2652 return self.csort.isConstructor()
2654 def isSelector(self):
2656 Is this a selector sort?
2658 :return: True if the sort is a selector sort.
2660 return self.csort.isSelector()
2664 Is this a tester sort?
2666 :return: True if the sort is a selector sort.
2668 return self.csort.isTester()
2670 def isUpdater(self):
2672 Is this a datatype updater sort?
2674 :return: True if the sort is a datatype updater sort.
2676 return self.csort.isUpdater()
2678 def isFunction(self):
2680 Is this a function sort?
2682 :return: True if the sort is a function sort.
2684 return self.csort.isFunction()
2686 def isPredicate(self):
2688 Is this a predicate sort?
2689 That is, is this a function sort mapping to Boolean? All predicate
2690 sorts are also function sorts.
2692 :return: True if the sort is a predicate sort.
2694 return self.csort.isPredicate()
2698 Is this a tuple sort?
2700 :return: True if the sort is a tuple sort.
2702 return self.csort.isTuple()
2706 Is this a record sort?
2708 :return: True if the sort is a record sort.
2710 return self.csort.isRecord()
2714 Is this an array sort?
2716 :return: True if the sort is an array sort.
2718 return self.csort.isArray()
2724 :return: True if the sort is a set sort.
2726 return self.csort.isSet()
2732 :return: True if the sort is a bag sort.
2734 return self.csort.isBag()
2736 def isSequence(self):
2738 Is this a sequence sort?
2740 :return: True if the sort is a sequence sort.
2742 return self.csort.isSequence()
2744 def isUninterpretedSort(self):
2746 Is this a sort uninterpreted?
2748 :return: True if the sort is uninterpreted.
2750 return self.csort.isUninterpretedSort()
2752 def isSortConstructor(self):
2754 Is this a sort constructor kind?
2756 :return: True if this a sort constructor kind.
2758 return self.csort.isSortConstructor()
2760 def getDatatype(self):
2762 :return: the underlying datatype of a datatype sort
2764 cdef Datatype d = Datatype(self.solver)
2765 d.cd = self.csort.getDatatype()
2768 def instantiate(self, params):
2770 Instantiate a parameterized datatype/sort sort.
2771 Create sorts parameter with :py:meth:`Solver.mkParamSort()`
2773 :param params: the list of sort parameters to instantiate with
2775 cdef Sort sort = Sort(self.solver)
2776 cdef vector[c_Sort] v
2778 v.push_back((<Sort?> s).csort)
2779 sort.csort = self.csort.instantiate(v)
2782 def substitute(self, sort_or_list_1, sort_or_list_2):
2784 Substitution of Sorts.
2786 :param sort_or_list_1: the subsort or subsorts to be substituted within this sort.
2787 :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort.
2789 Note that this replacement is applied during a pre-order traversal and
2790 only once to the sort. It is not run until fix point. In the case that
2791 sort_or_list_1 contains duplicates, the replacement earliest in the list
2795 ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])`` will
2796 return ``(Array (Array C D) B)``.
2799 # The resulting sort after substitution
2800 cdef Sort sort = Sort(self.solver)
2801 # lists for substitutions
2802 cdef vector[c_Sort] ces
2803 cdef vector[c_Sort] creplacements
2805 # normalize the input parameters to be lists
2806 if isinstance(sort_or_list_1, list):
2807 assert isinstance(sort_or_list_2, list)
2809 replacements = sort_or_list_2
2810 if len(es) != len(replacements):
2811 raise RuntimeError("Expecting list inputs to substitute to "
2812 "have the same length but got: "
2813 "{} and {}".format(len(es), len(replacements)))
2815 for e, r in zip(es, replacements):
2816 ces.push_back((<Sort?> e).csort)
2817 creplacements.push_back((<Sort?> r).csort)
2820 # add the single elements to the vectors
2821 ces.push_back((<Sort?> sort_or_list_1).csort)
2822 creplacements.push_back((<Sort?> sort_or_list_2).csort)
2824 # call the API substitute method with lists
2825 sort.csort = self.csort.substitute(ces, creplacements)
2829 def getConstructorArity(self):
2831 :return: the arity of a constructor sort.
2833 return self.csort.getConstructorArity()
2835 def getConstructorDomainSorts(self):
2837 :return: the domain sorts of a constructor sort
2840 for s in self.csort.getConstructorDomainSorts():
2841 sort = Sort(self.solver)
2843 domain_sorts.append(sort)
2846 def getConstructorCodomainSort(self):
2848 :return: the codomain sort of a constructor sort
2850 cdef Sort sort = Sort(self.solver)
2851 sort.csort = self.csort.getConstructorCodomainSort()
2854 def getSelectorDomainSort(self):
2856 :return: the domain sort of a selector sort
2858 cdef Sort sort = Sort(self.solver)
2859 sort.csort = self.csort.getSelectorDomainSort()
2862 def getSelectorCodomainSort(self):
2864 :return: the codomain sort of a selector sort
2866 cdef Sort sort = Sort(self.solver)
2867 sort.csort = self.csort.getSelectorCodomainSort()
2870 def getTesterDomainSort(self):
2872 :return: the domain sort of a tester sort
2874 cdef Sort sort = Sort(self.solver)
2875 sort.csort = self.csort.getTesterDomainSort()
2878 def getTesterCodomainSort(self):
2880 :return: the codomain sort of a tester sort, which is the Boolean sort
2882 cdef Sort sort = Sort(self.solver)
2883 sort.csort = self.csort.getTesterCodomainSort()
2886 def getFunctionArity(self):
2888 :return: the arity of a function sort
2890 return self.csort.getFunctionArity()
2892 def getFunctionDomainSorts(self):
2894 :return: the domain sorts of a function sort
2897 for s in self.csort.getFunctionDomainSorts():
2898 sort = Sort(self.solver)
2900 domain_sorts.append(sort)
2903 def getFunctionCodomainSort(self):
2905 :return: the codomain sort of a function sort
2907 cdef Sort sort = Sort(self.solver)
2908 sort.csort = self.csort.getFunctionCodomainSort()
2911 def getArrayIndexSort(self):
2913 :return: the array index sort of an array sort
2915 cdef Sort sort = Sort(self.solver)
2916 sort.csort = self.csort.getArrayIndexSort()
2919 def getArrayElementSort(self):
2921 :return: the array element sort of an array sort
2923 cdef Sort sort = Sort(self.solver)
2924 sort.csort = self.csort.getArrayElementSort()
2927 def getSetElementSort(self):
2929 :return: the element sort of a set sort
2931 cdef Sort sort = Sort(self.solver)
2932 sort.csort = self.csort.getSetElementSort()
2935 def getBagElementSort(self):
2937 :return: the element sort of a bag sort
2939 cdef Sort sort = Sort(self.solver)
2940 sort.csort = self.csort.getBagElementSort()
2943 def getSequenceElementSort(self):
2945 :return: the element sort of a sequence sort
2947 cdef Sort sort = Sort(self.solver)
2948 sort.csort = self.csort.getSequenceElementSort()
2951 def isUninterpretedSortParameterized(self):
2953 :return: True if an uninterpreted sort is parameterized
2955 return self.csort.isUninterpretedSortParameterized()
2957 def getUninterpretedSortParamSorts(self):
2959 :return: the parameter sorts of an uninterpreted sort
2962 for s in self.csort.getUninterpretedSortParamSorts():
2963 sort = Sort(self.solver)
2965 param_sorts.append(sort)
2968 def getSortConstructorArity(self):
2970 :return: the arity of a sort constructor sort
2972 return self.csort.getSortConstructorArity()
2974 def getBitVectorSize(self):
2976 :return: the bit-width of the bit-vector sort
2978 return self.csort.getBitVectorSize()
2980 def getFloatingPointExponentSize(self):
2982 :return: the bit-width of the exponent of the floating-point sort
2984 return self.csort.getFloatingPointExponentSize()
2986 def getFloatingPointSignificandSize(self):
2988 :return: the width of the significand of the floating-point sort
2990 return self.csort.getFloatingPointSignificandSize()
2992 def getDatatypeParamSorts(self):
2994 Return the parameters of a parametric datatype sort. If this sort
2995 is a non-instantiated parametric datatype, this returns the
2996 parameter sorts of the underlying datatype. If this sort is an
2997 instantiated parametric datatype, then this returns the sort
2998 parameters that were used to construct the sort via
2999 :py:meth:`instantiate()`.
3001 :return: the parameter sorts of a parametric datatype sort
3004 for s in self.csort.getDatatypeParamSorts():
3005 sort = Sort(self.solver)
3007 param_sorts.append(sort)
3010 def getDatatypeArity(self):
3012 :return: the arity of a datatype sort
3014 return self.csort.getDatatypeArity()
3016 def getTupleLength(self):
3018 :return: the length of a tuple sort
3020 return self.csort.getTupleLength()
3022 def getTupleSorts(self):
3024 :return: the element sorts of a tuple sort
3027 for s in self.csort.getTupleSorts():
3028 sort = Sort(self.solver)
3030 tuple_sorts.append(sort)
3034 cdef class Statistics:
3036 The cvc5 Statistics.
3037 Wrapper class for :cpp:class:`cvc5::api::Statistics`.
3038 Obtain a single statistic value using ``stats["name"]`` and a dictionary
3039 with all (visible) statistics using ``stats.get(internal=False, defaulted=False)``.
3041 cdef c_Statistics cstats
3043 cdef __stat_to_dict(self, const c_Stat& s):
3050 res = s.getString().decode()
3051 elif s.isHistogram():
3052 res = { h.first.decode(): h.second for h in s.getHistogram() }
3054 'defaulted': s.isDefault(),
3055 'internal': s.isInternal(),
3059 def __getitem__(self, str name):
3060 """Get the statistics information for the statistic called ``name``."""
3061 return self.__stat_to_dict(self.cstats.get(name.encode()))
3063 def get(self, bint internal = False, bint defaulted = False):
3064 """Get all statistics. See :cpp:class:`cvc5::api::Statistics::begin()` for more information."""
3065 cdef c_Statistics.iterator it = self.cstats.begin(internal, defaulted)
3066 cdef pair[string,c_Stat]* s
3068 while it != self.cstats.end():
3069 s = &dereference(it)
3070 res[s.first.decode()] = self.__stat_to_dict(s.second)
3078 Wrapper class for :cpp:class:`cvc5::api::Term`.
3082 def __cinit__(self, Solver solver):
3083 # cterm always set in the Solver object
3084 self.solver = solver
3086 def __eq__(self, Term other):
3087 return self.cterm == other.cterm
3089 def __ne__(self, Term other):
3090 return self.cterm != other.cterm
3092 def __lt__(self, Term other):
3093 return self.cterm < other.cterm
3095 def __gt__(self, Term other):
3096 return self.cterm > other.cterm
3098 def __le__(self, Term other):
3099 return self.cterm <= other.cterm
3101 def __ge__(self, Term other):
3102 return self.cterm >= other.cterm
3104 def __getitem__(self, int index):
3105 cdef Term term = Term(self.solver)
3107 term.cterm = self.cterm[index]
3109 raise ValueError("Expecting a non-negative integer or string")
3113 return self.cterm.toString().decode()
3116 return self.cterm.toString().decode()
3119 for ci in self.cterm:
3120 term = Term(self.solver)
3125 return ctermhash(self.cterm)
3127 def getNumChildren(self):
3128 """:return: the number of children of this term."""
3129 return self.cterm.getNumChildren()
3132 """:return: the id of this term."""
3133 return self.cterm.getId()
3136 """:return: the :py:class:`cvc5.Kind` of this term."""
3137 return Kind(<int> self.cterm.getKind())
3140 """:return: the :py:class:`cvc5.Sort` of this term."""
3141 cdef Sort sort = Sort(self.solver)
3142 sort.csort = self.cterm.getSort()
3145 def substitute(self, term_or_list_1, term_or_list_2):
3147 :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.
3149 Note that this replacement is applied during a pre-order traversal and
3150 only once to the term. It is not run until fix point. In the case that
3151 terms contains duplicates, the replacement earliest in the list takes
3152 priority. For example, calling substitute on ``f(x,y)`` with
3156 term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ]
3158 results in the term ``f(g(z),y)``.
3160 # The resulting term after substitution
3161 cdef Term term = Term(self.solver)
3162 # lists for substitutions
3163 cdef vector[c_Term] ces
3164 cdef vector[c_Term] creplacements
3166 # normalize the input parameters to be lists
3167 if isinstance(term_or_list_1, list):
3168 assert isinstance(term_or_list_2, list)
3170 replacements = term_or_list_2
3171 if len(es) != len(replacements):
3172 raise RuntimeError("Expecting list inputs to substitute to "
3173 "have the same length but got: "
3174 "{} and {}".format(len(es), len(replacements)))
3176 for e, r in zip(es, replacements):
3177 ces.push_back((<Term?> e).cterm)
3178 creplacements.push_back((<Term?> r).cterm)
3181 # add the single elements to the vectors
3182 ces.push_back((<Term?> term_or_list_1).cterm)
3183 creplacements.push_back((<Term?> term_or_list_2).cterm)
3185 # call the API substitute method with lists
3186 term.cterm = self.cterm.substitute(ces, creplacements)
3190 """:return: True iff this term has an operator."""
3191 return self.cterm.hasOp()
3195 .. note:: This is safe to call when :py:meth:`hasOp()` returns True.
3197 :return: the :py:class:`cvc5.Op` used to create this Term.
3199 cdef Op op = Op(self.solver)
3200 op.cop = self.cterm.getOp()
3203 def hasSymbol(self):
3204 """:return: True iff this term has a symbol."""
3205 return self.cterm.hasSymbol()
3207 def getSymbol(self):
3209 Asserts :py:meth:`hasSymbol()`.
3211 :return: the raw symbol of the term.
3213 return self.cterm.getSymbol().decode()
3216 """:return: True iff this term is a null term."""
3217 return self.cterm.isNull()
3223 :return: the Boolean negation of this term.
3225 cdef Term term = Term(self.solver)
3226 term.cterm = self.cterm.notTerm()
3229 def andTerm(self, Term t):
3233 :param t: a Boolean term
3234 :return: the conjunction of this term and the given term
3236 cdef Term term = Term(self.solver)
3237 term.cterm = self.cterm.andTerm((<Term> t).cterm)
3240 def orTerm(self, Term t):
3244 :param t: a Boolean term
3245 :return: the disjunction of this term and the given term
3247 cdef Term term = Term(self.solver)
3248 term.cterm = self.cterm.orTerm(t.cterm)
3251 def xorTerm(self, Term t):
3253 Boolean exclusive or.
3255 :param t: a Boolean term
3256 :return: the exclusive disjunction of this term and the given term
3258 cdef Term term = Term(self.solver)
3259 term.cterm = self.cterm.xorTerm(t.cterm)
3262 def eqTerm(self, Term t):
3266 :param t: a Boolean term
3267 :return: the Boolean equivalence of this term and the given term
3269 cdef Term term = Term(self.solver)
3270 term.cterm = self.cterm.eqTerm(t.cterm)
3273 def impTerm(self, Term t):
3275 Boolean Implication.
3277 :param t: a Boolean term
3278 :return: the implication of this term and the given term
3280 cdef Term term = Term(self.solver)
3281 term.cterm = self.cterm.impTerm(t.cterm)
3284 def iteTerm(self, Term then_t, Term else_t):
3286 If-then-else with this term as the Boolean condition.
3288 :param then_t: the `then` term
3289 :param else_t: the `else` term
3290 :return: the if-then-else term with this term as the Boolean condition
3292 cdef Term term = Term(self.solver)
3293 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
3296 def isConstArray(self):
3297 """:return: True iff this term is a constant array."""
3298 return self.cterm.isConstArray()
3300 def getConstArrayBase(self):
3302 Asserts :py:meth:`isConstArray()`.
3304 :return: the base (element stored at all indicies) of this constant array
3306 cdef Term term = Term(self.solver)
3307 term.cterm = self.cterm.getConstArrayBase()
3310 def isBooleanValue(self):
3311 """:return: True iff this term is a Boolean value."""
3312 return self.cterm.isBooleanValue()
3314 def getBooleanValue(self):
3316 Asserts :py:meth:`isBooleanValue()`
3318 :return: the representation of a Boolean value as a native Boolean value.
3320 return self.cterm.getBooleanValue()
3322 def isStringValue(self):
3323 """:return: True iff this term is a string value."""
3324 return self.cterm.isStringValue()
3326 def getStringValue(self):
3328 Asserts :py:meth:`isStringValue()`.
3331 This method is not to be confused with :py:meth:`__str__()` which
3332 returns the term in some string representation, whatever data it
3335 :return: the string term as a native string value.
3337 cdef Py_ssize_t size
3338 cdef c_wstring s = self.cterm.getStringValue()
3339 return PyUnicode_FromWideChar(s.data(), s.size())
3341 def getRealOrIntegerValueSign(self):
3343 Get integer or real value sign. Must be called on integer or real values,
3344 or otherwise an exception is thrown.
3346 :return: 0 if this term is zero, -1 if this term is a negative real or
3347 integer value, 1 if this term is a positive real or integer
3350 return self.cterm.getRealOrIntegerValueSign()
3352 def isIntegerValue(self):
3353 """:return: True iff this term is an integer value."""
3354 return self.cterm.isIntegerValue()
3356 def getIntegerValue(self):
3358 Asserts :py:meth:`isIntegerValue()`.
3360 :return: the integer term as a native python integer.
3362 return int(self.cterm.getIntegerValue().decode())
3364 def isFloatingPointPosZero(self):
3365 """:return: True iff the term is the floating-point value for positive zero."""
3366 return self.cterm.isFloatingPointPosZero()
3368 def isFloatingPointNegZero(self):
3369 """:return: True iff the term is the floating-point value for negative zero."""
3370 return self.cterm.isFloatingPointNegZero()
3372 def isFloatingPointPosInf(self):
3373 """:return: True iff the term is the floating-point value for positive infinity."""
3374 return self.cterm.isFloatingPointPosInf()
3376 def isFloatingPointNegInf(self):
3377 """:return: True iff the term is the floating-point value for negative infinity."""
3378 return self.cterm.isFloatingPointNegInf()
3380 def isFloatingPointNaN(self):
3381 """:return: True iff the term is the floating-point value for not a number."""
3382 return self.cterm.isFloatingPointNaN()
3384 def isFloatingPointValue(self):
3385 """:return: True iff this term is a floating-point value."""
3386 return self.cterm.isFloatingPointValue()
3388 def getFloatingPointValue(self):
3390 Asserts :py:meth:`isFloatingPointValue()`.
3392 :return: the representation of a floating-point value as a tuple of the exponent width, the significand width and a bit-vector value.
3394 cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
3395 cdef Term term = Term(self.solver)
3396 term.cterm = get2(t)
3397 return (get0(t), get1(t), term)
3399 def isSetValue(self):
3401 A term is a set value if it is considered to be a (canonical) constant
3402 set value. A canonical set value is one whose AST is:
3407 (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
3409 where ``c1 ... cn`` are values ordered by id such that
3410 ``c1 > ... > cn`` (see also :cpp:func:`cvc5::api::Term::operator>()`).
3413 A universe set term ``(kind SET_UNIVERSE)`` is not considered to be
3416 :return: True if the term is a set value.
3418 return self.cterm.isSetValue()
3420 def getSetValue(self):
3422 Asserts :py:meth:`isSetValue()`.
3424 :return: the representation of a set value as a set of terms.
3427 for e in self.cterm.getSetValue():
3428 term = Term(self.solver)
3433 def isSequenceValue(self):
3434 """:return: True iff this term is a sequence value."""
3435 return self.cterm.isSequenceValue()
3437 def getSequenceValue(self):
3439 Asserts :py:meth:`isSequenceValue()`.
3442 It is usually necessary for sequences to call
3443 :py:meth:`Solver.simplify()` to turn a sequence that is constructed
3444 by, e.g., concatenation of unit sequences, into a sequence value.
3446 :return: the representation of a sequence value as a vector of terms.
3449 for e in self.cterm.getSequenceValue():
3450 term = Term(self.solver)
3455 def isUninterpretedSortValue(self):
3456 """:return: True iff this term is a value from an uninterpreted sort."""
3457 return self.cterm.isUninterpretedSortValue()
3459 def getUninterpretedSortValue(self):
3461 Asserts :py:meth:`isUninterpretedSortValue()`.
3463 :return: the representation of an uninterpreted value as a pair of its sort and its index.
3465 return self.cterm.getUninterpretedSortValue()
3467 def isTupleValue(self):
3468 """:return: True iff this term is a tuple value."""
3469 return self.cterm.isTupleValue()
3471 def getTupleValue(self):
3473 Asserts :py:meth:`isTupleValue()`.
3475 :return: the representation of a tuple value as a vector of terms.
3478 for e in self.cterm.getTupleValue():
3479 term = Term(self.solver)
3484 def isRealValue(self):
3486 .. note:: A term of kind PI is not considered to be a real value.
3488 :return: True iff this term is a rational value.
3490 return self.cterm.isRealValue()
3492 def getRealValue(self):
3494 Asserts :py:meth:`isRealValue()`.
3496 :return: the representation of a rational value as a python Fraction.
3498 return Fraction(self.cterm.getRealValue().decode())
3500 def isBitVectorValue(self):
3501 """:return: True iff this term is a bit-vector value."""
3502 return self.cterm.isBitVectorValue()
3504 def getBitVectorValue(self, base = 2):
3506 Asserts :py:meth:`isBitVectorValue()`.
3507 Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexdecimal string).
3509 :return: the representation of a bit-vector value in string representation.
3511 return self.cterm.getBitVectorValue(base).decode()
3513 def toPythonObj(self):
3515 Converts a constant value Term to a Python object.
3519 - Boolean -- returns a Python bool
3520 - Int -- returns a Python int
3521 - Real -- returns a Python Fraction
3522 - BV -- returns a Python int (treats BV as unsigned)
3523 - String -- returns a Python Unicode string
3524 - Array -- returns a Python dict mapping indices to values. the constant base is returned as the default value
3528 if self.isBooleanValue():
3529 return self.getBooleanValue()
3530 elif self.isIntegerValue():
3531 return self.getIntegerValue()
3532 elif self.isRealValue():
3533 return self.getRealValue()
3534 elif self.isBitVectorValue():
3535 return int(self.getBitVectorValue(), 2)
3536 elif self.isStringValue():
3537 return self.getStringValue()
3538 elif self.getSort().isArray():
3544 # Array models are represented as a series of store operations
3545 # on a constant array
3548 if t.getKind().value == c_Kind.STORE:
3550 keys.append(t[1].toPythonObj())
3551 values.append(t[2].toPythonObj())
3552 to_visit.append(t[0])
3554 assert t.getKind().value == c_Kind.CONST_ARRAY
3555 base_value = t.getConstArrayBase().toPythonObj()
3557 assert len(keys) == len(values)
3558 assert base_value is not None
3560 # put everything in a dictionary with the constant
3561 # base as the result for any index not included in the stores
3562 res = defaultdict(lambda : base_value)
3563 for k, v in zip(keys, values):
3569 # Generate rounding modes
3570 cdef __rounding_modes = {
3571 <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
3572 <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
3573 <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
3574 <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
3575 <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway"
3578 mod_ref = sys.modules[__name__]
3579 for rm_int, name in __rounding_modes.items():
3580 r = RoundingMode(rm_int)
3582 if name in dir(mod_ref):
3583 raise RuntimeError("Redefinition of Python RoundingMode %s."%name)
3585 setattr(mod_ref, name, r)
3592 # Generate unknown explanations
3593 cdef __unknown_explanations = {
3594 <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
3595 <int> INCOMPLETE: "Incomplete",
3596 <int> TIMEOUT: "Timeout",
3597 <int> RESOURCEOUT: "Resourceout",
3598 <int> MEMOUT: "Memout",
3599 <int> INTERRUPTED: "Interrupted",
3600 <int> NO_STATUS: "NoStatus",
3601 <int> UNSUPPORTED: "Unsupported",
3602 <int> OTHER: "Other",
3603 <int> UNKNOWN_REASON: "UnknownReason"
3606 for ue_int, name in __unknown_explanations.items():
3607 u = UnknownExplanation(ue_int)
3609 if name in dir(mod_ref):
3610 raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
3612 setattr(mod_ref, name, u)