1 from collections import defaultdict, Set
2 from fractions import Fraction
3 from functools import wraps
6 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
7 from libc.stddef cimport wchar_t
9 from libcpp.pair cimport pair
10 from libcpp.set cimport set as c_set
11 from libcpp.string cimport string
12 from libcpp.vector cimport vector
14 from cvc5 cimport cout
15 from cvc5 cimport Datatype as c_Datatype
16 from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
17 from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
18 from cvc5 cimport DatatypeDecl as c_DatatypeDecl
19 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
20 from cvc5 cimport Result as c_Result
21 from cvc5 cimport RoundingMode as c_RoundingMode
22 from cvc5 cimport UnknownExplanation as c_UnknownExplanation
23 from cvc5 cimport Op as c_Op
24 from cvc5 cimport Solver as c_Solver
25 from cvc5 cimport Grammar as c_Grammar
26 from cvc5 cimport Sort as c_Sort
27 from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
28 from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
29 from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
30 from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT
31 from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED
32 from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON
33 from cvc5 cimport OTHER
34 from cvc5 cimport Term as c_Term
35 from cvc5 cimport hash as c_hash
36 from cvc5 cimport wstring as c_wstring
37 from cvc5 cimport tuple as c_tuple
38 from cvc5 cimport get0, get1, get2
39 from cvc5kinds cimport Kind as c_Kind
41 cdef extern from "Python.h":
42 wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
43 object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
44 void PyMem_Free(void*)
46 ################################## DECORATORS #################################
47 def expand_list_arg(num_req_args=0):
49 Creates a decorator that looks at index num_req_args of the args,
50 if it's a list, it expands it before calling the function.
54 def wrapper(owner, *args):
55 if len(args) == num_req_args + 1 and \
56 isinstance(args[num_req_args], list):
57 args = list(args[:num_req_args]) + args[num_req_args]
58 return func(owner, *args)
61 ###############################################################################
64 ### Using PEP-8 spacing recommendations
65 ### Limit linewidth to 79 characters
66 ### Break before binary operators
67 ### surround top level functions and classes with two spaces
68 ### separate methods by one space
69 ### use spaces in functions sparingly to separate logical blocks
70 ### can omit spaces between unrelated oneliners
71 ### always use c++ default arguments
72 #### only use default args of None at python level
74 # References and pointers
75 # The Solver object holds a pointer to a c_Solver.
76 # This is because the assignment operator is deleted in the C++ API for solvers.
77 # Cython has a limitation where you can't stack allocate objects
78 # that have constructors with arguments:
79 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
80 # To get around that you can either have a nullary constructor and assignment
81 # or, use a pointer (which is what we chose).
82 # An additional complication of this is that to free up resources, you must
83 # know when to delete the object.
84 # Python will not follow the same scoping rules as in C++, so it must be
85 # able to reference count. To do this correctly, the solver must be a
86 # reference in the Python class for any class that keeps a pointer to
87 # the solver in C++ (to ensure the solver is not deleted before something
88 # that depends on it).
91 ## Objects for hashing
92 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
93 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
94 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
100 Wrapper class for :cpp:class:`cvc5::api::Datatype`.
104 def __cinit__(self, Solver solver):
107 def __getitem__(self, index):
108 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
109 if isinstance(index, int) and index >= 0:
110 dc.cdc = self.cd[(<int?> index)]
111 elif isinstance(index, str):
112 dc.cdc = self.cd[(<const string &> index.encode())]
114 raise ValueError("Expecting a non-negative integer or string")
117 def getConstructor(self, str name):
119 :param name: the name of the constructor.
120 :return: a constructor by name.
122 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
123 dc.cdc = self.cd.getConstructor(name.encode())
126 def getConstructorTerm(self, str name):
128 :param name: the name of the constructor.
129 :return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`).
131 cdef Term term = Term(self.solver)
132 term.cterm = self.cd.getConstructorTerm(name.encode())
135 def getSelector(self, str name):
137 :param name: the name of the selector..
138 :return: a selector by name.
140 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
141 ds.cds = self.cd.getSelector(name.encode())
146 :return: the name of the datatype.
148 return self.cd.getName().decode()
150 def getNumConstructors(self):
152 :return: number of constructors in this datatype.
154 return self.cd.getNumConstructors()
156 def isParametric(self):
157 """:return: True if this datatype is parametric."""
158 return self.cd.isParametric()
160 def isCodatatype(self):
161 """:return: True if this datatype corresponds to a co-datatype."""
162 return self.cd.isCodatatype()
165 """:return: True if this datatype corresponds to a tuple."""
166 return self.cd.isTuple()
169 """:return: True if this datatype corresponds to a record."""
170 return self.cd.isRecord()
173 """:return: True if this datatype is finite."""
174 return self.cd.isFinite()
176 def isWellFounded(self):
177 """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
178 return self.cd.isWellFounded()
180 def hasNestedRecursion(self):
181 """:return: True if this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
182 return self.cd.hasNestedRecursion()
185 """:return: True if this Datatype is a null object."""
186 return self.cd.isNull()
189 return self.cd.toString().decode()
192 return self.cd.toString().decode()
196 dc = DatatypeConstructor(self.solver)
201 cdef class DatatypeConstructor:
203 A cvc5 datatype constructor.
204 Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.
206 cdef c_DatatypeConstructor cdc
208 def __cinit__(self, Solver solver):
209 self.cdc = c_DatatypeConstructor()
212 def __getitem__(self, index):
213 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
214 if isinstance(index, int) and index >= 0:
215 ds.cds = self.cdc[(<int?> index)]
216 elif isinstance(index, str):
217 ds.cds = self.cdc[(<const string &> index.encode())]
219 raise ValueError("Expecting a non-negative integer or string")
224 :return: the name of the constructor.
226 return self.cdc.getName().decode()
228 def getConstructorTerm(self):
230 :return: the constructor operator as a term.
232 cdef Term term = Term(self.solver)
233 term.cterm = self.cdc.getConstructorTerm()
236 def getSpecializedConstructorTerm(self, Sort retSort):
238 Specialized method for parametric datatypes (see :cpp:func:`DatatypeConstructor::getSpecializedConstructorTerm() <cvc5::api::DatatypeConstructor::getSpecializedConstructorTerm>`).
240 :param retSort: the desired return sort of the constructor
241 :return: the constructor operator as a term.
243 cdef Term term = Term(self.solver)
244 term.cterm = self.cdc.getSpecializedConstructorTerm(retSort.csort)
247 def getTesterTerm(self):
249 :return: the tester operator that is related to this constructor, as a term.
251 cdef Term term = Term(self.solver)
252 term.cterm = self.cdc.getTesterTerm()
255 def getNumSelectors(self):
257 :return: the number of selecters (so far) of this Datatype constructor.
259 return self.cdc.getNumSelectors()
261 def getSelector(self, str name):
263 :param name: the name of the datatype selector.
264 :return: the first datatype selector with the given name
266 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
267 ds.cds = self.cdc.getSelector(name.encode())
270 def getSelectorTerm(self, str name):
272 :param name: the name of the datatype selector.
273 :return: a term representing the firstdatatype selector with the given name.
275 cdef Term term = Term(self.solver)
276 term.cterm = self.cdc.getSelectorTerm(name.encode())
280 """:return: True if this DatatypeConstructor is a null object."""
281 return self.cdc.isNull()
284 return self.cdc.toString().decode()
287 return self.cdc.toString().decode()
291 ds = DatatypeSelector(self.solver)
296 cdef class DatatypeConstructorDecl:
298 A cvc5 datatype constructor declaration.
299 Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.
301 cdef c_DatatypeConstructorDecl cddc
304 def __cinit__(self, Solver solver):
307 def addSelector(self, str name, Sort sort):
309 Add datatype selector declaration.
311 :param name: the name of the datatype selector declaration to add.
312 :param sort: the range sort of the datatype selector declaration to add.
314 self.cddc.addSelector(name.encode(), sort.csort)
316 def addSelectorSelf(self, str name):
318 Add datatype selector declaration whose range sort is the datatype itself.
320 :param name: the name of the datatype selector declaration to add.
322 self.cddc.addSelectorSelf(name.encode())
325 """:return: True if this DatatypeConstructorDecl is a null object."""
326 return self.cddc.isNull()
329 return self.cddc.toString().decode()
332 return self.cddc.toString().decode()
335 cdef class DatatypeDecl:
337 A cvc5 datatype declaration.
338 Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.
340 cdef c_DatatypeDecl cdd
342 def __cinit__(self, Solver solver):
345 def addConstructor(self, DatatypeConstructorDecl ctor):
347 Add a datatype constructor declaration.
349 :param ctor: the datatype constructor declaration to add.
351 self.cdd.addConstructor(ctor.cddc)
353 def getNumConstructors(self):
355 :return: number of constructors (so far) for this datatype declaration.
357 return self.cdd.getNumConstructors()
359 def isParametric(self):
361 :return: is this datatype declaration parametric?
363 return self.cdd.isParametric()
367 :return: the name of this datatype declaration.
369 return self.cdd.getName().decode()
372 """:return: True if this DatatypeDecl is a null object."""
373 return self.cdd.isNull()
376 return self.cdd.toString().decode()
379 return self.cdd.toString().decode()
382 cdef class DatatypeSelector:
384 A cvc5 datatype selector.
385 Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.
387 cdef c_DatatypeSelector cds
389 def __cinit__(self, Solver solver):
390 self.cds = c_DatatypeSelector()
395 :return: the name of this datatype selector.
397 return self.cds.getName().decode()
399 def getSelectorTerm(self):
401 :return: the selector opeartor of this datatype selector as a term.
403 cdef Term term = Term(self.solver)
404 term.cterm = self.cds.getSelectorTerm()
407 def getUpdaterTerm(self):
409 :return: the updater opeartor of this datatype selector as a term.
411 cdef Term term = Term(self.solver)
412 term.cterm = self.cds.getUpdaterTerm()
415 def getRangeSort(self):
417 :return: the range sort of this selector.
419 cdef Sort sort = Sort(self.solver)
420 sort.csort = self.cds.getRangeSort()
424 """:return: True if this DatatypeSelector is a null object."""
425 return self.cds.isNull()
428 return self.cds.toString().decode()
431 return self.cds.toString().decode()
437 An operator is a term that represents certain operators,
438 instantiated with its required parameters, e.g.,
439 a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`.
440 Wrapper class for :cpp:class:`cvc5::api::Op`.
444 def __cinit__(self, Solver solver):
448 def __eq__(self, Op other):
449 return self.cop == other.cop
451 def __ne__(self, Op other):
452 return self.cop != other.cop
455 return self.cop.toString().decode()
458 return self.cop.toString().decode()
461 return cophash(self.cop)
465 :return: the kind of this operator.
467 return kind(<int> self.cop.getKind())
471 :return: True iff this operator is indexed.
473 return self.cop.isIndexed()
477 :return: True iff this operator is a null term.
479 return self.cop.isNull()
481 def getNumIndices(self):
483 :return: number of indices of this op.
485 return self.cop.getNumIndices()
487 def getIndices(self):
489 :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() <cvc5::api::Op::getIndices>`).
493 indices = self.cop.getIndices[string]().decode()
498 indices = self.cop.getIndices[uint32_t]()
503 indices = self.cop.getIndices[pair[uint32_t, uint32_t]]()
508 raise RuntimeError("Unable to retrieve indices from {}".format(self))
515 Wrapper class for :cpp:class:`cvc5::api::Grammar`.
517 cdef c_Grammar cgrammar
519 def __cinit__(self, Solver solver):
521 self.cgrammar = c_Grammar()
523 def addRule(self, Term ntSymbol, Term rule):
525 Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
527 :param ntSymbol: the non-terminal to which the rule is added.
528 :param rule: the rule to add.
530 self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
532 def addAnyConstant(self, Term ntSymbol):
534 Allow ``ntSymbol`` to be an arbitrary constant.
536 :param ntSymbol: the non-terminal allowed to be constant.
538 self.cgrammar.addAnyConstant(ntSymbol.cterm)
540 def addAnyVariable(self, Term ntSymbol):
542 Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``.
544 :param ntSymbol: the non-terminal allowed to be any input variable.
546 self.cgrammar.addAnyVariable(ntSymbol.cterm)
548 def addRules(self, Term ntSymbol, rules):
550 Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
552 :param ntSymbol: the non-terminal to which the rules are added.
553 :param rules: the rules to add.
555 cdef vector[c_Term] crules
557 crules.push_back((<Term?> r).cterm)
558 self.cgrammar.addRules(ntSymbol.cterm, crules)
562 Encapsulation of a three-valued solver result, with explanations.
563 Wrapper class for :cpp:class:`cvc5::api::Result`.
567 # gets populated by solver
572 :return: True if Result is empty, i.e., a nullary Result, and not an actual result returned from a
573 :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` (and friends) query.
575 return self.cr.isNull()
579 :return: True if query was a satisfiable :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query.
581 return self.cr.isSat()
585 :return: True if query was an usatisfiable :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query.
587 return self.cr.isUnsat()
589 def isSatUnknown(self):
591 :return: True if query was a :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query and cvc5 was not able to determine (un)satisfiability.
593 return self.cr.isSatUnknown()
595 def isEntailed(self):
597 :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query.
599 return self.cr.isEntailed()
601 def isNotEntailed(self):
603 :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query that is not entailed.
605 return self.cr.isNotEntailed()
607 def isEntailmentUnknown(self):
609 :return: True if query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query query and cvc5 was not able to determine if it is entailed.
611 return self.cr.isEntailmentUnknown()
613 def getUnknownExplanation(self):
615 :return: an explanation for an unknown query result.
617 return UnknownExplanation(<int> self.cr.getUnknownExplanation())
619 def __eq__(self, Result other):
620 return self.cr == other.cr
622 def __ne__(self, Result other):
623 return self.cr != other.cr
626 return self.cr.toString().decode()
629 return self.cr.toString().decode()
632 cdef class RoundingMode:
634 Rounding modes for floating-point numbers.
636 For many floating-point operations, infinitely precise results may not be
637 representable with the number of available bits. Thus, the results are
638 rounded in a certain way to one of the representable floating-point numbers.
640 These rounding modes directly follow the SMT-LIB theory for floating-point
641 arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
642 The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
645 Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`.
647 cdef c_RoundingMode crm
649 def __cinit__(self, int rm):
650 # crm always assigned externally
651 self.crm = <c_RoundingMode> rm
652 self.name = __rounding_modes[rm]
654 def __eq__(self, RoundingMode other):
655 return (<int> self.crm) == (<int> other.crm)
657 def __ne__(self, RoundingMode other):
658 return not self.__eq__(other)
661 return hash((<int> self.crm, self.name))
670 cdef class UnknownExplanation:
672 Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`.
674 cdef c_UnknownExplanation cue
676 def __cinit__(self, int ue):
677 # crm always assigned externally
678 self.cue = <c_UnknownExplanation> ue
679 self.name = __unknown_explanations[ue]
681 def __eq__(self, UnknownExplanation other):
682 return (<int> self.cue) == (<int> other.cue)
684 def __ne__(self, UnknownExplanation other):
685 return not self.__eq__(other)
688 return hash((<int> self.crm, self.name))
698 """Wrapper class for :cpp:class:`cvc5::api::Solver`."""
699 cdef c_Solver* csolver
702 self.csolver = new c_Solver()
704 def __dealloc__(self):
707 def getBooleanSort(self):
708 """:return: sort Boolean
710 cdef Sort sort = Sort(self)
711 sort.csort = self.csolver.getBooleanSort()
714 def getIntegerSort(self):
715 """:return: sort Integer
717 cdef Sort sort = Sort(self)
718 sort.csort = self.csolver.getIntegerSort()
721 def getNullSort(self):
722 """:return: sort null
724 cdef Sort sort = Sort(self)
725 sort.csort = self.csolver.getNullSort()
728 def getRealSort(self):
729 """:return: sort Real
731 cdef Sort sort = Sort(self)
732 sort.csort = self.csolver.getRealSort()
735 def getRegExpSort(self):
736 """:return: sort of RegExp
738 cdef Sort sort = Sort(self)
739 sort.csort = self.csolver.getRegExpSort()
742 def getRoundingModeSort(self):
743 """:return: sort RoundingMode
745 cdef Sort sort = Sort(self)
746 sort.csort = self.csolver.getRoundingModeSort()
749 def getStringSort(self):
750 """:return: sort String
752 cdef Sort sort = Sort(self)
753 sort.csort = self.csolver.getStringSort()
756 def mkArraySort(self, Sort indexSort, Sort elemSort):
757 """Create an array sort.
759 :param indexSort: the array index sort
760 :param elemSort: the array element sort
761 :return: the array sort
763 cdef Sort sort = Sort(self)
764 sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
767 def mkBitVectorSort(self, uint32_t size):
768 """Create a bit-vector sort.
770 :param size: the bit-width of the bit-vector sort
771 :return: the bit-vector sort
773 cdef Sort sort = Sort(self)
774 sort.csort = self.csolver.mkBitVectorSort(size)
777 def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
778 """Create a floating-point sort.
780 :param exp: the bit-width of the exponent of the floating-point sort.
781 :param sig: the bit-width of the significand of the floating-point sort.
783 cdef Sort sort = Sort(self)
784 sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
787 def mkDatatypeSort(self, DatatypeDecl dtypedecl):
788 """Create a datatype sort.
790 :param dtypedecl: the datatype declaration from which the sort is created
791 :return: the datatype sort
793 cdef Sort sort = Sort(self)
794 sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
797 def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
799 Create a vector of datatype sorts using unresolved sorts. The names of
800 the datatype declarations in dtypedecls must be distinct.
802 This method is called when the DatatypeDecl objects dtypedecls have been
803 built using "unresolved" sorts.
805 We associate each sort in unresolvedSorts with exacly one datatype from
806 dtypedecls. In particular, it must have the same name as exactly one
807 datatype declaration in dtypedecls.
809 When constructing datatypes, unresolved sorts are replaced by the datatype
810 sort constructed for the datatype declaration it is associated with.
812 :param dtypedecls: the datatype declarations from which the sort is created
813 :param unresolvedSorts: the list of unresolved sorts
814 :return: the datatype sorts
816 if unresolvedSorts == None:
817 unresolvedSorts = set([])
819 assert isinstance(unresolvedSorts, Set)
822 cdef vector[c_DatatypeDecl] decls
823 for decl in dtypedecls:
824 decls.push_back((<DatatypeDecl?> decl).cdd)
826 cdef c_set[c_Sort] usorts
827 for usort in unresolvedSorts:
828 usorts.insert((<Sort?> usort).csort)
830 csorts = self.csolver.mkDatatypeSorts(
831 <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
839 def mkFunctionSort(self, sorts, Sort codomain):
840 """ Create function sort.
842 :param sorts: the sort of the function arguments
843 :param codomain: the sort of the function return value
844 :return: the function sort
847 cdef Sort sort = Sort(self)
848 # populate a vector with dereferenced c_Sorts
849 cdef vector[c_Sort] v
851 if isinstance(sorts, Sort):
852 sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
854 elif isinstance(sorts, list):
856 v.push_back((<Sort?>s).csort)
858 sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
862 def mkParamSort(self, symbolname):
863 """ Create a sort parameter.
865 :param symbol: the name of the sort
866 :return: the sort parameter
868 cdef Sort sort = Sort(self)
869 sort.csort = self.csolver.mkParamSort(symbolname.encode())
872 @expand_list_arg(num_req_args=0)
873 def mkPredicateSort(self, *sorts):
874 """Create a predicate sort.
876 :param sorts: the list of sorts of the predicate, as a list or as distinct arguments.
877 :return: the predicate sort
879 cdef Sort sort = Sort(self)
880 cdef vector[c_Sort] v
882 v.push_back((<Sort?> s).csort)
883 sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
886 @expand_list_arg(num_req_args=0)
887 def mkRecordSort(self, *fields):
888 """Create a record sort
890 :param fields: the list of fields of the record, as a list or as distinct arguments
891 :return: the record sort
893 cdef Sort sort = Sort(self)
894 cdef vector[pair[string, c_Sort]] v
895 cdef pair[string, c_Sort] p
899 p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
901 sort.csort = self.csolver.mkRecordSort(
902 <const vector[pair[string, c_Sort]] &> v)
905 def mkSetSort(self, Sort elemSort):
906 """Create a set sort.
908 :param elemSort: the sort of the set elements
909 :return: the set sort
911 cdef Sort sort = Sort(self)
912 sort.csort = self.csolver.mkSetSort(elemSort.csort)
915 def mkBagSort(self, Sort elemSort):
916 """Create a bag sort.
918 :param elemSort: the sort of the bag elements
919 :return: the bag sort
921 cdef Sort sort = Sort(self)
922 sort.csort = self.csolver.mkBagSort(elemSort.csort)
925 def mkSequenceSort(self, Sort elemSort):
926 """Create a sequence sort.
928 :param elemSort: the sort of the sequence elements
929 :return: the sequence sort
931 cdef Sort sort = Sort(self)
932 sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
935 def mkUninterpretedSort(self, str name):
936 """Create an uninterpreted sort.
938 :param symbol: the name of the sort
939 :return: the uninterpreted sort
941 cdef Sort sort = Sort(self)
942 sort.csort = self.csolver.mkUninterpretedSort(name.encode())
945 def mkSortConstructorSort(self, str symbol, size_t arity):
946 """Create a sort constructor sort.
948 :param symbol: the symbol of the sort
949 :param arity: the arity of the sort
950 :return: the sort constructor sort
952 cdef Sort sort = Sort(self)
953 sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
956 @expand_list_arg(num_req_args=0)
957 def mkTupleSort(self, *sorts):
958 """Create a tuple sort.
960 :param sorts: of the elements of the tuple, as a list or as distinct arguments
961 :return: the tuple sort
963 cdef Sort sort = Sort(self)
964 cdef vector[c_Sort] v
966 v.push_back((<Sort?> s).csort)
967 sort.csort = self.csolver.mkTupleSort(v)
970 @expand_list_arg(num_req_args=1)
971 def mkTerm(self, kind_or_op, *args):
973 Supports the following arguments:
975 - ``Term mkTerm(Kind kind)``
976 - ``Term mkTerm(Kind kind, Op child1, List[Term] children)``
977 - ``Term mkTerm(Kind kind, List[Term] children)``
979 where ``List[Term]`` can also be comma-separated arguments
981 cdef Term term = Term(self)
982 cdef vector[c_Term] v
985 if isinstance(kind_or_op, kind):
986 op = self.mkOp(kind_or_op)
989 term.cterm = self.csolver.mkTerm((<Op?> op).cop)
992 v.push_back((<Term?> a).cterm)
993 term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
996 def mkTuple(self, sorts, terms):
997 """Create a tuple term. Terms are automatically converted if sorts are compatible.
999 :param sorts: The sorts of the elements in the tuple
1000 :param terms: The elements in the tuple
1001 :return: the tuple Term
1003 cdef vector[c_Sort] csorts
1004 cdef vector[c_Term] cterms
1007 csorts.push_back((<Sort?> s).csort)
1009 cterms.push_back((<Term?> s).cterm)
1010 cdef Term result = Term(self)
1011 result.cterm = self.csolver.mkTuple(csorts, cterms)
1014 @expand_list_arg(num_req_args=0)
1015 def mkOp(self, kind k, *args):
1017 Supports the following uses:
1019 - ``Op mkOp(Kind kind)``
1020 - ``Op mkOp(Kind kind, Kind k)``
1021 - ``Op mkOp(Kind kind, const string& arg)``
1022 - ``Op mkOp(Kind kind, uint32_t arg)``
1023 - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
1024 - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind)
1026 cdef Op op = Op(self)
1027 cdef vector[uint32_t] v
1030 op.cop = self.csolver.mkOp(k.k)
1031 elif len(args) == 1:
1032 if isinstance(args[0], str):
1033 op.cop = self.csolver.mkOp(k.k,
1036 elif isinstance(args[0], int):
1037 op.cop = self.csolver.mkOp(k.k, <int?> args[0])
1038 elif isinstance(args[0], list):
1040 if a < 0 or a >= 2 ** 31:
1041 raise ValueError("Argument {} must fit in a uint32_t".format(a))
1043 v.push_back((<uint32_t?> a))
1044 op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v)
1046 raise ValueError("Unsupported signature"
1047 " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
1048 elif len(args) == 2:
1049 if isinstance(args[0], int) and isinstance(args[1], int):
1050 op.cop = self.csolver.mkOp(k.k, <int> args[0], <int> args[1])
1052 raise ValueError("Unsupported signature"
1053 " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
1057 """Create a Boolean true constant.
1059 :return: the true constant
1061 cdef Term term = Term(self)
1062 term.cterm = self.csolver.mkTrue()
1066 """Create a Boolean false constant.
1068 :return: the false constant
1070 cdef Term term = Term(self)
1071 term.cterm = self.csolver.mkFalse()
1074 def mkBoolean(self, bint val):
1075 """Create a Boolean constant.
1077 :return: the Boolean constant
1078 :param val: the value of the constant
1080 cdef Term term = Term(self)
1081 term.cterm = self.csolver.mkBoolean(val)
1085 """Create a constant representing the number Pi.
1087 :return: a constant representing Pi
1089 cdef Term term = Term(self)
1090 term.cterm = self.csolver.mkPi()
1093 def mkInteger(self, val):
1094 """Create an integer constant.
1096 :param val: representation of the constant: either a string or integer
1097 :return: a constant of sort Integer
1099 cdef Term term = Term(self)
1100 if isinstance(val, str):
1101 term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
1103 assert(isinstance(val, int))
1104 term.cterm = self.csolver.mkInteger((<int?> val))
1107 def mkReal(self, val, den=None):
1108 """Create a real constant.
1110 :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.
1111 :param: `den` if not None, the value is `val`/`den`
1112 :return: a real term with literal value
1114 Can be used in various forms:
1116 - Given a string ``"N/D"`` constructs the corresponding rational.
1117 - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
1118 - 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``.
1119 - Given a string ``"W"`` or an integer, constructs that integer.
1120 - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``.
1122 cdef Term term = Term(self)
1124 term.cterm = self.csolver.mkReal(str(val).encode())
1126 if not isinstance(val, int) or not isinstance(den, int):
1127 raise ValueError("Expecting integers when"
1128 " constructing a rational"
1129 " but got: {}".format((val, den)))
1130 term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
1133 def mkRegexpEmpty(self):
1134 """Create a regular expression empty term.
1136 :return: the empty term
1138 cdef Term term = Term(self)
1139 term.cterm = self.csolver.mkRegexpEmpty()
1142 def mkRegexpSigma(self):
1143 """Create a regular expression sigma term.
1145 :return: the sigma term
1147 cdef Term term = Term(self)
1148 term.cterm = self.csolver.mkRegexpSigma()
1151 def mkEmptySet(self, Sort s):
1152 """Create a constant representing an empty set of the given sort.
1154 :param sort: the sort of the set elements.
1155 :return: the empty set constant
1157 cdef Term term = Term(self)
1158 term.cterm = self.csolver.mkEmptySet(s.csort)
1161 def mkEmptyBag(self, Sort s):
1162 """Create a constant representing an empty bag of the given sort.
1164 :param sort: the sort of the bag elements.
1165 :return: the empty bag constant
1167 cdef Term term = Term(self)
1168 term.cterm = self.csolver.mkEmptyBag(s.csort)
1172 """Create a separation logic empty term.
1174 :return: the separation logic empty term
1176 cdef Term term = Term(self)
1177 term.cterm = self.csolver.mkSepEmp()
1180 def mkSepNil(self, Sort sort):
1181 """Create a separation logic nil term.
1183 :param sort: the sort of the nil term
1184 :return: the separation logic nil term
1186 cdef Term term = Term(self)
1187 term.cterm = self.csolver.mkSepNil(sort.csort)
1190 def mkString(self, str s, useEscSequences = None):
1192 Create a String constant from a `str` which may contain SMT-LIB
1193 compatible escape sequences like ``\\u1234`` to encode unicode characters.
1195 :param s: the string this constant represents
1196 :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character
1197 :return: the String constant
1199 cdef Term term = Term(self)
1200 cdef Py_ssize_t size
1201 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1202 if isinstance(useEscSequences, bool):
1203 term.cterm = self.csolver.mkString(
1204 s.encode(), <bint> useEscSequences)
1206 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1210 def mkEmptySequence(self, Sort sort):
1211 """Create an empty sequence of the given element sort.
1213 :param sort: The element sort of the sequence.
1214 :return: the empty sequence with given element sort.
1216 cdef Term term = Term(self)
1217 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1220 def mkUniverseSet(self, Sort sort):
1221 """Create a universe set of the given sort.
1223 :param sort: the sort of the set elements
1224 :return: the universe set constant
1226 cdef Term term = Term(self)
1227 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1230 @expand_list_arg(num_req_args=0)
1231 def mkBitVector(self, *args):
1233 Supports the following arguments:
1235 - ``Term mkBitVector(int size, int val=0)``
1236 - ``Term mkBitVector(int size, string val, int base)``
1238 :return: a bit-vector literal term
1239 :param: `size` an integer size.
1240 :param: `val` an integer representating the value, in the first form. In the second form, a string representing the value.
1241 :param: `base` the base of the string representation (second form only)
1243 cdef Term term = Term(self)
1245 raise ValueError("Missing arguments to mkBitVector")
1247 if not isinstance(size, int):
1249 "Invalid first argument to mkBitVector '{}', "
1250 "expected bit-vector size".format(size))
1252 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1253 elif len(args) == 2:
1255 if not isinstance(val, int):
1257 "Invalid second argument to mkBitVector '{}', "
1258 "expected integer value".format(size))
1259 term.cterm = self.csolver.mkBitVector(
1260 <uint32_t> size, <uint32_t> val)
1261 elif len(args) == 3:
1264 if not isinstance(val, str):
1266 "Invalid second argument to mkBitVector '{}', "
1267 "expected value string".format(size))
1268 if not isinstance(base, int):
1270 "Invalid third argument to mkBitVector '{}', "
1271 "expected base given as integer".format(size))
1272 term.cterm = self.csolver.mkBitVector(
1274 <const string&> str(val).encode(),
1277 raise ValueError("Unexpected inputs to mkBitVector")
1280 def mkConstArray(self, Sort sort, Term val):
1282 Create a constant array with the provided constant value stored at every
1285 :param sort: the sort of the constant array (must be an array sort)
1286 :param val: the constant value to store (must match the sort's element sort)
1287 :return: the constant array term
1289 cdef Term term = Term(self)
1290 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1293 def mkPosInf(self, int exp, int sig):
1294 """Create a positive infinity floating-point constant.
1296 :param exp: Number of bits in the exponent
1297 :param sig: Number of bits in the significand
1298 :return: the floating-point constant
1300 cdef Term term = Term(self)
1301 term.cterm = self.csolver.mkPosInf(exp, sig)
1304 def mkNegInf(self, int exp, int sig):
1305 """Create a negative infinity floating-point constant.
1307 :param exp: Number of bits in the exponent
1308 :param sig: Number of bits in the significand
1309 :return: the floating-point constant
1311 cdef Term term = Term(self)
1312 term.cterm = self.csolver.mkNegInf(exp, sig)
1315 def mkNaN(self, int exp, int sig):
1316 """Create a not-a-number (NaN) floating-point constant.
1318 :param exp: Number of bits in the exponent
1319 :param sig: Number of bits in the significand
1320 :return: the floating-point constant
1322 cdef Term term = Term(self)
1323 term.cterm = self.csolver.mkNaN(exp, sig)
1326 def mkPosZero(self, int exp, int sig):
1327 """Create a positive zero (+0.0) floating-point constant.
1329 :param exp: Number of bits in the exponent
1330 :param sig: Number of bits in the significand
1331 :return: the floating-point constant
1333 cdef Term term = Term(self)
1334 term.cterm = self.csolver.mkPosZero(exp, sig)
1337 def mkNegZero(self, int exp, int sig):
1338 """Create a negative zero (+0.0) floating-point constant.
1340 :param exp: Number of bits in the exponent
1341 :param sig: Number of bits in the significand
1342 :return: the floating-point constant
1344 cdef Term term = Term(self)
1345 term.cterm = self.csolver.mkNegZero(exp, sig)
1348 def mkRoundingMode(self, RoundingMode rm):
1349 """Create a roundingmode constant.
1351 :param rm: the floating point rounding mode this constant represents
1353 cdef Term term = Term(self)
1354 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
1357 def mkUninterpretedConst(self, Sort sort, int index):
1358 """Create uninterpreted constant.
1360 :param sort: Sort of the constant
1361 :param index: Index of the constant
1363 cdef Term term = Term(self)
1364 term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index)
1367 def mkAbstractValue(self, index):
1369 Create an abstract value constant.
1370 The given index needs to be positive.
1372 :param index: Index of the abstract value
1374 cdef Term term = Term(self)
1376 term.cterm = self.csolver.mkAbstractValue(str(index).encode())
1379 "mkAbstractValue expects a str representing a number"
1380 " or an int, but got{}".format(index))
1383 def mkFloatingPoint(self, int exp, int sig, Term val):
1384 """Create a floating-point constant.
1386 :param exp: Size of the exponent
1387 :param sig: Size of the significand
1388 :param val: Value of the floating-point constant as a bit-vector term
1390 cdef Term term = Term(self)
1391 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1394 def mkCardinalityConstraint(self, Sort sort, int index):
1395 """Create cardinality constraint.
1397 :param sort: Sort of the constraint
1398 :param index: The upper bound for the cardinality of the sort
1400 cdef Term term = Term(self)
1401 term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
1404 def mkConst(self, Sort sort, symbol=None):
1406 Create (first-order) constant (0-arity function symbol).
1410 .. code-block:: smtlib
1412 ( declare-const <symbol> <sort> )
1413 ( declare-fun <symbol> ( ) <sort> )
1415 :param sort: the sort of the constant
1416 :param symbol: the name of the constant. If None, a default symbol is used.
1417 :return: the first-order constant
1419 cdef Term term = Term(self)
1421 term.cterm = self.csolver.mkConst(sort.csort)
1423 term.cterm = self.csolver.mkConst(sort.csort,
1424 (<str?> symbol).encode())
1427 def mkVar(self, Sort sort, symbol=None):
1429 Create a bound variable to be used in a binder (i.e. a quantifier, a
1430 lambda, or a witness binder).
1432 :param sort: the sort of the variable
1433 :param symbol: the name of the variable
1434 :return: the variable
1436 cdef Term term = Term(self)
1438 term.cterm = self.csolver.mkVar(sort.csort)
1440 term.cterm = self.csolver.mkVar(sort.csort,
1441 (<str?> symbol).encode())
1444 def mkDatatypeConstructorDecl(self, str name):
1446 :return: a datatype constructor declaration
1447 :param: `name` the constructor's name
1449 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1450 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1453 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1454 """Create a datatype declaration.
1456 :param name: the name of the datatype
1457 :param isCoDatatype: true if a codatatype is to be constructed
1458 :return: the DatatypeDecl
1460 cdef DatatypeDecl dd = DatatypeDecl(self)
1461 cdef vector[c_Sort] v
1464 if sorts_or_bool is None and isCoDatatype is None:
1465 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1466 elif sorts_or_bool is not None and isCoDatatype is None:
1467 if isinstance(sorts_or_bool, bool):
1468 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1469 <bint> sorts_or_bool)
1470 elif isinstance(sorts_or_bool, Sort):
1471 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1472 (<Sort> sorts_or_bool).csort)
1473 elif isinstance(sorts_or_bool, list):
1474 for s in sorts_or_bool:
1475 v.push_back((<Sort?> s).csort)
1476 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1477 <const vector[c_Sort]&> v)
1479 raise ValueError("Unhandled second argument type {}"
1480 .format(type(sorts_or_bool)))
1481 elif sorts_or_bool is not None and isCoDatatype is not None:
1482 if isinstance(sorts_or_bool, Sort):
1483 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1484 (<Sort> sorts_or_bool).csort,
1485 <bint> isCoDatatype)
1486 elif isinstance(sorts_or_bool, list):
1487 for s in sorts_or_bool:
1488 v.push_back((<Sort?> s).csort)
1489 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1490 <const vector[c_Sort]&> v,
1491 <bint> isCoDatatype)
1493 raise ValueError("Unhandled second argument type {}"
1494 .format(type(sorts_or_bool)))
1496 raise ValueError("Can't create DatatypeDecl with {}".format([type(a)
1503 def simplify(self, Term t):
1505 Simplify a formula without doing "much" work. Does not involve the
1506 SAT Engine in the simplification, but uses the current definitions,
1507 assertions, and the current partial model, if one has been constructed.
1508 It also involves theory normalization.
1510 :param t: the formula to simplify
1511 :return: the simplified formula
1513 cdef Term term = Term(self)
1514 term.cterm = self.csolver.simplify(t.cterm)
1517 def assertFormula(self, Term term):
1518 """ Assert a formula
1522 .. code-block:: smtlib
1526 :param term: the formula to assert
1528 self.csolver.assertFormula(term.cterm)
1532 Check satisfiability.
1536 .. code-block:: smtlib
1540 :return: the result of the satisfiability check.
1542 cdef Result r = Result()
1543 r.cr = self.csolver.checkSat()
1546 def mkSygusGrammar(self, boundVars, ntSymbols):
1548 Create a SyGuS grammar. The first non-terminal is treated as the
1549 starting non-terminal, so the order of non-terminals matters.
1551 :param boundVars: the parameters to corresponding synth-fun/synth-inv
1552 :param ntSymbols: the pre-declaration of the non-terminal symbols
1553 :return: the grammar
1555 cdef Grammar grammar = Grammar(self)
1556 cdef vector[c_Term] bvc
1557 cdef vector[c_Term] ntc
1558 for bv in boundVars:
1559 bvc.push_back((<Term?> bv).cterm)
1560 for nt in ntSymbols:
1561 ntc.push_back((<Term?> nt).cterm)
1562 grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1565 def mkSygusVar(self, Sort sort, str symbol=""):
1566 """Append symbol to the current list of universal variables.
1570 .. code-block:: smtlib
1572 ( declare-var <symbol> <sort> )
1574 :param sort: the sort of the universal variable
1575 :param symbol: the name of the universal variable
1576 :return: the universal variable
1578 cdef Term term = Term(self)
1579 term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode())
1582 def addSygusConstraint(self, Term t):
1584 Add a formula to the set of SyGuS constraints.
1588 .. code-block:: smtlib
1590 ( constraint <term> )
1592 :param term: the formula to add as a constraint
1594 self.csolver.addSygusConstraint(t.cterm)
1596 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1598 Add a set of SyGuS constraints to the current state that correspond to an
1599 invariant synthesis problem.
1603 .. code-block:: smtlib
1605 ( inv-constraint <inv> <pre> <trans> <post> )
1607 :param inv: the function-to-synthesize
1608 :param pre: the pre-condition
1609 :param trans: the transition relation
1610 :param post: the post-condition
1612 self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1614 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1616 Synthesize n-ary function following specified syntactic constraints.
1620 .. code-block:: smtlib
1622 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1624 :param symbol: the name of the function
1625 :param boundVars: the parameters to this function
1626 :param sort: the sort of the return value of this function
1627 :param grammar: the syntactic constraints
1628 :return: the function
1630 cdef Term term = Term(self)
1631 cdef vector[c_Term] v
1632 for bv in bound_vars:
1633 v.push_back((<Term?> bv).cterm)
1635 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1637 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1640 def checkSynth(self):
1642 Try to find a solution for the synthesis conjecture corresponding to the
1643 current list of functions-to-synthesize, universal variables and
1648 .. code-block:: smtlib
1652 :return: the result of the synthesis conjecture.
1654 cdef Result r = Result()
1655 r.cr = self.csolver.checkSynth()
1658 def getSynthSolution(self, Term term):
1660 Get the synthesis solution of the given term. This method should be
1661 called immediately after the solver answers unsat for sygus input.
1663 :param term: the term for which the synthesis solution is queried
1664 :return: the synthesis solution of the given term
1666 cdef Term t = Term(self)
1667 t.cterm = self.csolver.getSynthSolution(term.cterm)
1670 def getSynthSolutions(self, list terms):
1672 Get the synthesis solutions of the given terms. This method should be
1673 called immediately after the solver answers unsat for sygus input.
1675 :param terms: the terms for which the synthesis solutions is queried
1676 :return: the synthesis solutions of the given terms
1679 cdef vector[c_Term] vec
1681 vec.push_back((<Term?> t).cterm)
1682 cresult = self.csolver.getSynthSolutions(vec)
1690 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1692 Synthesize invariant.
1696 .. code-block:: smtlib
1698 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1700 :param symbol: the name of the invariant
1701 :param boundVars: the parameters to this invariant
1702 :param grammar: the syntactic constraints
1703 :return: the invariant
1705 cdef Term term = Term(self)
1706 cdef vector[c_Term] v
1707 for bv in bound_vars:
1708 v.push_back((<Term?> bv).cterm)
1710 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
1712 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
1715 @expand_list_arg(num_req_args=0)
1716 def checkSatAssuming(self, *assumptions):
1717 """ Check satisfiability assuming the given formula.
1721 .. code-block:: smtlib
1723 ( check-sat-assuming ( <prop_literal> ) )
1725 :param assumptions: the formulas to assume, as a list or as distinct arguments
1726 :return: the result of the satisfiability check.
1728 cdef Result r = Result()
1729 # used if assumptions is a list of terms
1730 cdef vector[c_Term] v
1731 for a in assumptions:
1732 v.push_back((<Term?> a).cterm)
1733 r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
1736 @expand_list_arg(num_req_args=0)
1737 def checkEntailed(self, *assumptions):
1738 """Check entailment of the given formula w.r.t. the current set of assertions.
1740 :param terms: the formulas to check entailment for, as a list or as distinct arguments
1741 :return: the result of the entailment check.
1743 cdef Result r = Result()
1744 # used if assumptions is a list of terms
1745 cdef vector[c_Term] v
1746 for a in assumptions:
1747 v.push_back((<Term?> a).cterm)
1748 r.cr = self.csolver.checkEntailed(<const vector[c_Term]&> v)
1751 @expand_list_arg(num_req_args=1)
1752 def declareDatatype(self, str symbol, *ctors):
1754 Create datatype sort.
1758 .. code-block:: smtlib
1760 ( declare-datatype <symbol> <datatype_decl> )
1762 :param symbol: the name of the datatype sort
1763 :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
1764 :return: the datatype sort
1766 cdef Sort sort = Sort(self)
1767 cdef vector[c_DatatypeConstructorDecl] v
1770 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1771 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1774 def declareFun(self, str symbol, list sorts, Sort sort):
1775 """Declare n-ary function symbol.
1779 .. code-block:: smtlib
1781 ( declare-fun <symbol> ( <sort>* ) <sort> )
1783 :param symbol: the name of the function
1784 :param sorts: the sorts of the parameters to this function
1785 :param sort: the sort of the return value of this function
1786 :return: the function
1788 cdef Term term = Term(self)
1789 cdef vector[c_Sort] v
1791 v.push_back((<Sort?> s).csort)
1792 term.cterm = self.csolver.declareFun(symbol.encode(),
1793 <const vector[c_Sort]&> v,
1797 def declareSort(self, str symbol, int arity):
1798 """Declare uninterpreted sort.
1802 .. code-block:: smtlib
1804 ( declare-sort <symbol> <numeral> )
1806 :param symbol: the name of the sort
1807 :param arity: the arity of the sort
1810 cdef Sort sort = Sort(self)
1811 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
1814 def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1816 Define n-ary function.
1819 - ``Term defineFun(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1820 - ``Term defineFun(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1825 .. code-block:: smtlib
1827 ( define-fun <function_def> )
1829 :param symbol: the name of the function
1830 :param bound_vars: the parameters to this function
1831 :param sort: the sort of the return value of this function
1832 :param term: the function body
1833 :param global: determines whether this definition is global (i.e. persists when popping the context)
1834 :return: the function
1836 cdef Term term = Term(self)
1837 cdef vector[c_Term] v
1838 for bv in bound_vars:
1839 v.push_back((<Term?> bv).cterm)
1842 term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(),
1843 <const vector[c_Term] &> v,
1844 (<Sort?> sort_or_term).csort,
1848 term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm,
1849 <const vector[c_Term]&> v,
1850 (<Term?> sort_or_term).cterm,
1855 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1856 """Define recursive functions.
1860 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1861 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1866 .. code-block:: smtlib
1868 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1870 Create elements of parameter ``funs`` with mkConst().
1872 :param funs: the sorted functions
1873 :param bound_vars: the list of parameters to the functions
1874 :param terms: the list of function bodies of the functions
1875 :param global: determines whether this definition is global (i.e. persists when popping the context)
1876 :return: the function
1878 cdef Term term = Term(self)
1879 cdef vector[c_Term] v
1880 for bv in bound_vars:
1881 v.push_back((<Term?> bv).cterm)
1884 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
1885 <const vector[c_Term] &> v,
1886 (<Sort?> sort_or_term).csort,
1890 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
1891 <const vector[c_Term]&> v,
1892 (<Term?> sort_or_term).cterm,
1897 def defineFunsRec(self, funs, bound_vars, terms):
1898 """Define recursive functions.
1902 .. code-block:: smtlib
1904 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1906 Create elements of parameter ``funs`` with mkConst().
1908 :param funs: the sorted functions
1909 :param bound_vars: the list of parameters to the functions
1910 :param terms: the list of function bodies of the functions
1911 :param global: determines whether this definition is global (i.e. persists when popping the context)
1912 :return: the function
1914 cdef vector[c_Term] vf
1915 cdef vector[vector[c_Term]] vbv
1916 cdef vector[c_Term] vt
1919 vf.push_back((<Term?> f).cterm)
1921 cdef vector[c_Term] temp
1922 for v in bound_vars:
1924 temp.push_back((<Term?> t).cterm)
1929 vf.push_back((<Term?> t).cterm)
1931 def getAssertions(self):
1932 """Get the list of asserted formulas.
1936 .. code-block:: smtlib
1940 :return: the list of asserted formulas
1943 for a in self.csolver.getAssertions():
1946 assertions.append(term)
1949 def getInfo(self, str flag):
1950 """Get info from the solver.
1954 .. code-block:: smtlib
1956 ( get-info <info_flag> )
1958 :param flag: the info flag
1961 return self.csolver.getInfo(flag.encode())
1963 def getOption(self, str option):
1964 """Get the value of a given option.
1968 .. code-block:: smtlib
1970 ( get-option <keyword> )
1972 :param option: the option for which the value is queried
1973 :return: a string representation of the option value
1975 return self.csolver.getOption(option.encode())
1977 def getUnsatAssumptions(self):
1979 Get the set of unsat ("failed") assumptions.
1983 .. code-block:: smtlib
1985 ( get-unsat-assumptions )
1987 Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
1989 :return: the set of unsat assumptions.
1992 for a in self.csolver.getUnsatAssumptions():
1995 assumptions.append(term)
1998 def getUnsatCore(self):
1999 """Get the unsatisfiable core.
2003 .. code-block:: smtlib
2007 Requires to enable option :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
2009 :return: a set of terms representing the unsatisfiable core
2012 for a in self.csolver.getUnsatCore():
2018 def getValue(self, Term t):
2019 """Get the value of the given term in the current model.
2023 .. code-block:: smtlib
2025 ( get-value ( <term> ) )
2027 :param term: the term for which the value is queried
2028 :return: the value of the given term
2030 cdef Term term = Term(self)
2031 term.cterm = self.csolver.getValue(t.cterm)
2034 def getModelDomainElements(self, Sort s):
2036 Get the domain elements of uninterpreted sort s in the current model. The
2037 current model interprets s as the finite sort whose domain elements are
2038 given in the return value of this method.
2040 :param s: The uninterpreted sort in question
2041 :return: the domain elements of s in the current model
2044 cresult = self.csolver.getModelDomainElements(s.csort)
2051 def isModelCoreSymbol(self, Term v):
2053 This returns false if the model value of free constant v was not
2054 essential for showing the satisfiability of the last call to checkSat
2055 using the current model. This method will only return false (for any v)
2056 if the model-cores option has been set.
2058 :param v: The term in question
2059 :return: true if v is a model core symbol
2061 return self.csolver.isModelCoreSymbol(v.cterm)
2063 def getSeparationHeap(self):
2064 """When using separation logic, obtain the term for the heap.
2066 :return: The term for the heap
2068 cdef Term term = Term(self)
2069 term.cterm = self.csolver.getSeparationHeap()
2072 def getSeparationNilTerm(self):
2073 """When using separation logic, obtain the term for nil.
2075 :return: The term for nil
2077 cdef Term term = Term(self)
2078 term.cterm = self.csolver.getSeparationNilTerm()
2081 def declareSeparationHeap(self, Sort locType, Sort dataType):
2083 When using separation logic, this sets the location sort and the
2084 datatype sort to the given ones. This method should be invoked exactly
2085 once, before any separation logic constraints are provided.
2087 :param locSort: The location sort of the heap
2088 :param dataSort: The data sort of the heap
2090 self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
2092 def declarePool(self, str symbol, Sort sort, initValue):
2093 """Declare a symbolic pool of terms with the given initial value.
2097 .. code-block:: smtlib
2099 ( declare-pool <symbol> <sort> ( <term>* ) )
2101 :param symbol: The name of the pool
2102 :param sort: The sort of the elements of the pool.
2103 :param initValue: The initial value of the pool
2105 cdef Term term = Term(self)
2106 cdef vector[c_Term] niv
2108 niv.push_back((<Term?> v).cterm)
2109 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
2112 def pop(self, nscopes=1):
2113 """Pop ``nscopes`` level(s) from the assertion stack.
2117 .. code-block:: smtlib
2121 :param nscopes: the number of levels to pop
2123 self.csolver.pop(nscopes)
2125 def push(self, nscopes=1):
2126 """ Push ``nscopes`` level(s) to the assertion stack.
2130 .. code-block:: smtlib
2134 :param nscopes: the number of levels to push
2136 self.csolver.push(nscopes)
2138 def resetAssertions(self):
2140 Remove all assertions.
2144 .. code-block:: smtlib
2146 ( reset-assertions )
2149 self.csolver.resetAssertions()
2151 def setInfo(self, str keyword, str value):
2156 .. code-block:: smtlib
2158 ( set-info <attribute> )
2160 :param keyword: the info flag
2161 :param value: the value of the info flag
2163 self.csolver.setInfo(keyword.encode(), value.encode())
2165 def setLogic(self, str logic):
2170 .. code-block:: smtlib
2172 ( set-logic <symbol> )
2174 :param logic: the logic to set
2176 self.csolver.setLogic(logic.encode())
2178 def setOption(self, str option, str value):
2183 .. code-block:: smtlib
2185 ( set-option <option> )
2187 :param option: the option name
2188 :param value: the option value
2190 self.csolver.setOption(option.encode(), value.encode())
2195 The sort of a cvc5 term.
2199 def __cinit__(self, Solver solver):
2200 # csort always set by Solver
2201 self.solver = solver
2203 def __eq__(self, Sort other):
2204 return self.csort == other.csort
2206 def __ne__(self, Sort other):
2207 return self.csort != other.csort
2209 def __lt__(self, Sort other):
2210 return self.csort < other.csort
2212 def __gt__(self, Sort other):
2213 return self.csort > other.csort
2215 def __le__(self, Sort other):
2216 return self.csort <= other.csort
2218 def __ge__(self, Sort other):
2219 return self.csort >= other.csort
2222 return self.csort.toString().decode()
2225 return self.csort.toString().decode()
2228 return csorthash(self.csort)
2231 """:return: True if this Sort is a null sort."""
2232 return self.csort.isNull()
2234 def isBoolean(self):
2236 Is this a Boolean sort?
2238 :return: True if the sort is the Boolean sort.
2240 return self.csort.isBoolean()
2242 def isInteger(self):
2244 Is this an integer sort?
2246 :return: True if the sort is the integer sort.
2248 return self.csort.isInteger()
2252 Is this a real sort?
2254 :return: True if the sort is the real sort.
2256 return self.csort.isReal()
2260 Is this a string sort?
2262 :return: True if the sort is the string sort.
2264 return self.csort.isString()
2268 Is this a regexp sort?
2270 :return: True if the sort is the regexp sort.
2272 return self.csort.isRegExp()
2274 def isRoundingMode(self):
2276 Is this a rounding mode sort?
2278 :return: True if the sort is the rounding mode sort.
2280 return self.csort.isRoundingMode()
2282 def isBitVector(self):
2284 Is this a bit-vector sort?
2286 :return: True if the sort is a bit-vector sort.
2288 return self.csort.isBitVector()
2290 def isFloatingPoint(self):
2292 Is this a floating-point sort?
2294 :return: True if the sort is a bit-vector sort.
2296 return self.csort.isFloatingPoint()
2298 def isDatatype(self):
2300 Is this a datatype sort?
2302 :return: True if the sort is a datatype sort.
2304 return self.csort.isDatatype()
2306 def isParametricDatatype(self):
2308 Is this a parametric datatype sort?
2310 :return: True if the sort is a parametric datatype sort.
2312 return self.csort.isParametricDatatype()
2314 def isConstructor(self):
2316 Is this a constructor sort?
2318 :return: True if the sort is a constructor sort.
2320 return self.csort.isConstructor()
2322 def isSelector(self):
2324 Is this a selector sort?
2326 :return: True if the sort is a selector sort.
2328 return self.csort.isSelector()
2332 Is this a tester sort?
2334 :return: True if the sort is a selector sort.
2336 return self.csort.isTester()
2338 def isUpdater(self):
2340 Is this a datatype updater sort?
2342 :return: True if the sort is a datatype updater sort.
2344 return self.csort.isUpdater()
2346 def isFunction(self):
2348 Is this a function sort?
2350 :return: True if the sort is a function sort.
2352 return self.csort.isFunction()
2354 def isPredicate(self):
2356 Is this a predicate sort?
2357 That is, is this a function sort mapping to Boolean? All predicate
2358 sorts are also function sorts.
2360 :return: True if the sort is a predicate sort.
2362 return self.csort.isPredicate()
2366 Is this a tuple sort?
2368 :return: True if the sort is a tuple sort.
2370 return self.csort.isTuple()
2374 Is this a record sort?
2376 :return: True if the sort is a record sort.
2378 return self.csort.isRecord()
2382 Is this an array sort?
2384 :return: True if the sort is an array sort.
2386 return self.csort.isArray()
2392 :return: True if the sort is a set sort.
2394 return self.csort.isSet()
2400 :return: True if the sort is a bag sort.
2402 return self.csort.isBag()
2404 def isSequence(self):
2406 Is this a sequence sort?
2408 :return: True if the sort is a sequence sort.
2410 return self.csort.isSequence()
2412 def isUninterpretedSort(self):
2414 Is this a sort uninterpreted?
2416 :return: True if the sort is uninterpreted.
2418 return self.csort.isUninterpretedSort()
2420 def isSortConstructor(self):
2422 Is this a sort constructor kind?
2424 :return: True if this a sort constructor kind.
2426 return self.csort.isSortConstructor()
2428 def isFirstClass(self):
2430 Is this a first-class sort?
2431 First-class sorts are sorts for which:
2433 1. we handle equalities between terms of that type, and
2434 2. they are allowed to be parameters of parametric sorts
2435 (e.g. index or element sorts of arrays).
2437 Examples of sorts that are not first-class include sort constructor
2438 sorts and regular expression sorts.
2440 :return: True if the sort is a first-class sort.
2442 return self.csort.isFirstClass()
2444 def isFunctionLike(self):
2446 Is this a function-LIKE sort?
2448 Anything function-like except arrays (e.g., datatype selectors) is
2449 considered a function here. Function-like terms can not be the argument
2450 or return value for any term that is function-like.
2451 This is mainly to avoid higher order.
2453 Note that arrays are explicitly not considered function-like here.
2455 :return: True if this is a function-like sort
2457 return self.csort.isFunctionLike()
2459 def isSubsortOf(self, Sort sort):
2461 Is this sort a subsort of the given sort?
2463 :return: True if this sort is a subsort of s
2465 return self.csort.isSubsortOf(sort.csort)
2467 def isComparableTo(self, Sort sort):
2469 Is this sort comparable to the given sort
2470 (i.e., do they share a common ancestor in the subsort tree)?
2472 :return: True if this sort is comparable to s
2474 return self.csort.isComparableTo(sort.csort)
2476 def getDatatype(self):
2478 :return: the underlying datatype of a datatype sort
2480 cdef Datatype d = Datatype(self.solver)
2481 d.cd = self.csort.getDatatype()
2484 def instantiate(self, params):
2486 Instantiate a parameterized datatype/sort sort.
2487 Create sorts parameter with :py:meth:`Solver.mkParamSort()`
2489 :param params: the list of sort parameters to instantiate with
2491 cdef Sort sort = Sort(self.solver)
2492 cdef vector[c_Sort] v
2494 v.push_back((<Sort?> s).csort)
2495 sort.csort = self.csort.instantiate(v)
2498 def substitute(self, sort_or_list_1, sort_or_list_2):
2500 Substitution of Sorts.
2502 :param sort_or_list_1: the subsort or subsorts to be substituted within this sort.
2503 :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort.
2506 # The resulting sort after substitution
2507 cdef Sort sort = Sort(self.solver)
2508 # lists for substitutions
2509 cdef vector[c_Sort] ces
2510 cdef vector[c_Sort] creplacements
2512 # normalize the input parameters to be lists
2513 if isinstance(sort_or_list_1, list):
2514 assert isinstance(sort_or_list_2, list)
2516 replacements = sort_or_list_2
2517 if len(es) != len(replacements):
2518 raise RuntimeError("Expecting list inputs to substitute to "
2519 "have the same length but got: "
2520 "{} and {}".format(len(es), len(replacements)))
2522 for e, r in zip(es, replacements):
2523 ces.push_back((<Sort?> e).csort)
2524 creplacements.push_back((<Sort?> r).csort)
2527 # add the single elements to the vectors
2528 ces.push_back((<Sort?> sort_or_list_1).csort)
2529 creplacements.push_back((<Sort?> sort_or_list_2).csort)
2531 # call the API substitute method with lists
2532 sort.csort = self.csort.substitute(ces, creplacements)
2536 def getConstructorArity(self):
2538 :return: the arity of a constructor sort.
2540 return self.csort.getConstructorArity()
2542 def getConstructorDomainSorts(self):
2544 :return: the domain sorts of a constructor sort
2547 for s in self.csort.getConstructorDomainSorts():
2548 sort = Sort(self.solver)
2550 domain_sorts.append(sort)
2553 def getConstructorCodomainSort(self):
2555 :return: the codomain sort of a constructor sort
2557 cdef Sort sort = Sort(self.solver)
2558 sort.csort = self.csort.getConstructorCodomainSort()
2561 def getSelectorDomainSort(self):
2563 :return: the domain sort of a selector sort
2565 cdef Sort sort = Sort(self.solver)
2566 sort.csort = self.csort.getSelectorDomainSort()
2569 def getSelectorCodomainSort(self):
2571 :return: the codomain sort of a selector sort
2573 cdef Sort sort = Sort(self.solver)
2574 sort.csort = self.csort.getSelectorCodomainSort()
2577 def getTesterDomainSort(self):
2579 :return: the domain sort of a tester sort
2581 cdef Sort sort = Sort(self.solver)
2582 sort.csort = self.csort.getTesterDomainSort()
2585 def getTesterCodomainSort(self):
2587 :return: the codomain sort of a tester sort, which is the Boolean sort
2589 cdef Sort sort = Sort(self.solver)
2590 sort.csort = self.csort.getTesterCodomainSort()
2593 def getFunctionArity(self):
2595 :return: the arity of a function sort
2597 return self.csort.getFunctionArity()
2599 def getFunctionDomainSorts(self):
2601 :return: the domain sorts of a function sort
2604 for s in self.csort.getFunctionDomainSorts():
2605 sort = Sort(self.solver)
2607 domain_sorts.append(sort)
2610 def getFunctionCodomainSort(self):
2612 :return: the codomain sort of a function sort
2614 cdef Sort sort = Sort(self.solver)
2615 sort.csort = self.csort.getFunctionCodomainSort()
2618 def getArrayIndexSort(self):
2620 :return: the array index sort of an array sort
2622 cdef Sort sort = Sort(self.solver)
2623 sort.csort = self.csort.getArrayIndexSort()
2626 def getArrayElementSort(self):
2628 :return: the array element sort of an array sort
2630 cdef Sort sort = Sort(self.solver)
2631 sort.csort = self.csort.getArrayElementSort()
2634 def getSetElementSort(self):
2636 :return: the element sort of a set sort
2638 cdef Sort sort = Sort(self.solver)
2639 sort.csort = self.csort.getSetElementSort()
2642 def getBagElementSort(self):
2644 :return: the element sort of a bag sort
2646 cdef Sort sort = Sort(self.solver)
2647 sort.csort = self.csort.getBagElementSort()
2650 def getSequenceElementSort(self):
2652 :return: the element sort of a sequence sort
2654 cdef Sort sort = Sort(self.solver)
2655 sort.csort = self.csort.getSequenceElementSort()
2658 def getUninterpretedSortName(self):
2660 :return: the name of an uninterpreted sort
2662 return self.csort.getUninterpretedSortName().decode()
2664 def isUninterpretedSortParameterized(self):
2666 :return: True if an uninterpreted sort is parameterized
2668 return self.csort.isUninterpretedSortParameterized()
2670 def getUninterpretedSortParamSorts(self):
2672 :return: the parameter sorts of an uninterpreted sort
2675 for s in self.csort.getUninterpretedSortParamSorts():
2676 sort = Sort(self.solver)
2678 param_sorts.append(sort)
2681 def getSortConstructorName(self):
2683 :return: the name of a sort constructor sort
2685 return self.csort.getSortConstructorName().decode()
2687 def getSortConstructorArity(self):
2689 :return: the arity of a sort constructor sort
2691 return self.csort.getSortConstructorArity()
2693 def getBitVectorSize(self):
2695 :return: the bit-width of the bit-vector sort
2697 return self.csort.getBitVectorSize()
2699 def getFloatingPointExponentSize(self):
2701 :return: the bit-width of the exponent of the floating-point sort
2703 return self.csort.getFloatingPointExponentSize()
2705 def getFloatingPointSignificandSize(self):
2707 :return: the width of the significand of the floating-point sort
2709 return self.csort.getFloatingPointSignificandSize()
2711 def getDatatypeParamSorts(self):
2713 :return: the parameter sorts of a datatype sort
2716 for s in self.csort.getDatatypeParamSorts():
2717 sort = Sort(self.solver)
2719 param_sorts.append(sort)
2722 def getDatatypeArity(self):
2724 :return: the arity of a datatype sort
2726 return self.csort.getDatatypeArity()
2728 def getTupleLength(self):
2730 :return: the length of a tuple sort
2732 return self.csort.getTupleLength()
2734 def getTupleSorts(self):
2736 :return: the element sorts of a tuple sort
2739 for s in self.csort.getTupleSorts():
2740 sort = Sort(self.solver)
2742 tuple_sorts.append(sort)
2749 def __cinit__(self, Solver solver):
2750 # cterm always set in the Solver object
2751 self.solver = solver
2753 def __eq__(self, Term other):
2754 return self.cterm == other.cterm
2756 def __ne__(self, Term other):
2757 return self.cterm != other.cterm
2759 def __lt__(self, Term other):
2760 return self.cterm < other.cterm
2762 def __gt__(self, Term other):
2763 return self.cterm > other.cterm
2765 def __le__(self, Term other):
2766 return self.cterm <= other.cterm
2768 def __ge__(self, Term other):
2769 return self.cterm >= other.cterm
2771 def __getitem__(self, int index):
2772 cdef Term term = Term(self.solver)
2774 term.cterm = self.cterm[index]
2776 raise ValueError("Expecting a non-negative integer or string")
2780 return self.cterm.toString().decode()
2783 return self.cterm.toString().decode()
2786 for ci in self.cterm:
2787 term = Term(self.solver)
2792 return ctermhash(self.cterm)
2794 def getNumChildren(self):
2795 return self.cterm.getNumChildren()
2798 return self.cterm.getId()
2801 return kind(<int> self.cterm.getKind())
2804 cdef Sort sort = Sort(self.solver)
2805 sort.csort = self.cterm.getSort()
2808 def substitute(self, term_or_list_1, term_or_list_2):
2809 # The resulting term after substitution
2810 cdef Term term = Term(self.solver)
2811 # lists for substitutions
2812 cdef vector[c_Term] ces
2813 cdef vector[c_Term] creplacements
2815 # normalize the input parameters to be lists
2816 if isinstance(term_or_list_1, list):
2817 assert isinstance(term_or_list_2, list)
2819 replacements = term_or_list_2
2820 if len(es) != len(replacements):
2821 raise RuntimeError("Expecting list inputs to substitute to "
2822 "have the same length but got: "
2823 "{} and {}".format(len(es), len(replacements)))
2825 for e, r in zip(es, replacements):
2826 ces.push_back((<Term?> e).cterm)
2827 creplacements.push_back((<Term?> r).cterm)
2830 # add the single elements to the vectors
2831 ces.push_back((<Term?> term_or_list_1).cterm)
2832 creplacements.push_back((<Term?> term_or_list_2).cterm)
2834 # call the API substitute method with lists
2835 term.cterm = self.cterm.substitute(ces, creplacements)
2839 return self.cterm.hasOp()
2842 cdef Op op = Op(self.solver)
2843 op.cop = self.cterm.getOp()
2847 return self.cterm.isNull()
2850 cdef Term term = Term(self.solver)
2851 term.cterm = self.cterm.notTerm()
2854 def andTerm(self, Term t):
2855 cdef Term term = Term(self.solver)
2856 term.cterm = self.cterm.andTerm((<Term> t).cterm)
2859 def orTerm(self, Term t):
2860 cdef Term term = Term(self.solver)
2861 term.cterm = self.cterm.orTerm(t.cterm)
2864 def xorTerm(self, Term t):
2865 cdef Term term = Term(self.solver)
2866 term.cterm = self.cterm.xorTerm(t.cterm)
2869 def eqTerm(self, Term t):
2870 cdef Term term = Term(self.solver)
2871 term.cterm = self.cterm.eqTerm(t.cterm)
2874 def impTerm(self, Term t):
2875 cdef Term term = Term(self.solver)
2876 term.cterm = self.cterm.impTerm(t.cterm)
2879 def iteTerm(self, Term then_t, Term else_t):
2880 cdef Term term = Term(self.solver)
2881 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
2884 def isConstArray(self):
2885 return self.cterm.isConstArray()
2887 def getConstArrayBase(self):
2888 cdef Term term = Term(self.solver)
2889 term.cterm = self.cterm.getConstArrayBase()
2892 def isBooleanValue(self):
2893 return self.cterm.isBooleanValue()
2895 def getBooleanValue(self):
2896 return self.cterm.getBooleanValue()
2898 def isStringValue(self):
2899 return self.cterm.isStringValue()
2901 def getStringValue(self):
2902 cdef Py_ssize_t size
2903 cdef c_wstring s = self.cterm.getStringValue()
2904 return PyUnicode_FromWideChar(s.data(), s.size())
2906 def isIntegerValue(self):
2907 return self.cterm.isIntegerValue()
2908 def isAbstractValue(self):
2909 return self.cterm.isAbstractValue()
2911 def getAbstractValue(self):
2912 return self.cterm.getAbstractValue().decode()
2914 def isFloatingPointPosZero(self):
2915 return self.cterm.isFloatingPointPosZero()
2917 def isFloatingPointNegZero(self):
2918 return self.cterm.isFloatingPointNegZero()
2920 def isFloatingPointPosInf(self):
2921 return self.cterm.isFloatingPointPosInf()
2923 def isFloatingPointNegInf(self):
2924 return self.cterm.isFloatingPointNegInf()
2926 def isFloatingPointNaN(self):
2927 return self.cterm.isFloatingPointNaN()
2929 def isFloatingPointValue(self):
2930 return self.cterm.isFloatingPointValue()
2932 def getFloatingPointValue(self):
2933 cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
2934 cdef Term term = Term(self.solver)
2935 term.cterm = get2(t)
2936 return (get0(t), get1(t), term)
2938 def isSetValue(self):
2939 return self.cterm.isSetValue()
2941 def getSetValue(self):
2943 for e in self.cterm.getSetValue():
2944 term = Term(self.solver)
2949 def isSequenceValue(self):
2950 return self.cterm.isSequenceValue()
2952 def getSequenceValue(self):
2954 for e in self.cterm.getSequenceValue():
2955 term = Term(self.solver)
2960 def isUninterpretedValue(self):
2961 return self.cterm.isUninterpretedValue()
2963 def getUninterpretedValue(self):
2964 cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue()
2965 cdef Sort sort = Sort(self.solver)
2966 sort.csort = p.first
2970 def isTupleValue(self):
2971 return self.cterm.isTupleValue()
2973 def getTupleValue(self):
2975 for e in self.cterm.getTupleValue():
2976 term = Term(self.solver)
2981 def getIntegerValue(self):
2982 return int(self.cterm.getIntegerValue().decode())
2984 def isRealValue(self):
2985 return self.cterm.isRealValue()
2987 def getRealValue(self):
2988 """Returns the value of a real term as a Fraction"""
2989 return Fraction(self.cterm.getRealValue().decode())
2991 def isBitVectorValue(self):
2992 return self.cterm.isBitVectorValue()
2994 def getBitVectorValue(self, base = 2):
2995 """Returns the value of a bit-vector term as a 0/1 string"""
2996 return self.cterm.getBitVectorValue(base).decode()
2998 def toPythonObj(self):
3000 Converts a constant value Term to a Python object.
3003 Boolean -- returns a Python bool
3004 Int -- returns a Python int
3005 Real -- returns a Python Fraction
3006 BV -- returns a Python int (treats BV as unsigned)
3007 String -- returns a Python Unicode string
3008 Array -- returns a Python dict mapping indices to values
3009 -- the constant base is returned as the default value
3012 if self.isBooleanValue():
3013 return self.getBooleanValue()
3014 elif self.isIntegerValue():
3015 return self.getIntegerValue()
3016 elif self.isRealValue():
3017 return self.getRealValue()
3018 elif self.isBitVectorValue():
3019 return int(self.getBitVectorValue(), 2)
3020 elif self.isStringValue():
3021 return self.getStringValue()
3022 elif self.getSort().isArray():
3028 # Array models are represented as a series of store operations
3029 # on a constant array
3032 if t.getKind() == kinds.Store:
3034 keys.append(t[1].toPythonObj())
3035 values.append(t[2].toPythonObj())
3036 to_visit.append(t[0])
3038 assert t.getKind() == kinds.ConstArray
3039 base_value = t.getConstArrayBase().toPythonObj()
3041 assert len(keys) == len(values)
3042 assert base_value is not None
3044 # put everything in a dictionary with the constant
3045 # base as the result for any index not included in the stores
3046 res = defaultdict(lambda : base_value)
3047 for k, v in zip(keys, values):
3053 # Generate rounding modes
3054 cdef __rounding_modes = {
3055 <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
3056 <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
3057 <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
3058 <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
3059 <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway"
3062 mod_ref = sys.modules[__name__]
3063 for rm_int, name in __rounding_modes.items():
3064 r = RoundingMode(rm_int)
3066 if name in dir(mod_ref):
3067 raise RuntimeError("Redefinition of Python RoundingMode %s."%name)
3069 setattr(mod_ref, name, r)
3076 # Generate unknown explanations
3077 cdef __unknown_explanations = {
3078 <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
3079 <int> INCOMPLETE: "Incomplete",
3080 <int> TIMEOUT: "Timeout",
3081 <int> RESOURCEOUT: "Resourceout",
3082 <int> MEMOUT: "Memout",
3083 <int> INTERRUPTED: "Interrupted",
3084 <int> NO_STATUS: "NoStatus",
3085 <int> UNSUPPORTED: "Unsupported",
3086 <int> OTHER: "Other",
3087 <int> UNKNOWN_REASON: "UnknownReason"
3090 for ue_int, name in __unknown_explanations.items():
3091 u = UnknownExplanation(ue_int)
3093 if name in dir(mod_ref):
3094 raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
3096 setattr(mod_ref, name, u)