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, Kind k)``
1067 - ``Op mkOp(Kind kind, const string& arg)``
1068 - ``Op mkOp(Kind kind, uint32_t arg)``
1069 - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
1070 - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind)
1072 cdef Op op = Op(self)
1073 cdef vector[uint32_t] v
1076 op.cop = self.csolver.mkOp(<c_Kind> k.value)
1077 elif len(args) == 1:
1078 if isinstance(args[0], str):
1079 op.cop = self.csolver.mkOp(<c_Kind> k.value,
1082 elif isinstance(args[0], int):
1083 op.cop = self.csolver.mkOp(<c_Kind> k.value, <int?> args[0])
1084 elif isinstance(args[0], list):
1086 if a < 0 or a >= 2 ** 31:
1087 raise ValueError("Argument {} must fit in a uint32_t".format(a))
1089 v.push_back((<uint32_t?> a))
1090 op.cop = self.csolver.mkOp(<c_Kind> k.value, <const vector[uint32_t]&> v)
1092 raise ValueError("Unsupported signature"
1093 " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
1094 elif len(args) == 2:
1095 if isinstance(args[0], int) and isinstance(args[1], int):
1096 op.cop = self.csolver.mkOp(<c_Kind> k.value, <int> args[0], <int> args[1])
1098 raise ValueError("Unsupported signature"
1099 " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
1103 """Create a Boolean true constant.
1105 :return: the true constant
1107 cdef Term term = Term(self)
1108 term.cterm = self.csolver.mkTrue()
1112 """Create a Boolean false constant.
1114 :return: the false constant
1116 cdef Term term = Term(self)
1117 term.cterm = self.csolver.mkFalse()
1120 def mkBoolean(self, bint val):
1121 """Create a Boolean constant.
1123 :return: the Boolean constant
1124 :param val: the value of the constant
1126 cdef Term term = Term(self)
1127 term.cterm = self.csolver.mkBoolean(val)
1131 """Create a constant representing the number Pi.
1133 :return: a constant representing Pi
1135 cdef Term term = Term(self)
1136 term.cterm = self.csolver.mkPi()
1139 def mkInteger(self, val):
1140 """Create an integer constant.
1142 :param val: representation of the constant: either a string or integer
1143 :return: a constant of sort Integer
1145 cdef Term term = Term(self)
1146 if isinstance(val, str):
1147 term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
1149 assert(isinstance(val, int))
1150 term.cterm = self.csolver.mkInteger((<int?> val))
1153 def mkReal(self, val, den=None):
1154 """Create a real constant.
1156 :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.
1157 :param den: if not None, the value is `val`/`den`
1158 :return: a real term with literal value
1160 Can be used in various forms:
1162 - Given a string ``"N/D"`` constructs the corresponding rational.
1163 - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
1164 - 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``.
1165 - Given a string ``"W"`` or an integer, constructs that integer.
1166 - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``.
1168 cdef Term term = Term(self)
1170 term.cterm = self.csolver.mkReal(str(val).encode())
1172 if not isinstance(val, int) or not isinstance(den, int):
1173 raise ValueError("Expecting integers when"
1174 " constructing a rational"
1175 " but got: {}".format((val, den)))
1176 term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
1179 def mkRegexpAll(self):
1180 """Create a regular expression all (re.all) term.
1182 :return: the all term
1184 cdef Term term = Term(self)
1185 term.cterm = self.csolver.mkRegexpAll()
1188 def mkRegexpAllchar(self):
1189 """Create a regular expression allchar (re.allchar) term.
1191 :return: the allchar term
1193 cdef Term term = Term(self)
1194 term.cterm = self.csolver.mkRegexpAllchar()
1197 def mkRegexpNone(self):
1198 """Create a regular expression none (re.none) term.
1200 :return: the none term
1202 cdef Term term = Term(self)
1203 term.cterm = self.csolver.mkRegexpNone()
1206 def mkEmptySet(self, Sort s):
1207 """Create a constant representing an empty set of the given sort.
1209 :param sort: the sort of the set elements.
1210 :return: the empty set constant
1212 cdef Term term = Term(self)
1213 term.cterm = self.csolver.mkEmptySet(s.csort)
1216 def mkEmptyBag(self, Sort s):
1217 """Create a constant representing an empty bag of the given sort.
1219 :param sort: the sort of the bag elements.
1220 :return: the empty bag constant
1222 cdef Term term = Term(self)
1223 term.cterm = self.csolver.mkEmptyBag(s.csort)
1227 """Create a separation logic empty term.
1229 :return: the separation logic empty term
1231 cdef Term term = Term(self)
1232 term.cterm = self.csolver.mkSepEmp()
1235 def mkSepNil(self, Sort sort):
1236 """Create a separation logic nil term.
1238 :param sort: the sort of the nil term
1239 :return: the separation logic nil term
1241 cdef Term term = Term(self)
1242 term.cterm = self.csolver.mkSepNil(sort.csort)
1245 def mkString(self, str s, useEscSequences = None):
1247 Create a String constant from a `str` which may contain SMT-LIB
1248 compatible escape sequences like ``\\u1234`` to encode unicode characters.
1250 :param s: the string this constant represents
1251 :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character
1252 :return: the String constant
1254 cdef Term term = Term(self)
1255 cdef Py_ssize_t size
1256 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1257 if isinstance(useEscSequences, bool):
1258 term.cterm = self.csolver.mkString(
1259 s.encode(), <bint> useEscSequences)
1261 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1265 def mkEmptySequence(self, Sort sort):
1266 """Create an empty sequence of the given element sort.
1268 :param sort: The element sort of the sequence.
1269 :return: the empty sequence with given element sort.
1271 cdef Term term = Term(self)
1272 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1275 def mkUniverseSet(self, Sort sort):
1276 """Create a universe set of the given sort.
1278 :param sort: the sort of the set elements
1279 :return: the universe set constant
1281 cdef Term term = Term(self)
1282 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1285 @expand_list_arg(num_req_args=0)
1286 def mkBitVector(self, *args):
1288 Supports the following arguments:
1290 - ``Term mkBitVector(int size, int val=0)``
1291 - ``Term mkBitVector(int size, string val, int base)``
1293 :return: a bit-vector literal term
1294 :param size: an integer size.
1295 :param val: an integer representating the value, in the first form. In the second form, a string representing the value.
1296 :param base: the base of the string representation (second form only)
1298 cdef Term term = Term(self)
1300 raise ValueError("Missing arguments to mkBitVector")
1302 if not isinstance(size, int):
1304 "Invalid first argument to mkBitVector '{}', "
1305 "expected bit-vector size".format(size))
1307 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1308 elif len(args) == 2:
1310 if not isinstance(val, int):
1312 "Invalid second argument to mkBitVector '{}', "
1313 "expected integer value".format(size))
1314 term.cterm = self.csolver.mkBitVector(
1315 <uint32_t> size, <uint32_t> val)
1316 elif len(args) == 3:
1319 if not isinstance(val, str):
1321 "Invalid second argument to mkBitVector '{}', "
1322 "expected value string".format(size))
1323 if not isinstance(base, int):
1325 "Invalid third argument to mkBitVector '{}', "
1326 "expected base given as integer".format(size))
1327 term.cterm = self.csolver.mkBitVector(
1329 <const string&> str(val).encode(),
1332 raise ValueError("Unexpected inputs to mkBitVector")
1335 def mkConstArray(self, Sort sort, Term val):
1337 Create a constant array with the provided constant value stored at every
1340 :param sort: the sort of the constant array (must be an array sort)
1341 :param val: the constant value to store (must match the sort's element sort)
1342 :return: the constant array term
1344 cdef Term term = Term(self)
1345 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1348 def mkFloatingPointPosInf(self, int exp, int sig):
1349 """Create a positive infinity floating-point constant.
1351 :param exp: Number of bits in the exponent
1352 :param sig: Number of bits in the significand
1353 :return: the floating-point constant
1355 cdef Term term = Term(self)
1356 term.cterm = self.csolver.mkFloatingPointPosInf(exp, sig)
1359 def mkFloatingPointNegInf(self, int exp, int sig):
1360 """Create a negative infinity floating-point constant.
1362 :param exp: Number of bits in the exponent
1363 :param sig: Number of bits in the significand
1364 :return: the floating-point constant
1366 cdef Term term = Term(self)
1367 term.cterm = self.csolver.mkFloatingPointNegInf(exp, sig)
1370 def mkFloatingPointNaN(self, int exp, int sig):
1371 """Create a not-a-number (NaN) floating-point constant.
1373 :param exp: Number of bits in the exponent
1374 :param sig: Number of bits in the significand
1375 :return: the floating-point constant
1377 cdef Term term = Term(self)
1378 term.cterm = self.csolver.mkFloatingPointNaN(exp, sig)
1381 def mkFloatingPointPosZero(self, int exp, int sig):
1382 """Create a positive zero (+0.0) floating-point constant.
1384 :param exp: Number of bits in the exponent
1385 :param sig: Number of bits in the significand
1386 :return: the floating-point constant
1388 cdef Term term = Term(self)
1389 term.cterm = self.csolver.mkFloatingPointPosZero(exp, sig)
1392 def mkFloatingPointNegZero(self, int exp, int sig):
1393 """Create a negative zero (+0.0) floating-point constant.
1395 :param exp: Number of bits in the exponent
1396 :param sig: Number of bits in the significand
1397 :return: the floating-point constant
1399 cdef Term term = Term(self)
1400 term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig)
1403 def mkRoundingMode(self, RoundingMode rm):
1404 """Create a roundingmode constant.
1406 :param rm: the floating point rounding mode this constant represents
1408 cdef Term term = Term(self)
1409 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
1412 def mkFloatingPoint(self, int exp, int sig, Term val):
1413 """Create a floating-point constant.
1415 :param exp: Size of the exponent
1416 :param sig: Size of the significand
1417 :param val: Value of the floating-point constant as a bit-vector term
1419 cdef Term term = Term(self)
1420 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1423 def mkCardinalityConstraint(self, Sort sort, int index):
1424 """Create cardinality constraint.
1426 :param sort: Sort of the constraint
1427 :param index: The upper bound for the cardinality of the sort
1429 cdef Term term = Term(self)
1430 term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
1433 def mkConst(self, Sort sort, symbol=None):
1435 Create (first-order) constant (0-arity function symbol).
1439 .. code-block:: smtlib
1441 ( declare-const <symbol> <sort> )
1442 ( declare-fun <symbol> ( ) <sort> )
1444 :param sort: the sort of the constant
1445 :param symbol: the name of the constant. If None, a default symbol is used.
1446 :return: the first-order constant
1448 cdef Term term = Term(self)
1450 term.cterm = self.csolver.mkConst(sort.csort)
1452 term.cterm = self.csolver.mkConst(sort.csort,
1453 (<str?> symbol).encode())
1456 def mkVar(self, Sort sort, symbol=None):
1458 Create a bound variable to be used in a binder (i.e. a quantifier, a
1459 lambda, or a witness binder).
1461 :param sort: the sort of the variable
1462 :param symbol: the name of the variable
1463 :return: the variable
1465 cdef Term term = Term(self)
1467 term.cterm = self.csolver.mkVar(sort.csort)
1469 term.cterm = self.csolver.mkVar(sort.csort,
1470 (<str?> symbol).encode())
1473 def mkDatatypeConstructorDecl(self, str name):
1475 :return: a datatype constructor declaration
1476 :param name: the constructor's name
1478 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1479 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1482 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1483 """Create a datatype declaration.
1485 :param name: the name of the datatype
1486 :param isCoDatatype: true if a codatatype is to be constructed
1487 :return: the DatatypeDecl
1489 cdef DatatypeDecl dd = DatatypeDecl(self)
1490 cdef vector[c_Sort] v
1493 if sorts_or_bool is None and isCoDatatype is None:
1494 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1495 elif sorts_or_bool is not None and isCoDatatype is None:
1496 if isinstance(sorts_or_bool, bool):
1497 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1498 <bint> sorts_or_bool)
1499 elif isinstance(sorts_or_bool, Sort):
1500 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1501 (<Sort> sorts_or_bool).csort)
1502 elif isinstance(sorts_or_bool, list):
1503 for s in sorts_or_bool:
1504 v.push_back((<Sort?> s).csort)
1505 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1506 <const vector[c_Sort]&> v)
1508 raise ValueError("Unhandled second argument type {}"
1509 .format(type(sorts_or_bool)))
1510 elif sorts_or_bool is not None and isCoDatatype is not None:
1511 if isinstance(sorts_or_bool, Sort):
1512 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1513 (<Sort> sorts_or_bool).csort,
1514 <bint> isCoDatatype)
1515 elif isinstance(sorts_or_bool, list):
1516 for s in sorts_or_bool:
1517 v.push_back((<Sort?> s).csort)
1518 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1519 <const vector[c_Sort]&> v,
1520 <bint> isCoDatatype)
1522 raise ValueError("Unhandled second argument type {}"
1523 .format(type(sorts_or_bool)))
1525 raise ValueError("Can't create DatatypeDecl with {}".format([type(a)
1532 def simplify(self, Term t):
1534 Simplify a formula without doing "much" work. Does not involve the
1535 SAT Engine in the simplification, but uses the current definitions,
1536 assertions, and the current partial model, if one has been constructed.
1537 It also involves theory normalization.
1539 :param t: the formula to simplify
1540 :return: the simplified formula
1542 cdef Term term = Term(self)
1543 term.cterm = self.csolver.simplify(t.cterm)
1546 def assertFormula(self, Term term):
1547 """ Assert a formula
1551 .. code-block:: smtlib
1555 :param term: the formula to assert
1557 self.csolver.assertFormula(term.cterm)
1561 Check satisfiability.
1565 .. code-block:: smtlib
1569 :return: the result of the satisfiability check.
1571 cdef Result r = Result()
1572 r.cr = self.csolver.checkSat()
1575 def mkSygusGrammar(self, boundVars, ntSymbols):
1577 Create a SyGuS grammar. The first non-terminal is treated as the
1578 starting non-terminal, so the order of non-terminals matters.
1580 :param boundVars: the parameters to corresponding synth-fun/synth-inv
1581 :param ntSymbols: the pre-declaration of the non-terminal symbols
1582 :return: the grammar
1584 cdef Grammar grammar = Grammar(self)
1585 cdef vector[c_Term] bvc
1586 cdef vector[c_Term] ntc
1587 for bv in boundVars:
1588 bvc.push_back((<Term?> bv).cterm)
1589 for nt in ntSymbols:
1590 ntc.push_back((<Term?> nt).cterm)
1591 grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1594 def declareSygusVar(self, Sort sort, str symbol=""):
1595 """Append symbol to the current list of universal variables.
1599 .. code-block:: smtlib
1601 ( declare-var <symbol> <sort> )
1603 :param sort: the sort of the universal variable
1604 :param symbol: the name of the universal variable
1605 :return: the universal variable
1607 cdef Term term = Term(self)
1608 term.cterm = self.csolver.declareSygusVar(sort.csort, symbol.encode())
1611 def addSygusConstraint(self, Term t):
1613 Add a formula to the set of SyGuS constraints.
1617 .. code-block:: smtlib
1619 ( constraint <term> )
1621 :param term: the formula to add as a constraint
1623 self.csolver.addSygusConstraint(t.cterm)
1625 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1627 Add a set of SyGuS constraints to the current state that correspond to an
1628 invariant synthesis problem.
1632 .. code-block:: smtlib
1634 ( inv-constraint <inv> <pre> <trans> <post> )
1636 :param inv: the function-to-synthesize
1637 :param pre: the pre-condition
1638 :param trans: the transition relation
1639 :param post: the post-condition
1641 self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1643 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1645 Synthesize n-ary function following specified syntactic constraints.
1649 .. code-block:: smtlib
1651 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1653 :param symbol: the name of the function
1654 :param boundVars: the parameters to this function
1655 :param sort: the sort of the return value of this function
1656 :param grammar: the syntactic constraints
1657 :return: the function
1659 cdef Term term = Term(self)
1660 cdef vector[c_Term] v
1661 for bv in bound_vars:
1662 v.push_back((<Term?> bv).cterm)
1664 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1666 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1669 def checkSynth(self):
1671 Try to find a solution for the synthesis conjecture corresponding to the
1672 current list of functions-to-synthesize, universal variables and
1677 .. code-block:: smtlib
1681 :return: the result of the check, which is "solution" if the check
1682 found a solution in which case solutions are available via
1683 getSynthSolutions, "no solution" if it was determined there is
1684 no solution, or "unknown" otherwise.
1686 cdef SynthResult r = SynthResult()
1687 r.cr = self.csolver.checkSynth()
1690 def checkSynthNext(self):
1692 Try to find a next solution for the synthesis conjecture corresponding
1693 to the current list of functions-to-synthesize, universal variables and
1694 constraints. Must be called immediately after a successful call to
1695 check-synth or check-synth-next. Requires incremental mode.
1699 .. code-block:: smtlib
1703 :return: the result of the check, which is "solution" if the check
1704 found a solution in which case solutions are available via
1705 getSynthSolutions, "no solution" if it was determined there is
1706 no solution, or "unknown" otherwise.
1708 cdef SynthResult r = SynthResult()
1709 r.cr = self.csolver.checkSynthNext()
1712 def getSynthSolution(self, Term term):
1714 Get the synthesis solution of the given term. This method should be
1715 called immediately after the solver answers unsat for sygus input.
1717 :param term: the term for which the synthesis solution is queried
1718 :return: the synthesis solution of the given term
1720 cdef Term t = Term(self)
1721 t.cterm = self.csolver.getSynthSolution(term.cterm)
1724 def getSynthSolutions(self, list terms):
1726 Get the synthesis solutions of the given terms. This method should be
1727 called immediately after the solver answers unsat for sygus input.
1729 :param terms: the terms for which the synthesis solutions is queried
1730 :return: the synthesis solutions of the given terms
1733 cdef vector[c_Term] vec
1735 vec.push_back((<Term?> t).cterm)
1736 cresult = self.csolver.getSynthSolutions(vec)
1744 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1746 Synthesize invariant.
1750 .. code-block:: smtlib
1752 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1754 :param symbol: the name of the invariant
1755 :param boundVars: the parameters to this invariant
1756 :param grammar: the syntactic constraints
1757 :return: the invariant
1759 cdef Term term = Term(self)
1760 cdef vector[c_Term] v
1761 for bv in bound_vars:
1762 v.push_back((<Term?> bv).cterm)
1764 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
1766 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
1769 @expand_list_arg(num_req_args=0)
1770 def checkSatAssuming(self, *assumptions):
1771 """ Check satisfiability assuming the given formula.
1775 .. code-block:: smtlib
1777 ( check-sat-assuming ( <prop_literal> ) )
1779 :param assumptions: the formulas to assume, as a list or as distinct arguments
1780 :return: the result of the satisfiability check.
1782 cdef Result r = Result()
1783 # used if assumptions is a list of terms
1784 cdef vector[c_Term] v
1785 for a in assumptions:
1786 v.push_back((<Term?> a).cterm)
1787 r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
1790 @expand_list_arg(num_req_args=1)
1791 def declareDatatype(self, str symbol, *ctors):
1793 Create datatype sort.
1797 .. code-block:: smtlib
1799 ( declare-datatype <symbol> <datatype_decl> )
1801 :param symbol: the name of the datatype sort
1802 :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
1803 :return: the datatype sort
1805 cdef Sort sort = Sort(self)
1806 cdef vector[c_DatatypeConstructorDecl] v
1809 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1810 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1813 def declareFun(self, str symbol, list sorts, Sort sort):
1814 """Declare n-ary function symbol.
1818 .. code-block:: smtlib
1820 ( declare-fun <symbol> ( <sort>* ) <sort> )
1822 :param symbol: the name of the function
1823 :param sorts: the sorts of the parameters to this function
1824 :param sort: the sort of the return value of this function
1825 :return: the function
1827 cdef Term term = Term(self)
1828 cdef vector[c_Sort] v
1830 v.push_back((<Sort?> s).csort)
1831 term.cterm = self.csolver.declareFun(symbol.encode(),
1832 <const vector[c_Sort]&> v,
1836 def declareSort(self, str symbol, int arity):
1837 """Declare uninterpreted sort.
1841 .. code-block:: smtlib
1843 ( declare-sort <symbol> <numeral> )
1845 :param symbol: the name of the sort
1846 :param arity: the arity of the sort
1849 cdef Sort sort = Sort(self)
1850 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
1853 def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
1854 """Define n-ary function.
1858 .. code-block:: smtlib
1860 ( define-fun <function_def> )
1862 :param symbol: the name of the function
1863 :param bound_vars: the parameters to this function
1864 :param sort: the sort of the return value of this function
1865 :param term: the function body
1866 :param glbl: determines whether this definition is global (i.e. persists when popping the context)
1867 :return: the function
1869 cdef Term fun = Term(self)
1870 cdef vector[c_Term] v
1871 for bv in bound_vars:
1872 v.push_back((<Term?> bv).cterm)
1874 fun.cterm = self.csolver.defineFun(symbol.encode(),
1875 <const vector[c_Term] &> v,
1881 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1882 """Define recursive functions.
1886 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1887 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1892 .. code-block:: smtlib
1894 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1896 Create elements of parameter ``funs`` with mkConst().
1898 :param funs: the sorted functions
1899 :param bound_vars: the list of parameters to the functions
1900 :param terms: the list of function bodies of the functions
1901 :param global: determines whether this definition is global (i.e. persists when popping the context)
1902 :return: the function
1904 cdef Term term = Term(self)
1905 cdef vector[c_Term] v
1906 for bv in bound_vars:
1907 v.push_back((<Term?> bv).cterm)
1910 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
1911 <const vector[c_Term] &> v,
1912 (<Sort?> sort_or_term).csort,
1916 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
1917 <const vector[c_Term]&> v,
1918 (<Term?> sort_or_term).cterm,
1923 def defineFunsRec(self, funs, bound_vars, terms):
1924 """Define recursive functions.
1928 .. code-block:: smtlib
1930 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1932 Create elements of parameter ``funs`` with mkConst().
1934 :param funs: the sorted functions
1935 :param bound_vars: the list of parameters to the functions
1936 :param terms: the list of function bodies of the functions
1937 :param global: determines whether this definition is global (i.e. persists when popping the context)
1938 :return: the function
1940 cdef vector[c_Term] vf
1941 cdef vector[vector[c_Term]] vbv
1942 cdef vector[c_Term] vt
1945 vf.push_back((<Term?> f).cterm)
1947 cdef vector[c_Term] temp
1948 for v in bound_vars:
1950 temp.push_back((<Term?> t).cterm)
1955 vf.push_back((<Term?> t).cterm)
1958 """Get the refutation proof
1962 .. code-block:: smtlib
1966 Requires to enable option
1967 :ref:`produce-proofs <lbl-option-produce-proofs>`.
1969 :return: a string representing the proof, according to the value of
1972 return self.csolver.getProof()
1974 def getLearnedLiterals(self):
1975 """Get a list of literals that are entailed by the current set of assertions
1979 .. code-block:: smtlib
1981 ( get-learned-literals )
1983 :return: the list of literals
1986 for a in self.csolver.getLearnedLiterals():
1992 def getAssertions(self):
1993 """Get the list of asserted formulas.
1997 .. code-block:: smtlib
2001 :return: the list of asserted formulas
2004 for a in self.csolver.getAssertions():
2007 assertions.append(term)
2010 def getInfo(self, str flag):
2011 """Get info from the solver.
2015 .. code-block:: smtlib
2017 ( get-info <info_flag> )
2019 :param flag: the info flag
2022 return self.csolver.getInfo(flag.encode())
2024 def getOption(self, str option):
2025 """Get the value of a given option.
2029 .. code-block:: smtlib
2031 ( get-option <keyword> )
2033 :param option: the option for which the value is queried
2034 :return: a string representation of the option value
2036 return self.csolver.getOption(option.encode()).decode()
2038 def getOptionNames(self):
2039 """Get all option names that can be used with `setOption`, `getOption` and `getOptionInfo`.
2041 :return: all option names
2043 return [s.decode() for s in self.csolver.getOptionNames()]
2045 def getOptionInfo(self, str option):
2046 """Get some information about the given option. Check the `OptionInfo`
2047 class for more details on which information is available.
2049 :return: information about the given option
2051 # declare all the variables we may need later
2052 cdef c_OptionInfo.ValueInfo[c_bool] vib
2053 cdef c_OptionInfo.ValueInfo[string] vis
2054 cdef c_OptionInfo.NumberInfo[int64_t] nii
2055 cdef c_OptionInfo.NumberInfo[uint64_t] niu
2056 cdef c_OptionInfo.NumberInfo[double] nid
2057 cdef c_OptionInfo.ModeInfo mi
2059 oi = self.csolver.getOptionInfo(option.encode())
2060 # generic information
2062 'name': oi.name.decode(),
2063 'aliases': [s.decode() for s in oi.aliases],
2064 'setByUser': oi.setByUser,
2067 # now check which type is actually in the variant
2068 if c_holds[c_OptionInfo.VoidInfo](oi.valueInfo):
2071 elif c_holds[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo):
2074 vib = c_getVariant[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo)
2075 res['current'] = vib.currentValue
2076 res['default'] = vib.defaultValue
2077 elif c_holds[c_OptionInfo.ValueInfo[string]](oi.valueInfo):
2080 vis = c_getVariant[c_OptionInfo.ValueInfo[string]](oi.valueInfo)
2081 res['current'] = vis.currentValue.decode()
2082 res['default'] = vis.defaultValue.decode()
2083 elif c_holds[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo):
2086 nii = c_getVariant[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo)
2087 res['current'] = nii.currentValue
2088 res['default'] = nii.defaultValue
2089 res['minimum'] = nii.minimum.value() if nii.minimum.has_value() else None
2090 res['maximum'] = nii.maximum.value() if nii.maximum.has_value() else None
2091 elif c_holds[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo):
2094 niu = c_getVariant[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo)
2095 res['current'] = niu.currentValue
2096 res['default'] = niu.defaultValue
2097 res['minimum'] = niu.minimum.value() if niu.minimum.has_value() else None
2098 res['maximum'] = niu.maximum.value() if niu.maximum.has_value() else None
2099 elif c_holds[c_OptionInfo.NumberInfo[double]](oi.valueInfo):
2102 nid = c_getVariant[c_OptionInfo.NumberInfo[double]](oi.valueInfo)
2103 res['current'] = nid.currentValue
2104 res['default'] = nid.defaultValue
2105 res['minimum'] = nid.minimum.value() if nid.minimum.has_value() else None
2106 res['maximum'] = nid.maximum.value() if nid.maximum.has_value() else None
2107 elif c_holds[c_OptionInfo.ModeInfo](oi.valueInfo):
2109 res['type'] = 'mode'
2110 mi = c_getVariant[c_OptionInfo.ModeInfo](oi.valueInfo)
2111 res['current'] = mi.currentValue.decode()
2112 res['default'] = mi.defaultValue.decode()
2113 res['modes'] = [s.decode() for s in mi.modes]
2116 def getUnsatAssumptions(self):
2118 Get the set of unsat ("failed") assumptions.
2122 .. code-block:: smtlib
2124 ( get-unsat-assumptions )
2126 Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
2128 :return: the set of unsat assumptions.
2131 for a in self.csolver.getUnsatAssumptions():
2134 assumptions.append(term)
2137 def getUnsatCore(self):
2138 """Get the unsatisfiable core.
2142 .. code-block:: smtlib
2146 Requires to enable option :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
2149 In contrast to SMT-LIB, the API does not distinguish between named and
2150 unnamed assertions when producing an unsatisfiable core. Additionally,
2151 the API allows this option to be called after a check with assumptions.
2152 A subset of those assumptions may be included in the unsatisfiable core
2153 returned by this method.
2155 :return: a set of terms representing the unsatisfiable core
2158 for a in self.csolver.getUnsatCore():
2164 def getValue(self, Term t):
2165 """Get the value of the given term in the current model.
2169 .. code-block:: smtlib
2171 ( get-value ( <term> ) )
2173 :param term: the term for which the value is queried
2174 :return: the value of the given term
2176 cdef Term term = Term(self)
2177 term.cterm = self.csolver.getValue(t.cterm)
2180 def getModelDomainElements(self, Sort s):
2182 Get the domain elements of uninterpreted sort s in the current model. The
2183 current model interprets s as the finite sort whose domain elements are
2184 given in the return value of this method.
2186 :param s: The uninterpreted sort in question
2187 :return: the domain elements of s in the current model
2190 cresult = self.csolver.getModelDomainElements(s.csort)
2197 def isModelCoreSymbol(self, Term v):
2199 This returns false if the model value of free constant v was not
2200 essential for showing the satisfiability of the last call to checkSat
2201 using the current model. This method will only return false (for any v)
2202 if the model-cores option has been set.
2204 :param v: The term in question
2205 :return: true if v is a model core symbol
2207 return self.csolver.isModelCoreSymbol(v.cterm)
2209 def getModel(self, sorts, consts):
2218 Requires to enable option
2219 :ref:`produce-models <lbl-option-produce-models>`.
2221 :param sorts: The list of uninterpreted sorts that should be printed in
2223 :param vars: The list of free constants that should be printed in the
2224 model. A subset of these may be printed based on
2226 :return: a string representing the model.
2229 cdef vector[c_Sort] csorts
2231 csorts.push_back((<Sort?> sort).csort)
2233 cdef vector[c_Term] cconsts
2234 for const in consts:
2235 cconsts.push_back((<Term?> const).cterm)
2237 return self.csolver.getModel(csorts, cconsts)
2239 def getValueSepHeap(self):
2240 """When using separation logic, obtain the term for the heap.
2242 :return: The term for the heap
2244 cdef Term term = Term(self)
2245 term.cterm = self.csolver.getValueSepHeap()
2248 def getValueSepNil(self):
2249 """When using separation logic, obtain the term for nil.
2251 :return: The term for nil
2253 cdef Term term = Term(self)
2254 term.cterm = self.csolver.getValueSepNil()
2257 def declareSepHeap(self, Sort locType, Sort dataType):
2259 When using separation logic, this sets the location sort and the
2260 datatype sort to the given ones. This method should be invoked exactly
2261 once, before any separation logic constraints are provided.
2263 :param locSort: The location sort of the heap
2264 :param dataSort: The data sort of the heap
2266 self.csolver.declareSepHeap(locType.csort, dataType.csort)
2268 def declarePool(self, str symbol, Sort sort, initValue):
2269 """Declare a symbolic pool of terms with the given initial value.
2273 .. code-block:: smtlib
2275 ( declare-pool <symbol> <sort> ( <term>* ) )
2277 :param symbol: The name of the pool
2278 :param sort: The sort of the elements of the pool.
2279 :param initValue: The initial value of the pool
2281 cdef Term term = Term(self)
2282 cdef vector[c_Term] niv
2284 niv.push_back((<Term?> v).cterm)
2285 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
2288 def pop(self, nscopes=1):
2289 """Pop ``nscopes`` level(s) from the assertion stack.
2293 .. code-block:: smtlib
2297 :param nscopes: the number of levels to pop
2299 self.csolver.pop(nscopes)
2301 def push(self, nscopes=1):
2302 """ Push ``nscopes`` level(s) to the assertion stack.
2306 .. code-block:: smtlib
2310 :param nscopes: the number of levels to push
2312 self.csolver.push(nscopes)
2314 def resetAssertions(self):
2316 Remove all assertions.
2320 .. code-block:: smtlib
2322 ( reset-assertions )
2325 self.csolver.resetAssertions()
2327 def setInfo(self, str keyword, str value):
2332 .. code-block:: smtlib
2334 ( set-info <attribute> )
2336 :param keyword: the info flag
2337 :param value: the value of the info flag
2339 self.csolver.setInfo(keyword.encode(), value.encode())
2341 def setLogic(self, str logic):
2346 .. code-block:: smtlib
2348 ( set-logic <symbol> )
2350 :param logic: the logic to set
2352 self.csolver.setLogic(logic.encode())
2354 def setOption(self, str option, str value):
2359 .. code-block:: smtlib
2361 ( set-option <option> )
2363 :param option: the option name
2364 :param value: the option value
2366 self.csolver.setOption(option.encode(), value.encode())
2369 def getInterpolant(self, Term conj, *args):
2370 """Get an interpolant.
2374 .. code-block:: smtlib
2376 ( get-interpol <conj> )
2377 ( get-interpol <conj> <grammar> )
2379 Requires option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
2381 Supports the following variants:
2383 - ``Term getInteprolant(Term conj)``
2384 - ``Term getInteprolant(Term conj, Grammar grammar)``
2386 :param conj: the conjecture term
2387 :param output: the term where the result will be stored
2388 :param grammar: a grammar for the inteprolant
2389 :return: True iff an interpolant was found
2391 cdef Term result = Term(self)
2393 result.cterm = self.csolver.getInterpolant(conj.cterm)
2395 assert len(args) == 1
2396 assert isinstance(args[0], Grammar)
2397 result.cterm = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> args[0]).cgrammar)
2401 def getInterpolantNext(self):
2403 Get the next interpolant. Can only be called immediately after
2404 a succesful call to get-interpol or get-interpol-next.
2405 Is guaranteed to produce a syntactically different interpolant wrt the
2406 last returned interpolant if successful.
2410 .. code-block:: smtlib
2412 ( get-interpol-next )
2414 Requires to enable incremental mode, and
2415 option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
2417 :param output: the term where the result will be stored
2418 :return: True iff an interpolant was found
2420 cdef Term result = Term(self)
2421 result.cterm = self.csolver.getInterpolantNext()
2424 def getAbduct(self, Term conj, *args):
2429 .. code-block:: smtlib
2431 ( get-abduct <conj> )
2432 ( get-abduct <conj> <grammar> )
2434 Requires to enable option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2436 Supports the following variants:
2438 - ``Term getAbduct(Term conj)``
2439 - ``Term getAbduct(Term conj, Grammar grammar)``
2441 :param conj: the conjecture term
2442 :param output: the term where the result will be stored
2443 :param grammar: a grammar for the abduct
2444 :return: True iff an abduct was found
2446 cdef Term result = Term(self)
2448 result.cterm = self.csolver.getAbduct(conj.cterm)
2450 assert len(args) == 1
2451 assert isinstance(args[0], Grammar)
2452 result.cterm = self.csolver.getAbduct(conj.cterm, (<Grammar ?> args[0]).cgrammar)
2455 def getAbductNext(self):
2457 Get the next abduct. Can only be called immediately after
2458 a succesful call to get-abduct or get-abduct-next.
2459 Is guaranteed to produce a syntactically different abduct wrt the
2460 last returned abduct if successful.
2464 .. code-block:: smtlib
2468 Requires to enable incremental mode, and
2469 option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2470 :param output: the term where the result will be stored
2471 :return: True iff an abduct was found
2473 cdef Term result = Term(self)
2474 result.cterm = self.csolver.getAbductNext()
2477 def blockModel(self):
2479 Block the current model. Can be called only if immediately preceded by a
2480 SAT or INVALID query.
2484 .. code-block:: smtlib
2488 Requires enabling option
2489 :ref:`produce-models <lbl-option-produce-models>`
2491 :ref:`block-models <lbl-option-block-models>`
2492 to a mode other than ``none``.
2494 self.csolver.blockModel()
2496 def blockModelValues(self, terms):
2498 Block the current model values of (at least) the values in terms. Can be
2499 called only if immediately preceded by a SAT or NOT_ENTAILED query.
2503 .. code-block:: smtlib
2505 (block-model-values ( <terms>+ ))
2507 Requires enabling option
2508 :ref:`produce-models <lbl-option-produce-models>`.
2510 cdef vector[c_Term] nts
2512 nts.push_back((<Term?> t).cterm)
2513 self.csolver.blockModelValues(nts)
2515 def getInstantiations(self):
2517 Return a string that contains information about all instantiations made
2518 by the quantifiers module.
2520 return self.csolver.getInstantiations()
2522 def getStatistics(self):
2524 Returns a snapshot of the current state of the statistic values of this
2525 solver. The returned object is completely decoupled from the solver and
2526 will not change when the solver is used again.
2529 res.cstats = self.csolver.getStatistics()
2535 The sort of a cvc5 term.
2539 def __cinit__(self, Solver solver):
2540 # csort always set by Solver
2541 self.solver = solver
2543 def __eq__(self, Sort other):
2544 return self.csort == other.csort
2546 def __ne__(self, Sort other):
2547 return self.csort != other.csort
2549 def __lt__(self, Sort other):
2550 return self.csort < other.csort
2552 def __gt__(self, Sort other):
2553 return self.csort > other.csort
2555 def __le__(self, Sort other):
2556 return self.csort <= other.csort
2558 def __ge__(self, Sort other):
2559 return self.csort >= other.csort
2562 return self.csort.toString().decode()
2565 return self.csort.toString().decode()
2568 return csorthash(self.csort)
2570 def hasSymbol(self):
2571 """:return: True iff this sort has a symbol."""
2572 return self.csort.hasSymbol()
2574 def getSymbol(self):
2576 Asserts :py:meth:`hasSymbol()`.
2578 :return: the raw symbol of the sort.
2580 return self.csort.getSymbol().decode()
2583 """:return: True if this Sort is a null sort."""
2584 return self.csort.isNull()
2586 def isBoolean(self):
2588 Is this a Boolean sort?
2590 :return: True if the sort is the Boolean sort.
2592 return self.csort.isBoolean()
2594 def isInteger(self):
2596 Is this an integer sort?
2598 :return: True if the sort is the integer sort.
2600 return self.csort.isInteger()
2604 Is this a real sort?
2606 :return: True if the sort is the real sort.
2608 return self.csort.isReal()
2612 Is this a string sort?
2614 :return: True if the sort is the string sort.
2616 return self.csort.isString()
2620 Is this a regexp sort?
2622 :return: True if the sort is the regexp sort.
2624 return self.csort.isRegExp()
2626 def isRoundingMode(self):
2628 Is this a rounding mode sort?
2630 :return: True if the sort is the rounding mode sort.
2632 return self.csort.isRoundingMode()
2634 def isBitVector(self):
2636 Is this a bit-vector sort?
2638 :return: True if the sort is a bit-vector sort.
2640 return self.csort.isBitVector()
2642 def isFloatingPoint(self):
2644 Is this a floating-point sort?
2646 :return: True if the sort is a bit-vector sort.
2648 return self.csort.isFloatingPoint()
2650 def isDatatype(self):
2652 Is this a datatype sort?
2654 :return: True if the sort is a datatype sort.
2656 return self.csort.isDatatype()
2658 def isParametricDatatype(self):
2660 Is this a parametric datatype sort?
2662 :return: True if the sort is a parametric datatype sort.
2664 return self.csort.isParametricDatatype()
2666 def isConstructor(self):
2668 Is this a constructor sort?
2670 :return: True if the sort is a constructor sort.
2672 return self.csort.isConstructor()
2674 def isSelector(self):
2676 Is this a selector sort?
2678 :return: True if the sort is a selector sort.
2680 return self.csort.isSelector()
2684 Is this a tester sort?
2686 :return: True if the sort is a selector sort.
2688 return self.csort.isTester()
2690 def isUpdater(self):
2692 Is this a datatype updater sort?
2694 :return: True if the sort is a datatype updater sort.
2696 return self.csort.isUpdater()
2698 def isFunction(self):
2700 Is this a function sort?
2702 :return: True if the sort is a function sort.
2704 return self.csort.isFunction()
2706 def isPredicate(self):
2708 Is this a predicate sort?
2709 That is, is this a function sort mapping to Boolean? All predicate
2710 sorts are also function sorts.
2712 :return: True if the sort is a predicate sort.
2714 return self.csort.isPredicate()
2718 Is this a tuple sort?
2720 :return: True if the sort is a tuple sort.
2722 return self.csort.isTuple()
2726 Is this a record sort?
2728 :return: True if the sort is a record sort.
2730 return self.csort.isRecord()
2734 Is this an array sort?
2736 :return: True if the sort is an array sort.
2738 return self.csort.isArray()
2744 :return: True if the sort is a set sort.
2746 return self.csort.isSet()
2752 :return: True if the sort is a bag sort.
2754 return self.csort.isBag()
2756 def isSequence(self):
2758 Is this a sequence sort?
2760 :return: True if the sort is a sequence sort.
2762 return self.csort.isSequence()
2764 def isUninterpretedSort(self):
2766 Is this a sort uninterpreted?
2768 :return: True if the sort is uninterpreted.
2770 return self.csort.isUninterpretedSort()
2772 def isSortConstructor(self):
2774 Is this a sort constructor kind?
2776 :return: True if this a sort constructor kind.
2778 return self.csort.isSortConstructor()
2780 def getDatatype(self):
2782 :return: the underlying datatype of a datatype sort
2784 cdef Datatype d = Datatype(self.solver)
2785 d.cd = self.csort.getDatatype()
2788 def instantiate(self, params):
2790 Instantiate a parameterized datatype/sort sort.
2791 Create sorts parameter with :py:meth:`Solver.mkParamSort()`
2793 :param params: the list of sort parameters to instantiate with
2795 cdef Sort sort = Sort(self.solver)
2796 cdef vector[c_Sort] v
2798 v.push_back((<Sort?> s).csort)
2799 sort.csort = self.csort.instantiate(v)
2802 def substitute(self, sort_or_list_1, sort_or_list_2):
2804 Substitution of Sorts.
2806 :param sort_or_list_1: the subsort or subsorts to be substituted within this sort.
2807 :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort.
2809 Note that this replacement is applied during a pre-order traversal and
2810 only once to the sort. It is not run until fix point. In the case that
2811 sort_or_list_1 contains duplicates, the replacement earliest in the list
2815 ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])`` will
2816 return ``(Array (Array C D) B)``.
2819 # The resulting sort after substitution
2820 cdef Sort sort = Sort(self.solver)
2821 # lists for substitutions
2822 cdef vector[c_Sort] ces
2823 cdef vector[c_Sort] creplacements
2825 # normalize the input parameters to be lists
2826 if isinstance(sort_or_list_1, list):
2827 assert isinstance(sort_or_list_2, list)
2829 replacements = sort_or_list_2
2830 if len(es) != len(replacements):
2831 raise RuntimeError("Expecting list inputs to substitute to "
2832 "have the same length but got: "
2833 "{} and {}".format(len(es), len(replacements)))
2835 for e, r in zip(es, replacements):
2836 ces.push_back((<Sort?> e).csort)
2837 creplacements.push_back((<Sort?> r).csort)
2840 # add the single elements to the vectors
2841 ces.push_back((<Sort?> sort_or_list_1).csort)
2842 creplacements.push_back((<Sort?> sort_or_list_2).csort)
2844 # call the API substitute method with lists
2845 sort.csort = self.csort.substitute(ces, creplacements)
2849 def getConstructorArity(self):
2851 :return: the arity of a constructor sort.
2853 return self.csort.getConstructorArity()
2855 def getConstructorDomainSorts(self):
2857 :return: the domain sorts of a constructor sort
2860 for s in self.csort.getConstructorDomainSorts():
2861 sort = Sort(self.solver)
2863 domain_sorts.append(sort)
2866 def getConstructorCodomainSort(self):
2868 :return: the codomain sort of a constructor sort
2870 cdef Sort sort = Sort(self.solver)
2871 sort.csort = self.csort.getConstructorCodomainSort()
2874 def getSelectorDomainSort(self):
2876 :return: the domain sort of a selector sort
2878 cdef Sort sort = Sort(self.solver)
2879 sort.csort = self.csort.getSelectorDomainSort()
2882 def getSelectorCodomainSort(self):
2884 :return: the codomain sort of a selector sort
2886 cdef Sort sort = Sort(self.solver)
2887 sort.csort = self.csort.getSelectorCodomainSort()
2890 def getTesterDomainSort(self):
2892 :return: the domain sort of a tester sort
2894 cdef Sort sort = Sort(self.solver)
2895 sort.csort = self.csort.getTesterDomainSort()
2898 def getTesterCodomainSort(self):
2900 :return: the codomain sort of a tester sort, which is the Boolean sort
2902 cdef Sort sort = Sort(self.solver)
2903 sort.csort = self.csort.getTesterCodomainSort()
2906 def getFunctionArity(self):
2908 :return: the arity of a function sort
2910 return self.csort.getFunctionArity()
2912 def getFunctionDomainSorts(self):
2914 :return: the domain sorts of a function sort
2917 for s in self.csort.getFunctionDomainSorts():
2918 sort = Sort(self.solver)
2920 domain_sorts.append(sort)
2923 def getFunctionCodomainSort(self):
2925 :return: the codomain sort of a function sort
2927 cdef Sort sort = Sort(self.solver)
2928 sort.csort = self.csort.getFunctionCodomainSort()
2931 def getArrayIndexSort(self):
2933 :return: the array index sort of an array sort
2935 cdef Sort sort = Sort(self.solver)
2936 sort.csort = self.csort.getArrayIndexSort()
2939 def getArrayElementSort(self):
2941 :return: the array element sort of an array sort
2943 cdef Sort sort = Sort(self.solver)
2944 sort.csort = self.csort.getArrayElementSort()
2947 def getSetElementSort(self):
2949 :return: the element sort of a set sort
2951 cdef Sort sort = Sort(self.solver)
2952 sort.csort = self.csort.getSetElementSort()
2955 def getBagElementSort(self):
2957 :return: the element sort of a bag sort
2959 cdef Sort sort = Sort(self.solver)
2960 sort.csort = self.csort.getBagElementSort()
2963 def getSequenceElementSort(self):
2965 :return: the element sort of a sequence sort
2967 cdef Sort sort = Sort(self.solver)
2968 sort.csort = self.csort.getSequenceElementSort()
2971 def isUninterpretedSortParameterized(self):
2973 :return: True if an uninterpreted sort is parameterized
2975 return self.csort.isUninterpretedSortParameterized()
2977 def getUninterpretedSortParamSorts(self):
2979 :return: the parameter sorts of an uninterpreted sort
2982 for s in self.csort.getUninterpretedSortParamSorts():
2983 sort = Sort(self.solver)
2985 param_sorts.append(sort)
2988 def getSortConstructorArity(self):
2990 :return: the arity of a sort constructor sort
2992 return self.csort.getSortConstructorArity()
2994 def getBitVectorSize(self):
2996 :return: the bit-width of the bit-vector sort
2998 return self.csort.getBitVectorSize()
3000 def getFloatingPointExponentSize(self):
3002 :return: the bit-width of the exponent of the floating-point sort
3004 return self.csort.getFloatingPointExponentSize()
3006 def getFloatingPointSignificandSize(self):
3008 :return: the width of the significand of the floating-point sort
3010 return self.csort.getFloatingPointSignificandSize()
3012 def getDatatypeParamSorts(self):
3014 Return the parameters of a parametric datatype sort. If this sort
3015 is a non-instantiated parametric datatype, this returns the
3016 parameter sorts of the underlying datatype. If this sort is an
3017 instantiated parametric datatype, then this returns the sort
3018 parameters that were used to construct the sort via
3019 :py:meth:`instantiate()`.
3021 :return: the parameter sorts of a parametric datatype sort
3024 for s in self.csort.getDatatypeParamSorts():
3025 sort = Sort(self.solver)
3027 param_sorts.append(sort)
3030 def getDatatypeArity(self):
3032 :return: the arity of a datatype sort
3034 return self.csort.getDatatypeArity()
3036 def getTupleLength(self):
3038 :return: the length of a tuple sort
3040 return self.csort.getTupleLength()
3042 def getTupleSorts(self):
3044 :return: the element sorts of a tuple sort
3047 for s in self.csort.getTupleSorts():
3048 sort = Sort(self.solver)
3050 tuple_sorts.append(sort)
3054 cdef class Statistics:
3056 The cvc5 Statistics.
3057 Wrapper class for :cpp:class:`cvc5::api::Statistics`.
3058 Obtain a single statistic value using ``stats["name"]`` and a dictionary
3059 with all (visible) statistics using ``stats.get(internal=False, defaulted=False)``.
3061 cdef c_Statistics cstats
3063 cdef __stat_to_dict(self, const c_Stat& s):
3070 res = s.getString().decode()
3071 elif s.isHistogram():
3072 res = { h.first.decode(): h.second for h in s.getHistogram() }
3074 'defaulted': s.isDefault(),
3075 'internal': s.isInternal(),
3079 def __getitem__(self, str name):
3080 """Get the statistics information for the statistic called ``name``."""
3081 return self.__stat_to_dict(self.cstats.get(name.encode()))
3083 def get(self, bint internal = False, bint defaulted = False):
3084 """Get all statistics. See :cpp:class:`cvc5::api::Statistics::begin()` for more information."""
3085 cdef c_Statistics.iterator it = self.cstats.begin(internal, defaulted)
3086 cdef pair[string,c_Stat]* s
3088 while it != self.cstats.end():
3089 s = &dereference(it)
3090 res[s.first.decode()] = self.__stat_to_dict(s.second)
3098 Wrapper class for :cpp:class:`cvc5::api::Term`.
3102 def __cinit__(self, Solver solver):
3103 # cterm always set in the Solver object
3104 self.solver = solver
3106 def __eq__(self, Term other):
3107 return self.cterm == other.cterm
3109 def __ne__(self, Term other):
3110 return self.cterm != other.cterm
3112 def __lt__(self, Term other):
3113 return self.cterm < other.cterm
3115 def __gt__(self, Term other):
3116 return self.cterm > other.cterm
3118 def __le__(self, Term other):
3119 return self.cterm <= other.cterm
3121 def __ge__(self, Term other):
3122 return self.cterm >= other.cterm
3124 def __getitem__(self, int index):
3125 cdef Term term = Term(self.solver)
3127 term.cterm = self.cterm[index]
3129 raise ValueError("Expecting a non-negative integer or string")
3133 return self.cterm.toString().decode()
3136 return self.cterm.toString().decode()
3139 for ci in self.cterm:
3140 term = Term(self.solver)
3145 return ctermhash(self.cterm)
3147 def getNumChildren(self):
3148 """:return: the number of children of this term."""
3149 return self.cterm.getNumChildren()
3152 """:return: the id of this term."""
3153 return self.cterm.getId()
3156 """:return: the :py:class:`cvc5.Kind` of this term."""
3157 return Kind(<int> self.cterm.getKind())
3160 """:return: the :py:class:`cvc5.Sort` of this term."""
3161 cdef Sort sort = Sort(self.solver)
3162 sort.csort = self.cterm.getSort()
3165 def substitute(self, term_or_list_1, term_or_list_2):
3167 :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.
3169 Note that this replacement is applied during a pre-order traversal and
3170 only once to the term. It is not run until fix point. In the case that
3171 terms contains duplicates, the replacement earliest in the list takes
3172 priority. For example, calling substitute on ``f(x,y)`` with
3176 term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ]
3178 results in the term ``f(g(z),y)``.
3180 # The resulting term after substitution
3181 cdef Term term = Term(self.solver)
3182 # lists for substitutions
3183 cdef vector[c_Term] ces
3184 cdef vector[c_Term] creplacements
3186 # normalize the input parameters to be lists
3187 if isinstance(term_or_list_1, list):
3188 assert isinstance(term_or_list_2, list)
3190 replacements = term_or_list_2
3191 if len(es) != len(replacements):
3192 raise RuntimeError("Expecting list inputs to substitute to "
3193 "have the same length but got: "
3194 "{} and {}".format(len(es), len(replacements)))
3196 for e, r in zip(es, replacements):
3197 ces.push_back((<Term?> e).cterm)
3198 creplacements.push_back((<Term?> r).cterm)
3201 # add the single elements to the vectors
3202 ces.push_back((<Term?> term_or_list_1).cterm)
3203 creplacements.push_back((<Term?> term_or_list_2).cterm)
3205 # call the API substitute method with lists
3206 term.cterm = self.cterm.substitute(ces, creplacements)
3210 """:return: True iff this term has an operator."""
3211 return self.cterm.hasOp()
3215 .. note:: This is safe to call when :py:meth:`hasOp()` returns True.
3217 :return: the :py:class:`cvc5.Op` used to create this Term.
3219 cdef Op op = Op(self.solver)
3220 op.cop = self.cterm.getOp()
3223 def hasSymbol(self):
3224 """:return: True iff this term has a symbol."""
3225 return self.cterm.hasSymbol()
3227 def getSymbol(self):
3229 Asserts :py:meth:`hasSymbol()`.
3231 :return: the raw symbol of the term.
3233 return self.cterm.getSymbol().decode()
3236 """:return: True iff this term is a null term."""
3237 return self.cterm.isNull()
3243 :return: the Boolean negation of this term.
3245 cdef Term term = Term(self.solver)
3246 term.cterm = self.cterm.notTerm()
3249 def andTerm(self, Term t):
3253 :param t: a Boolean term
3254 :return: the conjunction of this term and the given term
3256 cdef Term term = Term(self.solver)
3257 term.cterm = self.cterm.andTerm((<Term> t).cterm)
3260 def orTerm(self, Term t):
3264 :param t: a Boolean term
3265 :return: the disjunction of this term and the given term
3267 cdef Term term = Term(self.solver)
3268 term.cterm = self.cterm.orTerm(t.cterm)
3271 def xorTerm(self, Term t):
3273 Boolean exclusive or.
3275 :param t: a Boolean term
3276 :return: the exclusive disjunction of this term and the given term
3278 cdef Term term = Term(self.solver)
3279 term.cterm = self.cterm.xorTerm(t.cterm)
3282 def eqTerm(self, Term t):
3286 :param t: a Boolean term
3287 :return: the Boolean equivalence of this term and the given term
3289 cdef Term term = Term(self.solver)
3290 term.cterm = self.cterm.eqTerm(t.cterm)
3293 def impTerm(self, Term t):
3295 Boolean Implication.
3297 :param t: a Boolean term
3298 :return: the implication of this term and the given term
3300 cdef Term term = Term(self.solver)
3301 term.cterm = self.cterm.impTerm(t.cterm)
3304 def iteTerm(self, Term then_t, Term else_t):
3306 If-then-else with this term as the Boolean condition.
3308 :param then_t: the `then` term
3309 :param else_t: the `else` term
3310 :return: the if-then-else term with this term as the Boolean condition
3312 cdef Term term = Term(self.solver)
3313 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
3316 def isConstArray(self):
3317 """:return: True iff this term is a constant array."""
3318 return self.cterm.isConstArray()
3320 def getConstArrayBase(self):
3322 Asserts :py:meth:`isConstArray()`.
3324 :return: the base (element stored at all indicies) of this constant array
3326 cdef Term term = Term(self.solver)
3327 term.cterm = self.cterm.getConstArrayBase()
3330 def isBooleanValue(self):
3331 """:return: True iff this term is a Boolean value."""
3332 return self.cterm.isBooleanValue()
3334 def getBooleanValue(self):
3336 Asserts :py:meth:`isBooleanValue()`
3338 :return: the representation of a Boolean value as a native Boolean value.
3340 return self.cterm.getBooleanValue()
3342 def isStringValue(self):
3343 """:return: True iff this term is a string value."""
3344 return self.cterm.isStringValue()
3346 def getStringValue(self):
3348 Asserts :py:meth:`isStringValue()`.
3351 This method is not to be confused with :py:meth:`__str__()` which
3352 returns the term in some string representation, whatever data it
3355 :return: the string term as a native string value.
3357 cdef Py_ssize_t size
3358 cdef c_wstring s = self.cterm.getStringValue()
3359 return PyUnicode_FromWideChar(s.data(), s.size())
3361 def getRealOrIntegerValueSign(self):
3363 Get integer or real value sign. Must be called on integer or real values,
3364 or otherwise an exception is thrown.
3366 :return: 0 if this term is zero, -1 if this term is a negative real or
3367 integer value, 1 if this term is a positive real or integer
3370 return self.cterm.getRealOrIntegerValueSign()
3372 def isIntegerValue(self):
3373 """:return: True iff this term is an integer value."""
3374 return self.cterm.isIntegerValue()
3376 def getIntegerValue(self):
3378 Asserts :py:meth:`isIntegerValue()`.
3380 :return: the integer term as a native python integer.
3382 return int(self.cterm.getIntegerValue().decode())
3384 def isFloatingPointPosZero(self):
3385 """:return: True iff the term is the floating-point value for positive zero."""
3386 return self.cterm.isFloatingPointPosZero()
3388 def isFloatingPointNegZero(self):
3389 """:return: True iff the term is the floating-point value for negative zero."""
3390 return self.cterm.isFloatingPointNegZero()
3392 def isFloatingPointPosInf(self):
3393 """:return: True iff the term is the floating-point value for positive infinity."""
3394 return self.cterm.isFloatingPointPosInf()
3396 def isFloatingPointNegInf(self):
3397 """:return: True iff the term is the floating-point value for negative infinity."""
3398 return self.cterm.isFloatingPointNegInf()
3400 def isFloatingPointNaN(self):
3401 """:return: True iff the term is the floating-point value for not a number."""
3402 return self.cterm.isFloatingPointNaN()
3404 def isFloatingPointValue(self):
3405 """:return: True iff this term is a floating-point value."""
3406 return self.cterm.isFloatingPointValue()
3408 def getFloatingPointValue(self):
3410 Asserts :py:meth:`isFloatingPointValue()`.
3412 :return: the representation of a floating-point value as a tuple of the exponent width, the significand width and a bit-vector value.
3414 cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
3415 cdef Term term = Term(self.solver)
3416 term.cterm = get2(t)
3417 return (get0(t), get1(t), term)
3419 def isSetValue(self):
3421 A term is a set value if it is considered to be a (canonical) constant
3422 set value. A canonical set value is one whose AST is:
3427 (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
3429 where ``c1 ... cn`` are values ordered by id such that
3430 ``c1 > ... > cn`` (see also :cpp:func:`cvc5::api::Term::operator>()`).
3433 A universe set term ``(kind SET_UNIVERSE)`` is not considered to be
3436 :return: True if the term is a set value.
3438 return self.cterm.isSetValue()
3440 def getSetValue(self):
3442 Asserts :py:meth:`isSetValue()`.
3444 :return: the representation of a set value as a set of terms.
3447 for e in self.cterm.getSetValue():
3448 term = Term(self.solver)
3453 def isSequenceValue(self):
3454 """:return: True iff this term is a sequence value."""
3455 return self.cterm.isSequenceValue()
3457 def getSequenceValue(self):
3459 Asserts :py:meth:`isSequenceValue()`.
3462 It is usually necessary for sequences to call
3463 :py:meth:`Solver.simplify()` to turn a sequence that is constructed
3464 by, e.g., concatenation of unit sequences, into a sequence value.
3466 :return: the representation of a sequence value as a vector of terms.
3469 for e in self.cterm.getSequenceValue():
3470 term = Term(self.solver)
3475 def isUninterpretedSortValue(self):
3476 """:return: True iff this term is a value from an uninterpreted sort."""
3477 return self.cterm.isUninterpretedSortValue()
3479 def getUninterpretedSortValue(self):
3481 Asserts :py:meth:`isUninterpretedSortValue()`.
3483 :return: the representation of an uninterpreted value as a pair of its sort and its index.
3485 return self.cterm.getUninterpretedSortValue()
3487 def isTupleValue(self):
3488 """:return: True iff this term is a tuple value."""
3489 return self.cterm.isTupleValue()
3491 def getTupleValue(self):
3493 Asserts :py:meth:`isTupleValue()`.
3495 :return: the representation of a tuple value as a vector of terms.
3498 for e in self.cterm.getTupleValue():
3499 term = Term(self.solver)
3504 def isRealValue(self):
3506 .. note:: A term of kind PI is not considered to be a real value.
3508 :return: True iff this term is a rational value.
3510 return self.cterm.isRealValue()
3512 def getRealValue(self):
3514 Asserts :py:meth:`isRealValue()`.
3516 :return: the representation of a rational value as a python Fraction.
3518 return Fraction(self.cterm.getRealValue().decode())
3520 def isBitVectorValue(self):
3521 """:return: True iff this term is a bit-vector value."""
3522 return self.cterm.isBitVectorValue()
3524 def getBitVectorValue(self, base = 2):
3526 Asserts :py:meth:`isBitVectorValue()`.
3527 Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexdecimal string).
3529 :return: the representation of a bit-vector value in string representation.
3531 return self.cterm.getBitVectorValue(base).decode()
3533 def toPythonObj(self):
3535 Converts a constant value Term to a Python object.
3539 - Boolean -- returns a Python bool
3540 - Int -- returns a Python int
3541 - Real -- returns a Python Fraction
3542 - BV -- returns a Python int (treats BV as unsigned)
3543 - String -- returns a Python Unicode string
3544 - Array -- returns a Python dict mapping indices to values. the constant base is returned as the default value
3548 if self.isBooleanValue():
3549 return self.getBooleanValue()
3550 elif self.isIntegerValue():
3551 return self.getIntegerValue()
3552 elif self.isRealValue():
3553 return self.getRealValue()
3554 elif self.isBitVectorValue():
3555 return int(self.getBitVectorValue(), 2)
3556 elif self.isStringValue():
3557 return self.getStringValue()
3558 elif self.getSort().isArray():
3564 # Array models are represented as a series of store operations
3565 # on a constant array
3568 if t.getKind().value == c_Kind.STORE:
3570 keys.append(t[1].toPythonObj())
3571 values.append(t[2].toPythonObj())
3572 to_visit.append(t[0])
3574 assert t.getKind().value == c_Kind.CONST_ARRAY
3575 base_value = t.getConstArrayBase().toPythonObj()
3577 assert len(keys) == len(values)
3578 assert base_value is not None
3580 # put everything in a dictionary with the constant
3581 # base as the result for any index not included in the stores
3582 res = defaultdict(lambda : base_value)
3583 for k, v in zip(keys, values):
3589 # Generate rounding modes
3590 cdef __rounding_modes = {
3591 <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
3592 <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
3593 <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
3594 <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
3595 <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway"
3598 mod_ref = sys.modules[__name__]
3599 for rm_int, name in __rounding_modes.items():
3600 r = RoundingMode(rm_int)
3602 if name in dir(mod_ref):
3603 raise RuntimeError("Redefinition of Python RoundingMode %s."%name)
3605 setattr(mod_ref, name, r)
3612 # Generate unknown explanations
3613 cdef __unknown_explanations = {
3614 <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
3615 <int> INCOMPLETE: "Incomplete",
3616 <int> TIMEOUT: "Timeout",
3617 <int> RESOURCEOUT: "Resourceout",
3618 <int> MEMOUT: "Memout",
3619 <int> INTERRUPTED: "Interrupted",
3620 <int> NO_STATUS: "NoStatus",
3621 <int> UNSUPPORTED: "Unsupported",
3622 <int> OTHER: "Other",
3623 <int> UNKNOWN_REASON: "UnknownReason"
3626 for ue_int, name in __unknown_explanations.items():
3627 u = UnknownExplanation(ue_int)
3629 if name in dir(mod_ref):
3630 raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
3632 setattr(mod_ref, name, u)