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 Op as c_Op
26 from cvc5 cimport OptionInfo as c_OptionInfo
27 from cvc5 cimport holds as c_holds
28 from cvc5 cimport getVariant as c_getVariant
29 from cvc5 cimport Solver as c_Solver
30 from cvc5 cimport Statistics as c_Statistics
31 from cvc5 cimport Stat as c_Stat
32 from cvc5 cimport Grammar as c_Grammar
33 from cvc5 cimport Sort as c_Sort
34 from cvc5 cimport Term as c_Term
35 from cvc5 cimport hash as c_hash
36 from cvc5 cimport wstring as c_wstring
37 from cvc5 cimport tuple as c_tuple
38 from cvc5 cimport get0, get1, get2
39 from cvc5kinds cimport Kind as c_Kind
40 from cvc5types cimport RoundingMode as c_RoundingMode
41 from cvc5types cimport UnknownExplanation as c_UnknownExplanation
43 cdef extern from "Python.h":
44 wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
45 object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
46 void PyMem_Free(void*)
48 ################################## DECORATORS #################################
49 def expand_list_arg(num_req_args=0):
51 Creates a decorator that looks at index num_req_args of the args,
52 if it's a list, it expands it before calling the function.
56 def wrapper(owner, *args):
57 if len(args) == num_req_args + 1 and \
58 isinstance(args[num_req_args], list):
59 args = list(args[:num_req_args]) + args[num_req_args]
60 return func(owner, *args)
63 ###############################################################################
66 ### Using PEP-8 spacing recommendations
67 ### Limit linewidth to 79 characters
68 ### Break before binary operators
69 ### surround top level functions and classes with two spaces
70 ### separate methods by one space
71 ### use spaces in functions sparingly to separate logical blocks
72 ### can omit spaces between unrelated oneliners
73 ### always use c++ default arguments
74 #### only use default args of None at python level
76 # References and pointers
77 # The Solver object holds a pointer to a c_Solver.
78 # This is because the assignment operator is deleted in the C++ API for solvers.
79 # Cython has a limitation where you can't stack allocate objects
80 # that have constructors with arguments:
81 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
82 # To get around that you can either have a nullary constructor and assignment
83 # or, use a pointer (which is what we chose).
84 # An additional complication of this is that to free up resources, you must
85 # know when to delete the object.
86 # Python will not follow the same scoping rules as in C++, so it must be
87 # able to reference count. To do this correctly, the solver must be a
88 # reference in the Python class for any class that keeps a pointer to
89 # the solver in C++ (to ensure the solver is not deleted before something
90 # that depends on it).
93 ## Objects for hashing
94 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
95 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
96 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
102 Wrapper class for :cpp:class:`cvc5::Datatype`.
106 def __cinit__(self, Solver solver):
109 def __getitem__(self, index):
110 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
111 if isinstance(index, int) and index >= 0:
112 dc.cdc = self.cd[(<int?> index)]
113 elif isinstance(index, str):
114 dc.cdc = self.cd[(<const string &> index.encode())]
116 raise ValueError("Expecting a non-negative integer or string")
119 def getConstructor(self, str name):
121 :param name: the name of the constructor.
122 :return: a constructor by name.
124 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
125 dc.cdc = self.cd.getConstructor(name.encode())
128 def getConstructorTerm(self, str name):
130 :param name: the name of the constructor.
131 :return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::Datatype::getConstructorTerm>`).
133 cdef Term term = Term(self.solver)
134 term.cterm = self.cd.getConstructorTerm(name.encode())
137 def getSelector(self, str name):
139 :param name: the name of the selector..
140 :return: a selector by name.
142 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
143 ds.cds = self.cd.getSelector(name.encode())
148 :return: the name of the datatype.
150 return self.cd.getName().decode()
152 def getNumConstructors(self):
154 :return: number of constructors in this datatype.
156 return self.cd.getNumConstructors()
158 def getParameters(self):
160 :return: the parameters of this datatype, if it is parametric. An exception is thrown if this datatype is not parametric.
163 for s in self.cd.getParameters():
164 sort = Sort(self.solver)
166 param_sorts.append(sort)
169 def isParametric(self):
171 .. warning:: This method is experimental and may change in future
173 :return: True if this datatype is parametric.
175 return self.cd.isParametric()
177 def isCodatatype(self):
178 """:return: True if this datatype corresponds to a co-datatype."""
179 return self.cd.isCodatatype()
182 """:return: True if this datatype corresponds to a tuple."""
183 return self.cd.isTuple()
187 .. warning:: This method is experimental and may change in future
189 :return: True if this datatype corresponds to a record.
191 return self.cd.isRecord()
194 """:return: True if this datatype is finite."""
195 return self.cd.isFinite()
197 def isWellFounded(self):
198 """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::Datatype::isWellFounded>`)."""
199 return self.cd.isWellFounded()
202 """:return: True if this Datatype is a null object."""
203 return self.cd.isNull()
206 return self.cd.toString().decode()
209 return self.cd.toString().decode()
213 dc = DatatypeConstructor(self.solver)
218 cdef class DatatypeConstructor:
220 A cvc5 datatype constructor.
221 Wrapper class for :cpp:class:`cvc5::DatatypeConstructor`.
223 cdef c_DatatypeConstructor cdc
225 def __cinit__(self, Solver solver):
226 self.cdc = c_DatatypeConstructor()
229 def __getitem__(self, index):
230 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
231 if isinstance(index, int) and index >= 0:
232 ds.cds = self.cdc[(<int?> index)]
233 elif isinstance(index, str):
234 ds.cds = self.cdc[(<const string &> index.encode())]
236 raise ValueError("Expecting a non-negative integer or string")
241 :return: the name of the constructor.
243 return self.cdc.getName().decode()
245 def getConstructorTerm(self):
247 :return: the constructor operator as a term.
249 cdef Term term = Term(self.solver)
250 term.cterm = self.cdc.getConstructorTerm()
253 def getInstantiatedConstructorTerm(self, Sort retSort):
255 Specialized method for parametric datatypes (see
256 :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm()
257 <cvc5::DatatypeConstructor::getInstantiatedConstructorTerm>`).
259 .. warning:: This method is experimental and may change in future
262 :param retSort: the desired return sort of the constructor
263 :return: the constructor operator as a term.
265 cdef Term term = Term(self.solver)
266 term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort)
269 def getTesterTerm(self):
271 :return: the tester operator that is related to this constructor, as a term.
273 cdef Term term = Term(self.solver)
274 term.cterm = self.cdc.getTesterTerm()
277 def getNumSelectors(self):
279 :return: the number of selecters (so far) of this Datatype constructor.
281 return self.cdc.getNumSelectors()
283 def getSelector(self, str name):
285 :param name: the name of the datatype selector.
286 :return: the first datatype selector with the given name
288 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
289 ds.cds = self.cdc.getSelector(name.encode())
292 def getSelectorTerm(self, str name):
294 :param name: the name of the datatype selector.
295 :return: a term representing the firstdatatype selector with the given name.
297 cdef Term term = Term(self.solver)
298 term.cterm = self.cdc.getSelectorTerm(name.encode())
302 """:return: True if this DatatypeConstructor is a null object."""
303 return self.cdc.isNull()
306 return self.cdc.toString().decode()
309 return self.cdc.toString().decode()
313 ds = DatatypeSelector(self.solver)
318 cdef class DatatypeConstructorDecl:
320 A cvc5 datatype constructor declaration.
321 Wrapper class for :cpp:class:`cvc5::DatatypeConstructorDecl`.
323 cdef c_DatatypeConstructorDecl cddc
326 def __cinit__(self, Solver solver):
329 def addSelector(self, str name, Sort sort):
331 Add datatype selector declaration.
333 :param name: the name of the datatype selector declaration to add.
334 :param sort: the codomain sort of the datatype selector declaration
337 self.cddc.addSelector(name.encode(), sort.csort)
339 def addSelectorSelf(self, str name):
341 Add datatype selector declaration whose codomain sort is the
344 :param name: the name of the datatype selector declaration to add.
346 self.cddc.addSelectorSelf(name.encode())
349 """:return: True if this DatatypeConstructorDecl is a null object."""
350 return self.cddc.isNull()
353 return self.cddc.toString().decode()
356 return self.cddc.toString().decode()
359 cdef class DatatypeDecl:
361 A cvc5 datatype declaration.
362 Wrapper class for :cpp:class:`cvc5::DatatypeDecl`.
364 cdef c_DatatypeDecl cdd
366 def __cinit__(self, Solver solver):
369 def addConstructor(self, DatatypeConstructorDecl ctor):
371 Add a datatype constructor declaration.
373 :param ctor: the datatype constructor declaration to add.
375 self.cdd.addConstructor(ctor.cddc)
377 def getNumConstructors(self):
379 :return: number of constructors (so far) for this datatype declaration.
381 return self.cdd.getNumConstructors()
383 def isParametric(self):
385 :return: is this datatype declaration parametric?
387 return self.cdd.isParametric()
391 :return: the name of this datatype declaration.
393 return self.cdd.getName().decode()
396 """:return: True if this DatatypeDecl is a null object."""
397 return self.cdd.isNull()
400 return self.cdd.toString().decode()
403 return self.cdd.toString().decode()
406 cdef class DatatypeSelector:
408 A cvc5 datatype selector.
409 Wrapper class for :cpp:class:`cvc5::DatatypeSelector`.
411 cdef c_DatatypeSelector cds
413 def __cinit__(self, Solver solver):
414 self.cds = c_DatatypeSelector()
419 :return: the name of this datatype selector.
421 return self.cds.getName().decode()
423 def getSelectorTerm(self):
425 :return: the selector opeartor of this datatype selector as a term.
427 cdef Term term = Term(self.solver)
428 term.cterm = self.cds.getSelectorTerm()
431 def getUpdaterTerm(self):
433 :return: the updater opeartor of this datatype selector as a term.
435 cdef Term term = Term(self.solver)
436 term.cterm = self.cds.getUpdaterTerm()
439 def getCodomainSort(self):
441 :return: the codomain sort of this selector.
443 cdef Sort sort = Sort(self.solver)
444 sort.csort = self.cds.getCodomainSort()
448 """:return: True if this DatatypeSelector is a null object."""
449 return self.cds.isNull()
452 return self.cds.toString().decode()
455 return self.cds.toString().decode()
461 An operator is a term that represents certain operators,
462 instantiated with its required parameters, e.g.,
463 a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`.
464 Wrapper class for :cpp:class:`cvc5::Op`.
468 def __cinit__(self, Solver solver):
472 def __eq__(self, Op other):
473 return self.cop == other.cop
475 def __ne__(self, Op other):
476 return self.cop != other.cop
479 return self.cop.toString().decode()
482 return self.cop.toString().decode()
485 return cophash(self.cop)
489 :return: the kind of this operator.
491 return Kind(<int> self.cop.getKind())
495 :return: True iff this operator is indexed.
497 return self.cop.isIndexed()
501 :return: True iff this operator is a null term.
503 return self.cop.isNull()
505 def getNumIndices(self):
507 :return: number of indices of this op.
509 return self.cop.getNumIndices()
511 def __getitem__(self, i):
513 Get the index at position i.
514 :param i: the position of the index to return
515 :return: the index at position i
517 cdef Term term = Term(self.solver)
518 term.cterm = self.cop[i]
525 Wrapper class for :cpp:class:`cvc5::Grammar`.
527 cdef c_Grammar cgrammar
529 def __cinit__(self, Solver solver):
531 self.cgrammar = c_Grammar()
533 def addRule(self, Term ntSymbol, Term rule):
535 Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
537 :param ntSymbol: the non-terminal to which the rule is added.
538 :param rule: the rule to add.
540 self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
542 def addAnyConstant(self, Term ntSymbol):
544 Allow ``ntSymbol`` to be an arbitrary constant.
546 :param ntSymbol: the non-terminal allowed to be constant.
548 self.cgrammar.addAnyConstant(ntSymbol.cterm)
550 def addAnyVariable(self, Term ntSymbol):
552 Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``.
554 :param ntSymbol: the non-terminal allowed to be any input variable.
556 self.cgrammar.addAnyVariable(ntSymbol.cterm)
558 def addRules(self, Term ntSymbol, rules):
560 Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
562 :param ntSymbol: the non-terminal to which the rules are added.
563 :param rules: the rules to add.
565 cdef vector[c_Term] crules
567 crules.push_back((<Term?> r).cterm)
568 self.cgrammar.addRules(ntSymbol.cterm, crules)
572 Encapsulation of a three-valued solver result, with explanations.
573 Wrapper class for :cpp:class:`cvc5::Result`.
577 # gets populated by solver
582 :return: True if Result is empty, i.e., a nullary Result, and not an actual result returned from a
583 :cpp:func:`Solver::checkSat() <cvc5::Solver::checkSat>` (and friends) query.
585 return self.cr.isNull()
589 :return: True if query was a satisfiable :cpp:func:`Solver::checkSat() <cvc5::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::Solver::checkSatAssuming>` query.
591 return self.cr.isSat()
595 :return: True if query was an usatisfiable :cpp:func:`Solver::checkSat() <cvc5::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::Solver::checkSatAssuming>` query.
597 return self.cr.isUnsat()
601 :return: True if query was a :cpp:func:`Solver::checkSat() <cvc5::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::Solver::checkSatAssuming>` query and cvc5 was not able to determine (un)satisfiability.
603 return self.cr.isUnknown()
605 def getUnknownExplanation(self):
607 :return: an explanation for an unknown query result.
609 return UnknownExplanation(<int> self.cr.getUnknownExplanation())
611 def __eq__(self, Result other):
612 return self.cr == other.cr
614 def __ne__(self, Result other):
615 return self.cr != other.cr
618 return self.cr.toString().decode()
621 return self.cr.toString().decode()
623 cdef class SynthResult:
625 Encapsulation of a solver synth result. This is the return value of the
627 - :py:meth:`Solver.checkSynth()`
628 - :py:meth:`Solver.checkSynthNext()`
629 which we call synthesis queries. This class indicates whether the
630 synthesis query has a solution, has no solution, or is unknown.
632 cdef c_SynthResult cr
634 # gets populated by solver
635 self.cr = c_SynthResult()
639 :return: True if SynthResult is null, i.e. not a SynthResult returned from a synthesis query.
641 return self.cr.isNull()
643 def hasSolution(self):
645 :return: True if the synthesis query has a solution.
647 return self.cr.hasSolution()
649 def hasNoSolution(self):
651 :return: True if the synthesis query has no solution.
652 In this case, then it was determined there was no solution.
654 return self.cr.hasNoSolution()
658 :return: True if the result of the synthesis query could not be determined.
660 return self.cr.isUnknown()
663 return self.cr.toString().decode()
666 return self.cr.toString().decode()
670 """Wrapper class for :cpp:class:`cvc5::Solver`."""
671 cdef c_Solver* csolver
674 self.csolver = new c_Solver()
676 def __dealloc__(self):
679 def getBooleanSort(self):
680 """:return: sort Boolean
682 cdef Sort sort = Sort(self)
683 sort.csort = self.csolver.getBooleanSort()
686 def getIntegerSort(self):
687 """:return: sort Integer
689 cdef Sort sort = Sort(self)
690 sort.csort = self.csolver.getIntegerSort()
693 def getNullSort(self):
694 """:return: sort null
696 cdef Sort sort = Sort(self)
697 sort.csort = self.csolver.getNullSort()
700 def getRealSort(self):
701 """:return: sort Real
703 cdef Sort sort = Sort(self)
704 sort.csort = self.csolver.getRealSort()
707 def getRegExpSort(self):
708 """:return: sort of RegExp
710 cdef Sort sort = Sort(self)
711 sort.csort = self.csolver.getRegExpSort()
714 def getRoundingModeSort(self):
715 """:return: sort RoundingMode
717 cdef Sort sort = Sort(self)
718 sort.csort = self.csolver.getRoundingModeSort()
721 def getStringSort(self):
722 """:return: sort String
724 cdef Sort sort = Sort(self)
725 sort.csort = self.csolver.getStringSort()
728 def mkArraySort(self, Sort indexSort, Sort elemSort):
729 """Create an array sort.
731 :param indexSort: the array index sort
732 :param elemSort: the array element sort
733 :return: the array sort
735 cdef Sort sort = Sort(self)
736 sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
739 def mkBitVectorSort(self, uint32_t size):
740 """Create a bit-vector sort.
742 :param size: the bit-width of the bit-vector sort
743 :return: the bit-vector sort
745 cdef Sort sort = Sort(self)
746 sort.csort = self.csolver.mkBitVectorSort(size)
749 def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
750 """Create a floating-point sort.
752 :param exp: the bit-width of the exponent of the floating-point sort.
753 :param sig: the bit-width of the significand of the floating-point sort.
755 cdef Sort sort = Sort(self)
756 sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
759 def mkDatatypeSort(self, DatatypeDecl dtypedecl):
760 """Create a datatype sort.
762 :param dtypedecl: the datatype declaration from which the sort is created
763 :return: the datatype sort
765 cdef Sort sort = Sort(self)
766 sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
769 def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
771 Create a vector of datatype sorts using unresolved sorts. The names of
772 the datatype declarations in dtypedecls must be distinct.
774 This method is called when the DatatypeDecl objects dtypedecls have been
775 built using "unresolved" sorts.
777 We associate each sort in unresolvedSorts with exacly one datatype from
778 dtypedecls. In particular, it must have the same name as exactly one
779 datatype declaration in dtypedecls.
781 When constructing datatypes, unresolved sorts are replaced by the datatype
782 sort constructed for the datatype declaration it is associated with.
784 :param dtypedecls: the datatype declarations from which the sort is created
785 :param unresolvedSorts: the list of unresolved sorts
786 :return: the datatype sorts
788 if unresolvedSorts == None:
789 unresolvedSorts = set([])
791 assert isinstance(unresolvedSorts, set)
794 cdef vector[c_DatatypeDecl] decls
795 for decl in dtypedecls:
796 decls.push_back((<DatatypeDecl?> decl).cdd)
798 cdef c_set[c_Sort] usorts
799 for usort in unresolvedSorts:
800 usorts.insert((<Sort?> usort).csort)
802 csorts = self.csolver.mkDatatypeSorts(
803 <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
811 def mkFunctionSort(self, sorts, Sort codomain):
812 """ Create function sort.
814 :param sorts: the sort of the function arguments
815 :param codomain: the sort of the function return value
816 :return: the function sort
819 cdef Sort sort = Sort(self)
820 # populate a vector with dereferenced c_Sorts
821 cdef vector[c_Sort] v
823 if isinstance(sorts, Sort):
824 sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
826 elif isinstance(sorts, list):
828 v.push_back((<Sort?>s).csort)
830 sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
834 def mkParamSort(self, str symbolname = None):
835 """ Create a sort parameter.
837 .. warning:: This method is experimental and may change in future
840 :param symbol: the name of the sort
841 :return: the sort parameter
843 cdef Sort sort = Sort(self)
844 if symbolname is None:
845 sort.csort = self.csolver.mkParamSort()
847 sort.csort = self.csolver.mkParamSort(symbolname.encode())
850 @expand_list_arg(num_req_args=0)
851 def mkPredicateSort(self, *sorts):
852 """Create a predicate sort.
854 :param sorts: the list of sorts of the predicate, as a list or as distinct arguments.
855 :return: the predicate sort
857 cdef Sort sort = Sort(self)
858 cdef vector[c_Sort] v
860 v.push_back((<Sort?> s).csort)
861 sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
864 @expand_list_arg(num_req_args=0)
865 def mkRecordSort(self, *fields):
866 """Create a record sort
868 .. warning:: This method is experimental and may change in future
871 :param fields: the list of fields of the record, as a list or as distinct arguments
872 :return: the record sort
874 cdef Sort sort = Sort(self)
875 cdef vector[pair[string, c_Sort]] v
876 cdef pair[string, c_Sort] p
880 p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
882 sort.csort = self.csolver.mkRecordSort(
883 <const vector[pair[string, c_Sort]] &> v)
886 def mkSetSort(self, Sort elemSort):
887 """Create a set sort.
889 :param elemSort: the sort of the set elements
890 :return: the set sort
892 cdef Sort sort = Sort(self)
893 sort.csort = self.csolver.mkSetSort(elemSort.csort)
896 def mkBagSort(self, Sort elemSort):
897 """Create a bag sort.
899 :param elemSort: the sort of the bag elements
900 :return: the bag sort
902 cdef Sort sort = Sort(self)
903 sort.csort = self.csolver.mkBagSort(elemSort.csort)
906 def mkSequenceSort(self, Sort elemSort):
907 """Create a sequence sort.
909 :param elemSort: the sort of the sequence elements
910 :return: the sequence sort
912 cdef Sort sort = Sort(self)
913 sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
916 def mkUninterpretedSort(self, str name = None):
917 """Create an uninterpreted sort.
919 :param symbol: the name of the sort
920 :return: the uninterpreted sort
922 cdef Sort sort = Sort(self)
924 sort.csort = self.csolver.mkUninterpretedSort()
926 sort.csort = self.csolver.mkUninterpretedSort(name.encode())
929 def mkUnresolvedSort(self, str name, size_t arity = 0):
930 """Create an unresolved sort.
932 This is for creating yet unresolved sort placeholders for mutually
935 :param symbol: the name of the sort
936 :param arity: the number of sort parameters of the sort
937 :return: the unresolved sort
939 cdef Sort sort = Sort(self)
940 sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity)
943 def mkUninterpretedSortConstructorSort(self, size_t arity, str symbol = None):
944 """Create a sort constructor sort.
946 An uninterpreted sort constructor is an uninterpreted sort with
949 :param symbol: the symbol of the sort
950 :param arity: the arity of the sort (must be > 0)
951 :return: the sort constructor sort
953 cdef Sort sort = Sort(self)
955 sort.csort = self.csolver.mkUninterpretedSortConstructorSort(arity)
957 sort.csort = self.csolver.mkUninterpretedSortConstructorSort(
958 arity, symbol.encode())
961 @expand_list_arg(num_req_args=0)
962 def mkTupleSort(self, *sorts):
963 """Create a tuple sort.
965 :param sorts: of the elements of the tuple, as a list or as distinct arguments
966 :return: the tuple sort
968 cdef Sort sort = Sort(self)
969 cdef vector[c_Sort] v
971 v.push_back((<Sort?> s).csort)
972 sort.csort = self.csolver.mkTupleSort(v)
975 @expand_list_arg(num_req_args=1)
976 def mkTerm(self, kind_or_op, *args):
978 Supports the following arguments:
980 - ``Term mkTerm(Kind kind)``
981 - ``Term mkTerm(Kind kind, Op child1, List[Term] children)``
982 - ``Term mkTerm(Kind kind, List[Term] children)``
984 where ``List[Term]`` can also be comma-separated arguments
986 cdef Term term = Term(self)
987 cdef vector[c_Term] v
990 if isinstance(kind_or_op, Kind):
991 op = self.mkOp(kind_or_op)
994 term.cterm = self.csolver.mkTerm((<Op?> op).cop)
997 v.push_back((<Term?> a).cterm)
998 term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
1001 def mkTuple(self, sorts, terms):
1002 """Create a tuple term. Terms are automatically converted if sorts are compatible.
1004 :param sorts: The sorts of the elements in the tuple
1005 :param terms: The elements in the tuple
1006 :return: the tuple Term
1008 cdef vector[c_Sort] csorts
1009 cdef vector[c_Term] cterms
1012 csorts.push_back((<Sort?> s).csort)
1014 cterms.push_back((<Term?> s).cterm)
1015 cdef Term result = Term(self)
1016 result.cterm = self.csolver.mkTuple(csorts, cterms)
1019 @expand_list_arg(num_req_args=0)
1020 def mkOp(self, k, *args):
1022 Supports the following uses:
1024 - ``Op mkOp(Kind kind)``
1025 - ``Op mkOp(Kind kind, const string& arg)``
1026 - ``Op mkOp(Kind kind, uint32_t arg0, ...)``
1028 cdef Op op = Op(self)
1029 cdef vector[uint32_t] v
1032 op.cop = self.csolver.mkOp(<c_Kind> k.value)
1033 elif len(args) == 1 and isinstance(args[0], str):
1034 op.cop = self.csolver.mkOp(<c_Kind> k.value,
1039 if not isinstance(a, int):
1041 "Expected uint32_t for argument {}".format(a))
1042 if a < 0 or a >= 2 ** 31:
1044 "Argument {} must fit in a uint32_t".format(a))
1045 v.push_back((<uint32_t?> a))
1046 op.cop = self.csolver.mkOp(<c_Kind> k.value, v)
1050 """Create a Boolean true constant.
1052 :return: the true constant
1054 cdef Term term = Term(self)
1055 term.cterm = self.csolver.mkTrue()
1059 """Create a Boolean false constant.
1061 :return: the false constant
1063 cdef Term term = Term(self)
1064 term.cterm = self.csolver.mkFalse()
1067 def mkBoolean(self, bint val):
1068 """Create a Boolean constant.
1070 :return: the Boolean constant
1071 :param val: the value of the constant
1073 cdef Term term = Term(self)
1074 term.cterm = self.csolver.mkBoolean(val)
1078 """Create a constant representing the number Pi.
1080 :return: a constant representing Pi
1082 cdef Term term = Term(self)
1083 term.cterm = self.csolver.mkPi()
1086 def mkInteger(self, val):
1087 """Create an integer constant.
1089 :param val: representation of the constant: either a string or integer
1090 :return: a constant of sort Integer
1092 cdef Term term = Term(self)
1093 if isinstance(val, str):
1094 term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
1096 assert(isinstance(val, int))
1097 term.cterm = self.csolver.mkInteger((<int?> val))
1100 def mkReal(self, val, den=None):
1101 """Create a real constant.
1103 :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.
1104 :param den: if not None, the value is `val`/`den`
1105 :return: a real term with literal value
1107 Can be used in various forms:
1109 - Given a string ``"N/D"`` constructs the corresponding rational.
1110 - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
1111 - 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``.
1112 - Given a string ``"W"`` or an integer, constructs that integer.
1113 - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``.
1115 cdef Term term = Term(self)
1117 term.cterm = self.csolver.mkReal(str(val).encode())
1119 if not isinstance(val, int) or not isinstance(den, int):
1120 raise ValueError("Expecting integers when"
1121 " constructing a rational"
1122 " but got: {}".format((val, den)))
1123 term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
1126 def mkRegexpAll(self):
1127 """Create a regular expression all (re.all) term.
1129 :return: the all term
1131 cdef Term term = Term(self)
1132 term.cterm = self.csolver.mkRegexpAll()
1135 def mkRegexpAllchar(self):
1136 """Create a regular expression allchar (re.allchar) term.
1138 :return: the allchar term
1140 cdef Term term = Term(self)
1141 term.cterm = self.csolver.mkRegexpAllchar()
1144 def mkRegexpNone(self):
1145 """Create a regular expression none (re.none) term.
1147 :return: the none term
1149 cdef Term term = Term(self)
1150 term.cterm = self.csolver.mkRegexpNone()
1153 def mkEmptySet(self, Sort s):
1154 """Create a constant representing an empty set of the given sort.
1156 :param sort: the sort of the set elements.
1157 :return: the empty set constant
1159 cdef Term term = Term(self)
1160 term.cterm = self.csolver.mkEmptySet(s.csort)
1163 def mkEmptyBag(self, Sort s):
1164 """Create a constant representing an empty bag of the given sort.
1166 :param sort: the sort of the bag elements.
1167 :return: the empty bag constant
1169 cdef Term term = Term(self)
1170 term.cterm = self.csolver.mkEmptyBag(s.csort)
1174 """Create a separation logic empty term.
1176 .. warning:: This method is experimental and may change in future
1179 :return: the separation logic empty term
1181 cdef Term term = Term(self)
1182 term.cterm = self.csolver.mkSepEmp()
1185 def mkSepNil(self, Sort sort):
1186 """Create a separation logic nil term.
1188 .. warning:: This method is experimental and may change in future
1191 :param sort: the sort of the nil term
1192 :return: the separation logic nil term
1194 cdef Term term = Term(self)
1195 term.cterm = self.csolver.mkSepNil(sort.csort)
1198 def mkString(self, str s, useEscSequences = None):
1200 Create a String constant from a `str` which may contain SMT-LIB
1201 compatible escape sequences like ``\\u1234`` to encode unicode characters.
1203 :param s: the string this constant represents
1204 :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character
1205 :return: the String constant
1207 cdef Term term = Term(self)
1208 cdef Py_ssize_t size
1209 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1210 if isinstance(useEscSequences, bool):
1211 term.cterm = self.csolver.mkString(
1212 s.encode(), <bint> useEscSequences)
1214 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1218 def mkEmptySequence(self, Sort sort):
1219 """Create an empty sequence of the given element sort.
1221 :param sort: The element sort of the sequence.
1222 :return: the empty sequence with given element sort.
1224 cdef Term term = Term(self)
1225 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1228 def mkUniverseSet(self, Sort sort):
1229 """Create a universe set of the given sort.
1231 :param sort: the sort of the set elements
1232 :return: the universe set constant
1234 cdef Term term = Term(self)
1235 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1238 @expand_list_arg(num_req_args=0)
1239 def mkBitVector(self, *args):
1241 Supports the following arguments:
1243 - ``Term mkBitVector(int size, int val=0)``
1244 - ``Term mkBitVector(int size, string val, int base)``
1246 :return: a bit-vector literal term
1247 :param size: an integer size.
1248 :param val: an integer representating the value, in the first form. In the second form, a string representing the value.
1249 :param base: the base of the string representation (second form only)
1251 cdef Term term = Term(self)
1253 raise ValueError("Missing arguments to mkBitVector")
1255 if not isinstance(size, int):
1257 "Invalid first argument to mkBitVector '{}', "
1258 "expected bit-vector size".format(size))
1260 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1261 elif len(args) == 2:
1263 if not isinstance(val, int):
1265 "Invalid second argument to mkBitVector '{}', "
1266 "expected integer value".format(size))
1267 term.cterm = self.csolver.mkBitVector(
1268 <uint32_t> size, <uint32_t> val)
1269 elif len(args) == 3:
1272 if not isinstance(val, str):
1274 "Invalid second argument to mkBitVector '{}', "
1275 "expected value string".format(size))
1276 if not isinstance(base, int):
1278 "Invalid third argument to mkBitVector '{}', "
1279 "expected base given as integer".format(size))
1280 term.cterm = self.csolver.mkBitVector(
1282 <const string&> str(val).encode(),
1285 raise ValueError("Unexpected inputs to mkBitVector")
1288 def mkConstArray(self, Sort sort, Term val):
1290 Create a constant array with the provided constant value stored at every
1293 :param sort: the sort of the constant array (must be an array sort)
1294 :param val: the constant value to store (must match the sort's element sort)
1295 :return: the constant array term
1297 cdef Term term = Term(self)
1298 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1301 def mkFloatingPointPosInf(self, int exp, int sig):
1302 """Create a positive infinity floating-point constant.
1304 :param exp: Number of bits in the exponent
1305 :param sig: Number of bits in the significand
1306 :return: the floating-point constant
1308 cdef Term term = Term(self)
1309 term.cterm = self.csolver.mkFloatingPointPosInf(exp, sig)
1312 def mkFloatingPointNegInf(self, int exp, int sig):
1313 """Create a negative infinity floating-point constant.
1315 :param exp: Number of bits in the exponent
1316 :param sig: Number of bits in the significand
1317 :return: the floating-point constant
1319 cdef Term term = Term(self)
1320 term.cterm = self.csolver.mkFloatingPointNegInf(exp, sig)
1323 def mkFloatingPointNaN(self, int exp, int sig):
1324 """Create a not-a-number (NaN) floating-point constant.
1326 :param exp: Number of bits in the exponent
1327 :param sig: Number of bits in the significand
1328 :return: the floating-point constant
1330 cdef Term term = Term(self)
1331 term.cterm = self.csolver.mkFloatingPointNaN(exp, sig)
1334 def mkFloatingPointPosZero(self, int exp, int sig):
1335 """Create a positive zero (+0.0) floating-point constant.
1337 :param exp: Number of bits in the exponent
1338 :param sig: Number of bits in the significand
1339 :return: the floating-point constant
1341 cdef Term term = Term(self)
1342 term.cterm = self.csolver.mkFloatingPointPosZero(exp, sig)
1345 def mkFloatingPointNegZero(self, int exp, int sig):
1346 """Create a negative zero (+0.0) floating-point constant.
1348 :param exp: Number of bits in the exponent
1349 :param sig: Number of bits in the significand
1350 :return: the floating-point constant
1352 cdef Term term = Term(self)
1353 term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig)
1356 def mkRoundingMode(self, rm):
1357 """Create a roundingmode constant.
1359 :param rm: the floating point rounding mode this constant represents
1361 cdef Term term = Term(self)
1362 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.value)
1365 def mkFloatingPoint(self, int exp, int sig, Term val):
1366 """Create a floating-point constant.
1368 :param exp: Size of the exponent
1369 :param sig: Size of the significand
1370 :param val: Value of the floating-point constant as a bit-vector term
1372 cdef Term term = Term(self)
1373 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1376 def mkCardinalityConstraint(self, Sort sort, int index):
1377 """Create cardinality constraint.
1379 .. warning:: This method is experimental and may change in future
1382 :param sort: Sort of the constraint
1383 :param index: The upper bound for the cardinality of the sort
1385 cdef Term term = Term(self)
1386 term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
1389 def mkConst(self, Sort sort, symbol=None):
1391 Create (first-order) constant (0-arity function symbol).
1395 .. code-block:: smtlib
1397 ( declare-const <symbol> <sort> )
1398 ( declare-fun <symbol> ( ) <sort> )
1400 :param sort: the sort of the constant
1401 :param symbol: the name of the constant. If None, a default symbol is used.
1402 :return: the first-order constant
1404 cdef Term term = Term(self)
1406 term.cterm = self.csolver.mkConst(sort.csort)
1408 term.cterm = self.csolver.mkConst(sort.csort,
1409 (<str?> symbol).encode())
1412 def mkVar(self, Sort sort, symbol=None):
1414 Create a bound variable to be used in a binder (i.e. a quantifier, a
1415 lambda, or a witness binder).
1417 :param sort: the sort of the variable
1418 :param symbol: the name of the variable
1419 :return: the variable
1421 cdef Term term = Term(self)
1423 term.cterm = self.csolver.mkVar(sort.csort)
1425 term.cterm = self.csolver.mkVar(sort.csort,
1426 (<str?> symbol).encode())
1429 def mkDatatypeConstructorDecl(self, str name):
1431 :param name: the constructor's name
1432 :return: the DatatypeConstructorDecl
1434 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1435 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1438 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1439 """Create a datatype declaration.
1441 :param name: the name of the datatype
1442 :param isCoDatatype: true if a codatatype is to be constructed
1443 :return: the DatatypeDecl
1445 cdef DatatypeDecl dd = DatatypeDecl(self)
1446 cdef vector[c_Sort] v
1449 if sorts_or_bool is None and isCoDatatype is None:
1450 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1451 elif sorts_or_bool is not None and isCoDatatype is None:
1452 if isinstance(sorts_or_bool, bool):
1453 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1454 <bint> sorts_or_bool)
1455 elif isinstance(sorts_or_bool, Sort):
1456 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1457 (<Sort> sorts_or_bool).csort)
1458 elif isinstance(sorts_or_bool, list):
1459 for s in sorts_or_bool:
1460 v.push_back((<Sort?> s).csort)
1461 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1462 <const vector[c_Sort]&> v)
1464 raise ValueError("Unhandled second argument type {}"
1465 .format(type(sorts_or_bool)))
1466 elif sorts_or_bool is not None and isCoDatatype is not None:
1467 if isinstance(sorts_or_bool, Sort):
1468 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1469 (<Sort> sorts_or_bool).csort,
1470 <bint> isCoDatatype)
1471 elif isinstance(sorts_or_bool, list):
1472 for s in sorts_or_bool:
1473 v.push_back((<Sort?> s).csort)
1474 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1475 <const vector[c_Sort]&> v,
1476 <bint> isCoDatatype)
1478 raise ValueError("Unhandled second argument type {}"
1479 .format(type(sorts_or_bool)))
1481 raise ValueError("Can't create DatatypeDecl with {}".format([type(a)
1488 def simplify(self, Term t):
1490 Simplify a formula without doing "much" work. Does not involve the
1491 SAT Engine in the simplification, but uses the current definitions,
1492 assertions, and the current partial model, if one has been constructed.
1493 It also involves theory normalization.
1495 .. warning:: This method is experimental and may change in future
1498 :param t: the formula to simplify
1499 :return: the simplified formula
1501 cdef Term term = Term(self)
1502 term.cterm = self.csolver.simplify(t.cterm)
1505 def assertFormula(self, Term term):
1506 """ Assert a formula
1510 .. code-block:: smtlib
1514 :param term: the formula to assert
1516 self.csolver.assertFormula(term.cterm)
1520 Check satisfiability.
1524 .. code-block:: smtlib
1528 :return: the result of the satisfiability check.
1530 cdef Result r = Result()
1531 r.cr = self.csolver.checkSat()
1534 def mkSygusGrammar(self, boundVars, ntSymbols):
1536 Create a SyGuS grammar. The first non-terminal is treated as the
1537 starting non-terminal, so the order of non-terminals matters.
1539 :param boundVars: the parameters to corresponding synth-fun/synth-inv
1540 :param ntSymbols: the pre-declaration of the non-terminal symbols
1541 :return: the grammar
1543 cdef Grammar grammar = Grammar(self)
1544 cdef vector[c_Term] bvc
1545 cdef vector[c_Term] ntc
1546 for bv in boundVars:
1547 bvc.push_back((<Term?> bv).cterm)
1548 for nt in ntSymbols:
1549 ntc.push_back((<Term?> nt).cterm)
1550 grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1553 def declareSygusVar(self, str symbol, Sort sort):
1554 """Append symbol to the current list of universal variables.
1558 .. code-block:: smtlib
1560 ( declare-var <symbol> <sort> )
1562 :param sort: the sort of the universal variable
1563 :param symbol: the name of the universal variable
1564 :return: the universal variable
1566 cdef Term term = Term(self)
1567 term.cterm = self.csolver.declareSygusVar(symbol.encode(), sort.csort)
1570 def addSygusConstraint(self, Term t):
1572 Add a formula to the set of SyGuS constraints.
1576 .. code-block:: smtlib
1578 ( constraint <term> )
1580 :param term: the formula to add as a constraint
1582 self.csolver.addSygusConstraint(t.cterm)
1584 def addSygusAssume(self, Term t):
1586 Add a formula to the set of Sygus assumptions.
1590 .. code-block:: smtlib
1594 :param term: the formuula to add as an assumption
1596 self.csolver.addSygusAssume(t.cterm)
1598 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1600 Add a set of SyGuS constraints to the current state that correspond to an
1601 invariant synthesis problem.
1605 .. code-block:: smtlib
1607 ( inv-constraint <inv> <pre> <trans> <post> )
1609 :param inv: the function-to-synthesize
1610 :param pre: the pre-condition
1611 :param trans: the transition relation
1612 :param post: the post-condition
1614 self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1616 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1618 Synthesize n-ary function following specified syntactic constraints.
1622 .. code-block:: smtlib
1624 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1626 :param symbol: the name of the function
1627 :param boundVars: the parameters to this function
1628 :param sort: the sort of the return value of this function
1629 :param grammar: the syntactic constraints
1630 :return: the function
1632 cdef Term term = Term(self)
1633 cdef vector[c_Term] v
1634 for bv in bound_vars:
1635 v.push_back((<Term?> bv).cterm)
1637 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1639 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1642 def checkSynth(self):
1644 Try to find a solution for the synthesis conjecture corresponding to the
1645 current list of functions-to-synthesize, universal variables and
1650 .. code-block:: smtlib
1654 :return: the result of the check, which is "solution" if the check
1655 found a solution in which case solutions are available via
1656 getSynthSolutions, "no solution" if it was determined there is
1657 no solution, or "unknown" otherwise.
1659 cdef SynthResult r = SynthResult()
1660 r.cr = self.csolver.checkSynth()
1663 def checkSynthNext(self):
1665 Try to find a next solution for the synthesis conjecture corresponding
1666 to the current list of functions-to-synthesize, universal variables and
1667 constraints. Must be called immediately after a successful call to
1668 check-synth or check-synth-next. Requires incremental mode.
1672 .. code-block:: smtlib
1676 :return: the result of the check, which is "solution" if the check
1677 found a solution in which case solutions are available via
1678 getSynthSolutions, "no solution" if it was determined there is
1679 no solution, or "unknown" otherwise.
1681 cdef SynthResult r = SynthResult()
1682 r.cr = self.csolver.checkSynthNext()
1685 def getSynthSolution(self, Term term):
1687 Get the synthesis solution of the given term. This method should be
1688 called immediately after the solver answers unsat for sygus input.
1690 :param term: the term for which the synthesis solution is queried
1691 :return: the synthesis solution of the given term
1693 cdef Term t = Term(self)
1694 t.cterm = self.csolver.getSynthSolution(term.cterm)
1697 def getSynthSolutions(self, list terms):
1699 Get the synthesis solutions of the given terms. This method should be
1700 called immediately after the solver answers unsat for sygus input.
1702 :param terms: the terms for which the synthesis solutions is queried
1703 :return: the synthesis solutions of the given terms
1706 cdef vector[c_Term] vec
1708 vec.push_back((<Term?> t).cterm)
1709 cresult = self.csolver.getSynthSolutions(vec)
1717 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1719 Synthesize invariant.
1723 .. code-block:: smtlib
1725 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1727 :param symbol: the name of the invariant
1728 :param boundVars: the parameters to this invariant
1729 :param grammar: the syntactic constraints
1730 :return: the invariant
1732 cdef Term term = Term(self)
1733 cdef vector[c_Term] v
1734 for bv in bound_vars:
1735 v.push_back((<Term?> bv).cterm)
1737 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
1739 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
1742 @expand_list_arg(num_req_args=0)
1743 def checkSatAssuming(self, *assumptions):
1744 """ Check satisfiability assuming the given formula.
1748 .. code-block:: smtlib
1750 ( check-sat-assuming ( <prop_literal> ) )
1752 :param assumptions: the formulas to assume, as a list or as distinct arguments
1753 :return: the result of the satisfiability check.
1755 cdef Result r = Result()
1756 # used if assumptions is a list of terms
1757 cdef vector[c_Term] v
1758 for a in assumptions:
1759 v.push_back((<Term?> a).cterm)
1760 r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
1763 @expand_list_arg(num_req_args=1)
1764 def declareDatatype(self, str symbol, *ctors):
1766 Create datatype sort.
1770 .. code-block:: smtlib
1772 ( declare-datatype <symbol> <datatype_decl> )
1774 :param symbol: the name of the datatype sort
1775 :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
1776 :return: the datatype sort
1778 cdef Sort sort = Sort(self)
1779 cdef vector[c_DatatypeConstructorDecl] v
1782 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1783 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1786 def declareFun(self, str symbol, list sorts, Sort sort):
1787 """Declare n-ary function symbol.
1791 .. code-block:: smtlib
1793 ( declare-fun <symbol> ( <sort>* ) <sort> )
1795 :param symbol: the name of the function
1796 :param sorts: the sorts of the parameters to this function
1797 :param sort: the sort of the return value of this function
1798 :return: the function
1800 cdef Term term = Term(self)
1801 cdef vector[c_Sort] v
1803 v.push_back((<Sort?> s).csort)
1804 term.cterm = self.csolver.declareFun(symbol.encode(),
1805 <const vector[c_Sort]&> v,
1809 def declareSort(self, str symbol, int arity):
1810 """Declare uninterpreted sort.
1814 .. code-block:: smtlib
1816 ( declare-sort <symbol> <numeral> )
1819 This corresponds to :py:meth:`Solver.mkUninterpretedSort()` if
1821 :py:meth:`Solver.mkUninterpretedSortConstructorSort()` if arity > 0.
1823 :param symbol: the name of the sort
1824 :param arity: the arity of the sort
1827 cdef Sort sort = Sort(self)
1828 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
1831 def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
1832 """Define n-ary function.
1836 .. code-block:: smtlib
1838 ( define-fun <function_def> )
1840 :param symbol: the name of the function
1841 :param bound_vars: the parameters to this function
1842 :param sort: the sort of the return value of this function
1843 :param term: the function body
1844 :param glbl: determines whether this definition is global (i.e. persists when popping the context)
1845 :return: the function
1847 cdef Term fun = Term(self)
1848 cdef vector[c_Term] v
1849 for bv in bound_vars:
1850 v.push_back((<Term?> bv).cterm)
1852 fun.cterm = self.csolver.defineFun(symbol.encode(),
1853 <const vector[c_Term] &> v,
1859 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1860 """Define recursive functions.
1864 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1865 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1870 .. code-block:: smtlib
1872 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1874 Create elements of parameter ``funs`` with mkConst().
1876 :param funs: the sorted functions
1877 :param bound_vars: the list of parameters to the functions
1878 :param terms: the list of function bodies of the functions
1879 :param global: determines whether this definition is global (i.e. persists when popping the context)
1880 :return: the function
1882 cdef Term term = Term(self)
1883 cdef vector[c_Term] v
1884 for bv in bound_vars:
1885 v.push_back((<Term?> bv).cterm)
1888 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
1889 <const vector[c_Term] &> v,
1890 (<Sort?> sort_or_term).csort,
1894 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
1895 <const vector[c_Term]&> v,
1896 (<Term?> sort_or_term).cterm,
1901 def defineFunsRec(self, funs, bound_vars, terms):
1902 """Define recursive functions.
1906 .. code-block:: smtlib
1908 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1910 Create elements of parameter ``funs`` with mkConst().
1912 :param funs: the sorted functions
1913 :param bound_vars: the list of parameters to the functions
1914 :param terms: the list of function bodies of the functions
1915 :param global: determines whether this definition is global (i.e. persists when popping the context)
1916 :return: the function
1918 cdef vector[c_Term] vf
1919 cdef vector[vector[c_Term]] vbv
1920 cdef vector[c_Term] vt
1923 vf.push_back((<Term?> f).cterm)
1925 cdef vector[c_Term] temp
1926 for v in bound_vars:
1928 temp.push_back((<Term?> t).cterm)
1933 vf.push_back((<Term?> t).cterm)
1936 """Get the refutation proof
1940 .. code-block:: smtlib
1944 Requires to enable option
1945 :ref:`produce-proofs <lbl-option-produce-proofs>`.
1947 .. warning:: This method is experimental and may change in future
1950 :return: a string representing the proof, according to the value of
1953 return self.csolver.getProof()
1955 def getLearnedLiterals(self):
1956 """Get a list of literals that are entailed by the current set of assertions
1960 .. code-block:: smtlib
1962 ( get-learned-literals )
1964 .. warning:: This method is experimental and may change in future
1967 :return: the list of literals
1970 for a in self.csolver.getLearnedLiterals():
1976 def getAssertions(self):
1977 """Get the list of asserted formulas.
1981 .. code-block:: smtlib
1985 :return: the list of asserted formulas
1988 for a in self.csolver.getAssertions():
1991 assertions.append(term)
1994 def getInfo(self, str flag):
1996 Get info from the solver.
2000 .. code-block:: smtlib
2002 ( get-info <info_flag> )
2004 :param flag: the info flag
2007 return self.csolver.getInfo(flag.encode())
2009 def getOption(self, str option):
2010 """Get the value of a given option.
2014 .. code-block:: smtlib
2016 ( get-option <keyword> )
2018 :param option: the option for which the value is queried
2019 :return: a string representation of the option value
2021 return self.csolver.getOption(option.encode()).decode()
2023 def getOptionNames(self):
2024 """Get all option names that can be used with `setOption`, `getOption` and `getOptionInfo`.
2026 :return: all option names
2028 return [s.decode() for s in self.csolver.getOptionNames()]
2030 def getOptionInfo(self, str option):
2031 """Get some information about the given option. Check the `OptionInfo`
2032 class for more details on which information is available.
2034 :return: information about the given option
2036 # declare all the variables we may need later
2037 cdef c_OptionInfo.ValueInfo[c_bool] vib
2038 cdef c_OptionInfo.ValueInfo[string] vis
2039 cdef c_OptionInfo.NumberInfo[int64_t] nii
2040 cdef c_OptionInfo.NumberInfo[uint64_t] niu
2041 cdef c_OptionInfo.NumberInfo[double] nid
2042 cdef c_OptionInfo.ModeInfo mi
2044 oi = self.csolver.getOptionInfo(option.encode())
2045 # generic information
2047 'name': oi.name.decode(),
2048 'aliases': [s.decode() for s in oi.aliases],
2049 'setByUser': oi.setByUser,
2052 # now check which type is actually in the variant
2053 if c_holds[c_OptionInfo.VoidInfo](oi.valueInfo):
2056 elif c_holds[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo):
2059 vib = c_getVariant[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo)
2060 res['current'] = vib.currentValue
2061 res['default'] = vib.defaultValue
2062 elif c_holds[c_OptionInfo.ValueInfo[string]](oi.valueInfo):
2065 vis = c_getVariant[c_OptionInfo.ValueInfo[string]](oi.valueInfo)
2066 res['current'] = vis.currentValue.decode()
2067 res['default'] = vis.defaultValue.decode()
2068 elif c_holds[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo):
2071 nii = c_getVariant[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo)
2072 res['current'] = nii.currentValue
2073 res['default'] = nii.defaultValue
2074 res['minimum'] = nii.minimum.value() if nii.minimum.has_value() else None
2075 res['maximum'] = nii.maximum.value() if nii.maximum.has_value() else None
2076 elif c_holds[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo):
2079 niu = c_getVariant[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo)
2080 res['current'] = niu.currentValue
2081 res['default'] = niu.defaultValue
2082 res['minimum'] = niu.minimum.value() if niu.minimum.has_value() else None
2083 res['maximum'] = niu.maximum.value() if niu.maximum.has_value() else None
2084 elif c_holds[c_OptionInfo.NumberInfo[double]](oi.valueInfo):
2087 nid = c_getVariant[c_OptionInfo.NumberInfo[double]](oi.valueInfo)
2088 res['current'] = nid.currentValue
2089 res['default'] = nid.defaultValue
2090 res['minimum'] = nid.minimum.value() if nid.minimum.has_value() else None
2091 res['maximum'] = nid.maximum.value() if nid.maximum.has_value() else None
2092 elif c_holds[c_OptionInfo.ModeInfo](oi.valueInfo):
2094 res['type'] = 'mode'
2095 mi = c_getVariant[c_OptionInfo.ModeInfo](oi.valueInfo)
2096 res['current'] = mi.currentValue.decode()
2097 res['default'] = mi.defaultValue.decode()
2098 res['modes'] = [s.decode() for s in mi.modes]
2101 def getOptionNames(self):
2102 """Get all option names that can be used with `setOption`, `getOption` and `getOptionInfo`.
2103 :return: all option names
2106 for n in self.csolver.getOptionNames():
2107 result += [n.decode()]
2110 def getUnsatAssumptions(self):
2112 Get the set of unsat ("failed") assumptions.
2116 .. code-block:: smtlib
2118 ( get-unsat-assumptions )
2120 Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
2122 :return: the set of unsat assumptions.
2125 for a in self.csolver.getUnsatAssumptions():
2128 assumptions.append(term)
2131 def getUnsatCore(self):
2132 """Get the unsatisfiable core.
2136 .. code-block:: smtlib
2140 Requires to enable option :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
2143 In contrast to SMT-LIB, the API does not distinguish between named and
2144 unnamed assertions when producing an unsatisfiable core. Additionally,
2145 the API allows this option to be called after a check with assumptions.
2146 A subset of those assumptions may be included in the unsatisfiable core
2147 returned by this method.
2149 :return: a set of terms representing the unsatisfiable core
2152 for a in self.csolver.getUnsatCore():
2158 def getDifficulty(self):
2160 Get a difficulty estimate for an asserted formula. This method is intended to be called immediately after
2161 any response to a checkSat.
2163 .. warning:: This method is experimental and may change in future
2166 :return: a map from (a subset of) the input assertions to a real value that is an estimate of how difficult each assertion was to solver. Unmentioned assertions can be assumed to have zero difficulty.
2169 for p in self.csolver.getDifficulty():
2179 diffi[termk] = termv
2182 def getValue(self, Term t):
2183 """Get the value of the given term in the current model.
2187 .. code-block:: smtlib
2189 ( get-value ( <term> ) )
2191 :param term: the term for which the value is queried
2192 :return: the value of the given term
2194 cdef Term term = Term(self)
2195 term.cterm = self.csolver.getValue(t.cterm)
2198 def getModelDomainElements(self, Sort s):
2200 Get the domain elements of uninterpreted sort s in the current model. The
2201 current model interprets s as the finite sort whose domain elements are
2202 given in the return value of this method.
2204 :param s: The uninterpreted sort in question
2205 :return: the domain elements of s in the current model
2208 cresult = self.csolver.getModelDomainElements(s.csort)
2215 def isModelCoreSymbol(self, Term v):
2217 This returns false if the model value of free constant v was not
2218 essential for showing the satisfiability of the last call to checkSat
2219 using the current model. This method will only return false (for any v)
2220 if the model-cores option has been set.
2222 .. warning:: This method is experimental and may change in future
2225 :param v: The term in question
2226 :return: true if v is a model core symbol
2228 return self.csolver.isModelCoreSymbol(v.cterm)
2230 def getQuantifierElimination(self, Term term):
2231 """Do quantifier elimination.
2235 .. code-block:: smtlib
2239 Requires a logic that supports quantifier elimination.
2240 Currently, the only logics supported by quantifier elimination
2243 .. warning:: This method is experimental and may change in future
2246 :param q: a quantified formula of the form
2247 :math:`Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)'
2249 :math:'Q\bar{x}' is a set of quantified variables of the form
2250 :math:'Q x_1...x_k' and
2251 :math:'P( x_1...x_i, y_1...y_j )' is a quantifier-free formula
2252 :return: a formula :math:'\phi' such that, given the current set of formulas
2253 :math:'A asserted to this solver:
2254 - :math:'(A \wedge q)' :math:'(A \wedge \phi)' are equivalent
2255 - :math:'\phi' is quantifier-free formula containing only free
2256 variables in :math:'y_1...y_n'.
2258 cdef Term result = Term(self)
2259 result.cterm = self.csolver.getQuantifierElimination(term.cterm)
2262 def getQuantifierEliminationDisjunct(self, Term term):
2263 """Do partial quantifier elimination, which can be used for incrementally computing
2264 the result of a quantifier elimination.
2268 .. code-block:: smtlib
2270 ( get-qe-disjunct <q> )
2272 Requires a logic that supports quantifier elimination.
2273 Currently, the only logics supported by quantifier elimination
2276 .. warning:: This method is experimental and may change in future
2279 :param q: a quantified formula of the form
2280 @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
2282 @f$Q\bar{x}@f$ is a set of quantified variables of the form
2283 @f$Q x_1...x_k@f$ and
2284 @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
2285 :return: a formula @f$\phi@f$ such that, given the current set of formulas
2286 @f$A@f$ asserted to this solver:
2287 - @f$(A \wedge q \implies A \wedge \phi)@f$ if @f$Q@f$ is
2288 @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if
2289 @f$Q@f$ is @f$\exists@f$
2290 - @f$\phi@f$ is quantifier-free formula containing only free
2291 variables in @f$y_1...y_n@f$
2292 - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the
2294 @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge
2295 \neg (\phi \wedge Q_n))@f$
2296 where for each @f$i = 1...n@f$,
2297 formula @f$(\phi \wedge Q_i)@f$ is the result of calling
2298 Solver::getQuantifierEliminationDisjunct() for @f$q@f$ with the
2299 set of assertions @f$(A \wedge Q_{i-1})@f$.
2300 Similarly, if @f$Q@f$ is @f$\forall@f$, then let
2301 @f$(A \wedge Q_n)@f$ be
2302 @f$(A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge
2304 where @f$(\phi \wedge Q_i)@f$ is the same as above.
2305 In either case, we have that @f$(\phi \wedge Q_j)@f$ will
2306 eventually be true or false, for some finite j.
2308 cdef Term result = Term(self)
2309 result.cterm = self.csolver.getQuantifierEliminationDisjunct(term.cterm)
2312 def getModel(self, sorts, consts):
2321 Requires to enable option
2322 :ref:`produce-models <lbl-option-produce-models>`.
2324 .. warning:: This method is experimental and may change in future
2327 :param sorts: The list of uninterpreted sorts that should be printed in
2329 :param vars: The list of free constants that should be printed in the
2330 model. A subset of these may be printed based on
2332 :return: a string representing the model.
2335 cdef vector[c_Sort] csorts
2337 csorts.push_back((<Sort?> sort).csort)
2339 cdef vector[c_Term] cconsts
2340 for const in consts:
2341 cconsts.push_back((<Term?> const).cterm)
2343 return self.csolver.getModel(csorts, cconsts)
2345 def getValueSepHeap(self):
2346 """When using separation logic, obtain the term for the heap.
2348 .. warning:: This method is experimental and may change in future
2351 :return: The term for the heap
2353 cdef Term term = Term(self)
2354 term.cterm = self.csolver.getValueSepHeap()
2357 def getValueSepNil(self):
2358 """When using separation logic, obtain the term for nil.
2360 .. warning:: This method is experimental and may change in future
2363 :return: The term for nil
2365 cdef Term term = Term(self)
2366 term.cterm = self.csolver.getValueSepNil()
2369 def declareSepHeap(self, Sort locType, Sort dataType):
2371 When using separation logic, this sets the location sort and the
2372 datatype sort to the given ones. This method should be invoked exactly
2373 once, before any separation logic constraints are provided.
2375 .. warning:: This method is experimental and may change in future
2378 :param locSort: The location sort of the heap
2379 :param dataSort: The data sort of the heap
2381 self.csolver.declareSepHeap(locType.csort, dataType.csort)
2383 def declarePool(self, str symbol, Sort sort, initValue):
2384 """Declare a symbolic pool of terms with the given initial value.
2388 .. code-block:: smtlib
2390 ( declare-pool <symbol> <sort> ( <term>* ) )
2392 .. warning:: This method is experimental and may change in future
2395 :param symbol: The name of the pool
2396 :param sort: The sort of the elements of the pool.
2397 :param initValue: The initial value of the pool
2399 cdef Term term = Term(self)
2400 cdef vector[c_Term] niv
2402 niv.push_back((<Term?> v).cterm)
2403 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
2406 def pop(self, nscopes=1):
2407 """Pop ``nscopes`` level(s) from the assertion stack.
2411 .. code-block:: smtlib
2415 :param nscopes: the number of levels to pop
2417 self.csolver.pop(nscopes)
2419 def push(self, nscopes=1):
2420 """ Push ``nscopes`` level(s) to the assertion stack.
2424 .. code-block:: smtlib
2428 :param nscopes: the number of levels to push
2430 self.csolver.push(nscopes)
2432 def resetAssertions(self):
2434 Remove all assertions.
2438 .. code-block:: smtlib
2440 ( reset-assertions )
2443 self.csolver.resetAssertions()
2445 def setInfo(self, str keyword, str value):
2450 .. code-block:: smtlib
2452 ( set-info <attribute> )
2454 :param keyword: the info flag
2455 :param value: the value of the info flag
2457 self.csolver.setInfo(keyword.encode(), value.encode())
2459 def setLogic(self, str logic):
2464 .. code-block:: smtlib
2466 ( set-logic <symbol> )
2468 :param logic: the logic to set
2470 self.csolver.setLogic(logic.encode())
2472 def setOption(self, str option, str value):
2477 .. code-block:: smtlib
2479 ( set-option <option> )
2481 :param option: the option name
2482 :param value: the option value
2484 self.csolver.setOption(option.encode(), value.encode())
2487 def getInterpolant(self, Term conj, *args):
2488 """Get an interpolant.
2492 .. code-block:: smtlib
2494 ( get-interpolant <conj> )
2495 ( get-interpolant <conj> <grammar> )
2497 Requires option :ref:`produce-interpolants <lbl-option-produce-interpolants>` to be set to a mode different from `none`.
2499 Supports the following variants:
2501 - ``Term getInteprolant(Term conj)``
2502 - ``Term getInteprolant(Term conj, Grammar grammar)``
2504 .. warning:: This method is experimental and may change in future
2507 :param conj: the conjecture term
2508 :param output: the term where the result will be stored
2509 :param grammar: a grammar for the inteprolant
2510 :return: True iff an interpolant was found
2512 cdef Term result = Term(self)
2514 result.cterm = self.csolver.getInterpolant(conj.cterm)
2516 assert len(args) == 1
2517 assert isinstance(args[0], Grammar)
2518 result.cterm = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> args[0]).cgrammar)
2522 def getInterpolantNext(self):
2524 Get the next interpolant. Can only be called immediately after
2525 a succesful call to get-interpolant or get-interpolant-next.
2526 Is guaranteed to produce a syntactically different interpolant wrt the
2527 last returned interpolant if successful.
2531 .. code-block:: smtlib
2533 ( get-interpolant-next )
2535 Requires to enable incremental mode, and
2536 option :ref:`produce-interpolants <lbl-option-produce-interpolants>` to be set to a mode different from `none`.
2538 .. warning:: This method is experimental and may change in future
2541 :param output: the term where the result will be stored
2542 :return: True iff an interpolant was found
2544 cdef Term result = Term(self)
2545 result.cterm = self.csolver.getInterpolantNext()
2548 def getAbduct(self, Term conj, *args):
2553 .. code-block:: smtlib
2555 ( get-abduct <conj> )
2556 ( get-abduct <conj> <grammar> )
2558 Requires to enable option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2560 Supports the following variants:
2562 - ``Term getAbduct(Term conj)``
2563 - ``Term getAbduct(Term conj, Grammar grammar)``
2565 .. warning:: This method is experimental and may change in future
2568 :param conj: the conjecture term
2569 :param output: the term where the result will be stored
2570 :param grammar: a grammar for the abduct
2571 :return: True iff an abduct was found
2573 cdef Term result = Term(self)
2575 result.cterm = self.csolver.getAbduct(conj.cterm)
2577 assert len(args) == 1
2578 assert isinstance(args[0], Grammar)
2579 result.cterm = self.csolver.getAbduct(conj.cterm, (<Grammar ?> args[0]).cgrammar)
2582 def getAbductNext(self):
2584 Get the next abduct. Can only be called immediately after
2585 a succesful call to get-abduct or get-abduct-next.
2586 Is guaranteed to produce a syntactically different abduct wrt the
2587 last returned abduct if successful.
2591 .. code-block:: smtlib
2595 Requires to enable incremental mode, and
2596 option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2598 .. warning:: This method is experimental and may change in future
2601 :param output: the term where the result will be stored
2602 :return: True iff an abduct was found
2604 cdef Term result = Term(self)
2605 result.cterm = self.csolver.getAbductNext()
2608 def blockModel(self):
2610 Block the current model. Can be called only if immediately preceded by a
2611 SAT or INVALID query.
2615 .. code-block:: smtlib
2619 Requires enabling option
2620 :ref:`produce-models <lbl-option-produce-models>`
2622 :ref:`block-models <lbl-option-block-models>`
2623 to a mode other than ``none``.
2625 .. warning:: This method is experimental and may change in future
2628 self.csolver.blockModel()
2630 def blockModelValues(self, terms):
2632 Block the current model values of (at least) the values in terms. Can be
2633 called only if immediately preceded by a SAT or NOT_ENTAILED query.
2637 .. code-block:: smtlib
2639 (block-model-values ( <terms>+ ))
2641 Requires enabling option
2642 :ref:`produce-models <lbl-option-produce-models>`.
2644 .. warning:: This method is experimental and may change in future
2647 cdef vector[c_Term] nts
2649 nts.push_back((<Term?> t).cterm)
2650 self.csolver.blockModelValues(nts)
2652 def getInstantiations(self):
2654 Return a string that contains information about all instantiations made
2655 by the quantifiers module.
2657 .. warning:: This method is experimental and may change in future
2660 return self.csolver.getInstantiations()
2662 def getStatistics(self):
2664 Returns a snapshot of the current state of the statistic values of this
2665 solver. The returned object is completely decoupled from the solver and
2666 will not change when the solver is used again.
2669 res.cstats = self.csolver.getStatistics()
2675 The sort of a cvc5 term.
2679 def __cinit__(self, Solver solver):
2680 # csort always set by Solver
2681 self.solver = solver
2683 def __eq__(self, Sort other):
2684 return self.csort == other.csort
2686 def __ne__(self, Sort other):
2687 return self.csort != other.csort
2689 def __lt__(self, Sort other):
2690 return self.csort < other.csort
2692 def __gt__(self, Sort other):
2693 return self.csort > other.csort
2695 def __le__(self, Sort other):
2696 return self.csort <= other.csort
2698 def __ge__(self, Sort other):
2699 return self.csort >= other.csort
2702 return self.csort.toString().decode()
2705 return self.csort.toString().decode()
2708 return csorthash(self.csort)
2710 def hasSymbol(self):
2711 """:return: True iff this sort has a symbol."""
2712 return self.csort.hasSymbol()
2714 def getSymbol(self):
2716 Asserts :py:meth:`hasSymbol()`.
2718 :return: the raw symbol of the sort.
2720 return self.csort.getSymbol().decode()
2723 """:return: True if this Sort is a null sort."""
2724 return self.csort.isNull()
2726 def isBoolean(self):
2728 Is this a Boolean sort?
2730 :return: True if the sort is the Boolean sort.
2732 return self.csort.isBoolean()
2734 def isInteger(self):
2736 Is this an integer sort?
2738 :return: True if the sort is the integer sort.
2740 return self.csort.isInteger()
2744 Is this a real sort?
2746 :return: True if the sort is the real sort.
2748 return self.csort.isReal()
2752 Is this a string sort?
2754 :return: True if the sort is the string sort.
2756 return self.csort.isString()
2760 Is this a regexp sort?
2762 :return: True if the sort is the regexp sort.
2764 return self.csort.isRegExp()
2766 def isRoundingMode(self):
2768 Is this a rounding mode sort?
2770 :return: True if the sort is the rounding mode sort.
2772 return self.csort.isRoundingMode()
2774 def isBitVector(self):
2776 Is this a bit-vector sort?
2778 :return: True if the sort is a bit-vector sort.
2780 return self.csort.isBitVector()
2782 def isFloatingPoint(self):
2784 Is this a floating-point sort?
2786 :return: True if the sort is a bit-vector sort.
2788 return self.csort.isFloatingPoint()
2790 def isDatatype(self):
2792 Is this a datatype sort?
2794 :return: True if the sort is a datatype sort.
2796 return self.csort.isDatatype()
2798 def isDatatypeConstructor(self):
2800 Is this a datatype constructor sort?
2802 :return: True if the sort is a datatype constructor sort.
2804 return self.csort.isDatatypeConstructor()
2806 def isDatatypeSelector(self):
2808 Is this a datatype selector sort?
2810 :return: True if the sort is a datatype selector sort.
2812 return self.csort.isDatatypeSelector()
2814 def isDatatypeTester(self):
2816 Is this a tester sort?
2818 :return: True if the sort is a selector sort.
2820 return self.csort.isDatatypeTester()
2822 def isDatatypeUpdater(self):
2824 Is this a datatype updater sort?
2826 :return: True if the sort is a datatype updater sort.
2828 return self.csort.isDatatypeUpdater()
2830 def isFunction(self):
2832 Is this a function sort?
2834 :return: True if the sort is a function sort.
2836 return self.csort.isFunction()
2838 def isPredicate(self):
2840 Is this a predicate sort?
2841 That is, is this a function sort mapping to Boolean? All predicate
2842 sorts are also function sorts.
2844 :return: True if the sort is a predicate sort.
2846 return self.csort.isPredicate()
2850 Is this a tuple sort?
2852 :return: True if the sort is a tuple sort.
2854 return self.csort.isTuple()
2858 Is this a record sort?
2860 .. warning:: This method is experimental and may change in future
2863 :return: True if the sort is a record sort.
2865 return self.csort.isRecord()
2869 Is this an array sort?
2871 :return: True if the sort is an array sort.
2873 return self.csort.isArray()
2879 :return: True if the sort is a set sort.
2881 return self.csort.isSet()
2887 :return: True if the sort is a bag sort.
2889 return self.csort.isBag()
2891 def isSequence(self):
2893 Is this a sequence sort?
2895 :return: True if the sort is a sequence sort.
2897 return self.csort.isSequence()
2899 def isUninterpretedSort(self):
2901 Is this a sort uninterpreted?
2903 :return: True if the sort is uninterpreted.
2905 return self.csort.isUninterpretedSort()
2907 def isUninterpretedSortConstructor(self):
2909 Is this a sort constructor kind?
2911 An uninterpreted sort constructor is an uninterpreted sort with
2914 :return: True if this a sort constructor kind.
2916 return self.csort.isUninterpretedSortConstructor()
2918 def isInstantiated(self):
2920 Is this an instantiated (parametric datatype or uninterpreted sort
2923 An instantiated sort is a sort that has been constructed from
2924 instantiating a sort parameters with sort arguments
2925 (see Sort::instantiate()).
2927 :return: True if this is an instantiated sort.
2929 return self.csort.isInstantiated()
2931 def getUninterpretedSortConstructor(self):
2933 Get the associated uninterpreted sort constructor of an
2934 instantiated uninterpreted sort.
2936 :return: the uninterpreted sort constructor sort
2938 cdef Sort sort = Sort(self.solver)
2939 sort.csort = self.csort.getUninterpretedSortConstructor()
2942 def getDatatype(self):
2944 :return: the underlying datatype of a datatype sort
2946 cdef Datatype d = Datatype(self.solver)
2947 d.cd = self.csort.getDatatype()
2950 def instantiate(self, params):
2952 Instantiate a parameterized datatype sort or uninterpreted sort
2954 Create sorts parameter with :py:meth:`Solver.mkParamSort()`
2956 :param params: the list of sort parameters to instantiate with
2957 :return: the instantiated sort
2959 cdef Sort sort = Sort(self.solver)
2960 cdef vector[c_Sort] v
2962 v.push_back((<Sort?> s).csort)
2963 sort.csort = self.csort.instantiate(v)
2966 def getInstantiatedParameters(self):
2968 Get the sorts used to instantiate the sort parameters of a
2969 parametric sort (parametric datatype or uninterpreted sort
2970 constructor sort, see Sort.instantiate()).
2972 :return the sorts used to instantiate the sort parameters of a
2975 instantiated_sorts = []
2976 for s in self.csort.getInstantiatedParameters():
2977 sort = Sort(self.solver)
2979 instantiated_sorts.append(sort)
2980 return instantiated_sorts
2982 def substitute(self, sort_or_list_1, sort_or_list_2):
2984 Substitution of Sorts.
2986 Note that this replacement is applied during a pre-order traversal and
2987 only once to the sort. It is not run until fix point. In the case that
2988 sort_or_list_1 contains duplicates, the replacement earliest in the list
2992 ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])`` will
2993 return ``(Array (Array C D) B)``.
2995 .. warning:: This method is experimental and may change in future
2998 :param sort_or_list_1: the subsort or subsorts to be substituted within this sort.
2999 :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort.
3002 # The resulting sort after substitution
3003 cdef Sort sort = Sort(self.solver)
3004 # lists for substitutions
3005 cdef vector[c_Sort] ces
3006 cdef vector[c_Sort] creplacements
3008 # normalize the input parameters to be lists
3009 if isinstance(sort_or_list_1, list):
3010 assert isinstance(sort_or_list_2, list)
3012 replacements = sort_or_list_2
3013 if len(es) != len(replacements):
3014 raise RuntimeError("Expecting list inputs to substitute to "
3015 "have the same length but got: "
3016 "{} and {}".format(len(es), len(replacements)))
3018 for e, r in zip(es, replacements):
3019 ces.push_back((<Sort?> e).csort)
3020 creplacements.push_back((<Sort?> r).csort)
3023 # add the single elements to the vectors
3024 ces.push_back((<Sort?> sort_or_list_1).csort)
3025 creplacements.push_back((<Sort?> sort_or_list_2).csort)
3027 # call the API substitute method with lists
3028 sort.csort = self.csort.substitute(ces, creplacements)
3032 def getDatatypeConstructorArity(self):
3034 :return: the arity of a datatype constructor sort.
3036 return self.csort.getDatatypeConstructorArity()
3038 def getDatatypeConstructorDomainSorts(self):
3040 :return: the domain sorts of a datatype constructor sort
3043 for s in self.csort.getDatatypeConstructorDomainSorts():
3044 sort = Sort(self.solver)
3046 domain_sorts.append(sort)
3049 def getDatatypeConstructorCodomainSort(self):
3051 :return: the codomain sort of a datatype constructor sort
3053 cdef Sort sort = Sort(self.solver)
3054 sort.csort = self.csort.getDatatypeConstructorCodomainSort()
3057 def getDatatypeSelectorDomainSort(self):
3059 :return: the domain sort of a datatype selector sort
3061 cdef Sort sort = Sort(self.solver)
3062 sort.csort = self.csort.getDatatypeSelectorDomainSort()
3065 def getDatatypeSelectorCodomainSort(self):
3067 :return: the codomain sort of a datatype selector sort
3069 cdef Sort sort = Sort(self.solver)
3070 sort.csort = self.csort.getDatatypeSelectorCodomainSort()
3073 def getDatatypeTesterDomainSort(self):
3075 :return: the domain sort of a datatype tester sort
3077 cdef Sort sort = Sort(self.solver)
3078 sort.csort = self.csort.getDatatypeTesterDomainSort()
3081 def getDatatypeTesterCodomainSort(self):
3083 :return: the codomain sort of a datatype tester sort, which is the
3086 cdef Sort sort = Sort(self.solver)
3087 sort.csort = self.csort.getDatatypeTesterCodomainSort()
3090 def getFunctionArity(self):
3092 :return: the arity of a function sort
3094 return self.csort.getFunctionArity()
3096 def getFunctionDomainSorts(self):
3098 :return: the domain sorts of a function sort
3101 for s in self.csort.getFunctionDomainSorts():
3102 sort = Sort(self.solver)
3104 domain_sorts.append(sort)
3107 def getFunctionCodomainSort(self):
3109 :return: the codomain sort of a function sort
3111 cdef Sort sort = Sort(self.solver)
3112 sort.csort = self.csort.getFunctionCodomainSort()
3115 def getArrayIndexSort(self):
3117 :return: the array index sort of an array sort
3119 cdef Sort sort = Sort(self.solver)
3120 sort.csort = self.csort.getArrayIndexSort()
3123 def getArrayElementSort(self):
3125 :return: the array element sort of an array sort
3127 cdef Sort sort = Sort(self.solver)
3128 sort.csort = self.csort.getArrayElementSort()
3131 def getSetElementSort(self):
3133 :return: the element sort of a set sort
3135 cdef Sort sort = Sort(self.solver)
3136 sort.csort = self.csort.getSetElementSort()
3139 def getBagElementSort(self):
3141 :return: the element sort of a bag sort
3143 cdef Sort sort = Sort(self.solver)
3144 sort.csort = self.csort.getBagElementSort()
3147 def getSequenceElementSort(self):
3149 :return: the element sort of a sequence sort
3151 cdef Sort sort = Sort(self.solver)
3152 sort.csort = self.csort.getSequenceElementSort()
3155 def getUninterpretedSortConstructorArity(self):
3157 :return: the arity of a sort constructor sort
3159 return self.csort.getUninterpretedSortConstructorArity()
3161 def getBitVectorSize(self):
3163 :return: the bit-width of the bit-vector sort
3165 return self.csort.getBitVectorSize()
3167 def getFloatingPointExponentSize(self):
3169 :return: the bit-width of the exponent of the floating-point sort
3171 return self.csort.getFloatingPointExponentSize()
3173 def getFloatingPointSignificandSize(self):
3175 :return: the width of the significand of the floating-point sort
3177 return self.csort.getFloatingPointSignificandSize()
3179 def getDatatypeArity(self):
3181 :return: the arity of a datatype sort
3183 return self.csort.getDatatypeArity()
3185 def getTupleLength(self):
3187 :return: the length of a tuple sort
3189 return self.csort.getTupleLength()
3191 def getTupleSorts(self):
3193 :return: the element sorts of a tuple sort
3196 for s in self.csort.getTupleSorts():
3197 sort = Sort(self.solver)
3199 tuple_sorts.append(sort)
3203 cdef class Statistics:
3205 The cvc5 Statistics.
3206 Wrapper class for :cpp:class:`cvc5::Statistics`.
3207 Obtain a single statistic value using ``stats["name"]`` and a dictionary
3208 with all (visible) statistics using ``stats.get(internal=False, defaulted=False)``.
3210 cdef c_Statistics cstats
3212 cdef __stat_to_dict(self, const c_Stat& s):
3219 res = s.getString().decode()
3220 elif s.isHistogram():
3221 res = { h.first.decode(): h.second for h in s.getHistogram() }
3223 'defaulted': s.isDefault(),
3224 'internal': s.isInternal(),
3228 def __getitem__(self, str name):
3229 """Get the statistics information for the statistic called ``name``."""
3230 return self.__stat_to_dict(self.cstats.get(name.encode()))
3232 def get(self, bint internal = False, bint defaulted = False):
3233 """Get all statistics. See :cpp:class:`cvc5::Statistics::begin()` for more information."""
3234 cdef c_Statistics.iterator it = self.cstats.begin(internal, defaulted)
3235 cdef pair[string,c_Stat]* s
3237 while it != self.cstats.end():
3238 s = &dereference(it)
3239 res[s.first.decode()] = self.__stat_to_dict(s.second)
3247 Wrapper class for :cpp:class:`cvc5::Term`.
3251 def __cinit__(self, Solver solver):
3252 # cterm always set in the Solver object
3253 self.solver = solver
3255 def __eq__(self, Term other):
3256 return self.cterm == other.cterm
3258 def __ne__(self, Term other):
3259 return self.cterm != other.cterm
3261 def __lt__(self, Term other):
3262 return self.cterm < other.cterm
3264 def __gt__(self, Term other):
3265 return self.cterm > other.cterm
3267 def __le__(self, Term other):
3268 return self.cterm <= other.cterm
3270 def __ge__(self, Term other):
3271 return self.cterm >= other.cterm
3273 def __getitem__(self, int index):
3274 cdef Term term = Term(self.solver)
3276 term.cterm = self.cterm[index]
3278 raise ValueError("Expecting a non-negative integer or string")
3282 return self.cterm.toString().decode()
3285 return self.cterm.toString().decode()
3288 for ci in self.cterm:
3289 term = Term(self.solver)
3294 return ctermhash(self.cterm)
3296 def getNumChildren(self):
3297 """:return: the number of children of this term."""
3298 return self.cterm.getNumChildren()
3301 """:return: the id of this term."""
3302 return self.cterm.getId()
3305 """:return: the :py:class:`cvc5.Kind` of this term."""
3306 return Kind(<int> self.cterm.getKind())
3309 """:return: the :py:class:`cvc5.Sort` of this term."""
3310 cdef Sort sort = Sort(self.solver)
3311 sort.csort = self.cterm.getSort()
3314 def substitute(self, term_or_list_1, term_or_list_2):
3316 :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.
3318 Note that this replacement is applied during a pre-order traversal and
3319 only once to the term. It is not run until fix point. In the case that
3320 terms contains duplicates, the replacement earliest in the list takes
3321 priority. For example, calling substitute on ``f(x,y)`` with
3325 term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ]
3327 results in the term ``f(g(z),y)``.
3329 # The resulting term after substitution
3330 cdef Term term = Term(self.solver)
3331 # lists for substitutions
3332 cdef vector[c_Term] ces
3333 cdef vector[c_Term] creplacements
3335 # normalize the input parameters to be lists
3336 if isinstance(term_or_list_1, list):
3337 assert isinstance(term_or_list_2, list)
3339 replacements = term_or_list_2
3340 if len(es) != len(replacements):
3341 raise RuntimeError("Expecting list inputs to substitute to "
3342 "have the same length but got: "
3343 "{} and {}".format(len(es), len(replacements)))
3345 for e, r in zip(es, replacements):
3346 ces.push_back((<Term?> e).cterm)
3347 creplacements.push_back((<Term?> r).cterm)
3350 # add the single elements to the vectors
3351 ces.push_back((<Term?> term_or_list_1).cterm)
3352 creplacements.push_back((<Term?> term_or_list_2).cterm)
3354 # call the API substitute method with lists
3355 term.cterm = self.cterm.substitute(ces, creplacements)
3359 """:return: True iff this term has an operator."""
3360 return self.cterm.hasOp()
3364 .. note:: This is safe to call when :py:meth:`hasOp()` returns True.
3366 :return: the :py:class:`cvc5.Op` used to create this Term.
3368 cdef Op op = Op(self.solver)
3369 op.cop = self.cterm.getOp()
3372 def hasSymbol(self):
3373 """:return: True iff this term has a symbol."""
3374 return self.cterm.hasSymbol()
3376 def getSymbol(self):
3378 Asserts :py:meth:`hasSymbol()`.
3380 :return: the raw symbol of the term.
3382 return self.cterm.getSymbol().decode()
3385 """:return: True iff this term is a null term."""
3386 return self.cterm.isNull()
3392 :return: the Boolean negation of this term.
3394 cdef Term term = Term(self.solver)
3395 term.cterm = self.cterm.notTerm()
3398 def andTerm(self, Term t):
3402 :param t: a Boolean term
3403 :return: the conjunction of this term and the given term
3405 cdef Term term = Term(self.solver)
3406 term.cterm = self.cterm.andTerm((<Term> t).cterm)
3409 def orTerm(self, Term t):
3413 :param t: a Boolean term
3414 :return: the disjunction of this term and the given term
3416 cdef Term term = Term(self.solver)
3417 term.cterm = self.cterm.orTerm(t.cterm)
3420 def xorTerm(self, Term t):
3422 Boolean exclusive or.
3424 :param t: a Boolean term
3425 :return: the exclusive disjunction of this term and the given term
3427 cdef Term term = Term(self.solver)
3428 term.cterm = self.cterm.xorTerm(t.cterm)
3431 def eqTerm(self, Term t):
3435 :param t: a Boolean term
3436 :return: the Boolean equivalence of this term and the given term
3438 cdef Term term = Term(self.solver)
3439 term.cterm = self.cterm.eqTerm(t.cterm)
3442 def impTerm(self, Term t):
3444 Boolean Implication.
3446 :param t: a Boolean term
3447 :return: the implication of this term and the given term
3449 cdef Term term = Term(self.solver)
3450 term.cterm = self.cterm.impTerm(t.cterm)
3453 def iteTerm(self, Term then_t, Term else_t):
3455 If-then-else with this term as the Boolean condition.
3457 :param then_t: the `then` term
3458 :param else_t: the `else` term
3459 :return: the if-then-else term with this term as the Boolean condition
3461 cdef Term term = Term(self.solver)
3462 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
3465 def isConstArray(self):
3466 """:return: True iff this term is a constant array."""
3467 return self.cterm.isConstArray()
3469 def getConstArrayBase(self):
3471 Asserts :py:meth:`isConstArray()`.
3473 :return: the base (element stored at all indicies) of this constant array
3475 cdef Term term = Term(self.solver)
3476 term.cterm = self.cterm.getConstArrayBase()
3479 def isBooleanValue(self):
3480 """:return: True iff this term is a Boolean value."""
3481 return self.cterm.isBooleanValue()
3483 def getBooleanValue(self):
3485 Asserts :py:meth:`isBooleanValue()`
3487 :return: the representation of a Boolean value as a native Boolean value.
3489 return self.cterm.getBooleanValue()
3491 def isStringValue(self):
3492 """:return: True iff this term is a string value."""
3493 return self.cterm.isStringValue()
3495 def getStringValue(self):
3497 Asserts :py:meth:`isStringValue()`.
3500 This method is not to be confused with :py:meth:`__str__()` which
3501 returns the term in some string representation, whatever data it
3504 :return: the string term as a native string value.
3506 cdef Py_ssize_t size
3507 cdef c_wstring s = self.cterm.getStringValue()
3508 return PyUnicode_FromWideChar(s.data(), s.size())
3510 def getRealOrIntegerValueSign(self):
3512 Get integer or real value sign. Must be called on integer or real values,
3513 or otherwise an exception is thrown.
3515 :return: 0 if this term is zero, -1 if this term is a negative real or
3516 integer value, 1 if this term is a positive real or integer
3519 return self.cterm.getRealOrIntegerValueSign()
3521 def isIntegerValue(self):
3522 """:return: True iff this term is an integer value."""
3523 return self.cterm.isIntegerValue()
3525 def getIntegerValue(self):
3527 Asserts :py:meth:`isIntegerValue()`.
3529 :return: the integer term as a native python integer.
3531 return int(self.cterm.getIntegerValue().decode())
3533 def isFloatingPointPosZero(self):
3534 """:return: True iff the term is the floating-point value for positive zero."""
3535 return self.cterm.isFloatingPointPosZero()
3537 def isFloatingPointNegZero(self):
3538 """:return: True iff the term is the floating-point value for negative zero."""
3539 return self.cterm.isFloatingPointNegZero()
3541 def isFloatingPointPosInf(self):
3542 """:return: True iff the term is the floating-point value for positive infinity."""
3543 return self.cterm.isFloatingPointPosInf()
3545 def isFloatingPointNegInf(self):
3546 """:return: True iff the term is the floating-point value for negative infinity."""
3547 return self.cterm.isFloatingPointNegInf()
3549 def isFloatingPointNaN(self):
3550 """:return: True iff the term is the floating-point value for not a number."""
3551 return self.cterm.isFloatingPointNaN()
3553 def isFloatingPointValue(self):
3554 """:return: True iff this term is a floating-point value."""
3555 return self.cterm.isFloatingPointValue()
3557 def getFloatingPointValue(self):
3559 Asserts :py:meth:`isFloatingPointValue()`.
3561 :return: the representation of a floating-point value as a tuple of the exponent width, the significand width and a bit-vector value.
3563 cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
3564 cdef Term term = Term(self.solver)
3565 term.cterm = get2(t)
3566 return (get0(t), get1(t), term)
3568 def isSetValue(self):
3570 A term is a set value if it is considered to be a (canonical) constant
3571 set value. A canonical set value is one whose AST is:
3576 (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
3578 where ``c1 ... cn`` are values ordered by id such that
3579 ``c1 > ... > cn`` (see also :cpp:func:`cvc5::Term::operator>()`).
3582 A universe set term ``(kind SET_UNIVERSE)`` is not considered to be
3585 :return: True if the term is a set value.
3587 return self.cterm.isSetValue()
3589 def getSetValue(self):
3591 Asserts :py:meth:`isSetValue()`.
3593 :return: the representation of a set value as a set of terms.
3596 for e in self.cterm.getSetValue():
3597 term = Term(self.solver)
3602 def isSequenceValue(self):
3603 """:return: True iff this term is a sequence value."""
3604 return self.cterm.isSequenceValue()
3606 def getSequenceValue(self):
3608 Asserts :py:meth:`isSequenceValue()`.
3611 It is usually necessary for sequences to call
3612 :py:meth:`Solver.simplify()` to turn a sequence that is constructed
3613 by, e.g., concatenation of unit sequences, into a sequence value.
3615 :return: the representation of a sequence value as a vector of terms.
3618 for e in self.cterm.getSequenceValue():
3619 term = Term(self.solver)
3624 def isCardinalityConstraint(self):
3626 .. warning:: This method is experimental and may change in future
3628 :return: True if the term is a cardinality constraint.
3630 return self.cterm.isCardinalityConstraint()
3632 def getCardinalityConstraint(self):
3634 .. warning:: This method is experimental and may change in future
3636 :return: the sort the cardinality constraint is for and its upper bound.
3638 cdef pair[c_Sort, uint32_t] p
3639 p = self.cterm.getCardinalityConstraint()
3640 cdef Sort sort = Sort(self.solver)
3641 sort.csort = p.first
3642 return (sort, p.second)
3645 def isUninterpretedSortValue(self):
3646 """:return: True iff this term is a value from an uninterpreted sort."""
3647 return self.cterm.isUninterpretedSortValue()
3649 def getUninterpretedSortValue(self):
3651 Asserts :py:meth:`isUninterpretedSortValue()`.
3653 :return: the representation of an uninterpreted value as a pair of its sort and its index.
3655 return self.cterm.getUninterpretedSortValue()
3657 def isTupleValue(self):
3658 """:return: True iff this term is a tuple value."""
3659 return self.cterm.isTupleValue()
3661 def isRoundingModeValue(self):
3662 """:return: True if the term is a floating-point rounding mode value."""
3663 return self.cterm.isRoundingModeValue()
3665 def getRoundingModeValue(self):
3667 Asserts isRoundingModeValue().
3668 :return: the floating-point rounding mode value held by the term.
3670 return RoundingMode(<int> self.cterm.getRoundingModeValue())
3672 def getTupleValue(self):
3674 Asserts :py:meth:`isTupleValue()`.
3676 :return: the representation of a tuple value as a vector of terms.
3679 for e in self.cterm.getTupleValue():
3680 term = Term(self.solver)
3685 def isRealValue(self):
3687 .. note:: A term of kind PI is not considered to be a real value.
3689 :return: True iff this term is a rational value.
3691 return self.cterm.isRealValue()
3693 def getRealValue(self):
3695 Asserts :py:meth:`isRealValue()`.
3697 :return: the representation of a rational value as a python Fraction.
3699 return Fraction(self.cterm.getRealValue().decode())
3701 def isBitVectorValue(self):
3702 """:return: True iff this term is a bit-vector value."""
3703 return self.cterm.isBitVectorValue()
3705 def getBitVectorValue(self, base = 2):
3707 Asserts :py:meth:`isBitVectorValue()`.
3708 Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexdecimal string).
3710 :return: the representation of a bit-vector value in string representation.
3712 return self.cterm.getBitVectorValue(base).decode()
3714 def toPythonObj(self):
3716 Converts a constant value Term to a Python object.
3720 - Boolean -- returns a Python bool
3721 - Int -- returns a Python int
3722 - Real -- returns a Python Fraction
3723 - BV -- returns a Python int (treats BV as unsigned)
3724 - String -- returns a Python Unicode string
3725 - Array -- returns a Python dict mapping indices to values. the constant base is returned as the default value
3729 if self.isBooleanValue():
3730 return self.getBooleanValue()
3731 elif self.isIntegerValue():
3732 return self.getIntegerValue()
3733 elif self.isRealValue():
3734 return self.getRealValue()
3735 elif self.isBitVectorValue():
3736 return int(self.getBitVectorValue(), 2)
3737 elif self.isStringValue():
3738 return self.getStringValue()
3739 elif self.getSort().isArray():
3745 # Array models are represented as a series of store operations
3746 # on a constant array
3749 if t.getKind().value == c_Kind.STORE:
3751 keys.append(t[1].toPythonObj())
3752 values.append(t[2].toPythonObj())
3753 to_visit.append(t[0])
3755 assert t.getKind().value == c_Kind.CONST_ARRAY
3756 base_value = t.getConstArrayBase().toPythonObj()
3758 assert len(keys) == len(values)
3759 assert base_value is not None
3761 # put everything in a dictionary with the constant
3762 # base as the result for any index not included in the stores
3763 res = defaultdict(lambda : base_value)
3764 for k, v in zip(keys, values):