1 from collections import defaultdict
2 from fractions import Fraction
3 from functools import wraps
6 from cython.operator cimport dereference, preincrement
8 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
9 from libc.stddef cimport wchar_t
11 from libcpp cimport bool as c_bool
12 from libcpp.pair cimport pair
13 from libcpp.set cimport set as c_set
14 from libcpp.string cimport string
15 from libcpp.vector cimport vector
17 from cvc5 cimport cout
18 from cvc5 cimport Datatype as c_Datatype
19 from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
20 from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
21 from cvc5 cimport DatatypeDecl as c_DatatypeDecl
22 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
23 from cvc5 cimport Result as c_Result
24 from cvc5 cimport SynthResult as c_SynthResult
25 from cvc5 cimport Op as c_Op
26 from cvc5 cimport OptionInfo as c_OptionInfo
27 from cvc5 cimport holds as c_holds
28 from cvc5 cimport getVariant as c_getVariant
29 from cvc5 cimport Solver as c_Solver
30 from cvc5 cimport Statistics as c_Statistics
31 from cvc5 cimport Stat as c_Stat
32 from cvc5 cimport Grammar as c_Grammar
33 from cvc5 cimport Sort as c_Sort
34 from cvc5 cimport Term as c_Term
35 from cvc5 cimport hash as c_hash
36 from cvc5 cimport wstring as c_wstring
37 from cvc5 cimport tuple as c_tuple
38 from cvc5 cimport get0, get1, get2
39 from cvc5kinds cimport Kind as c_Kind
40 from cvc5types cimport BlockModelsMode as c_BlockModelsMode
41 from cvc5types cimport RoundingMode as c_RoundingMode
42 from cvc5types cimport UnknownExplanation as c_UnknownExplanation
44 cdef extern from "Python.h":
45 wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *) except NULL
46 object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
47 void PyMem_Free(void*)
50 ### Using PEP-8 spacing recommendations
51 ### Limit linewidth to 79 characters
52 ### Break before binary operators
53 ### surround top level functions and classes with two spaces
54 ### separate methods by one space
55 ### use spaces in functions sparingly to separate logical blocks
56 ### can omit spaces between unrelated oneliners
57 ### always use c++ default arguments
58 #### only use default args of None at python level
60 # References and pointers
61 # The Solver object holds a pointer to a c_Solver.
62 # This is because the assignment operator is deleted in the C++ API for solvers.
63 # Cython has a limitation where you can't stack allocate objects
64 # that have constructors with arguments:
65 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
66 # To get around that you can either have a nullary constructor and assignment
67 # or, use a pointer (which is what we chose).
68 # An additional complication of this is that to free up resources, you must
69 # know when to delete the object.
70 # Python will not follow the same scoping rules as in C++, so it must be
71 # able to reference count. To do this correctly, the solver must be a
72 # reference in the Python class for any class that keeps a pointer to
73 # the solver in C++ (to ensure the solver is not deleted before something
74 # that depends on it).
77 ## Objects for hashing
78 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
79 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
80 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
87 Wrapper class for the C++ class :cpp:class:`cvc5::Datatype`.
91 def __cinit__(self, Solver solver):
94 def __getitem__(self, index):
96 Get the datatype constructor with the given index, where index can
97 be either a numeric id starting with zero, or the name of the
98 constructor. In the latter case, this is a linear search through the
99 constructors, so in case of multiple, similarly-named constructors,
100 the first is returned.
102 :param index: The id or name of the datatype constructor.
103 :return: The matching datatype constructor.
105 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
106 if isinstance(index, int) and index >= 0:
107 dc.cdc = self.cd[(<int?> index)]
108 elif isinstance(index, str):
109 dc.cdc = self.cd[(<const string &> index.encode())]
111 raise ValueError("Expecting a non-negative integer or string")
114 def getConstructor(self, str name):
116 :param name: The name of the constructor.
117 :return: A constructor by name.
119 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
120 dc.cdc = self.cd.getConstructor(name.encode())
123 def getSelector(self, str name):
125 :param name: The name of the selector..
126 :return: A selector by name.
128 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
129 ds.cds = self.cd.getSelector(name.encode())
134 :return: The name of the datatype.
136 return self.cd.getName().decode()
138 def getNumConstructors(self):
140 :return: The number of constructors in this datatype.
142 return self.cd.getNumConstructors()
144 def getParameters(self):
146 :return: The parameters of this datatype, if it is parametric. An
147 exception is thrown if this datatype is not parametric.
150 for s in self.cd.getParameters():
151 sort = Sort(self.solver)
153 param_sorts.append(sort)
156 def isParametric(self):
158 .. warning:: This method is experimental and may change in future
161 :return: True if this datatype is parametric.
163 return self.cd.isParametric()
165 def isCodatatype(self):
167 :return: True if this datatype corresponds to a co-datatype.
169 return self.cd.isCodatatype()
173 :return: True if this datatype corresponds to a tuple.
175 return self.cd.isTuple()
179 .. warning:: This method is experimental and may change in future
182 :return: True if this datatype corresponds to a record.
184 return self.cd.isRecord()
188 :return: True if this datatype is finite.
190 return self.cd.isFinite()
192 def isWellFounded(self):
194 Determine if this datatype is well-founded.
196 If this datatype is not a codatatype, this returns false if there
197 are no values of this datatype that are of finite size.
199 :return: True if this datatype is well-founded
201 return self.cd.isWellFounded()
205 :return: True if this Datatype is a null object.
207 return self.cd.isNull()
210 return self.cd.toString().decode()
213 return self.cd.toString().decode()
216 """Iterate over all constructors."""
218 dc = DatatypeConstructor(self.solver)
223 cdef class DatatypeConstructor:
225 A cvc5 datatype constructor.
227 Wrapper class for :cpp:class:`cvc5::DatatypeConstructor`.
229 cdef c_DatatypeConstructor cdc
231 def __cinit__(self, Solver solver):
232 self.cdc = c_DatatypeConstructor()
235 def __getitem__(self, index):
237 Get the datatype selector with the given index, where index can be
238 either a numeric id starting with zero, or the name of the selector.
239 In the latter case, this is a linear search through the selectors,
240 so in case of multiple, similarly-named selectors, the first is
243 :param index: The id or name of the datatype selector.
244 :return: The matching datatype selector.
246 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
247 if isinstance(index, int) and index >= 0:
248 ds.cds = self.cdc[(<int?> index)]
249 elif isinstance(index, str):
250 ds.cds = self.cdc[(<const string &> index.encode())]
252 raise ValueError("Expecting a non-negative integer or string")
257 :return: The name of the constructor.
259 return self.cdc.getName().decode()
263 Get the constructor term of this datatype constructor.
265 Datatype constructors are a special class of function-like terms
266 whose sort is datatype constructor
267 (:py:meth:`Sort.isDatatypeConstructor()`). All datatype
268 constructors, including nullary ones, should be used as the first
269 argument to Terms whose kind is
270 :py:obj:`APPLY_CONSTRUCTOR <Kind.APPLY_CONSTRUCTOR>`.
271 For example, the nil list can be constructed via
272 ``Solver.mkTerm(APPLY_CONSTRUCTOR, [nil])``, where nil is the Term
273 returned by this method.
277 This method should not be used for parametric datatypes.
278 Instead, use the method
279 :py:meth:`DatatypeConstructor.getInstantiatedTerm()` below.
281 :return: The constructor term.
283 cdef Term term = Term(self.solver)
284 term.cterm = self.cdc.getTerm()
287 def getInstantiatedTerm(self, Sort retSort):
289 Get the constructor term of this datatype constructor whose
290 return type is retSort. This method is intended to be used on
291 constructors of parametric datatypes and can be seen as returning
292 the constructor term that has been explicitly cast to the given
295 This method is required for constructors of parametric datatypes
296 whose return type cannot be determined by type inference. For
301 (declare-datatype List
302 (par (T) ((nil) (cons (head T) (tail (List T))))))
304 The type of nil terms must be provided by the user. In SMT version
305 2.6, this is done via the syntax for qualified identifiers:
311 This method is equivalent of applying the above, where this
312 DatatypeConstructor is the one corresponding to nil, and retSort is
317 The returned constructor term ``t`` is used to construct the
318 above (nullary) application of ``nil`` with
319 ``Solver.mkTerm(APPLY_CONSTRUCTOR, t)``.
321 .. warning:: This method is experimental and may change in future
324 :param retSort: The desired return sort of the constructor.
325 :return: The constructor term.
327 cdef Term term = Term(self.solver)
328 term.cterm = self.cdc.getInstantiatedTerm(retSort.csort)
331 def getTesterTerm(self):
333 Get the tester term of this datatype constructor.
335 Similar to constructors, testers are a class of function-like terms
336 of tester sort (:py:meth:`Sort.isDatatypeTester`), and should
337 be used as the first argument of Terms of kind
338 :py:obj:`Kind.APPLY_TESTER`.
340 :return: The tester term for this constructor.
342 cdef Term term = Term(self.solver)
343 term.cterm = self.cdc.getTesterTerm()
346 def getNumSelectors(self):
348 :return: The number of selecters (so far) of this Datatype
351 return self.cdc.getNumSelectors()
353 def getSelector(self, str name):
355 :param name: The name of the datatype selector.
356 :return: The first datatype selector with the given name.
358 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
359 ds.cds = self.cdc.getSelector(name.encode())
364 :return: True if this DatatypeConstructor is a null object.
366 return self.cdc.isNull()
369 return self.cdc.toString().decode()
372 return self.cdc.toString().decode()
375 """Iterate over all datatype selectors."""
377 ds = DatatypeSelector(self.solver)
382 cdef class DatatypeConstructorDecl:
384 A cvc5 datatype constructor declaration. A datatype constructor
385 declaration is a specification used for creating a datatype constructor.
387 Wrapper class for :cpp:class:`cvc5::DatatypeConstructorDecl`.
389 cdef c_DatatypeConstructorDecl cddc
392 def __cinit__(self, Solver solver):
395 def addSelector(self, str name, Sort sort):
397 Add datatype selector declaration.
399 :param name: The name of the datatype selector declaration to add.
400 :param sort: The codomain sort of the datatype selector declaration
403 self.cddc.addSelector(name.encode(), sort.csort)
405 def addSelectorSelf(self, str name):
407 Add datatype selector declaration whose codomain sort is the
410 :param name: The name of the datatype selector declaration to add.
412 self.cddc.addSelectorSelf(name.encode())
414 def addSelectorUnresolved(self, str name, str unresDatatypeName):
416 Add datatype selector declaration whose codomain sort is an
417 unresolved datatype with the given name.
419 :param name: The name of the datatype selector declaration to add.
420 :param unresDataypeName: The name of the unresolved datatype. The
421 codomain of the selector will be the
422 resolved datatype with the given name.
424 self.cddc.addSelectorUnresolved(name.encode(), unresDatatypeName.encode())
428 :return: True if this DatatypeConstructorDecl is a null object.
430 return self.cddc.isNull()
433 return self.cddc.toString().decode()
436 return self.cddc.toString().decode()
439 cdef class DatatypeDecl:
441 A cvc5 datatype declaration. A datatype declaration is not itself a
442 datatype (see :py:class:`Datatype`), but a specification for creating a
445 The interface for a datatype declaration coincides with the syntax for
446 the SMT-LIB 2.6 command `declare-datatype`, or a single datatype within
447 the `declare-datatypes` command.
449 Datatype sorts can be constructed from :py:class:`DatatypeDecl` using
452 - :py:meth:`Solver.mkDatatypeSort()`
453 - :py:meth:`Solver.mkDatatypeSorts()`
455 Wrapper class for :cpp:class:`cvc5::DatatypeDecl`.
457 cdef c_DatatypeDecl cdd
459 def __cinit__(self, Solver solver):
462 def addConstructor(self, DatatypeConstructorDecl ctor):
464 Add a datatype constructor declaration.
466 :param ctor: The datatype constructor declaration to add.
468 self.cdd.addConstructor(ctor.cddc)
470 def getNumConstructors(self):
472 :return: The number of constructors (so far) for this datatype
475 return self.cdd.getNumConstructors()
477 def isParametric(self):
479 .. warning:: This method is experimental and may change in future
482 :return: True if this datatype declaration is parametric.
484 return self.cdd.isParametric()
488 :return: The name of this datatype declaration.
490 return self.cdd.getName().decode()
494 :return: True if this DatatypeDecl is a null object.
496 return self.cdd.isNull()
499 return self.cdd.toString().decode()
502 return self.cdd.toString().decode()
505 cdef class DatatypeSelector:
507 A cvc5 datatype selector.
509 Wrapper class for :cpp:class:`cvc5::DatatypeSelector`.
511 cdef c_DatatypeSelector cds
513 def __cinit__(self, Solver solver):
514 self.cds = c_DatatypeSelector()
519 :return: The name of this datatype selector.
521 return self.cds.getName().decode()
525 Get the selector term of this datatype selector.
527 Selector terms are a class of function-like terms of selector
528 sort (:py:meth:`Sort.isDatatypeSelector()`), and should be used as
529 the first argument of Terms of kind
530 :py:obj:`APPLY_SELECTOR <Kind.APPLY_SELECTOR>`.
532 :return: The selector term of this datatype selector.
534 cdef Term term = Term(self.solver)
535 term.cterm = self.cds.getTerm()
538 def getUpdaterTerm(self):
540 Get the updater term of this datatype selector.
542 Similar to selectors, updater terms are a class of function-like
543 terms of updater Sort (:py:meth:`Sort.isDatatypeUpdater()`), and
544 should be used as the first argument of Terms of kind
545 :py:obj:`APPLY_UPDATER <Kind.APPLY_UPDATER>`.
547 :return: The updater term of this datatype selector.
549 cdef Term term = Term(self.solver)
550 term.cterm = self.cds.getUpdaterTerm()
553 def getCodomainSort(self):
555 :return: The codomain sort of this selector.
557 cdef Sort sort = Sort(self.solver)
558 sort.csort = self.cds.getCodomainSort()
563 :return: True if this DatatypeSelector is a null object.
565 return self.cds.isNull()
568 return self.cds.toString().decode()
571 return self.cds.toString().decode()
578 An operator is a term that represents certain operators,
579 instantiated with its required parameters, e.g.,
581 :py:obj:`BITVECTOR_EXTRACT <Kind.BITVECTOR_EXTRACT>`.
583 Wrapper class for :cpp:class:`cvc5::Op`.
587 def __cinit__(self, Solver solver):
591 def __eq__(self, Op other):
592 return self.cop == other.cop
594 def __ne__(self, Op other):
595 return self.cop != other.cop
598 return self.cop.toString().decode()
601 return self.cop.toString().decode()
604 return cophash(self.cop)
608 :return: The kind of this operator.
610 return Kind(<int> self.cop.getKind())
614 :return: True iff this operator is indexed.
616 return self.cop.isIndexed()
620 :return: True iff this operator is a null term.
622 return self.cop.isNull()
624 def getNumIndices(self):
626 :return: The number of indices of this op.
628 return self.cop.getNumIndices()
630 def __getitem__(self, int i):
632 Get the index at position ``i``.
634 :param i: The position of the index to return.
635 :return: The index at position ``i``.
637 cdef Term term = Term(self.solver)
638 term.cterm = self.cop[i]
644 A Sygus Grammar. This class can be used to define a context-free grammar
645 of terms. Its interface coincides with the definition of grammars
646 (``GrammarDef``) in the SyGuS IF 2.1 standard.
648 Wrapper class for :cpp:class:`cvc5::Grammar`.
650 cdef c_Grammar cgrammar
652 def __cinit__(self, Solver solver):
654 self.cgrammar = c_Grammar()
656 def addRule(self, Term ntSymbol, Term rule):
658 Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
660 :param ntSymbol: The non-terminal to which the rule is added.
661 :param rule: The rule to add.
663 self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
665 def addAnyConstant(self, Term ntSymbol):
667 Allow ``ntSymbol`` to be an arbitrary constant.
669 :param ntSymbol: The non-terminal allowed to be constant.
671 self.cgrammar.addAnyConstant(ntSymbol.cterm)
673 def addAnyVariable(self, Term ntSymbol):
675 Allow ``ntSymbol`` to be any input variable to corresponding
676 synth-fun/synth-inv with the same sort as ``ntSymbol``.
678 :param ntSymbol: The non-terminal allowed to be any input variable.
680 self.cgrammar.addAnyVariable(ntSymbol.cterm)
682 def addRules(self, Term ntSymbol, rules):
684 Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
686 :param ntSymbol: The non-terminal to which the rules are added.
687 :param rules: The rules to add.
689 cdef vector[c_Term] crules
691 crules.push_back((<Term?> r).cterm)
692 self.cgrammar.addRules(ntSymbol.cterm, crules)
696 Encapsulation of a three-valued solver result, with explanations.
698 Wrapper class for :cpp:class:`cvc5::Result`.
702 # gets populated by solver
707 :return: True if Result is empty, i.e., a nullary Result, and not
708 an actual result returned from a
709 :py:meth:`Solver.checkSat()` (and friends) query.
711 return self.cr.isNull()
715 :return: True if query was a satisfiable
716 :py:meth:`Solver.checkSat()` or
717 :py:meth:`Solver.checkSatAssuming()` query.
719 return self.cr.isSat()
723 :return: True if query was an usatisfiable
724 :py:meth:`Solver.checkSat()` or
725 :py:meth:`Solver.checkSatAssuming()` query.
727 return self.cr.isUnsat()
731 :return: True if query was a :py:meth:`Solver.checkSat()` or
732 :py:meth:`Solver.checkSatAssuming()` query and cvc5 was
733 not able to determine (un)satisfiability.
735 return self.cr.isUnknown()
737 def getUnknownExplanation(self):
739 :return: An explanation for an unknown query result.
741 return UnknownExplanation(<int> self.cr.getUnknownExplanation())
743 def __eq__(self, Result other):
744 return self.cr == other.cr
746 def __ne__(self, Result other):
747 return self.cr != other.cr
750 return self.cr.toString().decode()
753 return self.cr.toString().decode()
755 cdef class SynthResult:
757 Encapsulation of a solver synth result.
759 This is the return value of the API methods:
761 - :py:meth:`Solver.checkSynth()`
762 - :py:meth:`Solver.checkSynthNext()`
764 which we call synthesis queries. This class indicates whether the
765 synthesis query has a solution, has no solution, or is unknown.
767 cdef c_SynthResult cr
769 # gets populated by solver
770 self.cr = c_SynthResult()
774 :return: True if SynthResult is null, i.e., not a SynthResult
775 returned from a synthesis query.
777 return self.cr.isNull()
779 def hasSolution(self):
781 :return: True if the synthesis query has a solution.
783 return self.cr.hasSolution()
785 def hasNoSolution(self):
787 :return: True if the synthesis query has no solution.
788 In this case, it was determined that there was no solution.
790 return self.cr.hasNoSolution()
794 :return: True if the result of the synthesis query could not be
797 return self.cr.isUnknown()
800 return self.cr.toString().decode()
803 return self.cr.toString().decode()
810 Wrapper class for :cpp:class:`cvc5::Solver`.
812 cdef c_Solver* csolver
815 self.csolver = new c_Solver()
817 def __dealloc__(self):
820 def getBooleanSort(self):
822 :return: Sort Boolean.
824 cdef Sort sort = Sort(self)
825 sort.csort = self.csolver.getBooleanSort()
828 def getIntegerSort(self):
830 :return: Sort Integer.
832 cdef Sort sort = Sort(self)
833 sort.csort = self.csolver.getIntegerSort()
836 def getNullSort(self):
838 :return: A null sort object.
840 cdef Sort sort = Sort(self)
841 sort.csort = self.csolver.getNullSort()
844 def getRealSort(self):
848 cdef Sort sort = Sort(self)
849 sort.csort = self.csolver.getRealSort()
852 def getRegExpSort(self):
853 """:return: The sort of regular expressions.
855 cdef Sort sort = Sort(self)
856 sort.csort = self.csolver.getRegExpSort()
859 def getRoundingModeSort(self):
860 """:return: Sort RoundingMode.
862 cdef Sort sort = Sort(self)
863 sort.csort = self.csolver.getRoundingModeSort()
866 def getStringSort(self):
867 """:return: Sort String.
869 cdef Sort sort = Sort(self)
870 sort.csort = self.csolver.getStringSort()
873 def mkArraySort(self, Sort indexSort, Sort elemSort):
875 Create an array sort.
877 :param indexSort: The array index sort.
878 :param elemSort: The array element sort.
879 :return: The array sort.
881 cdef Sort sort = Sort(self)
882 sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
885 def mkBitVectorSort(self, uint32_t size):
887 Create a bit-vector sort.
889 :param size: The bit-width of the bit-vector sort
890 :return: The bit-vector sort
892 cdef Sort sort = Sort(self)
893 sort.csort = self.csolver.mkBitVectorSort(size)
896 def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
898 Create a floating-point sort.
900 :param exp: The bit-width of the exponent of the floating-point
902 :param sig: The bit-width of the significand of the floating-point
905 cdef Sort sort = Sort(self)
906 sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
909 def mkDatatypeSort(self, DatatypeDecl dtypedecl):
911 Create a datatype sort.
913 :param dtypedecl: The datatype declaration from which the sort is
915 :return: The datatype sort.
917 cdef Sort sort = Sort(self)
918 sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
921 def mkDatatypeSorts(self, list dtypedecls):
923 Create a vector of datatype sorts using unresolved sorts. The names
924 of the datatype declarations in dtypedecls must be distinct.
926 When constructing datatypes, unresolved sorts are replaced by the
927 datatype sort constructed for the datatype declaration it is
930 :param dtypedecls: The datatype declarations from which the sort is
932 :return: The datatype sorts.
935 cdef vector[c_DatatypeDecl] decls
936 for decl in dtypedecls:
937 decls.push_back((<DatatypeDecl?> decl).cdd)
939 csorts = self.csolver.mkDatatypeSorts(
940 <const vector[c_DatatypeDecl]&> decls)
948 def mkFunctionSort(self, sorts, Sort codomain):
950 Create function sort.
952 :param sorts: The sort of the function arguments.
953 :param codomain: The sort of the function return value.
954 :return: The function sort.
957 cdef Sort sort = Sort(self)
958 # populate a vector with dereferenced c_Sorts
959 cdef vector[c_Sort] v
960 if isinstance(sorts, Sort):
961 v.push_back((<Sort?>sorts).csort)
964 v.push_back((<Sort?>s).csort)
966 sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
970 def mkParamSort(self, str symbolname = None):
972 Create a sort parameter.
974 .. warning:: This method is experimental and may change in future
977 :param symbol: The name of the sort.
978 :return: The sort parameter.
980 cdef Sort sort = Sort(self)
981 if symbolname is None:
982 sort.csort = self.csolver.mkParamSort()
984 sort.csort = self.csolver.mkParamSort(symbolname.encode())
987 def mkPredicateSort(self, *sorts):
989 Create a predicate sort.
991 :param sorts: The list of sorts of the predicate.
992 :return: The predicate sort.
994 cdef Sort sort = Sort(self)
995 cdef vector[c_Sort] v
997 v.push_back((<Sort?> s).csort)
998 sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
1001 def mkRecordSort(self, *fields):
1003 Create a record sort
1005 .. warning:: This method is experimental and may change in future
1008 :param fields: The list of fields of the record.
1009 :return: The record sort.
1011 cdef Sort sort = Sort(self)
1012 cdef vector[pair[string, c_Sort]] v
1013 cdef pair[string, c_Sort] p
1016 name = name.encode()
1017 p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
1019 sort.csort = self.csolver.mkRecordSort(
1020 <const vector[pair[string, c_Sort]] &> v)
1023 def mkSetSort(self, Sort elemSort):
1027 :param elemSort: The sort of the set elements.
1028 :return: The set sort.
1030 cdef Sort sort = Sort(self)
1031 sort.csort = self.csolver.mkSetSort(elemSort.csort)
1034 def mkBagSort(self, Sort elemSort):
1038 :param elemSort: The sort of the bag elements.
1039 :return: The bag sort.
1041 cdef Sort sort = Sort(self)
1042 sort.csort = self.csolver.mkBagSort(elemSort.csort)
1045 def mkSequenceSort(self, Sort elemSort):
1047 Create a sequence sort.
1049 :param elemSort: The sort of the sequence elements
1050 :return: The sequence sort.
1052 cdef Sort sort = Sort(self)
1053 sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
1056 def mkUninterpretedSort(self, str name = None):
1058 Create an uninterpreted sort.
1060 :param symbol: The name of the sort.
1061 :return: The uninterpreted sort.
1063 cdef Sort sort = Sort(self)
1065 sort.csort = self.csolver.mkUninterpretedSort()
1067 sort.csort = self.csolver.mkUninterpretedSort(name.encode())
1070 def mkUnresolvedDatatypeSort(self, str name, size_t arity = 0):
1072 Create an unresolved datatype sort.
1074 This is for creating yet unresolved sort placeholders for mutually
1075 recursive datatypes.
1077 :param symbol: The name of the sort.
1078 :param arity: The number of sort parameters of the sort.
1079 :return: The unresolved sort.
1081 cdef Sort sort = Sort(self)
1082 sort.csort = self.csolver.mkUnresolvedDatatypeSort(name.encode(), arity)
1085 def mkUninterpretedSortConstructorSort(self, size_t arity, str symbol = None):
1087 Create a sort constructor sort.
1089 An uninterpreted sort constructor is an uninterpreted sort with
1092 :param symbol: The symbol of the sort.
1093 :param arity: The arity of the sort (must be > 0).
1094 :return: The sort constructor sort.
1096 cdef Sort sort = Sort(self)
1098 sort.csort = self.csolver.mkUninterpretedSortConstructorSort(arity)
1100 sort.csort = self.csolver.mkUninterpretedSortConstructorSort(
1101 arity, symbol.encode())
1104 def mkTupleSort(self, *sorts):
1106 Create a tuple sort.
1108 :param sorts: Of the elements of the tuple.
1109 :return: The tuple sort.
1111 cdef Sort sort = Sort(self)
1112 cdef vector[c_Sort] v
1114 v.push_back((<Sort?> s).csort)
1115 sort.csort = self.csolver.mkTupleSort(v)
1118 def mkTerm(self, kind_or_op, *args):
1122 Supports the following arguments:
1124 - ``Term mkTerm(Kind kind)``
1125 - ``Term mkTerm(Kind kind, List[Term] children)``
1126 - ``Term mkTerm(Op op)``
1127 - ``Term mkTerm(Op op, List[Term] children)``
1129 where ``List[Term]`` can also be comma-separated arguments
1131 cdef Term term = Term(self)
1132 cdef vector[c_Term] v
1135 if isinstance(kind_or_op, Kind):
1136 op = self.mkOp(kind_or_op)
1139 term.cterm = self.csolver.mkTerm((<Op?> op).cop)
1142 v.push_back((<Term?> a).cterm)
1143 term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
1146 def mkTuple(self, sorts, terms):
1148 Create a tuple term. Terms are automatically converted if sorts are
1151 :param sorts: The sorts of the elements in the tuple.
1152 :param terms: The elements in the tuple.
1153 :return: The tuple Term.
1155 cdef vector[c_Sort] csorts
1156 cdef vector[c_Term] cterms
1159 csorts.push_back((<Sort?> s).csort)
1161 cterms.push_back((<Term?> s).cterm)
1162 cdef Term result = Term(self)
1163 result.cterm = self.csolver.mkTuple(csorts, cterms)
1166 def mkOp(self, k, *args):
1170 Supports the following arguments:
1172 - ``Op mkOp(Kind kind)``
1173 - ``Op mkOp(Kind kind, const string& arg)``
1174 - ``Op mkOp(Kind kind, uint32_t arg0, ...)``
1176 cdef Op op = Op(self)
1177 cdef vector[uint32_t] v
1180 op.cop = self.csolver.mkOp(<c_Kind> k.value)
1181 elif len(args) == 1 and isinstance(args[0], str):
1182 op.cop = self.csolver.mkOp(<c_Kind> k.value,
1187 if not isinstance(a, int):
1189 "Expected uint32_t for argument {}".format(a))
1190 if a < 0 or a >= 2 ** 31:
1192 "Argument {} must fit in a uint32_t".format(a))
1193 v.push_back((<uint32_t?> a))
1194 op.cop = self.csolver.mkOp(<c_Kind> k.value, v)
1199 Create a Boolean true constant.
1201 :return: The true constant.
1203 cdef Term term = Term(self)
1204 term.cterm = self.csolver.mkTrue()
1209 Create a Boolean false constant.
1211 :return: The false constant.
1213 cdef Term term = Term(self)
1214 term.cterm = self.csolver.mkFalse()
1217 def mkBoolean(self, bint val):
1219 Create a Boolean constant.
1221 :return: The Boolean constant.
1222 :param val: The value of the constant.
1224 cdef Term term = Term(self)
1225 term.cterm = self.csolver.mkBoolean(val)
1230 Create a constant representing the number Pi.
1232 :return: A constant representing :py:obj:`PI <Kind.PI>`.
1234 cdef Term term = Term(self)
1235 term.cterm = self.csolver.mkPi()
1238 def mkInteger(self, val):
1240 Create an integer constant.
1242 :param val: Representation of the constant: either a string or
1244 :return: A constant of sort Integer.
1246 cdef Term term = Term(self)
1247 if isinstance(val, str):
1248 term.cterm = self.csolver.mkInteger(
1249 <const string &> str(val).encode())
1251 assert(isinstance(val, int))
1252 term.cterm = self.csolver.mkInteger((<int?> val))
1255 def mkReal(self, numerator, denominator=None):
1257 Create a real constant from a numerator and an optional denominator.
1259 First converts the arguments to a temporary string, either
1260 ``"<numerator>"`` or ``"<numerator>/<denominator>"``. This temporary
1261 string is forwarded to :cpp:func:`cvc5::Solver::mkReal()` and should
1262 thus represent an integer, a decimal number or a fraction.
1264 :param numerator: The numerator.
1265 :param denominator: The denominator, or ``None``.
1266 :return: A real term with literal value.
1268 cdef Term term = Term(self)
1269 if denominator is None:
1270 term.cterm = self.csolver.mkReal(str(numerator).encode())
1272 term.cterm = self.csolver.mkReal("{}/{}".format(numerator, denominator).encode())
1275 def mkRegexpAll(self):
1277 Create a regular expression all (``re.all``) term.
1279 :return: The all term.
1281 cdef Term term = Term(self)
1282 term.cterm = self.csolver.mkRegexpAll()
1285 def mkRegexpAllchar(self):
1287 Create a regular expression allchar (``re.allchar``) term.
1289 :return: The allchar term.
1291 cdef Term term = Term(self)
1292 term.cterm = self.csolver.mkRegexpAllchar()
1295 def mkRegexpNone(self):
1297 Create a regular expression none (``re.none``) term.
1299 :return: The none term.
1301 cdef Term term = Term(self)
1302 term.cterm = self.csolver.mkRegexpNone()
1305 def mkEmptySet(self, Sort s):
1307 Create a constant representing an empty set of the given sort.
1309 :param sort: The sort of the set elements.
1310 :return: The empty set constant.
1312 cdef Term term = Term(self)
1313 term.cterm = self.csolver.mkEmptySet(s.csort)
1316 def mkEmptyBag(self, Sort s):
1318 Create a constant representing an empty bag of the given sort.
1320 :param sort: The sort of the bag elements.
1321 :return: The empty bag constant.
1323 cdef Term term = Term(self)
1324 term.cterm = self.csolver.mkEmptyBag(s.csort)
1329 Create a separation logic empty term.
1331 .. warning:: This method is experimental and may change in future
1334 :return: The separation logic empty term.
1336 cdef Term term = Term(self)
1337 term.cterm = self.csolver.mkSepEmp()
1340 def mkSepNil(self, Sort sort):
1342 Create a separation logic nil term.
1344 .. warning:: This method is experimental and may change in future
1347 :param sort: The sort of the nil term.
1348 :return: The separation logic nil term.
1350 cdef Term term = Term(self)
1351 term.cterm = self.csolver.mkSepNil(sort.csort)
1354 def mkString(self, str s, useEscSequences = None):
1356 Create a String constant from a ``str`` which may contain SMT-LIB
1357 compatible escape sequences like ``\\u1234`` to encode unicode
1360 :param s: The string this constant represents.
1361 :param useEscSequences: Determines whether escape sequences in `s`
1362 should be converted to the corresponding
1364 :return: The String constant.
1366 cdef Term term = Term(self)
1367 cdef Py_ssize_t size
1368 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1369 if isinstance(useEscSequences, bool):
1370 term.cterm = self.csolver.mkString(
1371 s.encode(), <bint> useEscSequences)
1373 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1377 def mkEmptySequence(self, Sort sort):
1379 Create an empty sequence of the given element sort.
1381 :param sort: The element sort of the sequence.
1382 :return: The empty sequence with given element sort.
1384 cdef Term term = Term(self)
1385 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1388 def mkUniverseSet(self, Sort sort):
1390 Create a universe set of the given sort.
1392 :param sort: The sort of the set elements
1393 :return: The universe set constant
1395 cdef Term term = Term(self)
1396 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1399 def mkBitVector(self, int size, *args):
1401 Create bit-vector value.
1403 Supports the following arguments:
1405 - ``Term mkBitVector(int size, int val=0)``
1406 - ``Term mkBitVector(int size, string val, int base)``
1408 :return: A Term representing a bit-vector value.
1409 :param size: The bit-width.
1410 :param val: An integer representating the value, in the first form.
1411 In the second form, a string representing the value.
1412 :param base: The base of the string representation (second form
1415 cdef Term term = Term(self)
1417 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1418 elif len(args) == 1:
1420 if not isinstance(val, int):
1422 "Invalid second argument to mkBitVector '{}', "
1423 "expected integer value".format(size))
1424 term.cterm = self.csolver.mkBitVector(
1425 <uint32_t> size, <uint32_t> val)
1426 elif len(args) == 2:
1429 if not isinstance(val, str):
1431 "Invalid second argument to mkBitVector '{}', "
1432 "expected value string".format(size))
1433 if not isinstance(base, int):
1435 "Invalid third argument to mkBitVector '{}', "
1436 "expected base given as integer".format(size))
1437 term.cterm = self.csolver.mkBitVector(
1439 <const string&> str(val).encode(),
1442 raise ValueError("Unexpected inputs to mkBitVector")
1445 def mkConstArray(self, Sort sort, Term val):
1447 Create a constant array with the provided constant value stored at
1450 :param sort: The sort of the constant array (must be an array sort).
1451 :param val: The constant value to store (must match the sort's
1453 :return: The constant array term.
1455 cdef Term term = Term(self)
1456 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1459 def mkFloatingPointPosInf(self, int exp, int sig):
1461 Create a positive infinity floating-point constant.
1463 :param exp: Number of bits in the exponent.
1464 :param sig: Number of bits in the significand.
1465 :return: The floating-point constant.
1467 cdef Term term = Term(self)
1468 term.cterm = self.csolver.mkFloatingPointPosInf(exp, sig)
1471 def mkFloatingPointNegInf(self, int exp, int sig):
1473 Create a negative infinity floating-point constant.
1475 :param exp: Number of bits in the exponent.
1476 :param sig: Number of bits in the significand.
1477 :return: The floating-point constant.
1479 cdef Term term = Term(self)
1480 term.cterm = self.csolver.mkFloatingPointNegInf(exp, sig)
1483 def mkFloatingPointNaN(self, int exp, int sig):
1485 Create a not-a-number (NaN) floating-point constant.
1487 :param exp: Number of bits in the exponent.
1488 :param sig: Number of bits in the significand.
1489 :return: The floating-point constant.
1491 cdef Term term = Term(self)
1492 term.cterm = self.csolver.mkFloatingPointNaN(exp, sig)
1495 def mkFloatingPointPosZero(self, int exp, int sig):
1497 Create a positive zero (+0.0) floating-point constant.
1499 :param exp: Number of bits in the exponent.
1500 :param sig: Number of bits in the significand.
1501 :return: The floating-point constant.
1503 cdef Term term = Term(self)
1504 term.cterm = self.csolver.mkFloatingPointPosZero(exp, sig)
1507 def mkFloatingPointNegZero(self, int exp, int sig):
1509 Create a negative zero (+0.0) floating-point constant.
1511 :param exp: Number of bits in the exponent.
1512 :param sig: Number of bits in the significand.
1513 :return: The floating-point constant.
1515 cdef Term term = Term(self)
1516 term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig)
1519 def mkRoundingMode(self, rm):
1521 Create a roundingmode constant.
1523 :param rm: The floating point rounding mode this constant
1526 cdef Term term = Term(self)
1527 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.value)
1530 def mkFloatingPoint(self, int exp, int sig, Term val):
1532 Create a floating-point constant.
1534 :param exp: Size of the exponent.
1535 :param sig: Size of the significand.
1536 :param val: Value of the floating-point constant as a bit-vector
1539 cdef Term term = Term(self)
1540 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1543 def mkCardinalityConstraint(self, Sort sort, int index):
1545 Create cardinality constraint.
1547 .. warning:: This method is experimental and may change in future
1550 :param sort: Sort of the constraint.
1551 :param index: The upper bound for the cardinality of the sort.
1553 cdef Term term = Term(self)
1554 term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
1557 def mkConst(self, Sort sort, symbol=None):
1559 Create (first-order) constant (0-arity function symbol).
1563 .. code-block:: smtlib
1565 ( declare-const <symbol> <sort> )
1566 ( declare-fun <symbol> ( ) <sort> )
1568 :param sort: The sort of the constant.
1569 :param symbol: The name of the constant. If None, a default symbol
1571 :return: The first-order constant.
1573 cdef Term term = Term(self)
1575 term.cterm = self.csolver.mkConst(sort.csort)
1577 term.cterm = self.csolver.mkConst(sort.csort,
1578 (<str?> symbol).encode())
1581 def mkVar(self, Sort sort, symbol=None):
1583 Create a bound variable to be used in a binder (i.e. a quantifier,
1584 a lambda, or a witness binder).
1586 :param sort: The sort of the variable.
1587 :param symbol: The name of the variable.
1588 :return: The variable.
1590 cdef Term term = Term(self)
1592 term.cterm = self.csolver.mkVar(sort.csort)
1594 term.cterm = self.csolver.mkVar(sort.csort,
1595 (<str?> symbol).encode())
1598 def mkDatatypeConstructorDecl(self, str name):
1600 Create datatype constructor declaration.
1602 :param name: The name of the constructor.
1603 :return: The datatype constructor declaration.
1605 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1606 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1609 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1611 Create a datatype declaration.
1613 :param name: The name of the datatype.
1614 :param isCoDatatype: True if a codatatype is to be constructed.
1615 :return: The datatype declaration.
1617 cdef DatatypeDecl dd = DatatypeDecl(self)
1618 cdef vector[c_Sort] v
1621 if sorts_or_bool is None and isCoDatatype is None:
1622 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1623 elif sorts_or_bool is not None and isCoDatatype is None:
1624 if isinstance(sorts_or_bool, bool):
1625 dd.cdd = self.csolver.mkDatatypeDecl(
1626 <const string &> name.encode(), <bint> sorts_or_bool)
1627 elif isinstance(sorts_or_bool, list):
1628 for s in sorts_or_bool:
1629 v.push_back((<Sort?> s).csort)
1630 dd.cdd = self.csolver.mkDatatypeDecl(
1631 <const string &> name.encode(),
1632 <const vector[c_Sort]&> v)
1634 raise ValueError("Unhandled second argument type {}"
1635 .format(type(sorts_or_bool)))
1636 elif sorts_or_bool is not None and isCoDatatype is not None:
1637 if isinstance(sorts_or_bool, list):
1638 for s in sorts_or_bool:
1639 v.push_back((<Sort?> s).csort)
1640 dd.cdd = self.csolver.mkDatatypeDecl(
1641 <const string &> name.encode(),
1642 <const vector[c_Sort]&> v,
1643 <bint> isCoDatatype)
1645 raise ValueError("Unhandled second argument type {}"
1646 .format(type(sorts_or_bool)))
1648 raise ValueError("Can't create DatatypeDecl with {}".format(
1649 [type(a) for a in [name, sorts_or_bool, isCoDatatype]]))
1653 def simplify(self, Term t):
1655 Simplify a formula without doing "much" work. Does not involve the
1656 SAT Engine in the simplification, but uses the current definitions,
1657 assertions, and the current partial model, if one has been
1658 constructed. It also involves theory normalization.
1660 .. warning:: This method is experimental and may change in future
1663 :param t: The formula to simplify.
1664 :return: The simplified formula.
1666 cdef Term term = Term(self)
1667 term.cterm = self.csolver.simplify(t.cterm)
1670 def assertFormula(self, Term term):
1676 .. code-block:: smtlib
1680 :param term: The formula to assert.
1682 self.csolver.assertFormula(term.cterm)
1686 Check satisfiability.
1690 .. code-block:: smtlib
1694 :return: The result of the satisfiability check.
1696 cdef Result r = Result()
1697 r.cr = self.csolver.checkSat()
1700 def mkGrammar(self, boundVars, ntSymbols):
1702 Create a SyGuS grammar. The first non-terminal is treated as the
1703 starting non-terminal, so the order of non-terminals matters.
1705 :param boundVars: The parameters to corresponding
1706 synth-fun/synth-inv.
1707 :param ntSymbols: The pre-declaration of the non-terminal symbols.
1708 :return: The grammar.
1710 cdef Grammar grammar = Grammar(self)
1711 cdef vector[c_Term] bvc
1712 cdef vector[c_Term] ntc
1713 for bv in boundVars:
1714 bvc.push_back((<Term?> bv).cterm)
1715 for nt in ntSymbols:
1716 ntc.push_back((<Term?> nt).cterm)
1717 grammar.cgrammar = self.csolver.mkGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1720 def declareSygusVar(self, str symbol, Sort sort):
1722 Append symbol to the current list of universal variables.
1726 .. code-block:: smtlib
1728 ( declare-var <symbol> <sort> )
1730 :param sort: The sort of the universal variable.
1731 :param symbol: The name of the universal variable.
1732 :return: The universal variable.
1734 cdef Term term = Term(self)
1735 term.cterm = self.csolver.declareSygusVar(symbol.encode(), sort.csort)
1738 def addSygusConstraint(self, Term t):
1740 Add a formula to the set of SyGuS constraints.
1744 .. code-block:: smtlib
1746 ( constraint <term> )
1748 :param term: The formula to add as a constraint.
1750 self.csolver.addSygusConstraint(t.cterm)
1752 def addSygusAssume(self, Term t):
1754 Add a formula to the set of Sygus assumptions.
1758 .. code-block:: smtlib
1762 :param term: The formuula to add as an assumption.
1764 self.csolver.addSygusAssume(t.cterm)
1766 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1768 Add a set of SyGuS constraints to the current state that correspond
1769 to an invariant synthesis problem.
1773 .. code-block:: smtlib
1775 ( inv-constraint <inv> <pre> <trans> <post> )
1777 :param inv: The function-to-synthesize.
1778 :param pre: The pre-condition.
1779 :param trans: The transition relation.
1780 :param post: The post-condition.
1782 self.csolver.addSygusInvConstraint(
1783 inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1785 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1787 Synthesize n-ary function following specified syntactic constraints.
1791 .. code-block:: smtlib
1793 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1795 :param symbol: The name of the function.
1796 :param boundVars: The parameters to this function.
1797 :param sort: The sort of the return value of this function.
1798 :param grammar: The syntactic constraints.
1799 :return: The function.
1801 cdef Term term = Term(self)
1802 cdef vector[c_Term] v
1803 for bv in bound_vars:
1804 v.push_back((<Term?> bv).cterm)
1806 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1808 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1811 def checkSynth(self):
1813 Try to find a solution for the synthesis conjecture corresponding
1814 to the current list of functions-to-synthesize, universal variables
1819 .. code-block:: smtlib
1823 :return: The result of the check, which is "solution" if the check
1824 found a solution in which case solutions are available via
1825 getSynthSolutions, "no solution" if it was determined
1826 there is no solution, or "unknown" otherwise.
1828 cdef SynthResult r = SynthResult()
1829 r.cr = self.csolver.checkSynth()
1832 def checkSynthNext(self):
1834 Try to find a next solution for the synthesis conjecture
1835 corresponding to the current list of functions-to-synthesize,
1836 universal variables and constraints. Must be called immediately
1837 after a successful call to check-synth or check-synth-next.
1838 Requires incremental mode.
1842 .. code-block:: smtlib
1846 :return: The result of the check, which is "solution" if the check
1847 found a solution in which case solutions are available via
1848 getSynthSolutions, "no solution" if it was determined
1849 there is no solution, or "unknown" otherwise.
1851 cdef SynthResult r = SynthResult()
1852 r.cr = self.csolver.checkSynthNext()
1855 def getSynthSolution(self, Term term):
1857 Get the synthesis solution of the given term. This method should be
1858 called immediately after the solver answers unsat for sygus input.
1860 :param term: The term for which the synthesis solution is queried.
1861 :return: The synthesis solution of the given term.
1863 cdef Term t = Term(self)
1864 t.cterm = self.csolver.getSynthSolution(term.cterm)
1867 def getSynthSolutions(self, list terms):
1869 Get the synthesis solutions of the given terms. This method should
1870 be called immediately after the solver answers unsat for sygus
1873 :param terms: The terms for which the synthesis solutions is
1875 :return: The synthesis solutions of the given terms.
1878 cdef vector[c_Term] vec
1880 vec.push_back((<Term?> t).cterm)
1881 cresult = self.csolver.getSynthSolutions(vec)
1889 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1891 Synthesize invariant.
1895 .. code-block:: smtlib
1897 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1899 :param symbol: The name of the invariant.
1900 :param boundVars: The parameters to this invariant.
1901 :param grammar: The syntactic constraints.
1902 :return: The invariant.
1904 cdef Term term = Term(self)
1905 cdef vector[c_Term] v
1906 for bv in bound_vars:
1907 v.push_back((<Term?> bv).cterm)
1909 term.cterm = self.csolver.synthInv(
1910 symbol.encode(), <const vector[c_Term]&> v)
1912 term.cterm = self.csolver.synthInv(
1914 <const vector[c_Term]&> v,
1918 def checkSatAssuming(self, *assumptions):
1920 Check satisfiability assuming the given formula.
1924 .. code-block:: smtlib
1926 ( check-sat-assuming ( <prop_literal> ) )
1928 :param assumptions: The formulas to assume.
1929 :return: The result of the satisfiability check.
1931 cdef Result r = Result()
1932 # used if assumptions is a list of terms
1933 cdef vector[c_Term] v
1934 for a in assumptions:
1935 v.push_back((<Term?> a).cterm)
1936 r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
1939 def declareDatatype(self, str symbol, *ctors):
1941 Create datatype sort.
1945 .. code-block:: smtlib
1947 ( declare-datatype <symbol> <datatype_decl> )
1949 :param symbol: The name of the datatype sort.
1950 :param ctors: The constructor declarations of the datatype sort.
1951 :return: The datatype sort.
1953 cdef Sort sort = Sort(self)
1954 cdef vector[c_DatatypeConstructorDecl] v
1957 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1958 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1961 def declareFun(self, str symbol, list sorts, Sort sort):
1963 Declare n-ary function symbol.
1967 .. code-block:: smtlib
1969 ( declare-fun <symbol> ( <sort>* ) <sort> )
1971 :param symbol: The name of the function.
1972 :param sorts: The sorts of the parameters to this function.
1973 :param sort: The sort of the return value of this function.
1974 :return: The function.
1976 cdef Term term = Term(self)
1977 cdef vector[c_Sort] v
1979 v.push_back((<Sort?> s).csort)
1980 term.cterm = self.csolver.declareFun(symbol.encode(),
1981 <const vector[c_Sort]&> v,
1985 def declareSort(self, str symbol, int arity):
1987 Declare uninterpreted sort.
1991 .. code-block:: smtlib
1993 ( declare-sort <symbol> <numeral> )
1997 This corresponds to :py:meth:`Solver.mkUninterpretedSort()` if
1999 :py:meth:`Solver.mkUninterpretedSortConstructorSort()` if
2002 :param symbol: The name of the sort.
2003 :param arity: The arity of the sort.
2006 cdef Sort sort = Sort(self)
2007 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
2010 def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
2012 Define n-ary function.
2016 .. code-block:: smtlib
2018 ( define-fun <function_def> )
2020 :param symbol: The name of the function.
2021 :param bound_vars: The parameters to this function.
2022 :param sort: The sort of the return value of this function.
2023 :param term: The function body.
2024 :param glbl: Determines whether this definition is global (i.e.
2025 persists when popping the context).
2026 :return: The function.
2028 cdef Term fun = Term(self)
2029 cdef vector[c_Term] v
2030 for bv in bound_vars:
2031 v.push_back((<Term?> bv).cterm)
2033 fun.cterm = self.csolver.defineFun(symbol.encode(),
2034 <const vector[c_Term] &> v,
2040 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
2042 Define recursive functions.
2044 Supports the following arguments:
2046 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
2047 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
2051 .. code-block:: smtlib
2053 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
2055 Create elements of parameter ``funs`` with :py:meth:`mkConst()`.
2057 :param funs: The sorted functions.
2058 :param bound_vars: The list of parameters to the functions.
2059 :param terms: The list of function bodies of the functions.
2060 :param global: Determines whether this definition is global (i.e.
2061 persists when popping the context).
2062 :return: The function.
2064 cdef Term term = Term(self)
2065 cdef vector[c_Term] v
2066 for bv in bound_vars:
2067 v.push_back((<Term?> bv).cterm)
2070 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
2071 <const vector[c_Term] &> v,
2072 (<Sort?> sort_or_term).csort,
2076 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
2077 <const vector[c_Term]&> v,
2078 (<Term?> sort_or_term).cterm,
2083 def defineFunsRec(self, funs, bound_vars, terms):
2085 Define recursive functions.
2089 .. code-block:: smtlib
2091 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
2093 Create elements of parameter ``funs`` with :py:meth:`mkConst()`.
2095 :param funs: The sorted functions.
2096 :param bound_vars: The list of parameters to the functions.
2097 :param terms: The list of function bodies of the functions.
2098 :param global: Determines whether this definition is global (i.e.
2099 persists when popping the context).
2100 :return: The function.
2102 cdef vector[c_Term] vf
2103 cdef vector[vector[c_Term]] vbv
2104 cdef vector[c_Term] vt
2107 vf.push_back((<Term?> f).cterm)
2109 cdef vector[c_Term] temp
2110 for v in bound_vars:
2112 temp.push_back((<Term?> t).cterm)
2117 vf.push_back((<Term?> t).cterm)
2121 Get the refutation proof
2125 .. code-block:: smtlib
2129 Requires to enable option
2130 :ref:`produce-proofs <lbl-option-produce-proofs>`.
2132 .. warning:: This method is experimental and may change in future
2135 :return: A string representing the proof, according to the value of
2136 :ref:`proof-format-mode <lbl-option-proof-format-mode>`.
2138 return self.csolver.getProof()
2140 def getLearnedLiterals(self):
2142 Get a list of literals that are entailed by the current set of assertions
2146 .. code-block:: smtlib
2148 ( get-learned-literals )
2150 .. warning:: This method is experimental and may change in future
2153 :return: The list of literals.
2156 for a in self.csolver.getLearnedLiterals():
2162 def getAssertions(self):
2164 Get the list of asserted formulas.
2168 .. code-block:: smtlib
2172 :return: The list of asserted formulas.
2175 for a in self.csolver.getAssertions():
2178 assertions.append(term)
2181 def getInfo(self, str flag):
2183 Get info from the solver.
2187 .. code-block:: smtlib
2189 ( get-info <info_flag> )
2191 :param flag: The info flag.
2194 return self.csolver.getInfo(flag.encode())
2196 def getOption(self, str option):
2198 Get the value of a given option.
2202 .. code-block:: smtlib
2204 ( get-option <keyword> )
2206 :param option: The option for which the value is queried.
2207 :return: A string representation of the option value.
2209 return self.csolver.getOption(option.encode()).decode()
2211 def getOptionNames(self):
2213 Get all option names that can be used with
2214 :py:meth:`Solver.setOption()`, :py:meth:`Solver.getOption()`
2215 and :py:meth:`Solver.getOptionInfo()`.
2217 :return: All option names.
2219 return [s.decode() for s in self.csolver.getOptionNames()]
2221 def getOptionInfo(self, str option):
2223 Get some information about the given option.
2224 Returns the information provided by the C++
2225 :cpp:class:`OptionInfo <cvc5::OptionInfo>` as a dictionary.
2227 :return: Information about the given option.
2229 # declare all the variables we may need later
2230 cdef c_OptionInfo.ValueInfo[c_bool] vib
2231 cdef c_OptionInfo.ValueInfo[string] vis
2232 cdef c_OptionInfo.NumberInfo[int64_t] nii
2233 cdef c_OptionInfo.NumberInfo[uint64_t] niu
2234 cdef c_OptionInfo.NumberInfo[double] nid
2235 cdef c_OptionInfo.ModeInfo mi
2237 oi = self.csolver.getOptionInfo(option.encode())
2238 # generic information
2240 'name': oi.name.decode(),
2241 'aliases': [s.decode() for s in oi.aliases],
2242 'setByUser': oi.setByUser,
2245 # now check which type is actually in the variant
2246 if c_holds[c_OptionInfo.VoidInfo](oi.valueInfo):
2249 elif c_holds[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo):
2252 vib = c_getVariant[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo)
2253 res['current'] = vib.currentValue
2254 res['default'] = vib.defaultValue
2255 elif c_holds[c_OptionInfo.ValueInfo[string]](oi.valueInfo):
2258 vis = c_getVariant[c_OptionInfo.ValueInfo[string]](oi.valueInfo)
2259 res['current'] = vis.currentValue.decode()
2260 res['default'] = vis.defaultValue.decode()
2261 elif c_holds[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo):
2264 nii = c_getVariant[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo)
2265 res['current'] = nii.currentValue
2266 res['default'] = nii.defaultValue
2267 res['minimum'] = nii.minimum.value() \
2268 if nii.minimum.has_value() else None
2269 res['maximum'] = nii.maximum.value() \
2270 if nii.maximum.has_value() else None
2271 elif c_holds[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo):
2274 niu = c_getVariant[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo)
2275 res['current'] = niu.currentValue
2276 res['default'] = niu.defaultValue
2277 res['minimum'] = niu.minimum.value() \
2278 if niu.minimum.has_value() else None
2279 res['maximum'] = niu.maximum.value() \
2280 if niu.maximum.has_value() else None
2281 elif c_holds[c_OptionInfo.NumberInfo[double]](oi.valueInfo):
2284 nid = c_getVariant[c_OptionInfo.NumberInfo[double]](oi.valueInfo)
2285 res['current'] = nid.currentValue
2286 res['default'] = nid.defaultValue
2287 res['minimum'] = nid.minimum.value() \
2288 if nid.minimum.has_value() else None
2289 res['maximum'] = nid.maximum.value() \
2290 if nid.maximum.has_value() else None
2291 elif c_holds[c_OptionInfo.ModeInfo](oi.valueInfo):
2293 res['type'] = 'mode'
2294 mi = c_getVariant[c_OptionInfo.ModeInfo](oi.valueInfo)
2295 res['current'] = mi.currentValue.decode()
2296 res['default'] = mi.defaultValue.decode()
2297 res['modes'] = [s.decode() for s in mi.modes]
2300 def getUnsatAssumptions(self):
2302 Get the set of unsat ("failed") assumptions.
2306 .. code-block:: smtlib
2308 ( get-unsat-assumptions )
2310 Requires to enable option :ref:`produce-unsat-assumptions
2311 <lbl-option-produce-unsat-assumptions>`.
2313 :return: The set of unsat assumptions.
2316 for a in self.csolver.getUnsatAssumptions():
2319 assumptions.append(term)
2322 def getUnsatCore(self):
2324 Get the unsatisfiable core.
2328 .. code-block:: smtlib
2332 Requires to enable option :ref:`produce-unsat-cores
2333 <lbl-option-produce-unsat-cores>`.
2337 In contrast to SMT-LIB, the API does not distinguish between
2338 named and unnamed assertions when producing an unsatisfiable
2339 core. Additionally, the API allows this option to be called after
2340 a check with assumptions. A subset of those assumptions may be
2341 included in the unsatisfiable core returned by this method.
2343 :return: A set of terms representing the unsatisfiable core.
2346 for a in self.csolver.getUnsatCore():
2352 def getDifficulty(self):
2354 Get a difficulty estimate for an asserted formula. This method is
2355 intended to be called immediately after any response to a
2356 :py:meth:`Solver.checkSat()` call.
2358 .. warning:: This method is experimental and may change in future
2361 :return: A map from (a subset of) the input assertions to a real
2362 value that is an estimate of how difficult each assertion
2363 was to solver. Unmentioned assertions can be assumed to
2364 have zero difficulty.
2367 for p in self.csolver.getDifficulty():
2377 diffi[termk] = termv
2380 def getValue(self, Term t):
2382 Get the value of the given term in the current model.
2386 .. code-block:: smtlib
2388 ( get-value ( <term> ) )
2390 :param term: The term for which the value is queried.
2391 :return: The value of the given term.
2393 cdef Term term = Term(self)
2394 term.cterm = self.csolver.getValue(t.cterm)
2397 def getModelDomainElements(self, Sort s):
2399 Get the domain elements of uninterpreted sort s in the current
2400 model. The current model interprets s as the finite sort whose
2401 domain elements are given in the return value of this method.
2403 :param s: The uninterpreted sort in question.
2404 :return: The domain elements of s in the current model.
2407 cresult = self.csolver.getModelDomainElements(s.csort)
2414 def isModelCoreSymbol(self, Term v):
2416 This returns False if the model value of free constant v was not
2417 essential for showing the satisfiability of the last call to
2418 checkSat using the current model. This method will only return
2419 false (for any v) if the model-cores option has been set.
2421 .. warning:: This method is experimental and may change in future
2424 :param v: The term in question.
2425 :return: True if v is a model core symbol.
2427 return self.csolver.isModelCoreSymbol(v.cterm)
2429 def getQuantifierElimination(self, Term term):
2431 Do quantifier elimination.
2435 .. code-block:: smtlib
2439 Requires a logic that supports quantifier elimination.
2440 Currently, the only logics supported by quantifier elimination
2443 .. warning:: This method is experimental and may change in future
2446 :param q: A quantified formula of the form
2447 :math:`Q\\bar{x_1}\\dots Q\\bar{x}_n. P( x_1 \\dots x_i, y_1 \\dots y_j)`
2449 :math:`Q\\bar{x}` is a set of quantified variables of the
2450 form :math:`Q x_1...x_k` and
2451 :math:`P( x_1...x_i, y_1...y_j )` is a quantifier-free
2453 :return: A formula :math:`\\phi` such that, given the current set
2454 of formulas :math:`A` asserted to this solver:
2456 - :math:`(A \\wedge q)` :math:`(A \\wedge \\phi)` are
2458 - :math:`\\phi` is quantifier-free formula containing only
2459 free variables in :math:`y_1...y_n`.
2461 cdef Term result = Term(self)
2462 result.cterm = self.csolver.getQuantifierElimination(term.cterm)
2465 def getQuantifierEliminationDisjunct(self, Term term):
2467 Do partial quantifier elimination, which can be used for
2468 incrementally computing the result of a quantifier elimination.
2472 .. code-block:: smtlib
2474 ( get-qe-disjunct <q> )
2476 Requires a logic that supports quantifier elimination.
2477 Currently, the only logics supported by quantifier elimination
2480 .. warning:: This method is experimental and may change in future
2483 :param q: A quantified formula of the form
2484 :math:`Q\\bar{x_1} ... Q\\bar{x_n}. P( x_1...x_i, y_1...y_j)`
2485 where :math:`Q\\bar{x}` is a set of quantified variables of
2486 the form :math:`Q x_1...x_k` and
2487 :math:`P( x_1...x_i, y_1...y_j )` is a quantifier-free formula.
2489 :return: A formula :math:`\\phi` such that, given the current set
2490 of formulas :math:`A` asserted to this solver:
2492 - :math:`(A \\wedge q \\implies A \\wedge \\phi)` if :math:`Q`
2493 is :math:`\\forall`, and
2494 :math:`(A \\wedge \\phi \\implies A \\wedge q)` if
2495 :math:`Q` is :math:`\\exists`
2496 - :math:`\\phi` is quantifier-free formula containing only
2497 free variables in :math:`y_1...y_n`
2498 - If :math:`Q` is :math:`\\exists`, let :math:`(A \\wedge Q_n)`
2500 :math:`(A \\wedge \\neg (\\phi \wedge Q_1) \\wedge ... \\wedge \\neg (\\phi \\wedge Q_n))`
2501 where for each :math:`i = 1...n`, formula
2502 :math:`(\\phi \\wedge Q_i)` is the result of calling
2503 :py:meth:`getQuantifierEliminationDisjunct()`
2504 for :math:`q` with the set of assertions
2505 :math:`(A \\wedge Q_{i-1})`.
2506 Similarly, if :math:`Q` is :math:`\\forall`, then let
2507 :math:`(A \\wedge Q_n)` be
2508 :math:`(A \\wedge (\\phi \\wedge Q_1) \\wedge ... \\wedge (\\phi \\wedge Q_n))`
2509 where :math:`(\\phi \\wedge Q_i)` is the same as above.
2510 In either case, we have that :math:`(\\phi \\wedge Q_j)`
2511 will eventually be true or false, for some finite :math:`j`.
2513 cdef Term result = Term(self)
2514 result.cterm = self.csolver.getQuantifierEliminationDisjunct(term.cterm)
2517 def getModel(self, sorts, consts):
2527 Requires to enable option
2528 :ref:`produce-models <lbl-option-produce-models>`.
2530 .. warning:: This method is experimental and may change in future
2533 :param sorts: The list of uninterpreted sorts that should be
2534 printed in the model.
2535 :param vars: The list of free constants that should be printed in
2536 the model. A subset of these may be printed based on
2537 :py:meth:`Solver.isModelCoreSymbol()`.
2538 :return: A string representing the model.
2541 cdef vector[c_Sort] csorts
2543 csorts.push_back((<Sort?> sort).csort)
2545 cdef vector[c_Term] cconsts
2546 for const in consts:
2547 cconsts.push_back((<Term?> const).cterm)
2549 return self.csolver.getModel(csorts, cconsts)
2551 def getValueSepHeap(self):
2553 When using separation logic, obtain the term for the heap.
2555 .. warning:: This method is experimental and may change in future
2558 :return: The term for the heap.
2560 cdef Term term = Term(self)
2561 term.cterm = self.csolver.getValueSepHeap()
2564 def getValueSepNil(self):
2566 When using separation logic, obtain the term for nil.
2568 .. warning:: This method is experimental and may change in future
2571 :return: The term for nil.
2573 cdef Term term = Term(self)
2574 term.cterm = self.csolver.getValueSepNil()
2577 def declareSepHeap(self, Sort locType, Sort dataType):
2579 When using separation logic, this sets the location sort and the
2580 datatype sort to the given ones. This method should be invoked
2581 exactly once, before any separation logic constraints are provided.
2583 .. warning:: This method is experimental and may change in future
2586 :param locSort: The location sort of the heap.
2587 :param dataSort: The data sort of the heap.
2589 self.csolver.declareSepHeap(locType.csort, dataType.csort)
2591 def declarePool(self, str symbol, Sort sort, initValue):
2593 Declare a symbolic pool of terms with the given initial value.
2597 .. code-block:: smtlib
2599 ( declare-pool <symbol> <sort> ( <term>* ) )
2601 .. warning:: This method is experimental and may change in future
2604 :param symbol: The name of the pool.
2605 :param sort: The sort of the elements of the pool.
2606 :param initValue: The initial value of the pool.
2608 cdef Term term = Term(self)
2609 cdef vector[c_Term] niv
2611 niv.push_back((<Term?> v).cterm)
2612 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
2615 def pop(self, nscopes=1):
2617 Pop ``nscopes`` level(s) from the assertion stack.
2621 .. code-block:: smtlib
2625 :param nscopes: The number of levels to pop.
2627 self.csolver.pop(nscopes)
2629 def push(self, nscopes=1):
2631 Push ``nscopes`` level(s) to the assertion stack.
2635 .. code-block:: smtlib
2639 :param nscopes: The number of levels to push.
2641 self.csolver.push(nscopes)
2643 def resetAssertions(self):
2645 Remove all assertions.
2649 .. code-block:: smtlib
2651 ( reset-assertions )
2654 self.csolver.resetAssertions()
2656 def setInfo(self, str keyword, str value):
2662 .. code-block:: smtlib
2664 ( set-info <attribute> )
2666 :param keyword: The info flag.
2667 :param value: The value of the info flag.
2669 self.csolver.setInfo(keyword.encode(), value.encode())
2671 def setLogic(self, str logic):
2677 .. code-block:: smtlib
2679 ( set-logic <symbol> )
2681 :param logic: The logic to set.
2683 self.csolver.setLogic(logic.encode())
2685 def setOption(self, str option, str value):
2691 .. code-block:: smtlib
2693 ( set-option <option> )
2695 :param option: The option name.
2696 :param value: The option value.
2698 self.csolver.setOption(option.encode(), value.encode())
2701 def getInterpolant(self, Term conj, Grammar grammar=None):
2707 .. code-block:: smtlib
2709 ( get-interpolant <conj> )
2710 ( get-interpolant <conj> <grammar> )
2713 :ref:`produce-interpolants <lbl-option-produce-interpolants>`
2714 to be set to a mode different from `none`.
2716 .. warning:: This method is experimental and may change in future
2719 :param conj: The conjecture term.
2720 :param grammar: A grammar for the inteprolant.
2721 :return: The interpolant.
2722 See :cpp:func:`cvc5::Solver::getInterpolant` for details.
2724 cdef Term result = Term(self)
2726 result.cterm = self.csolver.getInterpolant(conj.cterm)
2728 result.cterm = self.csolver.getInterpolant(
2729 conj.cterm, grammar.cgrammar)
2733 def getInterpolantNext(self):
2735 Get the next interpolant.
2737 Can only be called immediately after a successful call to
2738 :py:func:`Solver.getInterpolant()` or
2739 :py:func:`Solver.getInterpolantNext()`.
2740 Is guaranteed to produce a syntactically different interpolant wrt
2741 the last returned interpolant if successful.
2745 .. code-block:: smtlib
2747 ( get-interpolant-next )
2749 Requires to enable incremental mode, and option
2750 :ref:`produce-interpolants <lbl-option-produce-interpolants>` to be
2751 set to a mode different from ``none``.
2753 .. warning:: This method is experimental and may change in future
2756 :param output: The term where the result will be stored.
2757 :return: True iff an interpolant was found.
2759 cdef Term result = Term(self)
2760 result.cterm = self.csolver.getInterpolantNext()
2764 def getAbduct(self, Term conj, Grammar grammar=None):
2770 .. code-block:: smtlib
2772 ( get-abduct <conj> )
2773 ( get-abduct <conj> <grammar> )
2775 Requires to enable option
2776 :ref:`produce-abducts <lbl-option-produce-abducts>`.
2778 .. warning:: This method is experimental and may change in future
2781 :param conj: The conjecture term.
2782 :param grammar: A grammar for the abduct.
2783 :return: The abduct.
2784 See :cpp:func:`cvc5::Solver::getAbduct` for details.
2786 cdef Term result = Term(self)
2788 result.cterm = self.csolver.getAbduct(conj.cterm)
2790 result.cterm = self.csolver.getAbduct(conj.cterm, grammar.cgrammar)
2793 def getAbductNext(self):
2795 Get the next abduct.
2797 Can only be called immediately after a succesful call to
2798 :py:func:`Solver.getAbduct()` or
2799 :py:func:`Solver.getAbductNext()`.
2800 Is guaranteed to produce a syntactically different abduct wrt the
2801 last returned abduct if successful.
2805 .. code-block:: smtlib
2809 Requires to enable incremental mode, and
2810 option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2812 .. warning:: This method is experimental and may change in future
2815 :param output: The term where the result will be stored.
2816 :return: True iff an abduct was found.
2818 cdef Term result = Term(self)
2819 result.cterm = self.csolver.getAbductNext()
2822 def blockModel(self, mode):
2824 Block the current model. Can be called only if immediately preceded
2825 by a SAT or INVALID query.
2829 .. code-block:: smtlib
2833 Requires enabling option
2834 :ref:`produce-models <lbl-option-produce-models>`
2835 to a mode other than ``none``.
2837 .. warning:: This method is experimental and may change in future
2840 :param mode: The mode to use for blocking
2842 self.csolver.blockModel(<c_BlockModelsMode> mode.value)
2844 def blockModelValues(self, terms):
2846 Block the current model values of (at least) the values in terms.
2847 Can be called only if immediately preceded by a SAT or NOT_ENTAILED
2852 .. code-block:: smtlib
2854 (block-model-values ( <terms>+ ))
2856 Requires enabling option
2857 :ref:`produce-models <lbl-option-produce-models>`.
2859 .. warning:: This method is experimental and may change in future
2862 cdef vector[c_Term] nts
2864 nts.push_back((<Term?> t).cterm)
2865 self.csolver.blockModelValues(nts)
2867 def getInstantiations(self):
2869 Return a string that contains information about all instantiations
2870 made by the quantifiers module.
2872 .. warning:: This method is experimental and may change in future
2875 return self.csolver.getInstantiations()
2877 def getStatistics(self):
2879 Returns a snapshot of the current state of the statistic values of
2880 this solver. The returned object is completely decoupled from the
2881 solver and will not change when the solver is used again.
2884 res.cstats = self.csolver.getStatistics()
2890 The sort of a cvc5 term.
2892 Wrapper class for :cpp:class:`cvc5::Sort`.
2896 def __cinit__(self, Solver solver):
2897 # csort always set by Solver
2898 self.solver = solver
2900 def __eq__(self, Sort other):
2901 return self.csort == other.csort
2903 def __ne__(self, Sort other):
2904 return self.csort != other.csort
2906 def __lt__(self, Sort other):
2907 return self.csort < other.csort
2909 def __gt__(self, Sort other):
2910 return self.csort > other.csort
2912 def __le__(self, Sort other):
2913 return self.csort <= other.csort
2915 def __ge__(self, Sort other):
2916 return self.csort >= other.csort
2919 return self.csort.toString().decode()
2922 return self.csort.toString().decode()
2925 return csorthash(self.csort)
2927 def hasSymbol(self):
2929 :return: True iff this sort has a symbol.
2931 return self.csort.hasSymbol()
2933 def getSymbol(self):
2935 .. note:: Asserts :py:meth:`hasSymbol()`.
2937 :return: The raw symbol of the sort.
2939 return self.csort.getSymbol().decode()
2943 :return: True if this Sort is a null sort.
2945 return self.csort.isNull()
2947 def isBoolean(self):
2949 Determine if this is the Boolean sort (SMT-LIB: ``Bool``).
2951 :return: True if the sort is the Boolean sort.
2953 return self.csort.isBoolean()
2955 def isInteger(self):
2957 Determine if this is the integer sort (SMT-LIB: ``Int``).
2959 :return: True if the sort is the integer sort.
2961 return self.csort.isInteger()
2965 Determine if this is the real sort (SMT-LIB: `Real`).
2967 :return: True if the sort is the real sort.
2969 return self.csort.isReal()
2973 Determine if this is the string sort (SMT-LIB: `String`).
2975 :return: True if the sort is the string sort.
2977 return self.csort.isString()
2981 Determine if this is the regular expression sort (SMT-LIB:
2984 :return: True if the sort is the regexp sort.
2986 return self.csort.isRegExp()
2988 def isRoundingMode(self):
2990 Determine if this is the rounding mode sort (SMT-LIB:
2993 :return: True if the sort is the rounding mode sort.
2995 return self.csort.isRoundingMode()
2997 def isBitVector(self):
2999 Determine if this is a bit-vector sort (SMT-LIB: ``(_ BitVec i)``).
3001 :return: True if the sort is a bit-vector sort.
3003 return self.csort.isBitVector()
3005 def isFloatingPoint(self):
3007 Determine if this is a floatingpoint sort
3008 (SMT-LIB: ``(_ FloatingPoint eb sb)``).
3010 :return: True if the sort is a bit-vector sort.
3012 return self.csort.isFloatingPoint()
3014 def isDatatype(self):
3016 Determine if this is a datatype sort.
3018 :return: True if the sort is a datatype sort.
3020 return self.csort.isDatatype()
3022 def isDatatypeConstructor(self):
3024 Determine if this is a datatype constructor sort.
3026 :return: True if the sort is a datatype constructor sort.
3028 return self.csort.isDatatypeConstructor()
3030 def isDatatypeSelector(self):
3032 Determine if this is a datatype selector sort.
3034 :return: True if the sort is a datatype selector sort.
3036 return self.csort.isDatatypeSelector()
3038 def isDatatypeTester(self):
3040 Determine if this is a tester sort.
3042 :return: True if the sort is a selector sort.
3044 return self.csort.isDatatypeTester()
3046 def isDatatypeUpdater(self):
3048 Determine if this is a datatype updater sort.
3050 :return: True if the sort is a datatype updater sort.
3052 return self.csort.isDatatypeUpdater()
3054 def isFunction(self):
3056 Determine if this is a function sort.
3058 :return: True if the sort is a function sort.
3060 return self.csort.isFunction()
3062 def isPredicate(self):
3064 Determine if this is a predicate sort.
3066 A predicate sort is a function sort that maps to the Boolean sort.
3067 All predicate sorts are also function sorts.
3069 :return: True if the sort is a predicate sort.
3071 return self.csort.isPredicate()
3075 Determine if this is a tuple sort.
3077 :return: True if the sort is a tuple sort.
3079 return self.csort.isTuple()
3083 Determine if this is a record sort.
3085 .. warning:: This method is experimental and may change in future
3088 :return: True if the sort is a record sort.
3090 return self.csort.isRecord()
3094 Determine if this is an array sort.
3096 :return: True if the sort is an array sort.
3098 return self.csort.isArray()
3102 Determine if this is a set sort.
3104 :return: True if the sort is a set sort.
3106 return self.csort.isSet()
3110 Determine if this is a bag sort.
3112 :return: True if the sort is a bag sort.
3114 return self.csort.isBag()
3116 def isSequence(self):
3118 Determine if this is a sequence sort.
3120 :return: True if the sort is a sequence sort.
3122 return self.csort.isSequence()
3124 def isUninterpretedSort(self):
3126 Determine if this is a sort uninterpreted.
3128 :return: True if the sort is uninterpreted.
3130 return self.csort.isUninterpretedSort()
3132 def isUninterpretedSortConstructor(self):
3134 Determine if this is a sort constructor kind.
3136 An uninterpreted sort constructor is an uninterpreted sort with
3139 :return: True if this a sort constructor kind.
3141 return self.csort.isUninterpretedSortConstructor()
3143 def isInstantiated(self):
3145 Determine if this is an instantiated (parametric datatype or
3146 uninterpreted sort constructor) sort.
3148 An instantiated sort is a sort that has been constructed from
3149 instantiating a sort parameters with sort arguments
3150 (see :py:meth:`instantiate()`).
3152 :return: True if this is an instantiated sort.
3154 return self.csort.isInstantiated()
3156 def getUninterpretedSortConstructor(self):
3158 Get the associated uninterpreted sort constructor of an
3159 instantiated uninterpreted sort.
3161 :return: The uninterpreted sort constructor sort
3163 cdef Sort sort = Sort(self.solver)
3164 sort.csort = self.csort.getUninterpretedSortConstructor()
3167 def getDatatype(self):
3169 :return: The underlying datatype of a datatype sort
3171 cdef Datatype d = Datatype(self.solver)
3172 d.cd = self.csort.getDatatype()
3175 def instantiate(self, params):
3177 Instantiate a parameterized datatype sort or uninterpreted sort
3180 Create sorts parameter with :py:meth:`Solver.mkParamSort()`
3182 .. warning:: This method is experimental and may change in future
3185 :param params: The list of sort parameters to instantiate with
3186 :return: The instantiated sort
3188 cdef Sort sort = Sort(self.solver)
3189 cdef vector[c_Sort] v
3191 v.push_back((<Sort?> s).csort)
3192 sort.csort = self.csort.instantiate(v)
3195 def getInstantiatedParameters(self):
3197 Get the sorts used to instantiate the sort parameters of a
3198 parametric sort (parametric datatype or uninterpreted sort
3199 constructor sort, see :py:meth:`instantiate()`).
3201 :return: The sorts used to instantiate the sort parameters of a
3204 instantiated_sorts = []
3205 for s in self.csort.getInstantiatedParameters():
3206 sort = Sort(self.solver)
3208 instantiated_sorts.append(sort)
3209 return instantiated_sorts
3211 def substitute(self, sort_or_list_1, sort_or_list_2):
3213 Substitution of Sorts.
3215 Note that this replacement is applied during a pre-order traversal
3216 and only once to the sort. It is not run until fix point. In the
3217 case that sort_or_list_1 contains duplicates, the replacement
3218 earliest in the list takes priority.
3221 ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])``
3222 will return ``(Array (Array C D) B)``.
3224 .. warning:: This method is experimental and may change in future
3227 :param sort_or_list_1: The subsort or subsorts to be substituted
3229 :param sort_or_list_2: The sort or list of sorts replacing the
3230 substituted subsort.
3233 # The resulting sort after substitution
3234 cdef Sort sort = Sort(self.solver)
3235 # lists for substitutions
3236 cdef vector[c_Sort] ces
3237 cdef vector[c_Sort] creplacements
3239 # normalize the input parameters to be lists
3240 if isinstance(sort_or_list_1, list):
3241 assert isinstance(sort_or_list_2, list)
3243 replacements = sort_or_list_2
3244 if len(es) != len(replacements):
3245 raise RuntimeError("Expecting list inputs to substitute to "
3246 "have the same length but got: "
3248 len(es), len(replacements)))
3250 for e, r in zip(es, replacements):
3251 ces.push_back((<Sort?> e).csort)
3252 creplacements.push_back((<Sort?> r).csort)
3255 # add the single elements to the vectors
3256 ces.push_back((<Sort?> sort_or_list_1).csort)
3257 creplacements.push_back((<Sort?> sort_or_list_2).csort)
3259 # call the API substitute method with lists
3260 sort.csort = self.csort.substitute(ces, creplacements)
3264 def getDatatypeConstructorArity(self):
3266 :return: The arity of a datatype constructor sort.
3268 return self.csort.getDatatypeConstructorArity()
3270 def getDatatypeConstructorDomainSorts(self):
3272 :return: The domain sorts of a datatype constructor sort.
3275 for s in self.csort.getDatatypeConstructorDomainSorts():
3276 sort = Sort(self.solver)
3278 domain_sorts.append(sort)
3281 def getDatatypeConstructorCodomainSort(self):
3283 :return: The codomain sort of a datatype constructor sort.
3285 cdef Sort sort = Sort(self.solver)
3286 sort.csort = self.csort.getDatatypeConstructorCodomainSort()
3289 def getDatatypeSelectorDomainSort(self):
3291 :return: The domain sort of a datatype selector sort.
3293 cdef Sort sort = Sort(self.solver)
3294 sort.csort = self.csort.getDatatypeSelectorDomainSort()
3297 def getDatatypeSelectorCodomainSort(self):
3299 :return: The codomain sort of a datatype selector sort.
3301 cdef Sort sort = Sort(self.solver)
3302 sort.csort = self.csort.getDatatypeSelectorCodomainSort()
3305 def getDatatypeTesterDomainSort(self):
3307 :return: The domain sort of a datatype tester sort.
3309 cdef Sort sort = Sort(self.solver)
3310 sort.csort = self.csort.getDatatypeTesterDomainSort()
3313 def getDatatypeTesterCodomainSort(self):
3315 :return: the codomain sort of a datatype tester sort, which is the
3318 cdef Sort sort = Sort(self.solver)
3319 sort.csort = self.csort.getDatatypeTesterCodomainSort()
3322 def getFunctionArity(self):
3324 :return: The arity of a function sort.
3326 return self.csort.getFunctionArity()
3328 def getFunctionDomainSorts(self):
3330 :return: The domain sorts of a function sort.
3333 for s in self.csort.getFunctionDomainSorts():
3334 sort = Sort(self.solver)
3336 domain_sorts.append(sort)
3339 def getFunctionCodomainSort(self):
3341 :return: The codomain sort of a function sort.
3343 cdef Sort sort = Sort(self.solver)
3344 sort.csort = self.csort.getFunctionCodomainSort()
3347 def getArrayIndexSort(self):
3349 :return: The array index sort of an array sort.
3351 cdef Sort sort = Sort(self.solver)
3352 sort.csort = self.csort.getArrayIndexSort()
3355 def getArrayElementSort(self):
3357 :return: The array element sort of an array sort.
3359 cdef Sort sort = Sort(self.solver)
3360 sort.csort = self.csort.getArrayElementSort()
3363 def getSetElementSort(self):
3365 :return: The element sort of a set sort.
3367 cdef Sort sort = Sort(self.solver)
3368 sort.csort = self.csort.getSetElementSort()
3371 def getBagElementSort(self):
3373 :return: The element sort of a bag sort.
3375 cdef Sort sort = Sort(self.solver)
3376 sort.csort = self.csort.getBagElementSort()
3379 def getSequenceElementSort(self):
3381 :return: The element sort of a sequence sort.
3383 cdef Sort sort = Sort(self.solver)
3384 sort.csort = self.csort.getSequenceElementSort()
3387 def getUninterpretedSortConstructorArity(self):
3389 :return: The arity of a sort constructor sort.
3391 return self.csort.getUninterpretedSortConstructorArity()
3393 def getBitVectorSize(self):
3395 :return: The bit-width of the bit-vector sort.
3397 return self.csort.getBitVectorSize()
3399 def getFloatingPointExponentSize(self):
3401 :return: The bit-width of the exponent of the floating-point sort.
3403 return self.csort.getFloatingPointExponentSize()
3405 def getFloatingPointSignificandSize(self):
3407 :return: The width of the significand of the floating-point sort.
3409 return self.csort.getFloatingPointSignificandSize()
3411 def getDatatypeArity(self):
3413 :return: The arity of a datatype sort.
3415 return self.csort.getDatatypeArity()
3417 def getTupleLength(self):
3419 :return: The length of a tuple sort.
3421 return self.csort.getTupleLength()
3423 def getTupleSorts(self):
3425 :return: The element sorts of a tuple sort.
3428 for s in self.csort.getTupleSorts():
3429 sort = Sort(self.solver)
3431 tuple_sorts.append(sort)
3435 cdef class Statistics:
3437 The cvc5 Statistics.
3439 Wrapper class for :cpp:class:`cvc5::Statistics`.
3440 Obtain a single statistic value using ``stats["name"]`` and a dictionary
3441 with all (visible) statistics using
3442 ``stats.get(internal=False, defaulted=False)``.
3444 cdef c_Statistics cstats
3446 cdef __stat_to_dict(self, const c_Stat& s):
3453 res = s.getString().decode()
3454 elif s.isHistogram():
3455 res = { h.first.decode(): h.second for h in s.getHistogram() }
3457 'defaulted': s.isDefault(),
3458 'internal': s.isInternal(),
3462 def __getitem__(self, str name):
3464 Get the statistics information for the statistic called ``name``.
3466 return self.__stat_to_dict(self.cstats.get(name.encode()))
3468 def get(self, bint internal = False, bint defaulted = False):
3470 Get all statistics as a dictionary. See :cpp:func:`cvc5::Statistics::begin()`
3471 for more information on which statistics are included based on the parameters.
3473 :return: A dictionary with all available statistics.
3475 cdef c_Statistics.iterator it = self.cstats.begin(internal, defaulted)
3476 cdef pair[string,c_Stat]* s
3478 while it != self.cstats.end():
3479 s = &dereference(it)
3480 res[s.first.decode()] = self.__stat_to_dict(s.second)
3489 Wrapper class for :cpp:class:`cvc5::Term`.
3493 def __cinit__(self, Solver solver):
3494 # cterm always set in the Solver object
3495 self.solver = solver
3497 def __eq__(self, Term other):
3498 return self.cterm == other.cterm
3500 def __ne__(self, Term other):
3501 return self.cterm != other.cterm
3503 def __lt__(self, Term other):
3504 return self.cterm < other.cterm
3506 def __gt__(self, Term other):
3507 return self.cterm > other.cterm
3509 def __le__(self, Term other):
3510 return self.cterm <= other.cterm
3512 def __ge__(self, Term other):
3513 return self.cterm >= other.cterm
3515 def __getitem__(self, int index):
3517 Get the child term at a given index.
3519 :param index: The index of the child term to return.
3520 :return: The child term with the given index.
3522 cdef Term term = Term(self.solver)
3524 term.cterm = self.cterm[index]
3526 raise ValueError("Expecting a non-negative integer or string")
3530 return self.cterm.toString().decode()
3533 return self.cterm.toString().decode()
3536 """Iterate over all child terms."""
3537 for ci in self.cterm:
3538 term = Term(self.solver)
3543 return ctermhash(self.cterm)
3545 def getNumChildren(self):
3547 :return: The number of children of this term.
3549 return self.cterm.getNumChildren()
3553 :return: The id of this term.
3555 return self.cterm.getId()
3559 :return: The :py:class:`Kind` of this term.
3561 return Kind(<int> self.cterm.getKind())
3565 :return: The :py:class:`Sort` of this term.
3567 cdef Sort sort = Sort(self.solver)
3568 sort.csort = self.cterm.getSort()
3571 def substitute(self, term_or_list_1, term_or_list_2):
3573 :return: The result of simultaneously replacing the term(s) stored
3574 in ``term_or_list_1`` by the term(s) stored in
3575 ``term_or_list_2`` in this term.
3579 This replacement is applied during a pre-order traversal and
3580 only once to the term. It is not run until fix point. In the
3581 case that terms contains duplicates, the replacement earliest
3582 in the list takes priority. For example, calling substitute on
3587 term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ]
3589 results in the term ``f(g(z),y)``.
3591 # The resulting term after substitution
3592 cdef Term term = Term(self.solver)
3593 # lists for substitutions
3594 cdef vector[c_Term] ces
3595 cdef vector[c_Term] creplacements
3597 # normalize the input parameters to be lists
3598 if isinstance(term_or_list_1, list):
3599 assert isinstance(term_or_list_2, list)
3601 replacements = term_or_list_2
3602 if len(es) != len(replacements):
3603 raise RuntimeError("Expecting list inputs to substitute to "
3604 "have the same length but got: "
3605 "{} and {}".format(len(es), len(replacements)))
3607 for e, r in zip(es, replacements):
3608 ces.push_back((<Term?> e).cterm)
3609 creplacements.push_back((<Term?> r).cterm)
3612 # add the single elements to the vectors
3613 ces.push_back((<Term?> term_or_list_1).cterm)
3614 creplacements.push_back((<Term?> term_or_list_2).cterm)
3616 # call the API substitute method with lists
3617 term.cterm = self.cterm.substitute(ces, creplacements)
3622 :return: True iff this term has an operator.
3624 return self.cterm.hasOp()
3628 :return: The :py:class:`Op` used to create this Term.
3632 This is safe to call when :py:meth:`hasOp()` returns True.
3634 cdef Op op = Op(self.solver)
3635 op.cop = self.cterm.getOp()
3638 def hasSymbol(self):
3640 :return: True iff this term has a symbol.
3642 return self.cterm.hasSymbol()
3644 def getSymbol(self):
3646 ..note:: Asserts :py:meth:`hasSymbol()`.
3648 :return: The raw symbol of the term.
3650 return self.cterm.getSymbol().decode()
3654 :return: True iff this term is a null term.
3656 return self.cterm.isNull()
3662 :return: The Boolean negation of this term.
3664 cdef Term term = Term(self.solver)
3665 term.cterm = self.cterm.notTerm()
3668 def andTerm(self, Term t):
3672 :param t: A Boolean term.
3673 :return: The conjunction of this term and the given term.
3675 cdef Term term = Term(self.solver)
3676 term.cterm = self.cterm.andTerm((<Term> t).cterm)
3679 def orTerm(self, Term t):
3683 :param t: A Boolean term.
3684 :return: The disjunction of this term and the given term.
3686 cdef Term term = Term(self.solver)
3687 term.cterm = self.cterm.orTerm(t.cterm)
3690 def xorTerm(self, Term t):
3692 Boolean exclusive or.
3694 :param t: A Boolean term.
3695 :return: The exclusive disjunction of this term and the given term.
3697 cdef Term term = Term(self.solver)
3698 term.cterm = self.cterm.xorTerm(t.cterm)
3701 def eqTerm(self, Term t):
3705 :param t: A Boolean term.
3706 :return: The Boolean equivalence of this term and the given term.
3708 cdef Term term = Term(self.solver)
3709 term.cterm = self.cterm.eqTerm(t.cterm)
3712 def impTerm(self, Term t):
3714 Boolean Implication.
3716 :param t: A Boolean term.
3717 :return: The implication of this term and the given term.
3719 cdef Term term = Term(self.solver)
3720 term.cterm = self.cterm.impTerm(t.cterm)
3723 def iteTerm(self, Term then_t, Term else_t):
3725 If-then-else with this term as the Boolean condition.
3727 :param then_t: The `then` term.
3728 :param else_t: The `else` term.
3729 :return: The if-then-else term with this term as the Boolean
3732 cdef Term term = Term(self.solver)
3733 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
3736 def isConstArray(self):
3738 :return: True iff this term is a constant array.
3740 return self.cterm.isConstArray()
3742 def getConstArrayBase(self):
3744 .. note:: Asserts :py:meth:`isConstArray()`.
3746 :return: The base (element stored at all indicies) of this constant
3749 cdef Term term = Term(self.solver)
3750 term.cterm = self.cterm.getConstArrayBase()
3753 def isBooleanValue(self):
3755 :return: True iff this term is a Boolean value.
3757 return self.cterm.isBooleanValue()
3759 def getBooleanValue(self):
3761 .. note:: Asserts :py:meth:`isBooleanValue()`
3763 :return: The representation of a Boolean value as a native Boolean
3766 return self.cterm.getBooleanValue()
3768 def isStringValue(self):
3770 :return: True iff this term is a string value.
3772 return self.cterm.isStringValue()
3774 def getStringValue(self):
3776 .. note:: Asserts :py:meth:`isStringValue()`.
3779 This method is not to be confused with :py:meth:`__str__()`
3780 which returns the term in some string representation, whatever
3783 :return: The string term as a native string value.
3785 cdef Py_ssize_t size
3786 cdef c_wstring s = self.cterm.getStringValue()
3787 return PyUnicode_FromWideChar(s.data(), s.size())
3789 def getRealOrIntegerValueSign(self):
3791 Get integer or real value sign. Must be called on integer or real
3792 values, or otherwise an exception is thrown.
3794 :return: 0 if this term is zero, -1 if this term is a negative real
3795 or integer value, 1 if this term is a positive real or
3798 return self.cterm.getRealOrIntegerValueSign()
3800 def isIntegerValue(self):
3802 :return: True iff this term is an integer value.
3804 return self.cterm.isIntegerValue()
3806 def getIntegerValue(self):
3808 .. note:: Asserts :py:meth:`isIntegerValue()`.
3810 :return: The integer term as a native python integer.
3812 return int(self.cterm.getIntegerValue().decode())
3814 def isFloatingPointPosZero(self):
3816 :return: True iff the term is the floating-point value for positive
3819 return self.cterm.isFloatingPointPosZero()
3821 def isFloatingPointNegZero(self):
3823 :return: True iff the term is the floating-point value for negative
3826 return self.cterm.isFloatingPointNegZero()
3828 def isFloatingPointPosInf(self):
3830 :return: True iff the term is the floating-point value for positive
3833 return self.cterm.isFloatingPointPosInf()
3835 def isFloatingPointNegInf(self):
3837 :return: True iff the term is the floating-point value for negative
3840 return self.cterm.isFloatingPointNegInf()
3842 def isFloatingPointNaN(self):
3844 :return: True iff the term is the floating-point value for not a
3847 return self.cterm.isFloatingPointNaN()
3849 def isFloatingPointValue(self):
3851 :return: True iff this term is a floating-point value.
3853 return self.cterm.isFloatingPointValue()
3855 def getFloatingPointValue(self):
3857 .. note:: Asserts :py:meth:`isFloatingPointValue()`.
3859 :return: The representation of a floating-point value as a tuple of
3860 the exponent width, the significand width and a bit-vector
3863 cdef c_tuple[uint32_t, uint32_t, c_Term] t = \
3864 self.cterm.getFloatingPointValue()
3865 cdef Term term = Term(self.solver)
3866 term.cterm = get2(t)
3867 return (get0(t), get1(t), term)
3869 def isSetValue(self):
3871 A term is a set value if it is considered to be a (canonical)
3872 constant set value. A canonical set value is one whose AST is:
3877 (set.singleton c1) ...
3878 (set.union (set.singleton c_{n-1}) (set.singleton c_n))))
3880 where :math:`c_1 \dots c_n` are values ordered by id such that
3881 :math:`c_1 > \cdots > c_n`.
3885 (kind :py:obj:`SET_UNIVERSE <Kind.SET_UNIVERSE>`)
3886 is not considered to be a set value.
3888 :return: True if the term is a set value.
3890 return self.cterm.isSetValue()
3892 def getSetValue(self):
3894 .. note:: Asserts :py:meth:`isSetValue()`.
3896 :return: The representation of a set value as a set of terms.
3899 for e in self.cterm.getSetValue():
3900 term = Term(self.solver)
3905 def isSequenceValue(self):
3907 :return: True iff this term is a sequence value.
3909 return self.cterm.isSequenceValue()
3911 def getSequenceValue(self):
3913 .. note:: Asserts :py:meth:`isSequenceValue()`.
3917 It is usually necessary for sequences to call
3918 :py:meth:`Solver.simplify()` to turn a sequence that is
3919 constructed by, e.g., concatenation of unit sequences, into a
3922 :return: The representation of a sequence value as a vector of
3926 for e in self.cterm.getSequenceValue():
3927 term = Term(self.solver)
3932 def isCardinalityConstraint(self):
3934 :return: True if the term is a cardinality constraint.
3936 .. warning:: This method is experimental and may change in future
3939 return self.cterm.isCardinalityConstraint()
3941 def getCardinalityConstraint(self):
3943 :return: The sort the cardinality constraint is for and its upper
3946 .. warning:: This method is experimental and may change in future
3949 cdef pair[c_Sort, uint32_t] p
3950 p = self.cterm.getCardinalityConstraint()
3951 cdef Sort sort = Sort(self.solver)
3952 sort.csort = p.first
3953 return (sort, p.second)
3956 def isUninterpretedSortValue(self):
3958 :return: True iff this term is a value from an uninterpreted sort.
3960 return self.cterm.isUninterpretedSortValue()
3962 def getUninterpretedSortValue(self):
3964 .. note:: Asserts :py:meth:`isUninterpretedSortValue()`.
3966 :return: The representation of an uninterpreted value as a pair of
3967 its sort and its index.
3969 return self.cterm.getUninterpretedSortValue()
3971 def isTupleValue(self):
3973 :return: True iff this term is a tuple value.
3975 return self.cterm.isTupleValue()
3977 def isRoundingModeValue(self):
3979 :return: True if the term is a floating-point rounding mode
3982 return self.cterm.isRoundingModeValue()
3984 def getRoundingModeValue(self):
3986 .. note:: Asserts :py:meth:`isRoundingModeValue()`.
3988 :return: The floating-point rounding mode value held by the term.
3990 return RoundingMode(<int> self.cterm.getRoundingModeValue())
3992 def getTupleValue(self):
3994 .. note:: Asserts :py:meth:`isTupleValue()`.
3996 :return: The representation of a tuple value as a vector of terms.
3999 for e in self.cterm.getTupleValue():
4000 term = Term(self.solver)
4005 def isRealValue(self):
4007 :return: True iff this term is a rational value.
4011 A term of kind :py:obj:`PI <Kind.PI>` is not considered
4015 return self.cterm.isRealValue()
4017 def getRealValue(self):
4019 .. note:: Asserts :py:meth:`isRealValue()`.
4021 :return: The representation of a rational value as a python Fraction.
4023 return Fraction(self.cterm.getRealValue().decode())
4025 def isBitVectorValue(self):
4027 :return: True iff this term is a bit-vector value.
4029 return self.cterm.isBitVectorValue()
4031 def getBitVectorValue(self, base = 2):
4033 .. note:: Asserts :py:meth:`isBitVectorValue()`.
4035 Supported bases are 2 (bit string), 10 (decimal string) or 16
4036 (hexdecimal string).
4038 :return: The representation of a bit-vector value in string
4041 return self.cterm.getBitVectorValue(base).decode()
4043 def toPythonObj(self):
4045 Converts a constant value Term to a Python object.
4049 - **Boolean:** Returns a Python bool
4050 - **Int :** Returns a Python int
4051 - **Real :** Returns a Python Fraction
4052 - **BV :** Returns a Python int (treats BV as unsigned)
4053 - **String :** Returns a Python Unicode string
4054 - **Array :** Returns a Python dict mapping indices to values. The constant base is returned as the default value.
4058 if self.isBooleanValue():
4059 return self.getBooleanValue()
4060 elif self.isIntegerValue():
4061 return self.getIntegerValue()
4062 elif self.isRealValue():
4063 return self.getRealValue()
4064 elif self.isBitVectorValue():
4065 return int(self.getBitVectorValue(), 2)
4066 elif self.isStringValue():
4067 return self.getStringValue()
4068 elif self.getSort().isArray():
4074 # Array models are represented as a series of store operations
4075 # on a constant array
4078 if t.getKind().value == c_Kind.STORE:
4080 keys.append(t[1].toPythonObj())
4081 values.append(t[2].toPythonObj())
4082 to_visit.append(t[0])
4084 assert t.getKind().value == c_Kind.CONST_ARRAY
4085 base_value = t.getConstArrayBase().toPythonObj()
4087 assert len(keys) == len(values)
4088 assert base_value is not None
4090 # put everything in a dictionary with the constant
4091 # base as the result for any index not included in the stores
4092 res = defaultdict(lambda : base_value)
4093 for k, v in zip(keys, values):