1 from collections import defaultdict
2 from fractions import Fraction
3 from functools import wraps
6 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
7 from libc.stddef cimport wchar_t
9 from libcpp.pair cimport pair
10 from libcpp.set cimport set as c_set
11 from libcpp.string cimport string
12 from libcpp.vector cimport vector
14 from cvc5 cimport cout
15 from cvc5 cimport Datatype as c_Datatype
16 from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
17 from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
18 from cvc5 cimport DatatypeDecl as c_DatatypeDecl
19 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
20 from cvc5 cimport Result as c_Result
21 from cvc5 cimport RoundingMode as c_RoundingMode
22 from cvc5 cimport UnknownExplanation as c_UnknownExplanation
23 from cvc5 cimport Op as c_Op
24 from cvc5 cimport Solver as c_Solver
25 from cvc5 cimport Grammar as c_Grammar
26 from cvc5 cimport Sort as c_Sort
27 from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
28 from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
29 from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
30 from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT
31 from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED
32 from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON
33 from cvc5 cimport OTHER
34 from cvc5 cimport Term as c_Term
35 from cvc5 cimport hash as c_hash
36 from cvc5 cimport wstring as c_wstring
37 from cvc5 cimport tuple as c_tuple
38 from cvc5 cimport get0, get1, get2
39 from cvc5kinds cimport Kind as c_Kind
41 cdef extern from "Python.h":
42 wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
43 object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
44 void PyMem_Free(void*)
46 ################################## DECORATORS #################################
47 def expand_list_arg(num_req_args=0):
49 Creates a decorator that looks at index num_req_args of the args,
50 if it's a list, it expands it before calling the function.
54 def wrapper(owner, *args):
55 if len(args) == num_req_args + 1 and \
56 isinstance(args[num_req_args], list):
57 args = list(args[:num_req_args]) + args[num_req_args]
58 return func(owner, *args)
61 ###############################################################################
64 ### Using PEP-8 spacing recommendations
65 ### Limit linewidth to 79 characters
66 ### Break before binary operators
67 ### surround top level functions and classes with two spaces
68 ### separate methods by one space
69 ### use spaces in functions sparingly to separate logical blocks
70 ### can omit spaces between unrelated oneliners
71 ### always use c++ default arguments
72 #### only use default args of None at python level
74 # References and pointers
75 # The Solver object holds a pointer to a c_Solver.
76 # This is because the assignment operator is deleted in the C++ API for solvers.
77 # Cython has a limitation where you can't stack allocate objects
78 # that have constructors with arguments:
79 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
80 # To get around that you can either have a nullary constructor and assignment
81 # or, use a pointer (which is what we chose).
82 # An additional complication of this is that to free up resources, you must
83 # know when to delete the object.
84 # Python will not follow the same scoping rules as in C++, so it must be
85 # able to reference count. To do this correctly, the solver must be a
86 # reference in the Python class for any class that keeps a pointer to
87 # the solver in C++ (to ensure the solver is not deleted before something
88 # that depends on it).
91 ## Objects for hashing
92 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
93 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
94 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
100 Wrapper class for :cpp:class:`cvc5::api::Datatype`.
104 def __cinit__(self, Solver solver):
107 def __getitem__(self, index):
108 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
109 if isinstance(index, int) and index >= 0:
110 dc.cdc = self.cd[(<int?> index)]
111 elif isinstance(index, str):
112 dc.cdc = self.cd[(<const string &> index.encode())]
114 raise ValueError("Expecting a non-negative integer or string")
117 def getConstructor(self, str name):
119 :param name: the name of the constructor.
120 :return: a constructor by name.
122 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
123 dc.cdc = self.cd.getConstructor(name.encode())
126 def getConstructorTerm(self, str name):
128 :param name: the name of the constructor.
129 :return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`).
131 cdef Term term = Term(self.solver)
132 term.cterm = self.cd.getConstructorTerm(name.encode())
135 def getSelector(self, str name):
137 :param name: the name of the selector..
138 :return: a selector by name.
140 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
141 ds.cds = self.cd.getSelector(name.encode())
146 :return: the name of the datatype.
148 return self.cd.getName().decode()
150 def getNumConstructors(self):
152 :return: number of constructors in this datatype.
154 return self.cd.getNumConstructors()
156 def getParameters(self):
158 :return: the parameters of this datatype, if it is parametric. An
159 exception is thrown if this datatype is not parametric.
162 for s in self.cd.getParameters():
163 sort = Sort(self.solver)
165 param_sorts.append(sort)
168 def isParametric(self):
169 """:return: True if this datatype is parametric."""
170 return self.cd.isParametric()
172 def isCodatatype(self):
173 """:return: True if this datatype corresponds to a co-datatype."""
174 return self.cd.isCodatatype()
177 """:return: True if this datatype corresponds to a tuple."""
178 return self.cd.isTuple()
181 """:return: True if this datatype corresponds to a record."""
182 return self.cd.isRecord()
185 """:return: True if this datatype is finite."""
186 return self.cd.isFinite()
188 def isWellFounded(self):
189 """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
190 return self.cd.isWellFounded()
193 """:return: True if this Datatype is a null object."""
194 return self.cd.isNull()
197 return self.cd.toString().decode()
200 return self.cd.toString().decode()
204 dc = DatatypeConstructor(self.solver)
209 cdef class DatatypeConstructor:
211 A cvc5 datatype constructor.
212 Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.
214 cdef c_DatatypeConstructor cdc
216 def __cinit__(self, Solver solver):
217 self.cdc = c_DatatypeConstructor()
220 def __getitem__(self, index):
221 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
222 if isinstance(index, int) and index >= 0:
223 ds.cds = self.cdc[(<int?> index)]
224 elif isinstance(index, str):
225 ds.cds = self.cdc[(<const string &> index.encode())]
227 raise ValueError("Expecting a non-negative integer or string")
232 :return: the name of the constructor.
234 return self.cdc.getName().decode()
236 def getConstructorTerm(self):
238 :return: the constructor operator as a term.
240 cdef Term term = Term(self.solver)
241 term.cterm = self.cdc.getConstructorTerm()
244 def getInstantiatedConstructorTerm(self, Sort retSort):
246 Specialized method for parametric datatypes (see
247 :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm()
248 <cvc5::api::DatatypeConstructor::getInstantiatedConstructorTerm>`).
250 :param retSort: the desired return sort of the constructor
251 :return: the constructor operator as a term.
253 cdef Term term = Term(self.solver)
254 term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort)
257 def getTesterTerm(self):
259 :return: the tester operator that is related to this constructor, as a term.
261 cdef Term term = Term(self.solver)
262 term.cterm = self.cdc.getTesterTerm()
265 def getNumSelectors(self):
267 :return: the number of selecters (so far) of this Datatype constructor.
269 return self.cdc.getNumSelectors()
271 def getSelector(self, str name):
273 :param name: the name of the datatype selector.
274 :return: the first datatype selector with the given name
276 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
277 ds.cds = self.cdc.getSelector(name.encode())
280 def getSelectorTerm(self, str name):
282 :param name: the name of the datatype selector.
283 :return: a term representing the firstdatatype selector with the given name.
285 cdef Term term = Term(self.solver)
286 term.cterm = self.cdc.getSelectorTerm(name.encode())
290 """:return: True if this DatatypeConstructor is a null object."""
291 return self.cdc.isNull()
294 return self.cdc.toString().decode()
297 return self.cdc.toString().decode()
301 ds = DatatypeSelector(self.solver)
306 cdef class DatatypeConstructorDecl:
308 A cvc5 datatype constructor declaration.
309 Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.
311 cdef c_DatatypeConstructorDecl cddc
314 def __cinit__(self, Solver solver):
317 def addSelector(self, str name, Sort sort):
319 Add datatype selector declaration.
321 :param name: the name of the datatype selector declaration to add.
322 :param sort: the codomain sort of the datatype selector declaration
325 self.cddc.addSelector(name.encode(), sort.csort)
327 def addSelectorSelf(self, str name):
329 Add datatype selector declaration whose codomain sort is the
332 :param name: the name of the datatype selector declaration to add.
334 self.cddc.addSelectorSelf(name.encode())
337 """:return: True if this DatatypeConstructorDecl is a null object."""
338 return self.cddc.isNull()
341 return self.cddc.toString().decode()
344 return self.cddc.toString().decode()
347 cdef class DatatypeDecl:
349 A cvc5 datatype declaration.
350 Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.
352 cdef c_DatatypeDecl cdd
354 def __cinit__(self, Solver solver):
357 def addConstructor(self, DatatypeConstructorDecl ctor):
359 Add a datatype constructor declaration.
361 :param ctor: the datatype constructor declaration to add.
363 self.cdd.addConstructor(ctor.cddc)
365 def getNumConstructors(self):
367 :return: number of constructors (so far) for this datatype declaration.
369 return self.cdd.getNumConstructors()
371 def isParametric(self):
373 :return: is this datatype declaration parametric?
375 return self.cdd.isParametric()
379 :return: the name of this datatype declaration.
381 return self.cdd.getName().decode()
384 """:return: True if this DatatypeDecl is a null object."""
385 return self.cdd.isNull()
388 return self.cdd.toString().decode()
391 return self.cdd.toString().decode()
394 cdef class DatatypeSelector:
396 A cvc5 datatype selector.
397 Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.
399 cdef c_DatatypeSelector cds
401 def __cinit__(self, Solver solver):
402 self.cds = c_DatatypeSelector()
407 :return: the name of this datatype selector.
409 return self.cds.getName().decode()
411 def getSelectorTerm(self):
413 :return: the selector opeartor of this datatype selector as a term.
415 cdef Term term = Term(self.solver)
416 term.cterm = self.cds.getSelectorTerm()
419 def getUpdaterTerm(self):
421 :return: the updater opeartor of this datatype selector as a term.
423 cdef Term term = Term(self.solver)
424 term.cterm = self.cds.getUpdaterTerm()
427 def getCodomainSort(self):
429 :return: the codomain sort of this selector.
431 cdef Sort sort = Sort(self.solver)
432 sort.csort = self.cds.getCodomainSort()
436 """:return: True if this DatatypeSelector is a null object."""
437 return self.cds.isNull()
440 return self.cds.toString().decode()
443 return self.cds.toString().decode()
449 An operator is a term that represents certain operators,
450 instantiated with its required parameters, e.g.,
451 a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`.
452 Wrapper class for :cpp:class:`cvc5::api::Op`.
456 def __cinit__(self, Solver solver):
460 def __eq__(self, Op other):
461 return self.cop == other.cop
463 def __ne__(self, Op other):
464 return self.cop != other.cop
467 return self.cop.toString().decode()
470 return self.cop.toString().decode()
473 return cophash(self.cop)
477 :return: the kind of this operator.
479 return Kind(<int> self.cop.getKind())
483 :return: True iff this operator is indexed.
485 return self.cop.isIndexed()
489 :return: True iff this operator is a null term.
491 return self.cop.isNull()
493 def getNumIndices(self):
495 :return: number of indices of this op.
497 return self.cop.getNumIndices()
499 def getIndices(self):
501 :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() <cvc5::api::Op::getIndices>`).
505 indices = self.cop.getIndices[string]().decode()
510 indices = self.cop.getIndices[uint32_t]()
515 indices = self.cop.getIndices[pair[uint32_t, uint32_t]]()
520 raise RuntimeError("Unable to retrieve indices from {}".format(self))
527 Wrapper class for :cpp:class:`cvc5::api::Grammar`.
529 cdef c_Grammar cgrammar
531 def __cinit__(self, Solver solver):
533 self.cgrammar = c_Grammar()
535 def addRule(self, Term ntSymbol, Term rule):
537 Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
539 :param ntSymbol: the non-terminal to which the rule is added.
540 :param rule: the rule to add.
542 self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
544 def addAnyConstant(self, Term ntSymbol):
546 Allow ``ntSymbol`` to be an arbitrary constant.
548 :param ntSymbol: the non-terminal allowed to be constant.
550 self.cgrammar.addAnyConstant(ntSymbol.cterm)
552 def addAnyVariable(self, Term ntSymbol):
554 Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``.
556 :param ntSymbol: the non-terminal allowed to be any input variable.
558 self.cgrammar.addAnyVariable(ntSymbol.cterm)
560 def addRules(self, Term ntSymbol, rules):
562 Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
564 :param ntSymbol: the non-terminal to which the rules are added.
565 :param rules: the rules to add.
567 cdef vector[c_Term] crules
569 crules.push_back((<Term?> r).cterm)
570 self.cgrammar.addRules(ntSymbol.cterm, crules)
574 Encapsulation of a three-valued solver result, with explanations.
575 Wrapper class for :cpp:class:`cvc5::api::Result`.
579 # gets populated by solver
584 :return: True if Result is empty, i.e., a nullary Result, and not an actual result returned from a
585 :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` (and friends) query.
587 return self.cr.isNull()
591 :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.
593 return self.cr.isSat()
597 :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.
599 return self.cr.isUnsat()
601 def isSatUnknown(self):
603 :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.
605 return self.cr.isSatUnknown()
607 def isEntailed(self):
609 :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query.
611 return self.cr.isEntailed()
613 def isNotEntailed(self):
615 :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query that is not entailed.
617 return self.cr.isNotEntailed()
619 def isEntailmentUnknown(self):
621 :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.
623 return self.cr.isEntailmentUnknown()
625 def getUnknownExplanation(self):
627 :return: an explanation for an unknown query result.
629 return UnknownExplanation(<int> self.cr.getUnknownExplanation())
631 def __eq__(self, Result other):
632 return self.cr == other.cr
634 def __ne__(self, Result other):
635 return self.cr != other.cr
638 return self.cr.toString().decode()
641 return self.cr.toString().decode()
644 cdef class RoundingMode:
646 Rounding modes for floating-point numbers.
648 For many floating-point operations, infinitely precise results may not be
649 representable with the number of available bits. Thus, the results are
650 rounded in a certain way to one of the representable floating-point numbers.
652 These rounding modes directly follow the SMT-LIB theory for floating-point
653 arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
654 The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
657 Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`.
659 cdef c_RoundingMode crm
661 def __cinit__(self, int rm):
662 # crm always assigned externally
663 self.crm = <c_RoundingMode> rm
664 self.name = __rounding_modes[rm]
666 def __eq__(self, RoundingMode other):
667 return (<int> self.crm) == (<int> other.crm)
669 def __ne__(self, RoundingMode other):
670 return not self.__eq__(other)
673 return hash((<int> self.crm, self.name))
682 cdef class UnknownExplanation:
684 Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`.
686 cdef c_UnknownExplanation cue
688 def __cinit__(self, int ue):
689 # crm always assigned externally
690 self.cue = <c_UnknownExplanation> ue
691 self.name = __unknown_explanations[ue]
693 def __eq__(self, UnknownExplanation other):
694 return (<int> self.cue) == (<int> other.cue)
696 def __ne__(self, UnknownExplanation other):
697 return not self.__eq__(other)
700 return hash((<int> self.crm, self.name))
710 """Wrapper class for :cpp:class:`cvc5::api::Solver`."""
711 cdef c_Solver* csolver
714 self.csolver = new c_Solver()
716 def __dealloc__(self):
719 def getBooleanSort(self):
720 """:return: sort Boolean
722 cdef Sort sort = Sort(self)
723 sort.csort = self.csolver.getBooleanSort()
726 def getIntegerSort(self):
727 """:return: sort Integer
729 cdef Sort sort = Sort(self)
730 sort.csort = self.csolver.getIntegerSort()
733 def getNullSort(self):
734 """:return: sort null
736 cdef Sort sort = Sort(self)
737 sort.csort = self.csolver.getNullSort()
740 def getRealSort(self):
741 """:return: sort Real
743 cdef Sort sort = Sort(self)
744 sort.csort = self.csolver.getRealSort()
747 def getRegExpSort(self):
748 """:return: sort of RegExp
750 cdef Sort sort = Sort(self)
751 sort.csort = self.csolver.getRegExpSort()
754 def getRoundingModeSort(self):
755 """:return: sort RoundingMode
757 cdef Sort sort = Sort(self)
758 sort.csort = self.csolver.getRoundingModeSort()
761 def getStringSort(self):
762 """:return: sort String
764 cdef Sort sort = Sort(self)
765 sort.csort = self.csolver.getStringSort()
768 def mkArraySort(self, Sort indexSort, Sort elemSort):
769 """Create an array sort.
771 :param indexSort: the array index sort
772 :param elemSort: the array element sort
773 :return: the array sort
775 cdef Sort sort = Sort(self)
776 sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
779 def mkBitVectorSort(self, uint32_t size):
780 """Create a bit-vector sort.
782 :param size: the bit-width of the bit-vector sort
783 :return: the bit-vector sort
785 cdef Sort sort = Sort(self)
786 sort.csort = self.csolver.mkBitVectorSort(size)
789 def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
790 """Create a floating-point sort.
792 :param exp: the bit-width of the exponent of the floating-point sort.
793 :param sig: the bit-width of the significand of the floating-point sort.
795 cdef Sort sort = Sort(self)
796 sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
799 def mkDatatypeSort(self, DatatypeDecl dtypedecl):
800 """Create a datatype sort.
802 :param dtypedecl: the datatype declaration from which the sort is created
803 :return: the datatype sort
805 cdef Sort sort = Sort(self)
806 sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
809 def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
811 Create a vector of datatype sorts using unresolved sorts. The names of
812 the datatype declarations in dtypedecls must be distinct.
814 This method is called when the DatatypeDecl objects dtypedecls have been
815 built using "unresolved" sorts.
817 We associate each sort in unresolvedSorts with exacly one datatype from
818 dtypedecls. In particular, it must have the same name as exactly one
819 datatype declaration in dtypedecls.
821 When constructing datatypes, unresolved sorts are replaced by the datatype
822 sort constructed for the datatype declaration it is associated with.
824 :param dtypedecls: the datatype declarations from which the sort is created
825 :param unresolvedSorts: the list of unresolved sorts
826 :return: the datatype sorts
828 if unresolvedSorts == None:
829 unresolvedSorts = set([])
831 assert isinstance(unresolvedSorts, set)
834 cdef vector[c_DatatypeDecl] decls
835 for decl in dtypedecls:
836 decls.push_back((<DatatypeDecl?> decl).cdd)
838 cdef c_set[c_Sort] usorts
839 for usort in unresolvedSorts:
840 usorts.insert((<Sort?> usort).csort)
842 csorts = self.csolver.mkDatatypeSorts(
843 <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
851 def mkFunctionSort(self, sorts, Sort codomain):
852 """ Create function sort.
854 :param sorts: the sort of the function arguments
855 :param codomain: the sort of the function return value
856 :return: the function sort
859 cdef Sort sort = Sort(self)
860 # populate a vector with dereferenced c_Sorts
861 cdef vector[c_Sort] v
863 if isinstance(sorts, Sort):
864 sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
866 elif isinstance(sorts, list):
868 v.push_back((<Sort?>s).csort)
870 sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
874 def mkParamSort(self, symbolname):
875 """ Create a sort parameter.
877 :param symbol: the name of the sort
878 :return: the sort parameter
880 cdef Sort sort = Sort(self)
881 sort.csort = self.csolver.mkParamSort(symbolname.encode())
884 @expand_list_arg(num_req_args=0)
885 def mkPredicateSort(self, *sorts):
886 """Create a predicate sort.
888 :param sorts: the list of sorts of the predicate, as a list or as distinct arguments.
889 :return: the predicate sort
891 cdef Sort sort = Sort(self)
892 cdef vector[c_Sort] v
894 v.push_back((<Sort?> s).csort)
895 sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
898 @expand_list_arg(num_req_args=0)
899 def mkRecordSort(self, *fields):
900 """Create a record sort
902 :param fields: the list of fields of the record, as a list or as distinct arguments
903 :return: the record sort
905 cdef Sort sort = Sort(self)
906 cdef vector[pair[string, c_Sort]] v
907 cdef pair[string, c_Sort] p
911 p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
913 sort.csort = self.csolver.mkRecordSort(
914 <const vector[pair[string, c_Sort]] &> v)
917 def mkSetSort(self, Sort elemSort):
918 """Create a set sort.
920 :param elemSort: the sort of the set elements
921 :return: the set sort
923 cdef Sort sort = Sort(self)
924 sort.csort = self.csolver.mkSetSort(elemSort.csort)
927 def mkBagSort(self, Sort elemSort):
928 """Create a bag sort.
930 :param elemSort: the sort of the bag elements
931 :return: the bag sort
933 cdef Sort sort = Sort(self)
934 sort.csort = self.csolver.mkBagSort(elemSort.csort)
937 def mkSequenceSort(self, Sort elemSort):
938 """Create a sequence sort.
940 :param elemSort: the sort of the sequence elements
941 :return: the sequence sort
943 cdef Sort sort = Sort(self)
944 sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
947 def mkUninterpretedSort(self, str name):
948 """Create an uninterpreted sort.
950 :param symbol: the name of the sort
951 :return: the uninterpreted sort
953 cdef Sort sort = Sort(self)
954 sort.csort = self.csolver.mkUninterpretedSort(name.encode())
957 def mkUnresolvedSort(self, str name, size_t arity = 0):
958 """Create an unresolved sort.
960 This is for creating yet unresolved sort placeholders for mutually
963 :param symbol: the name of the sort
964 :param arity: the number of sort parameters of the sort
965 :return: the unresolved sort
967 cdef Sort sort = Sort(self)
968 sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity)
971 def mkSortConstructorSort(self, str symbol, size_t arity):
972 """Create a sort constructor sort.
974 :param symbol: the symbol of the sort
975 :param arity: the arity of the sort
976 :return: the sort constructor sort
978 cdef Sort sort = Sort(self)
979 sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
982 @expand_list_arg(num_req_args=0)
983 def mkTupleSort(self, *sorts):
984 """Create a tuple sort.
986 :param sorts: of the elements of the tuple, as a list or as distinct arguments
987 :return: the tuple sort
989 cdef Sort sort = Sort(self)
990 cdef vector[c_Sort] v
992 v.push_back((<Sort?> s).csort)
993 sort.csort = self.csolver.mkTupleSort(v)
996 @expand_list_arg(num_req_args=1)
997 def mkTerm(self, kind_or_op, *args):
999 Supports the following arguments:
1001 - ``Term mkTerm(Kind kind)``
1002 - ``Term mkTerm(Kind kind, Op child1, List[Term] children)``
1003 - ``Term mkTerm(Kind kind, List[Term] children)``
1005 where ``List[Term]`` can also be comma-separated arguments
1007 cdef Term term = Term(self)
1008 cdef vector[c_Term] v
1011 if isinstance(kind_or_op, Kind):
1012 op = self.mkOp(kind_or_op)
1015 term.cterm = self.csolver.mkTerm((<Op?> op).cop)
1018 v.push_back((<Term?> a).cterm)
1019 term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
1022 def mkTuple(self, sorts, terms):
1023 """Create a tuple term. Terms are automatically converted if sorts are compatible.
1025 :param sorts: The sorts of the elements in the tuple
1026 :param terms: The elements in the tuple
1027 :return: the tuple Term
1029 cdef vector[c_Sort] csorts
1030 cdef vector[c_Term] cterms
1033 csorts.push_back((<Sort?> s).csort)
1035 cterms.push_back((<Term?> s).cterm)
1036 cdef Term result = Term(self)
1037 result.cterm = self.csolver.mkTuple(csorts, cterms)
1040 @expand_list_arg(num_req_args=0)
1041 def mkOp(self, k, *args):
1043 Supports the following uses:
1045 - ``Op mkOp(Kind kind)``
1046 - ``Op mkOp(Kind kind, Kind k)``
1047 - ``Op mkOp(Kind kind, const string& arg)``
1048 - ``Op mkOp(Kind kind, uint32_t arg)``
1049 - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
1050 - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind)
1052 cdef Op op = Op(self)
1053 cdef vector[uint32_t] v
1056 op.cop = self.csolver.mkOp(<c_Kind> k.value)
1057 elif len(args) == 1:
1058 if isinstance(args[0], str):
1059 op.cop = self.csolver.mkOp(<c_Kind> k.value,
1062 elif isinstance(args[0], int):
1063 op.cop = self.csolver.mkOp(<c_Kind> k.value, <int?> args[0])
1064 elif isinstance(args[0], list):
1066 if a < 0 or a >= 2 ** 31:
1067 raise ValueError("Argument {} must fit in a uint32_t".format(a))
1069 v.push_back((<uint32_t?> a))
1070 op.cop = self.csolver.mkOp(<c_Kind> k.value, <const vector[uint32_t]&> v)
1072 raise ValueError("Unsupported signature"
1073 " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
1074 elif len(args) == 2:
1075 if isinstance(args[0], int) and isinstance(args[1], int):
1076 op.cop = self.csolver.mkOp(<c_Kind> k.value, <int> args[0], <int> args[1])
1078 raise ValueError("Unsupported signature"
1079 " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
1083 """Create a Boolean true constant.
1085 :return: the true constant
1087 cdef Term term = Term(self)
1088 term.cterm = self.csolver.mkTrue()
1092 """Create a Boolean false constant.
1094 :return: the false constant
1096 cdef Term term = Term(self)
1097 term.cterm = self.csolver.mkFalse()
1100 def mkBoolean(self, bint val):
1101 """Create a Boolean constant.
1103 :return: the Boolean constant
1104 :param val: the value of the constant
1106 cdef Term term = Term(self)
1107 term.cterm = self.csolver.mkBoolean(val)
1111 """Create a constant representing the number Pi.
1113 :return: a constant representing Pi
1115 cdef Term term = Term(self)
1116 term.cterm = self.csolver.mkPi()
1119 def mkInteger(self, val):
1120 """Create an integer constant.
1122 :param val: representation of the constant: either a string or integer
1123 :return: a constant of sort Integer
1125 cdef Term term = Term(self)
1126 if isinstance(val, str):
1127 term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
1129 assert(isinstance(val, int))
1130 term.cterm = self.csolver.mkInteger((<int?> val))
1133 def mkReal(self, val, den=None):
1134 """Create a real constant.
1136 :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.
1137 :param den: if not None, the value is `val`/`den`
1138 :return: a real term with literal value
1140 Can be used in various forms:
1142 - Given a string ``"N/D"`` constructs the corresponding rational.
1143 - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
1144 - 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``.
1145 - Given a string ``"W"`` or an integer, constructs that integer.
1146 - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``.
1148 cdef Term term = Term(self)
1150 term.cterm = self.csolver.mkReal(str(val).encode())
1152 if not isinstance(val, int) or not isinstance(den, int):
1153 raise ValueError("Expecting integers when"
1154 " constructing a rational"
1155 " but got: {}".format((val, den)))
1156 term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
1159 def mkRegexpAll(self):
1160 """Create a regular expression all (re.all) term.
1162 :return: the all term
1164 cdef Term term = Term(self)
1165 term.cterm = self.csolver.mkRegexpAll()
1168 def mkRegexpAllchar(self):
1169 """Create a regular expression allchar (re.allchar) term.
1171 :return: the allchar term
1173 cdef Term term = Term(self)
1174 term.cterm = self.csolver.mkRegexpAllchar()
1177 def mkRegexpNone(self):
1178 """Create a regular expression none (re.none) term.
1180 :return: the none term
1182 cdef Term term = Term(self)
1183 term.cterm = self.csolver.mkRegexpNone()
1186 def mkEmptySet(self, Sort s):
1187 """Create a constant representing an empty set of the given sort.
1189 :param sort: the sort of the set elements.
1190 :return: the empty set constant
1192 cdef Term term = Term(self)
1193 term.cterm = self.csolver.mkEmptySet(s.csort)
1196 def mkEmptyBag(self, Sort s):
1197 """Create a constant representing an empty bag of the given sort.
1199 :param sort: the sort of the bag elements.
1200 :return: the empty bag constant
1202 cdef Term term = Term(self)
1203 term.cterm = self.csolver.mkEmptyBag(s.csort)
1207 """Create a separation logic empty term.
1209 :return: the separation logic empty term
1211 cdef Term term = Term(self)
1212 term.cterm = self.csolver.mkSepEmp()
1215 def mkSepNil(self, Sort sort):
1216 """Create a separation logic nil term.
1218 :param sort: the sort of the nil term
1219 :return: the separation logic nil term
1221 cdef Term term = Term(self)
1222 term.cterm = self.csolver.mkSepNil(sort.csort)
1225 def mkString(self, str s, useEscSequences = None):
1227 Create a String constant from a `str` which may contain SMT-LIB
1228 compatible escape sequences like ``\\u1234`` to encode unicode characters.
1230 :param s: the string this constant represents
1231 :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character
1232 :return: the String constant
1234 cdef Term term = Term(self)
1235 cdef Py_ssize_t size
1236 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1237 if isinstance(useEscSequences, bool):
1238 term.cterm = self.csolver.mkString(
1239 s.encode(), <bint> useEscSequences)
1241 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1245 def mkEmptySequence(self, Sort sort):
1246 """Create an empty sequence of the given element sort.
1248 :param sort: The element sort of the sequence.
1249 :return: the empty sequence with given element sort.
1251 cdef Term term = Term(self)
1252 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1255 def mkUniverseSet(self, Sort sort):
1256 """Create a universe set of the given sort.
1258 :param sort: the sort of the set elements
1259 :return: the universe set constant
1261 cdef Term term = Term(self)
1262 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1265 @expand_list_arg(num_req_args=0)
1266 def mkBitVector(self, *args):
1268 Supports the following arguments:
1270 - ``Term mkBitVector(int size, int val=0)``
1271 - ``Term mkBitVector(int size, string val, int base)``
1273 :return: a bit-vector literal term
1274 :param size: an integer size.
1275 :param val: an integer representating the value, in the first form. In the second form, a string representing the value.
1276 :param base: the base of the string representation (second form only)
1278 cdef Term term = Term(self)
1280 raise ValueError("Missing arguments to mkBitVector")
1282 if not isinstance(size, int):
1284 "Invalid first argument to mkBitVector '{}', "
1285 "expected bit-vector size".format(size))
1287 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1288 elif len(args) == 2:
1290 if not isinstance(val, int):
1292 "Invalid second argument to mkBitVector '{}', "
1293 "expected integer value".format(size))
1294 term.cterm = self.csolver.mkBitVector(
1295 <uint32_t> size, <uint32_t> val)
1296 elif len(args) == 3:
1299 if not isinstance(val, str):
1301 "Invalid second argument to mkBitVector '{}', "
1302 "expected value string".format(size))
1303 if not isinstance(base, int):
1305 "Invalid third argument to mkBitVector '{}', "
1306 "expected base given as integer".format(size))
1307 term.cterm = self.csolver.mkBitVector(
1309 <const string&> str(val).encode(),
1312 raise ValueError("Unexpected inputs to mkBitVector")
1315 def mkConstArray(self, Sort sort, Term val):
1317 Create a constant array with the provided constant value stored at every
1320 :param sort: the sort of the constant array (must be an array sort)
1321 :param val: the constant value to store (must match the sort's element sort)
1322 :return: the constant array term
1324 cdef Term term = Term(self)
1325 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1328 def mkPosInf(self, int exp, int sig):
1329 """Create a positive infinity floating-point constant.
1331 :param exp: Number of bits in the exponent
1332 :param sig: Number of bits in the significand
1333 :return: the floating-point constant
1335 cdef Term term = Term(self)
1336 term.cterm = self.csolver.mkPosInf(exp, sig)
1339 def mkNegInf(self, int exp, int sig):
1340 """Create a negative infinity floating-point constant.
1342 :param exp: Number of bits in the exponent
1343 :param sig: Number of bits in the significand
1344 :return: the floating-point constant
1346 cdef Term term = Term(self)
1347 term.cterm = self.csolver.mkNegInf(exp, sig)
1350 def mkNaN(self, int exp, int sig):
1351 """Create a not-a-number (NaN) floating-point constant.
1353 :param exp: Number of bits in the exponent
1354 :param sig: Number of bits in the significand
1355 :return: the floating-point constant
1357 cdef Term term = Term(self)
1358 term.cterm = self.csolver.mkNaN(exp, sig)
1361 def mkPosZero(self, int exp, int sig):
1362 """Create a positive zero (+0.0) floating-point constant.
1364 :param exp: Number of bits in the exponent
1365 :param sig: Number of bits in the significand
1366 :return: the floating-point constant
1368 cdef Term term = Term(self)
1369 term.cterm = self.csolver.mkPosZero(exp, sig)
1372 def mkNegZero(self, int exp, int sig):
1373 """Create a negative zero (+0.0) floating-point constant.
1375 :param exp: Number of bits in the exponent
1376 :param sig: Number of bits in the significand
1377 :return: the floating-point constant
1379 cdef Term term = Term(self)
1380 term.cterm = self.csolver.mkNegZero(exp, sig)
1383 def mkRoundingMode(self, RoundingMode rm):
1384 """Create a roundingmode constant.
1386 :param rm: the floating point rounding mode this constant represents
1388 cdef Term term = Term(self)
1389 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
1392 def mkUninterpretedConst(self, Sort sort, int index):
1393 """Create uninterpreted constant.
1395 :param sort: Sort of the constant
1396 :param index: Index of the constant
1398 cdef Term term = Term(self)
1399 term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index)
1402 def mkAbstractValue(self, index):
1404 Create an abstract value constant.
1405 The given index needs to be positive.
1407 :param index: Index of the abstract value
1409 cdef Term term = Term(self)
1411 term.cterm = self.csolver.mkAbstractValue(str(index).encode())
1414 "mkAbstractValue expects a str representing a number"
1415 " or an int, but got{}".format(index))
1418 def mkFloatingPoint(self, int exp, int sig, Term val):
1419 """Create a floating-point constant.
1421 :param exp: Size of the exponent
1422 :param sig: Size of the significand
1423 :param val: Value of the floating-point constant as a bit-vector term
1425 cdef Term term = Term(self)
1426 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1429 def mkCardinalityConstraint(self, Sort sort, int index):
1430 """Create cardinality constraint.
1432 :param sort: Sort of the constraint
1433 :param index: The upper bound for the cardinality of the sort
1435 cdef Term term = Term(self)
1436 term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
1439 def mkConst(self, Sort sort, symbol=None):
1441 Create (first-order) constant (0-arity function symbol).
1445 .. code-block:: smtlib
1447 ( declare-const <symbol> <sort> )
1448 ( declare-fun <symbol> ( ) <sort> )
1450 :param sort: the sort of the constant
1451 :param symbol: the name of the constant. If None, a default symbol is used.
1452 :return: the first-order constant
1454 cdef Term term = Term(self)
1456 term.cterm = self.csolver.mkConst(sort.csort)
1458 term.cterm = self.csolver.mkConst(sort.csort,
1459 (<str?> symbol).encode())
1462 def mkVar(self, Sort sort, symbol=None):
1464 Create a bound variable to be used in a binder (i.e. a quantifier, a
1465 lambda, or a witness binder).
1467 :param sort: the sort of the variable
1468 :param symbol: the name of the variable
1469 :return: the variable
1471 cdef Term term = Term(self)
1473 term.cterm = self.csolver.mkVar(sort.csort)
1475 term.cterm = self.csolver.mkVar(sort.csort,
1476 (<str?> symbol).encode())
1479 def mkDatatypeConstructorDecl(self, str name):
1481 :return: a datatype constructor declaration
1482 :param name: the constructor's name
1484 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1485 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1488 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1489 """Create a datatype declaration.
1491 :param name: the name of the datatype
1492 :param isCoDatatype: true if a codatatype is to be constructed
1493 :return: the DatatypeDecl
1495 cdef DatatypeDecl dd = DatatypeDecl(self)
1496 cdef vector[c_Sort] v
1499 if sorts_or_bool is None and isCoDatatype is None:
1500 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1501 elif sorts_or_bool is not None and isCoDatatype is None:
1502 if isinstance(sorts_or_bool, bool):
1503 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1504 <bint> sorts_or_bool)
1505 elif isinstance(sorts_or_bool, Sort):
1506 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1507 (<Sort> sorts_or_bool).csort)
1508 elif isinstance(sorts_or_bool, list):
1509 for s in sorts_or_bool:
1510 v.push_back((<Sort?> s).csort)
1511 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1512 <const vector[c_Sort]&> v)
1514 raise ValueError("Unhandled second argument type {}"
1515 .format(type(sorts_or_bool)))
1516 elif sorts_or_bool is not None and isCoDatatype is not None:
1517 if isinstance(sorts_or_bool, Sort):
1518 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1519 (<Sort> sorts_or_bool).csort,
1520 <bint> isCoDatatype)
1521 elif isinstance(sorts_or_bool, list):
1522 for s in sorts_or_bool:
1523 v.push_back((<Sort?> s).csort)
1524 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1525 <const vector[c_Sort]&> v,
1526 <bint> isCoDatatype)
1528 raise ValueError("Unhandled second argument type {}"
1529 .format(type(sorts_or_bool)))
1531 raise ValueError("Can't create DatatypeDecl with {}".format([type(a)
1538 def simplify(self, Term t):
1540 Simplify a formula without doing "much" work. Does not involve the
1541 SAT Engine in the simplification, but uses the current definitions,
1542 assertions, and the current partial model, if one has been constructed.
1543 It also involves theory normalization.
1545 :param t: the formula to simplify
1546 :return: the simplified formula
1548 cdef Term term = Term(self)
1549 term.cterm = self.csolver.simplify(t.cterm)
1552 def assertFormula(self, Term term):
1553 """ Assert a formula
1557 .. code-block:: smtlib
1561 :param term: the formula to assert
1563 self.csolver.assertFormula(term.cterm)
1567 Check satisfiability.
1571 .. code-block:: smtlib
1575 :return: the result of the satisfiability check.
1577 cdef Result r = Result()
1578 r.cr = self.csolver.checkSat()
1581 def mkSygusGrammar(self, boundVars, ntSymbols):
1583 Create a SyGuS grammar. The first non-terminal is treated as the
1584 starting non-terminal, so the order of non-terminals matters.
1586 :param boundVars: the parameters to corresponding synth-fun/synth-inv
1587 :param ntSymbols: the pre-declaration of the non-terminal symbols
1588 :return: the grammar
1590 cdef Grammar grammar = Grammar(self)
1591 cdef vector[c_Term] bvc
1592 cdef vector[c_Term] ntc
1593 for bv in boundVars:
1594 bvc.push_back((<Term?> bv).cterm)
1595 for nt in ntSymbols:
1596 ntc.push_back((<Term?> nt).cterm)
1597 grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1600 def mkSygusVar(self, Sort sort, str symbol=""):
1601 """Append symbol to the current list of universal variables.
1605 .. code-block:: smtlib
1607 ( declare-var <symbol> <sort> )
1609 :param sort: the sort of the universal variable
1610 :param symbol: the name of the universal variable
1611 :return: the universal variable
1613 cdef Term term = Term(self)
1614 term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode())
1617 def addSygusConstraint(self, Term t):
1619 Add a formula to the set of SyGuS constraints.
1623 .. code-block:: smtlib
1625 ( constraint <term> )
1627 :param term: the formula to add as a constraint
1629 self.csolver.addSygusConstraint(t.cterm)
1631 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1633 Add a set of SyGuS constraints to the current state that correspond to an
1634 invariant synthesis problem.
1638 .. code-block:: smtlib
1640 ( inv-constraint <inv> <pre> <trans> <post> )
1642 :param inv: the function-to-synthesize
1643 :param pre: the pre-condition
1644 :param trans: the transition relation
1645 :param post: the post-condition
1647 self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1649 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1651 Synthesize n-ary function following specified syntactic constraints.
1655 .. code-block:: smtlib
1657 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1659 :param symbol: the name of the function
1660 :param boundVars: the parameters to this function
1661 :param sort: the sort of the return value of this function
1662 :param grammar: the syntactic constraints
1663 :return: the function
1665 cdef Term term = Term(self)
1666 cdef vector[c_Term] v
1667 for bv in bound_vars:
1668 v.push_back((<Term?> bv).cterm)
1670 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1672 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1675 def checkSynth(self):
1677 Try to find a solution for the synthesis conjecture corresponding to the
1678 current list of functions-to-synthesize, universal variables and
1683 .. code-block:: smtlib
1687 :return: the result of the synthesis conjecture.
1689 cdef Result r = Result()
1690 r.cr = self.csolver.checkSynth()
1693 def checkSynthNext(self):
1695 Try to find a next solution for the synthesis conjecture corresponding
1696 to the current list of functions-to-synthesize, universal variables and
1697 constraints. Must be called immediately after a successful call to
1698 check-synth or check-synth-next. Requires incremental mode.
1702 .. code-block:: smtlib
1706 :return: the result of the check, which is unsat if the check succeeded,
1707 in which case solutions are available via getSynthSolutions.
1709 cdef Result r = Result()
1710 r.cr = self.csolver.checkSynthNext()
1713 def getSynthSolution(self, Term term):
1715 Get the synthesis solution of the given term. This method should be
1716 called immediately after the solver answers unsat for sygus input.
1718 :param term: the term for which the synthesis solution is queried
1719 :return: the synthesis solution of the given term
1721 cdef Term t = Term(self)
1722 t.cterm = self.csolver.getSynthSolution(term.cterm)
1725 def getSynthSolutions(self, list terms):
1727 Get the synthesis solutions of the given terms. This method should be
1728 called immediately after the solver answers unsat for sygus input.
1730 :param terms: the terms for which the synthesis solutions is queried
1731 :return: the synthesis solutions of the given terms
1734 cdef vector[c_Term] vec
1736 vec.push_back((<Term?> t).cterm)
1737 cresult = self.csolver.getSynthSolutions(vec)
1745 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1747 Synthesize invariant.
1751 .. code-block:: smtlib
1753 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1755 :param symbol: the name of the invariant
1756 :param boundVars: the parameters to this invariant
1757 :param grammar: the syntactic constraints
1758 :return: the invariant
1760 cdef Term term = Term(self)
1761 cdef vector[c_Term] v
1762 for bv in bound_vars:
1763 v.push_back((<Term?> bv).cterm)
1765 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
1767 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
1770 @expand_list_arg(num_req_args=0)
1771 def checkSatAssuming(self, *assumptions):
1772 """ Check satisfiability assuming the given formula.
1776 .. code-block:: smtlib
1778 ( check-sat-assuming ( <prop_literal> ) )
1780 :param assumptions: the formulas to assume, as a list or as distinct arguments
1781 :return: the result of the satisfiability check.
1783 cdef Result r = Result()
1784 # used if assumptions is a list of terms
1785 cdef vector[c_Term] v
1786 for a in assumptions:
1787 v.push_back((<Term?> a).cterm)
1788 r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
1791 @expand_list_arg(num_req_args=0)
1792 def checkEntailed(self, *assumptions):
1793 """Check entailment of the given formula w.r.t. the current set of assertions.
1795 :param terms: the formulas to check entailment for, as a list or as distinct arguments
1796 :return: the result of the entailment check.
1798 cdef Result r = Result()
1799 # used if assumptions is a list of terms
1800 cdef vector[c_Term] v
1801 for a in assumptions:
1802 v.push_back((<Term?> a).cterm)
1803 r.cr = self.csolver.checkEntailed(<const vector[c_Term]&> v)
1806 @expand_list_arg(num_req_args=1)
1807 def declareDatatype(self, str symbol, *ctors):
1809 Create datatype sort.
1813 .. code-block:: smtlib
1815 ( declare-datatype <symbol> <datatype_decl> )
1817 :param symbol: the name of the datatype sort
1818 :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
1819 :return: the datatype sort
1821 cdef Sort sort = Sort(self)
1822 cdef vector[c_DatatypeConstructorDecl] v
1825 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1826 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1829 def declareFun(self, str symbol, list sorts, Sort sort):
1830 """Declare n-ary function symbol.
1834 .. code-block:: smtlib
1836 ( declare-fun <symbol> ( <sort>* ) <sort> )
1838 :param symbol: the name of the function
1839 :param sorts: the sorts of the parameters to this function
1840 :param sort: the sort of the return value of this function
1841 :return: the function
1843 cdef Term term = Term(self)
1844 cdef vector[c_Sort] v
1846 v.push_back((<Sort?> s).csort)
1847 term.cterm = self.csolver.declareFun(symbol.encode(),
1848 <const vector[c_Sort]&> v,
1852 def declareSort(self, str symbol, int arity):
1853 """Declare uninterpreted sort.
1857 .. code-block:: smtlib
1859 ( declare-sort <symbol> <numeral> )
1861 :param symbol: the name of the sort
1862 :param arity: the arity of the sort
1865 cdef Sort sort = Sort(self)
1866 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
1869 def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
1870 """Define n-ary function.
1874 .. code-block:: smtlib
1876 ( define-fun <function_def> )
1878 :param symbol: the name of the function
1879 :param bound_vars: the parameters to this function
1880 :param sort: the sort of the return value of this function
1881 :param term: the function body
1882 :param glbl: determines whether this definition is global (i.e. persists when popping the context)
1883 :return: the function
1885 cdef Term fun = Term(self)
1886 cdef vector[c_Term] v
1887 for bv in bound_vars:
1888 v.push_back((<Term?> bv).cterm)
1890 fun.cterm = self.csolver.defineFun(symbol.encode(),
1891 <const vector[c_Term] &> v,
1897 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1898 """Define recursive functions.
1902 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1903 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1908 .. code-block:: smtlib
1910 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1912 Create elements of parameter ``funs`` with mkConst().
1914 :param funs: the sorted functions
1915 :param bound_vars: the list of parameters to the functions
1916 :param terms: the list of function bodies of the functions
1917 :param global: determines whether this definition is global (i.e. persists when popping the context)
1918 :return: the function
1920 cdef Term term = Term(self)
1921 cdef vector[c_Term] v
1922 for bv in bound_vars:
1923 v.push_back((<Term?> bv).cterm)
1926 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
1927 <const vector[c_Term] &> v,
1928 (<Sort?> sort_or_term).csort,
1932 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
1933 <const vector[c_Term]&> v,
1934 (<Term?> sort_or_term).cterm,
1939 def defineFunsRec(self, funs, bound_vars, terms):
1940 """Define recursive functions.
1944 .. code-block:: smtlib
1946 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1948 Create elements of parameter ``funs`` with mkConst().
1950 :param funs: the sorted functions
1951 :param bound_vars: the list of parameters to the functions
1952 :param terms: the list of function bodies of the functions
1953 :param global: determines whether this definition is global (i.e. persists when popping the context)
1954 :return: the function
1956 cdef vector[c_Term] vf
1957 cdef vector[vector[c_Term]] vbv
1958 cdef vector[c_Term] vt
1961 vf.push_back((<Term?> f).cterm)
1963 cdef vector[c_Term] temp
1964 for v in bound_vars:
1966 temp.push_back((<Term?> t).cterm)
1971 vf.push_back((<Term?> t).cterm)
1973 def getAssertions(self):
1974 """Get the list of asserted formulas.
1978 .. code-block:: smtlib
1982 :return: the list of asserted formulas
1985 for a in self.csolver.getAssertions():
1988 assertions.append(term)
1991 def getInfo(self, str flag):
1992 """Get info from the solver.
1996 .. code-block:: smtlib
1998 ( get-info <info_flag> )
2000 :param flag: the info flag
2003 return self.csolver.getInfo(flag.encode())
2005 def getOption(self, str option):
2006 """Get the value of a given option.
2010 .. code-block:: smtlib
2012 ( get-option <keyword> )
2014 :param option: the option for which the value is queried
2015 :return: a string representation of the option value
2017 return self.csolver.getOption(option.encode())
2019 def getUnsatAssumptions(self):
2021 Get the set of unsat ("failed") assumptions.
2025 .. code-block:: smtlib
2027 ( get-unsat-assumptions )
2029 Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
2031 :return: the set of unsat assumptions.
2034 for a in self.csolver.getUnsatAssumptions():
2037 assumptions.append(term)
2040 def getUnsatCore(self):
2041 """Get the unsatisfiable core.
2045 .. code-block:: smtlib
2049 Requires to enable option :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
2051 :return: a set of terms representing the unsatisfiable core
2054 for a in self.csolver.getUnsatCore():
2060 def getValue(self, Term t):
2061 """Get the value of the given term in the current model.
2065 .. code-block:: smtlib
2067 ( get-value ( <term> ) )
2069 :param term: the term for which the value is queried
2070 :return: the value of the given term
2072 cdef Term term = Term(self)
2073 term.cterm = self.csolver.getValue(t.cterm)
2076 def getModelDomainElements(self, Sort s):
2078 Get the domain elements of uninterpreted sort s in the current model. The
2079 current model interprets s as the finite sort whose domain elements are
2080 given in the return value of this method.
2082 :param s: The uninterpreted sort in question
2083 :return: the domain elements of s in the current model
2086 cresult = self.csolver.getModelDomainElements(s.csort)
2093 def isModelCoreSymbol(self, Term v):
2095 This returns false if the model value of free constant v was not
2096 essential for showing the satisfiability of the last call to checkSat
2097 using the current model. This method will only return false (for any v)
2098 if the model-cores option has been set.
2100 :param v: The term in question
2101 :return: true if v is a model core symbol
2103 return self.csolver.isModelCoreSymbol(v.cterm)
2105 def getValueSepHeap(self):
2106 """When using separation logic, obtain the term for the heap.
2108 :return: The term for the heap
2110 cdef Term term = Term(self)
2111 term.cterm = self.csolver.getValueSepHeap()
2114 def getValueSepNil(self):
2115 """When using separation logic, obtain the term for nil.
2117 :return: The term for nil
2119 cdef Term term = Term(self)
2120 term.cterm = self.csolver.getValueSepNil()
2123 def declareSepHeap(self, Sort locType, Sort dataType):
2125 When using separation logic, this sets the location sort and the
2126 datatype sort to the given ones. This method should be invoked exactly
2127 once, before any separation logic constraints are provided.
2129 :param locSort: The location sort of the heap
2130 :param dataSort: The data sort of the heap
2132 self.csolver.declareSepHeap(locType.csort, dataType.csort)
2134 def declarePool(self, str symbol, Sort sort, initValue):
2135 """Declare a symbolic pool of terms with the given initial value.
2139 .. code-block:: smtlib
2141 ( declare-pool <symbol> <sort> ( <term>* ) )
2143 :param symbol: The name of the pool
2144 :param sort: The sort of the elements of the pool.
2145 :param initValue: The initial value of the pool
2147 cdef Term term = Term(self)
2148 cdef vector[c_Term] niv
2150 niv.push_back((<Term?> v).cterm)
2151 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
2154 def pop(self, nscopes=1):
2155 """Pop ``nscopes`` level(s) from the assertion stack.
2159 .. code-block:: smtlib
2163 :param nscopes: the number of levels to pop
2165 self.csolver.pop(nscopes)
2167 def push(self, nscopes=1):
2168 """ Push ``nscopes`` level(s) to the assertion stack.
2172 .. code-block:: smtlib
2176 :param nscopes: the number of levels to push
2178 self.csolver.push(nscopes)
2180 def resetAssertions(self):
2182 Remove all assertions.
2186 .. code-block:: smtlib
2188 ( reset-assertions )
2191 self.csolver.resetAssertions()
2193 def setInfo(self, str keyword, str value):
2198 .. code-block:: smtlib
2200 ( set-info <attribute> )
2202 :param keyword: the info flag
2203 :param value: the value of the info flag
2205 self.csolver.setInfo(keyword.encode(), value.encode())
2207 def setLogic(self, str logic):
2212 .. code-block:: smtlib
2214 ( set-logic <symbol> )
2216 :param logic: the logic to set
2218 self.csolver.setLogic(logic.encode())
2220 def setOption(self, str option, str value):
2225 .. code-block:: smtlib
2227 ( set-option <option> )
2229 :param option: the option name
2230 :param value: the option value
2232 self.csolver.setOption(option.encode(), value.encode())
2234 def getInterpolant(self, Term conj, *args):
2235 """Get an interpolant.
2239 .. code-block:: smtlib
2241 ( get-interpol <conj> )
2242 ( get-interpol <conj> <grammar> )
2244 Requires option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
2246 Supports the following variants:
2248 - ``bool getInteprolant(Term conj, Term output)``
2249 - ``bool getInteprolant(Term conj, Grammar grammar, Term output)``
2251 :param conj: the conjecture term
2252 :param output: the term where the result will be stored
2253 :param grammar: a grammar for the inteprolant
2254 :return: True iff an interpolant was found
2258 assert isinstance(args[0], Term)
2259 result = self.csolver.getInterpolant(conj.cterm, (<Term ?> args[0]).cterm)
2261 assert len(args) == 2
2262 assert isinstance(args[0], Grammar)
2263 assert isinstance(args[1], Term)
2264 result = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
2268 def getInterpolantNext(self, Term output):
2270 Get the next interpolant. Can only be called immediately after
2271 a succesful call to get-interpol or get-interpol-next.
2272 Is guaranteed to produce a syntactically different interpolant wrt the
2273 last returned interpolant if successful.
2277 .. code-block:: smtlib
2279 ( get-interpol-next )
2281 Requires to enable incremental mode, and
2282 option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
2284 :param output: the term where the result will be stored
2285 :return: True iff an interpolant was found
2287 result = self.csolver.getInterpolantNext(output.cterm)
2290 def getAbduct(self, Term conj, *args):
2295 .. code-block:: smtlib
2297 ( get-abduct <conj> )
2298 ( get-abduct <conj> <grammar> )
2300 Requires to enable option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2302 Supports the following variants:
2304 - ``bool getAbduct(Term conj, Term output)``
2305 - ``bool getAbduct(Term conj, Grammar grammar, Term output)``
2307 :param conj: the conjecture term
2308 :param output: the term where the result will be stored
2309 :param grammar: a grammar for the abduct
2310 :return: True iff an abduct was found
2314 assert isinstance(args[0], Term)
2315 result = self.csolver.getAbduct(conj.cterm, (<Term ?> args[0]).cterm)
2317 assert len(args) == 2
2318 assert isinstance(args[0], Grammar)
2319 assert isinstance(args[1], Term)
2320 result = self.csolver.getAbduct(conj.cterm, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
2323 def getAbductNext(self, Term output):
2325 Get the next abduct. Can only be called immediately after
2326 a succesful call to get-abduct or get-abduct-next.
2327 Is guaranteed to produce a syntactically different abduct wrt the
2328 last returned abduct if successful.
2332 .. code-block:: smtlib
2336 Requires to enable incremental mode, and
2337 option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2338 :param output: the term where the result will be stored
2339 :return: True iff an abduct was found
2341 result = self.csolver.getAbductNext(output.cterm)
2348 The sort of a cvc5 term.
2352 def __cinit__(self, Solver solver):
2353 # csort always set by Solver
2354 self.solver = solver
2356 def __eq__(self, Sort other):
2357 return self.csort == other.csort
2359 def __ne__(self, Sort other):
2360 return self.csort != other.csort
2362 def __lt__(self, Sort other):
2363 return self.csort < other.csort
2365 def __gt__(self, Sort other):
2366 return self.csort > other.csort
2368 def __le__(self, Sort other):
2369 return self.csort <= other.csort
2371 def __ge__(self, Sort other):
2372 return self.csort >= other.csort
2375 return self.csort.toString().decode()
2378 return self.csort.toString().decode()
2381 return csorthash(self.csort)
2383 def hasSymbol(self):
2384 """:return: True iff this sort has a symbol."""
2385 return self.csort.hasSymbol()
2387 def getSymbol(self):
2389 Asserts :py:meth:`hasSymbol()`.
2391 :return: the raw symbol of the sort.
2393 return self.csort.getSymbol().decode()
2396 """:return: True if this Sort is a null sort."""
2397 return self.csort.isNull()
2399 def isBoolean(self):
2401 Is this a Boolean sort?
2403 :return: True if the sort is the Boolean sort.
2405 return self.csort.isBoolean()
2407 def isInteger(self):
2409 Is this an integer sort?
2411 :return: True if the sort is the integer sort.
2413 return self.csort.isInteger()
2417 Is this a real sort?
2419 :return: True if the sort is the real sort.
2421 return self.csort.isReal()
2425 Is this a string sort?
2427 :return: True if the sort is the string sort.
2429 return self.csort.isString()
2433 Is this a regexp sort?
2435 :return: True if the sort is the regexp sort.
2437 return self.csort.isRegExp()
2439 def isRoundingMode(self):
2441 Is this a rounding mode sort?
2443 :return: True if the sort is the rounding mode sort.
2445 return self.csort.isRoundingMode()
2447 def isBitVector(self):
2449 Is this a bit-vector sort?
2451 :return: True if the sort is a bit-vector sort.
2453 return self.csort.isBitVector()
2455 def isFloatingPoint(self):
2457 Is this a floating-point sort?
2459 :return: True if the sort is a bit-vector sort.
2461 return self.csort.isFloatingPoint()
2463 def isDatatype(self):
2465 Is this a datatype sort?
2467 :return: True if the sort is a datatype sort.
2469 return self.csort.isDatatype()
2471 def isParametricDatatype(self):
2473 Is this a parametric datatype sort?
2475 :return: True if the sort is a parametric datatype sort.
2477 return self.csort.isParametricDatatype()
2479 def isConstructor(self):
2481 Is this a constructor sort?
2483 :return: True if the sort is a constructor sort.
2485 return self.csort.isConstructor()
2487 def isSelector(self):
2489 Is this a selector sort?
2491 :return: True if the sort is a selector sort.
2493 return self.csort.isSelector()
2497 Is this a tester sort?
2499 :return: True if the sort is a selector sort.
2501 return self.csort.isTester()
2503 def isUpdater(self):
2505 Is this a datatype updater sort?
2507 :return: True if the sort is a datatype updater sort.
2509 return self.csort.isUpdater()
2511 def isFunction(self):
2513 Is this a function sort?
2515 :return: True if the sort is a function sort.
2517 return self.csort.isFunction()
2519 def isPredicate(self):
2521 Is this a predicate sort?
2522 That is, is this a function sort mapping to Boolean? All predicate
2523 sorts are also function sorts.
2525 :return: True if the sort is a predicate sort.
2527 return self.csort.isPredicate()
2531 Is this a tuple sort?
2533 :return: True if the sort is a tuple sort.
2535 return self.csort.isTuple()
2539 Is this a record sort?
2541 :return: True if the sort is a record sort.
2543 return self.csort.isRecord()
2547 Is this an array sort?
2549 :return: True if the sort is an array sort.
2551 return self.csort.isArray()
2557 :return: True if the sort is a set sort.
2559 return self.csort.isSet()
2565 :return: True if the sort is a bag sort.
2567 return self.csort.isBag()
2569 def isSequence(self):
2571 Is this a sequence sort?
2573 :return: True if the sort is a sequence sort.
2575 return self.csort.isSequence()
2577 def isUninterpretedSort(self):
2579 Is this a sort uninterpreted?
2581 :return: True if the sort is uninterpreted.
2583 return self.csort.isUninterpretedSort()
2585 def isSortConstructor(self):
2587 Is this a sort constructor kind?
2589 :return: True if this a sort constructor kind.
2591 return self.csort.isSortConstructor()
2593 def isFirstClass(self):
2595 Is this a first-class sort?
2596 First-class sorts are sorts for which:
2598 1. we handle equalities between terms of that type, and
2599 2. they are allowed to be parameters of parametric sorts
2600 (e.g. index or element sorts of arrays).
2602 Examples of sorts that are not first-class include sort constructor
2603 sorts and regular expression sorts.
2605 :return: True if the sort is a first-class sort.
2607 return self.csort.isFirstClass()
2609 def isFunctionLike(self):
2611 Is this a function-LIKE sort?
2613 Anything function-like except arrays (e.g., datatype selectors) is
2614 considered a function here. Function-like terms can not be the argument
2615 or return value for any term that is function-like.
2616 This is mainly to avoid higher order.
2618 .. note:: Arrays are explicitly not considered function-like here.
2620 :return: True if this is a function-like sort
2622 return self.csort.isFunctionLike()
2624 def isSubsortOf(self, Sort sort):
2626 Is this sort a subsort of the given sort?
2628 :return: True if this sort is a subsort of s
2630 return self.csort.isSubsortOf(sort.csort)
2632 def getDatatype(self):
2634 :return: the underlying datatype of a datatype sort
2636 cdef Datatype d = Datatype(self.solver)
2637 d.cd = self.csort.getDatatype()
2640 def instantiate(self, params):
2642 Instantiate a parameterized datatype/sort sort.
2643 Create sorts parameter with :py:meth:`Solver.mkParamSort()`
2645 :param params: the list of sort parameters to instantiate with
2647 cdef Sort sort = Sort(self.solver)
2648 cdef vector[c_Sort] v
2650 v.push_back((<Sort?> s).csort)
2651 sort.csort = self.csort.instantiate(v)
2654 def substitute(self, sort_or_list_1, sort_or_list_2):
2656 Substitution of Sorts.
2658 :param sort_or_list_1: the subsort or subsorts to be substituted within this sort.
2659 :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort.
2662 # The resulting sort after substitution
2663 cdef Sort sort = Sort(self.solver)
2664 # lists for substitutions
2665 cdef vector[c_Sort] ces
2666 cdef vector[c_Sort] creplacements
2668 # normalize the input parameters to be lists
2669 if isinstance(sort_or_list_1, list):
2670 assert isinstance(sort_or_list_2, list)
2672 replacements = sort_or_list_2
2673 if len(es) != len(replacements):
2674 raise RuntimeError("Expecting list inputs to substitute to "
2675 "have the same length but got: "
2676 "{} and {}".format(len(es), len(replacements)))
2678 for e, r in zip(es, replacements):
2679 ces.push_back((<Sort?> e).csort)
2680 creplacements.push_back((<Sort?> r).csort)
2683 # add the single elements to the vectors
2684 ces.push_back((<Sort?> sort_or_list_1).csort)
2685 creplacements.push_back((<Sort?> sort_or_list_2).csort)
2687 # call the API substitute method with lists
2688 sort.csort = self.csort.substitute(ces, creplacements)
2692 def getConstructorArity(self):
2694 :return: the arity of a constructor sort.
2696 return self.csort.getConstructorArity()
2698 def getConstructorDomainSorts(self):
2700 :return: the domain sorts of a constructor sort
2703 for s in self.csort.getConstructorDomainSorts():
2704 sort = Sort(self.solver)
2706 domain_sorts.append(sort)
2709 def getConstructorCodomainSort(self):
2711 :return: the codomain sort of a constructor sort
2713 cdef Sort sort = Sort(self.solver)
2714 sort.csort = self.csort.getConstructorCodomainSort()
2717 def getSelectorDomainSort(self):
2719 :return: the domain sort of a selector sort
2721 cdef Sort sort = Sort(self.solver)
2722 sort.csort = self.csort.getSelectorDomainSort()
2725 def getSelectorCodomainSort(self):
2727 :return: the codomain sort of a selector sort
2729 cdef Sort sort = Sort(self.solver)
2730 sort.csort = self.csort.getSelectorCodomainSort()
2733 def getTesterDomainSort(self):
2735 :return: the domain sort of a tester sort
2737 cdef Sort sort = Sort(self.solver)
2738 sort.csort = self.csort.getTesterDomainSort()
2741 def getTesterCodomainSort(self):
2743 :return: the codomain sort of a tester sort, which is the Boolean sort
2745 cdef Sort sort = Sort(self.solver)
2746 sort.csort = self.csort.getTesterCodomainSort()
2749 def getFunctionArity(self):
2751 :return: the arity of a function sort
2753 return self.csort.getFunctionArity()
2755 def getFunctionDomainSorts(self):
2757 :return: the domain sorts of a function sort
2760 for s in self.csort.getFunctionDomainSorts():
2761 sort = Sort(self.solver)
2763 domain_sorts.append(sort)
2766 def getFunctionCodomainSort(self):
2768 :return: the codomain sort of a function sort
2770 cdef Sort sort = Sort(self.solver)
2771 sort.csort = self.csort.getFunctionCodomainSort()
2774 def getArrayIndexSort(self):
2776 :return: the array index sort of an array sort
2778 cdef Sort sort = Sort(self.solver)
2779 sort.csort = self.csort.getArrayIndexSort()
2782 def getArrayElementSort(self):
2784 :return: the array element sort of an array sort
2786 cdef Sort sort = Sort(self.solver)
2787 sort.csort = self.csort.getArrayElementSort()
2790 def getSetElementSort(self):
2792 :return: the element sort of a set sort
2794 cdef Sort sort = Sort(self.solver)
2795 sort.csort = self.csort.getSetElementSort()
2798 def getBagElementSort(self):
2800 :return: the element sort of a bag sort
2802 cdef Sort sort = Sort(self.solver)
2803 sort.csort = self.csort.getBagElementSort()
2806 def getSequenceElementSort(self):
2808 :return: the element sort of a sequence sort
2810 cdef Sort sort = Sort(self.solver)
2811 sort.csort = self.csort.getSequenceElementSort()
2814 def getUninterpretedSortName(self):
2816 :return: the name of an uninterpreted sort
2818 return self.csort.getUninterpretedSortName().decode()
2820 def isUninterpretedSortParameterized(self):
2822 :return: True if an uninterpreted sort is parameterized
2824 return self.csort.isUninterpretedSortParameterized()
2826 def getUninterpretedSortParamSorts(self):
2828 :return: the parameter sorts of an uninterpreted sort
2831 for s in self.csort.getUninterpretedSortParamSorts():
2832 sort = Sort(self.solver)
2834 param_sorts.append(sort)
2837 def getSortConstructorName(self):
2839 :return: the name of a sort constructor sort
2841 return self.csort.getSortConstructorName().decode()
2843 def getSortConstructorArity(self):
2845 :return: the arity of a sort constructor sort
2847 return self.csort.getSortConstructorArity()
2849 def getBitVectorSize(self):
2851 :return: the bit-width of the bit-vector sort
2853 return self.csort.getBitVectorSize()
2855 def getFloatingPointExponentSize(self):
2857 :return: the bit-width of the exponent of the floating-point sort
2859 return self.csort.getFloatingPointExponentSize()
2861 def getFloatingPointSignificandSize(self):
2863 :return: the width of the significand of the floating-point sort
2865 return self.csort.getFloatingPointSignificandSize()
2867 def getDatatypeParamSorts(self):
2869 Return the parameters of a parametric datatype sort. If this sort
2870 is a non-instantiated parametric datatype, this returns the
2871 parameter sorts of the underlying datatype. If this sort is an
2872 instantiated parametric datatype, then this returns the sort
2873 parameters that were used to construct the sort via
2874 :py:meth:`instantiate()`.
2876 :return: the parameter sorts of a parametric datatype sort
2879 for s in self.csort.getDatatypeParamSorts():
2880 sort = Sort(self.solver)
2882 param_sorts.append(sort)
2885 def getDatatypeArity(self):
2887 :return: the arity of a datatype sort
2889 return self.csort.getDatatypeArity()
2891 def getTupleLength(self):
2893 :return: the length of a tuple sort
2895 return self.csort.getTupleLength()
2897 def getTupleSorts(self):
2899 :return: the element sorts of a tuple sort
2902 for s in self.csort.getTupleSorts():
2903 sort = Sort(self.solver)
2905 tuple_sorts.append(sort)
2912 Wrapper class for :cpp:class:`cvc5::api::Term`.
2916 def __cinit__(self, Solver solver):
2917 # cterm always set in the Solver object
2918 self.solver = solver
2920 def __eq__(self, Term other):
2921 return self.cterm == other.cterm
2923 def __ne__(self, Term other):
2924 return self.cterm != other.cterm
2926 def __lt__(self, Term other):
2927 return self.cterm < other.cterm
2929 def __gt__(self, Term other):
2930 return self.cterm > other.cterm
2932 def __le__(self, Term other):
2933 return self.cterm <= other.cterm
2935 def __ge__(self, Term other):
2936 return self.cterm >= other.cterm
2938 def __getitem__(self, int index):
2939 cdef Term term = Term(self.solver)
2941 term.cterm = self.cterm[index]
2943 raise ValueError("Expecting a non-negative integer or string")
2947 return self.cterm.toString().decode()
2950 return self.cterm.toString().decode()
2953 for ci in self.cterm:
2954 term = Term(self.solver)
2959 return ctermhash(self.cterm)
2961 def getNumChildren(self):
2962 """:return: the number of children of this term."""
2963 return self.cterm.getNumChildren()
2966 """:return: the id of this term."""
2967 return self.cterm.getId()
2970 """:return: the :py:class:`pycvc5.Kind` of this term."""
2971 return Kind(<int> self.cterm.getKind())
2974 """:return: the :py:class:`pycvc5.Sort` of this term."""
2975 cdef Sort sort = Sort(self.solver)
2976 sort.csort = self.cterm.getSort()
2979 def substitute(self, term_or_list_1, term_or_list_2):
2981 :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.
2983 # The resulting term after substitution
2984 cdef Term term = Term(self.solver)
2985 # lists for substitutions
2986 cdef vector[c_Term] ces
2987 cdef vector[c_Term] creplacements
2989 # normalize the input parameters to be lists
2990 if isinstance(term_or_list_1, list):
2991 assert isinstance(term_or_list_2, list)
2993 replacements = term_or_list_2
2994 if len(es) != len(replacements):
2995 raise RuntimeError("Expecting list inputs to substitute to "
2996 "have the same length but got: "
2997 "{} and {}".format(len(es), len(replacements)))
2999 for e, r in zip(es, replacements):
3000 ces.push_back((<Term?> e).cterm)
3001 creplacements.push_back((<Term?> r).cterm)
3004 # add the single elements to the vectors
3005 ces.push_back((<Term?> term_or_list_1).cterm)
3006 creplacements.push_back((<Term?> term_or_list_2).cterm)
3008 # call the API substitute method with lists
3009 term.cterm = self.cterm.substitute(ces, creplacements)
3013 """:return: True iff this term has an operator."""
3014 return self.cterm.hasOp()
3018 .. note:: This is safe to call when :py:meth:`hasOp()` returns True.
3020 :return: the :py:class:`pycvc5.Op` used to create this Term.
3022 cdef Op op = Op(self.solver)
3023 op.cop = self.cterm.getOp()
3026 def hasSymbol(self):
3027 """:return: True iff this term has a symbol."""
3028 return self.cterm.hasSymbol()
3030 def getSymbol(self):
3032 Asserts :py:meth:`hasSymbol()`.
3034 :return: the raw symbol of the term.
3036 return self.cterm.getSymbol().decode()
3039 """:return: True iff this term is a null term."""
3040 return self.cterm.isNull()
3046 :return: the Boolean negation of this term.
3048 cdef Term term = Term(self.solver)
3049 term.cterm = self.cterm.notTerm()
3052 def andTerm(self, Term t):
3056 :param t: a Boolean term
3057 :return: the conjunction of this term and the given term
3059 cdef Term term = Term(self.solver)
3060 term.cterm = self.cterm.andTerm((<Term> t).cterm)
3063 def orTerm(self, Term t):
3067 :param t: a Boolean term
3068 :return: the disjunction of this term and the given term
3070 cdef Term term = Term(self.solver)
3071 term.cterm = self.cterm.orTerm(t.cterm)
3074 def xorTerm(self, Term t):
3076 Boolean exclusive or.
3078 :param t: a Boolean term
3079 :return: the exclusive disjunction of this term and the given term
3081 cdef Term term = Term(self.solver)
3082 term.cterm = self.cterm.xorTerm(t.cterm)
3085 def eqTerm(self, Term t):
3089 :param t: a Boolean term
3090 :return: the Boolean equivalence of this term and the given term
3092 cdef Term term = Term(self.solver)
3093 term.cterm = self.cterm.eqTerm(t.cterm)
3096 def impTerm(self, Term t):
3098 Boolean Implication.
3100 :param t: a Boolean term
3101 :return: the implication of this term and the given term
3103 cdef Term term = Term(self.solver)
3104 term.cterm = self.cterm.impTerm(t.cterm)
3107 def iteTerm(self, Term then_t, Term else_t):
3109 If-then-else with this term as the Boolean condition.
3111 :param then_t: the `then` term
3112 :param else_t: the `else` term
3113 :return: the if-then-else term with this term as the Boolean condition
3115 cdef Term term = Term(self.solver)
3116 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
3119 def isConstArray(self):
3120 """:return: True iff this term is a constant array."""
3121 return self.cterm.isConstArray()
3123 def getConstArrayBase(self):
3125 Asserts :py:meth:`isConstArray()`.
3127 :return: the base (element stored at all indicies) of this constant array
3129 cdef Term term = Term(self.solver)
3130 term.cterm = self.cterm.getConstArrayBase()
3133 def isBooleanValue(self):
3134 """:return: True iff this term is a Boolean value."""
3135 return self.cterm.isBooleanValue()
3137 def getBooleanValue(self):
3139 Asserts :py:meth:`isBooleanValue()`
3141 :return: the representation of a Boolean value as a native Boolean value.
3143 return self.cterm.getBooleanValue()
3145 def isStringValue(self):
3146 """:return: True iff this term is a string value."""
3147 return self.cterm.isStringValue()
3149 def getStringValue(self):
3151 Asserts :py:meth:`isStringValue()`.
3154 This method is not to be confused with :py:meth:`__str__()` which
3155 returns the term in some string representation, whatever data it
3158 :return: the string term as a native string value.
3160 cdef Py_ssize_t size
3161 cdef c_wstring s = self.cterm.getStringValue()
3162 return PyUnicode_FromWideChar(s.data(), s.size())
3164 def getRealOrIntegerValueSign(self):
3166 Get integer or real value sign. Must be called on integer or real values,
3167 or otherwise an exception is thrown.
3169 :return: 0 if this term is zero, -1 if this term is a negative real or
3170 integer value, 1 if this term is a positive real or integer value.
3172 return self.cterm.getRealOrIntegerValueSign()
3174 def isIntegerValue(self):
3175 """:return: True iff this term is an integer value."""
3176 return self.cterm.isIntegerValue()
3178 def getIntegerValue(self):
3180 Asserts :py:meth:`isIntegerValue()`.
3182 :return: the integer term as a native python integer.
3184 return int(self.cterm.getIntegerValue().decode())
3186 def isAbstractValue(self):
3187 """:return: True iff this term is an abstract value."""
3188 return self.cterm.isAbstractValue()
3190 def getAbstractValue(self):
3192 Asserts :py:meth:`isAbstractValue()`.
3194 :return: the representation of an abstract value as a string.
3196 return self.cterm.getAbstractValue().decode()
3198 def isFloatingPointPosZero(self):
3199 """:return: True iff the term is the floating-point value for positive zero."""
3200 return self.cterm.isFloatingPointPosZero()
3202 def isFloatingPointNegZero(self):
3203 """:return: True iff the term is the floating-point value for negative zero."""
3204 return self.cterm.isFloatingPointNegZero()
3206 def isFloatingPointPosInf(self):
3207 """:return: True iff the term is the floating-point value for positive infinity."""
3208 return self.cterm.isFloatingPointPosInf()
3210 def isFloatingPointNegInf(self):
3211 """:return: True iff the term is the floating-point value for negative infinity."""
3212 return self.cterm.isFloatingPointNegInf()
3214 def isFloatingPointNaN(self):
3215 """:return: True iff the term is the floating-point value for not a number."""
3216 return self.cterm.isFloatingPointNaN()
3218 def isFloatingPointValue(self):
3219 """:return: True iff this term is a floating-point value."""
3220 return self.cterm.isFloatingPointValue()
3222 def getFloatingPointValue(self):
3224 Asserts :py:meth:`isFloatingPointValue()`.
3226 :return: the representation of a floating-point value as a tuple of the exponent width, the significand width and a bit-vector value.
3228 cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
3229 cdef Term term = Term(self.solver)
3230 term.cterm = get2(t)
3231 return (get0(t), get1(t), term)
3233 def isSetValue(self):
3235 A term is a set value if it is considered to be a (canonical) constant
3236 set value. A canonical set value is one whose AST is:
3241 (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
3243 where ``c1 ... cn`` are values ordered by id such that
3244 ``c1 > ... > cn`` (see also :cpp:func:`cvc5::api::Term::operator>()`).
3247 A universe set term ``(kind SET_UNIVERSE)`` is not considered to be
3250 :return: True if the term is a set value.
3252 return self.cterm.isSetValue()
3254 def getSetValue(self):
3256 Asserts :py:meth:`isSetValue()`.
3258 :return: the representation of a set value as a set of terms.
3261 for e in self.cterm.getSetValue():
3262 term = Term(self.solver)
3267 def isSequenceValue(self):
3268 """:return: True iff this term is a sequence value."""
3269 return self.cterm.isSequenceValue()
3271 def getSequenceValue(self):
3273 Asserts :py:meth:`isSequenceValue()`.
3276 It is usually necessary for sequences to call
3277 :py:meth:`Solver.simplify()` to turn a sequence that is constructed
3278 by, e.g., concatenation of unit sequences, into a sequence value.
3280 :return: the representation of a sequence value as a vector of terms.
3283 for e in self.cterm.getSequenceValue():
3284 term = Term(self.solver)
3289 def isUninterpretedValue(self):
3290 """:return: True iff this term is a value from an uninterpreted sort."""
3291 return self.cterm.isUninterpretedValue()
3293 def getUninterpretedValue(self):
3295 Asserts :py:meth:`isUninterpretedValue()`.
3297 :return: the representation of an uninterpreted value as a pair of its sort and its index.
3299 cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue()
3300 cdef Sort sort = Sort(self.solver)
3301 sort.csort = p.first
3305 def isTupleValue(self):
3306 """:return: True iff this term is a tuple value."""
3307 return self.cterm.isTupleValue()
3309 def getTupleValue(self):
3311 Asserts :py:meth:`isTupleValue()`.
3313 :return: the representation of a tuple value as a vector of terms.
3316 for e in self.cterm.getTupleValue():
3317 term = Term(self.solver)
3322 def isRealValue(self):
3324 .. note:: A term of kind PI is not considered to be a real value.
3326 :return: True iff this term is a rational value.
3328 return self.cterm.isRealValue()
3330 def getRealValue(self):
3332 Asserts :py:meth:`isRealValue()`.
3334 :return: the representation of a rational value as a python Fraction.
3336 return Fraction(self.cterm.getRealValue().decode())
3338 def isBitVectorValue(self):
3339 """:return: True iff this term is a bit-vector value."""
3340 return self.cterm.isBitVectorValue()
3342 def getBitVectorValue(self, base = 2):
3344 Asserts :py:meth:`isBitVectorValue()`.
3345 Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexdecimal string).
3347 :return: the representation of a bit-vector value in string representation.
3349 return self.cterm.getBitVectorValue(base).decode()
3351 def toPythonObj(self):
3353 Converts a constant value Term to a Python object.
3357 - Boolean -- returns a Python bool
3358 - Int -- returns a Python int
3359 - Real -- returns a Python Fraction
3360 - BV -- returns a Python int (treats BV as unsigned)
3361 - String -- returns a Python Unicode string
3362 - Array -- returns a Python dict mapping indices to values. the constant base is returned as the default value
3366 if self.isBooleanValue():
3367 return self.getBooleanValue()
3368 elif self.isIntegerValue():
3369 return self.getIntegerValue()
3370 elif self.isRealValue():
3371 return self.getRealValue()
3372 elif self.isBitVectorValue():
3373 return int(self.getBitVectorValue(), 2)
3374 elif self.isStringValue():
3375 return self.getStringValue()
3376 elif self.getSort().isArray():
3382 # Array models are represented as a series of store operations
3383 # on a constant array
3386 if t.getKind().value == c_Kind.STORE:
3388 keys.append(t[1].toPythonObj())
3389 values.append(t[2].toPythonObj())
3390 to_visit.append(t[0])
3392 assert t.getKind().value == c_Kind.CONST_ARRAY
3393 base_value = t.getConstArrayBase().toPythonObj()
3395 assert len(keys) == len(values)
3396 assert base_value is not None
3398 # put everything in a dictionary with the constant
3399 # base as the result for any index not included in the stores
3400 res = defaultdict(lambda : base_value)
3401 for k, v in zip(keys, values):
3407 # Generate rounding modes
3408 cdef __rounding_modes = {
3409 <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
3410 <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
3411 <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
3412 <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
3413 <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway"
3416 mod_ref = sys.modules[__name__]
3417 for rm_int, name in __rounding_modes.items():
3418 r = RoundingMode(rm_int)
3420 if name in dir(mod_ref):
3421 raise RuntimeError("Redefinition of Python RoundingMode %s."%name)
3423 setattr(mod_ref, name, r)
3430 # Generate unknown explanations
3431 cdef __unknown_explanations = {
3432 <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
3433 <int> INCOMPLETE: "Incomplete",
3434 <int> TIMEOUT: "Timeout",
3435 <int> RESOURCEOUT: "Resourceout",
3436 <int> MEMOUT: "Memout",
3437 <int> INTERRUPTED: "Interrupted",
3438 <int> NO_STATUS: "NoStatus",
3439 <int> UNSUPPORTED: "Unsupported",
3440 <int> OTHER: "Other",
3441 <int> UNKNOWN_REASON: "UnknownReason"
3444 for ue_int, name in __unknown_explanations.items():
3445 u = UnknownExplanation(ue_int)
3447 if name in dir(mod_ref):
3448 raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
3450 setattr(mod_ref, name, u)