1 from collections import defaultdict
2 from fractions import Fraction
3 from functools import wraps
6 from cython.operator cimport dereference, preincrement
8 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
9 from libc.stddef cimport wchar_t
11 from libcpp cimport bool as c_bool
12 from libcpp.pair cimport pair
13 from libcpp.set cimport set as c_set
14 from libcpp.string cimport string
15 from libcpp.vector cimport vector
17 from cvc5 cimport cout
18 from cvc5 cimport Datatype as c_Datatype
19 from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
20 from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
21 from cvc5 cimport DatatypeDecl as c_DatatypeDecl
22 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
23 from cvc5 cimport Result as c_Result
24 from cvc5 cimport SynthResult as c_SynthResult
25 from cvc5 cimport Op as c_Op
26 from cvc5 cimport OptionInfo as c_OptionInfo
27 from cvc5 cimport holds as c_holds
28 from cvc5 cimport getVariant as c_getVariant
29 from cvc5 cimport Solver as c_Solver
30 from cvc5 cimport Statistics as c_Statistics
31 from cvc5 cimport Stat as c_Stat
32 from cvc5 cimport Grammar as c_Grammar
33 from cvc5 cimport Sort as c_Sort
34 from cvc5 cimport Term as c_Term
35 from cvc5 cimport hash as c_hash
36 from cvc5 cimport wstring as c_wstring
37 from cvc5 cimport tuple as c_tuple
38 from cvc5 cimport get0, get1, get2
39 from cvc5kinds cimport Kind as c_Kind
40 from cvc5types cimport RoundingMode as c_RoundingMode
41 from cvc5types cimport UnknownExplanation as c_UnknownExplanation
43 cdef extern from "Python.h":
44 wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
45 object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
46 void PyMem_Free(void*)
48 ################################## DECORATORS #################################
49 def expand_list_arg(num_req_args=0):
51 Creates a decorator that looks at index num_req_args of the args,
52 if it's a list, it expands it before calling the function.
56 def wrapper(owner, *args):
57 if len(args) == num_req_args + 1 and \
58 isinstance(args[num_req_args], list):
59 args = list(args[:num_req_args]) + args[num_req_args]
60 return func(owner, *args)
63 ###############################################################################
66 ### Using PEP-8 spacing recommendations
67 ### Limit linewidth to 79 characters
68 ### Break before binary operators
69 ### surround top level functions and classes with two spaces
70 ### separate methods by one space
71 ### use spaces in functions sparingly to separate logical blocks
72 ### can omit spaces between unrelated oneliners
73 ### always use c++ default arguments
74 #### only use default args of None at python level
76 # References and pointers
77 # The Solver object holds a pointer to a c_Solver.
78 # This is because the assignment operator is deleted in the C++ API for solvers.
79 # Cython has a limitation where you can't stack allocate objects
80 # that have constructors with arguments:
81 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
82 # To get around that you can either have a nullary constructor and assignment
83 # or, use a pointer (which is what we chose).
84 # An additional complication of this is that to free up resources, you must
85 # know when to delete the object.
86 # Python will not follow the same scoping rules as in C++, so it must be
87 # able to reference count. To do this correctly, the solver must be a
88 # reference in the Python class for any class that keeps a pointer to
89 # the solver in C++ (to ensure the solver is not deleted before something
90 # that depends on it).
93 ## Objects for hashing
94 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
95 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
96 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
103 Wrapper class for the C++ class :cpp:class:`cvc5::Datatype`.
107 def __cinit__(self, Solver solver):
110 def __getitem__(self, index):
111 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
112 if isinstance(index, int) and index >= 0:
113 dc.cdc = self.cd[(<int?> index)]
114 elif isinstance(index, str):
115 dc.cdc = self.cd[(<const string &> index.encode())]
117 raise ValueError("Expecting a non-negative integer or string")
120 def getConstructor(self, str name):
122 :param name: The name of the constructor.
123 :return: A constructor by name.
125 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
126 dc.cdc = self.cd.getConstructor(name.encode())
129 def getConstructorTerm(self, str name):
131 :param name: The name of the constructor.
132 :return: The term representing the datatype constructor with the
135 cdef Term term = Term(self.solver)
136 term.cterm = self.cd.getConstructorTerm(name.encode())
139 def getSelector(self, str name):
141 :param name: The name of the selector..
142 :return: A selector by name.
144 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
145 ds.cds = self.cd.getSelector(name.encode())
150 :return: The name of the datatype.
152 return self.cd.getName().decode()
154 def getNumConstructors(self):
156 :return: The number of constructors in this datatype.
158 return self.cd.getNumConstructors()
160 def getParameters(self):
162 :return: The parameters of this datatype, if it is parametric. An
163 exception is thrown if this datatype is not parametric.
166 for s in self.cd.getParameters():
167 sort = Sort(self.solver)
169 param_sorts.append(sort)
172 def isParametric(self):
174 .. warning:: This method is experimental and may change in future
176 :return: True if this datatype is parametric.
178 return self.cd.isParametric()
180 def isCodatatype(self):
182 :return: True if this datatype corresponds to a co-datatype.
184 return self.cd.isCodatatype()
188 :return: True if this datatype corresponds to a tuple.
190 return self.cd.isTuple()
194 .. warning:: This method is experimental and may change in future
196 :return: True if this datatype corresponds to a record.
198 return self.cd.isRecord()
202 :return: True if this datatype is finite.
204 return self.cd.isFinite()
206 def isWellFounded(self):
208 Is this datatype well-founded?
210 If this datatype is not a codatatype, this returns false if there
211 are no values of this datatype that are of finite size.
213 :return: True if this datatype is well-founded
215 return self.cd.isWellFounded()
219 :return: True if this Datatype is a null object.
221 return self.cd.isNull()
224 return self.cd.toString().decode()
227 return self.cd.toString().decode()
231 dc = DatatypeConstructor(self.solver)
236 cdef class DatatypeConstructor:
238 A cvc5 datatype constructor.
240 Wrapper class for :cpp:class:`cvc5::DatatypeConstructor`.
242 cdef c_DatatypeConstructor cdc
244 def __cinit__(self, Solver solver):
245 self.cdc = c_DatatypeConstructor()
248 def __getitem__(self, index):
249 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
250 if isinstance(index, int) and index >= 0:
251 ds.cds = self.cdc[(<int?> index)]
252 elif isinstance(index, str):
253 ds.cds = self.cdc[(<const string &> index.encode())]
255 raise ValueError("Expecting a non-negative integer or string")
260 :return: The name of the constructor.
262 return self.cdc.getName().decode()
264 def getConstructorTerm(self):
266 :return: The constructor operator as a term.
268 cdef Term term = Term(self.solver)
269 term.cterm = self.cdc.getConstructorTerm()
272 def getInstantiatedConstructorTerm(self, Sort retSort):
274 Get the constructor operator of this datatype constructor whose
275 return type is retSort. This method is intended to be used on
276 constructors of parametric datatypes and can be seen as returning
277 the constructor term that has been explicitly cast to the given
280 This method is required for constructors of parametric datatypes
281 whose return type cannot be determined by type inference. For
286 (declare-datatype List
287 (par (T) ((nil) (cons (head T) (tail (List T))))))
289 The type of nil terms must be provided by the user. In SMT version
290 2.6, this is done via the syntax for qualified identifiers:
296 This method is equivalent of applying the above, where this
297 DatatypeConstructor is the one corresponding to nil, and retSort is
302 The returned constructor term ``t`` is an operator, while
303 ``Solver.mkTerm(APPLY_CONSTRUCTOR, [t])`` is used to construct
304 the above (nullary) application of nil.
306 .. warning:: This method is experimental and may change in future
309 :param retSort: The desired return sort of the constructor.
310 :return: The constructor operator as a term.
312 cdef Term term = Term(self.solver)
313 term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort)
316 def getTesterTerm(self):
318 :return: The tester operator that is related to this constructor,
321 cdef Term term = Term(self.solver)
322 term.cterm = self.cdc.getTesterTerm()
325 def getNumSelectors(self):
327 :return: The number of selecters (so far) of this Datatype
330 return self.cdc.getNumSelectors()
332 def getSelector(self, str name):
334 :param name: The name of the datatype selector.
335 :return: The first datatype selector with the given name.
337 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
338 ds.cds = self.cdc.getSelector(name.encode())
341 def getSelectorTerm(self, str name):
343 :param name: The name of the datatype selector.
344 :return: A term representing the firstdatatype selector with the
347 cdef Term term = Term(self.solver)
348 term.cterm = self.cdc.getSelectorTerm(name.encode())
353 :return: True if this DatatypeConstructor is a null object.
355 return self.cdc.isNull()
358 return self.cdc.toString().decode()
361 return self.cdc.toString().decode()
365 ds = DatatypeSelector(self.solver)
370 cdef class DatatypeConstructorDecl:
372 A cvc5 datatype constructor declaration.
374 Wrapper class for :cpp:class:`cvc5::DatatypeConstructorDecl`.
376 cdef c_DatatypeConstructorDecl cddc
379 def __cinit__(self, Solver solver):
382 def addSelector(self, str name, Sort sort):
384 Add datatype selector declaration.
386 :param name: The name of the datatype selector declaration to add.
387 :param sort: The codomain sort of the datatype selector declaration
390 self.cddc.addSelector(name.encode(), sort.csort)
392 def addSelectorSelf(self, str name):
394 Add datatype selector declaration whose codomain sort is the
397 :param name: The name of the datatype selector declaration to add.
399 self.cddc.addSelectorSelf(name.encode())
403 :return: True if this DatatypeConstructorDecl is a null object.
405 return self.cddc.isNull()
408 return self.cddc.toString().decode()
411 return self.cddc.toString().decode()
414 cdef class DatatypeDecl:
416 A cvc5 datatype declaration.
418 Wrapper class for :cpp:class:`cvc5::DatatypeDecl`.
420 cdef c_DatatypeDecl cdd
422 def __cinit__(self, Solver solver):
425 def addConstructor(self, DatatypeConstructorDecl ctor):
427 Add a datatype constructor declaration.
429 :param ctor: The datatype constructor declaration to add.
431 self.cdd.addConstructor(ctor.cddc)
433 def getNumConstructors(self):
435 :return: The number of constructors (so far) for this datatype
438 return self.cdd.getNumConstructors()
440 def isParametric(self):
442 :return: True if this datatype declaration is parametric.
444 return self.cdd.isParametric()
448 :return: The name of this datatype declaration.
450 return self.cdd.getName().decode()
454 :return: True if this DatatypeDecl is a null object.
456 return self.cdd.isNull()
459 return self.cdd.toString().decode()
462 return self.cdd.toString().decode()
465 cdef class DatatypeSelector:
467 A cvc5 datatype selector.
469 Wrapper class for :cpp:class:`cvc5::DatatypeSelector`.
471 cdef c_DatatypeSelector cds
473 def __cinit__(self, Solver solver):
474 self.cds = c_DatatypeSelector()
479 :return: The name of this datatype selector.
481 return self.cds.getName().decode()
483 def getSelectorTerm(self):
485 :return: The selector opeartor of this datatype selector as a term.
487 cdef Term term = Term(self.solver)
488 term.cterm = self.cds.getSelectorTerm()
491 def getUpdaterTerm(self):
493 :return: The updater opeartor of this datatype selector as a term.
495 cdef Term term = Term(self.solver)
496 term.cterm = self.cds.getUpdaterTerm()
499 def getCodomainSort(self):
501 :return: The codomain sort of this selector.
503 cdef Sort sort = Sort(self.solver)
504 sort.csort = self.cds.getCodomainSort()
509 :return: True if this DatatypeSelector is a null object.
511 return self.cds.isNull()
514 return self.cds.toString().decode()
517 return self.cds.toString().decode()
524 An operator is a term that represents certain operators,
525 instantiated with its required parameters, e.g.,
526 a term of kind :py:obj:`BVExtract <cvc5.Kind.BVExtract>`.
528 Wrapper class for :cpp:class:`cvc5::Op`.
532 def __cinit__(self, Solver solver):
536 def __eq__(self, Op other):
537 return self.cop == other.cop
539 def __ne__(self, Op other):
540 return self.cop != other.cop
543 return self.cop.toString().decode()
546 return self.cop.toString().decode()
549 return cophash(self.cop)
553 :return: The kind of this operator.
555 return Kind(<int> self.cop.getKind())
559 :return: True iff this operator is indexed.
561 return self.cop.isIndexed()
565 :return: True iff this operator is a null term.
567 return self.cop.isNull()
569 def getNumIndices(self):
571 :return: The number of indices of this op.
573 return self.cop.getNumIndices()
575 def __getitem__(self, i):
577 Get the index at position ``i``.
579 :param i: The position of the index to return.
580 :return: The index at position ``i``.
582 cdef Term term = Term(self.solver)
583 term.cterm = self.cop[i]
591 Wrapper class for :cpp:class:`cvc5::Grammar`.
593 cdef c_Grammar cgrammar
595 def __cinit__(self, Solver solver):
597 self.cgrammar = c_Grammar()
599 def addRule(self, Term ntSymbol, Term rule):
601 Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
603 :param ntSymbol: The non-terminal to which the rule is added.
604 :param rule: The rule to add.
606 self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
608 def addAnyConstant(self, Term ntSymbol):
610 Allow ``ntSymbol`` to be an arbitrary constant.
612 :param ntSymbol: The non-terminal allowed to be constant.
614 self.cgrammar.addAnyConstant(ntSymbol.cterm)
616 def addAnyVariable(self, Term ntSymbol):
618 Allow ``ntSymbol`` to be any input variable to corresponding
619 synth-fun/synth-inv with the same sort as ``ntSymbol``.
621 :param ntSymbol: The non-terminal allowed to be any input variable.
623 self.cgrammar.addAnyVariable(ntSymbol.cterm)
625 def addRules(self, Term ntSymbol, rules):
627 Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
629 :param ntSymbol: The non-terminal to which the rules are added.
630 :param rules: The rules to add.
632 cdef vector[c_Term] crules
634 crules.push_back((<Term?> r).cterm)
635 self.cgrammar.addRules(ntSymbol.cterm, crules)
639 Encapsulation of a three-valued solver result, with explanations.
641 Wrapper class for :cpp:class:`cvc5::Result`.
645 # gets populated by solver
650 :return: True if Result is empty, i.e., a nullary Result, and not
651 an actual result returned from a
652 :py:meth:`Solver.checkSat()` (and friends) query.
654 return self.cr.isNull()
658 :return: True if query was a satisfiable
659 :py:meth:`Solver.checkSat()` or
660 :py:meth:`Solver.checkSatAssuming()` query.
662 return self.cr.isSat()
666 :return: True if query was an usatisfiable
667 :py:meth:`Solver.checkSat()` or
668 :py:meth:`Solver.checkSatAssuming()` query.
670 return self.cr.isUnsat()
674 :return: True if query was a :py:meth:`Solver.checkSat()` or
675 :py:meth:`Solver.checkSatAssuming()` query and cvc5 was
676 not able to determine (un)satisfiability.
678 return self.cr.isUnknown()
680 def getUnknownExplanation(self):
682 :return: An explanation for an unknown query result.
684 return UnknownExplanation(<int> self.cr.getUnknownExplanation())
686 def __eq__(self, Result other):
687 return self.cr == other.cr
689 def __ne__(self, Result other):
690 return self.cr != other.cr
693 return self.cr.toString().decode()
696 return self.cr.toString().decode()
698 cdef class SynthResult:
700 Encapsulation of a solver synth result.
702 This is the return value of the API methods:
704 - :py:meth:`Solver.checkSynth()`
705 - :py:meth:`Solver.checkSynthNext()`
707 which we call synthesis queries. This class indicates whether the
708 synthesis query has a solution, has no solution, or is unknown.
710 cdef c_SynthResult cr
712 # gets populated by solver
713 self.cr = c_SynthResult()
717 :return: True if SynthResult is null, i.e., not a SynthResult
718 returned from a synthesis query.
720 return self.cr.isNull()
722 def hasSolution(self):
724 :return: True if the synthesis query has a solution.
726 return self.cr.hasSolution()
728 def hasNoSolution(self):
730 :return: True if the synthesis query has no solution.
731 In this case, it was determined that there was no solution.
733 return self.cr.hasNoSolution()
737 :return: True if the result of the synthesis query could not be
740 return self.cr.isUnknown()
743 return self.cr.toString().decode()
746 return self.cr.toString().decode()
753 Wrapper class for :cpp:class:`cvc5::Solver`.
755 cdef c_Solver* csolver
758 self.csolver = new c_Solver()
760 def __dealloc__(self):
763 def getBooleanSort(self):
765 :return: Sort Boolean.
767 cdef Sort sort = Sort(self)
768 sort.csort = self.csolver.getBooleanSort()
771 def getIntegerSort(self):
773 :return: Sort Integer.
775 cdef Sort sort = Sort(self)
776 sort.csort = self.csolver.getIntegerSort()
779 def getNullSort(self):
781 :return: A null sort object.
783 cdef Sort sort = Sort(self)
784 sort.csort = self.csolver.getNullSort()
787 def getRealSort(self):
791 cdef Sort sort = Sort(self)
792 sort.csort = self.csolver.getRealSort()
795 def getRegExpSort(self):
796 """:return: The sort of regular expressions.
798 cdef Sort sort = Sort(self)
799 sort.csort = self.csolver.getRegExpSort()
802 def getRoundingModeSort(self):
803 """:return: Sort RoundingMode.
805 cdef Sort sort = Sort(self)
806 sort.csort = self.csolver.getRoundingModeSort()
809 def getStringSort(self):
810 """:return: Sort String.
812 cdef Sort sort = Sort(self)
813 sort.csort = self.csolver.getStringSort()
816 def mkArraySort(self, Sort indexSort, Sort elemSort):
818 Create an array sort.
820 :param indexSort: The array index sort.
821 :param elemSort: The array element sort.
822 :return: The array sort.
824 cdef Sort sort = Sort(self)
825 sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
828 def mkBitVectorSort(self, uint32_t size):
830 Create a bit-vector sort.
832 :param size: The bit-width of the bit-vector sort
833 :return: The bit-vector sort
835 cdef Sort sort = Sort(self)
836 sort.csort = self.csolver.mkBitVectorSort(size)
839 def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
841 Create a floating-point sort.
843 :param exp: The bit-width of the exponent of the floating-point
845 :param sig: The bit-width of the significand of the floating-point
848 cdef Sort sort = Sort(self)
849 sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
852 def mkDatatypeSort(self, DatatypeDecl dtypedecl):
854 Create a datatype sort.
856 :param dtypedecl: The datatype declaration from which the sort is
858 :return: The datatype sort.
860 cdef Sort sort = Sort(self)
861 sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
864 def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
866 Create a vector of datatype sorts using unresolved sorts. The names
867 of the datatype declarations in dtypedecls must be distinct.
869 This method is called when the DatatypeDecl objects dtypedecls have
870 been built using "unresolved" sorts.
872 We associate each sort in unresolvedSorts with exacly one datatype
873 from dtypedecls. In particular, it must have the same name as
874 exactly one datatype declaration in dtypedecls.
876 When constructing datatypes, unresolved sorts are replaced by the
877 datatype sort constructed for the datatype declaration it is
880 :param dtypedecls: The datatype declarations from which the sort is
882 :param unresolvedSorts: The list of unresolved sorts.
883 :return: The datatype sorts.
885 if unresolvedSorts == None:
886 unresolvedSorts = set([])
888 assert isinstance(unresolvedSorts, set)
891 cdef vector[c_DatatypeDecl] decls
892 for decl in dtypedecls:
893 decls.push_back((<DatatypeDecl?> decl).cdd)
895 cdef c_set[c_Sort] usorts
896 for usort in unresolvedSorts:
897 usorts.insert((<Sort?> usort).csort)
899 csorts = self.csolver.mkDatatypeSorts(
900 <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
908 def mkFunctionSort(self, sorts, Sort codomain):
910 Create function sort.
912 :param sorts: The sort of the function arguments.
913 :param codomain: The sort of the function return value.
914 :return: The function sort.
917 cdef Sort sort = Sort(self)
918 # populate a vector with dereferenced c_Sorts
919 cdef vector[c_Sort] v
920 if isinstance(sorts, Sort):
921 v.push_back((<Sort?>sorts).csort)
924 v.push_back((<Sort?>s).csort)
926 sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
930 def mkParamSort(self, str symbolname = None):
932 Create a sort parameter.
934 .. warning:: This method is experimental and may change in future
937 :param symbol: The name of the sort.
938 :return: The sort parameter.
940 cdef Sort sort = Sort(self)
941 if symbolname is None:
942 sort.csort = self.csolver.mkParamSort()
944 sort.csort = self.csolver.mkParamSort(symbolname.encode())
947 @expand_list_arg(num_req_args=0)
948 def mkPredicateSort(self, *sorts):
950 Create a predicate sort.
952 :param sorts: The list of sorts of the predicate, as a list or as
954 :return: The predicate sort.
956 cdef Sort sort = Sort(self)
957 cdef vector[c_Sort] v
959 v.push_back((<Sort?> s).csort)
960 sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
963 @expand_list_arg(num_req_args=0)
964 def mkRecordSort(self, *fields):
968 .. warning:: This method is experimental and may change in future
971 :param fields: The list of fields of the record, as a list or as
973 :return: The record sort.
975 cdef Sort sort = Sort(self)
976 cdef vector[pair[string, c_Sort]] v
977 cdef pair[string, c_Sort] p
981 p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
983 sort.csort = self.csolver.mkRecordSort(
984 <const vector[pair[string, c_Sort]] &> v)
987 def mkSetSort(self, Sort elemSort):
991 :param elemSort: The sort of the set elements.
992 :return: The set sort.
994 cdef Sort sort = Sort(self)
995 sort.csort = self.csolver.mkSetSort(elemSort.csort)
998 def mkBagSort(self, Sort elemSort):
1002 :param elemSort: The sort of the bag elements.
1003 :return: The bag sort.
1005 cdef Sort sort = Sort(self)
1006 sort.csort = self.csolver.mkBagSort(elemSort.csort)
1009 def mkSequenceSort(self, Sort elemSort):
1011 Create a sequence sort.
1013 :param elemSort: The sort of the sequence elements
1014 :return: The sequence sort.
1016 cdef Sort sort = Sort(self)
1017 sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
1020 def mkUninterpretedSort(self, str name = None):
1022 Create an uninterpreted sort.
1024 :param symbol: The name of the sort.
1025 :return: The uninterpreted sort.
1027 cdef Sort sort = Sort(self)
1029 sort.csort = self.csolver.mkUninterpretedSort()
1031 sort.csort = self.csolver.mkUninterpretedSort(name.encode())
1034 def mkUnresolvedSort(self, str name, size_t arity = 0):
1036 Create an unresolved sort.
1038 This is for creating yet unresolved sort placeholders for mutually
1039 recursive datatypes.
1041 :param symbol: The name of the sort.
1042 :param arity: The number of sort parameters of the sort.
1043 :return: The unresolved sort.
1045 cdef Sort sort = Sort(self)
1046 sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity)
1049 def mkUninterpretedSortConstructorSort(self, size_t arity, str symbol = None):
1051 Create a sort constructor sort.
1053 An uninterpreted sort constructor is an uninterpreted sort with
1056 :param symbol: The symbol of the sort.
1057 :param arity: The arity of the sort (must be > 0).
1058 :return: The sort constructor sort.
1060 cdef Sort sort = Sort(self)
1062 sort.csort = self.csolver.mkUninterpretedSortConstructorSort(arity)
1064 sort.csort = self.csolver.mkUninterpretedSortConstructorSort(
1065 arity, symbol.encode())
1068 @expand_list_arg(num_req_args=0)
1069 def mkTupleSort(self, *sorts):
1071 Create a tuple sort.
1073 :param sorts: Of the elements of the tuple, as a list or as
1075 :return: The tuple sort.
1077 cdef Sort sort = Sort(self)
1078 cdef vector[c_Sort] v
1080 v.push_back((<Sort?> s).csort)
1081 sort.csort = self.csolver.mkTupleSort(v)
1084 @expand_list_arg(num_req_args=1)
1085 def mkTerm(self, kind_or_op, *args):
1089 Supports the following arguments:
1091 - ``Term mkTerm(Kind kind)``
1092 - ``Term mkTerm(Kind kind, List[Term] children)``
1093 - ``Term mkTerm(Op op)``
1094 - ``Term mkTerm(Op op, List[Term] children)``
1096 where ``List[Term]`` can also be comma-separated arguments
1098 cdef Term term = Term(self)
1099 cdef vector[c_Term] v
1102 if isinstance(kind_or_op, Kind):
1103 op = self.mkOp(kind_or_op)
1106 term.cterm = self.csolver.mkTerm((<Op?> op).cop)
1109 v.push_back((<Term?> a).cterm)
1110 term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
1113 def mkTuple(self, sorts, terms):
1115 Create a tuple term. Terms are automatically converted if sorts are
1118 :param sorts: The sorts of the elements in the tuple.
1119 :param terms: The elements in the tuple.
1120 :return: The tuple Term.
1122 cdef vector[c_Sort] csorts
1123 cdef vector[c_Term] cterms
1126 csorts.push_back((<Sort?> s).csort)
1128 cterms.push_back((<Term?> s).cterm)
1129 cdef Term result = Term(self)
1130 result.cterm = self.csolver.mkTuple(csorts, cterms)
1133 @expand_list_arg(num_req_args=0)
1134 def mkOp(self, k, *args):
1138 Supports the following arguments:
1140 - ``Op mkOp(Kind kind)``
1141 - ``Op mkOp(Kind kind, const string& arg)``
1142 - ``Op mkOp(Kind kind, uint32_t arg0, ...)``
1144 cdef Op op = Op(self)
1145 cdef vector[uint32_t] v
1148 op.cop = self.csolver.mkOp(<c_Kind> k.value)
1149 elif len(args) == 1 and isinstance(args[0], str):
1150 op.cop = self.csolver.mkOp(<c_Kind> k.value,
1155 if not isinstance(a, int):
1157 "Expected uint32_t for argument {}".format(a))
1158 if a < 0 or a >= 2 ** 31:
1160 "Argument {} must fit in a uint32_t".format(a))
1161 v.push_back((<uint32_t?> a))
1162 op.cop = self.csolver.mkOp(<c_Kind> k.value, v)
1167 Create a Boolean true constant.
1169 :return: The true constant.
1171 cdef Term term = Term(self)
1172 term.cterm = self.csolver.mkTrue()
1177 Create a Boolean false constant.
1179 :return: The false constant.
1181 cdef Term term = Term(self)
1182 term.cterm = self.csolver.mkFalse()
1185 def mkBoolean(self, bint val):
1187 Create a Boolean constant.
1189 :return: The Boolean constant.
1190 :param val: The value of the constant.
1192 cdef Term term = Term(self)
1193 term.cterm = self.csolver.mkBoolean(val)
1198 Create a constant representing the number Pi.
1200 :return: A constant representing :py:obj:`Pi <cvc5.Kind.Pi>`.
1202 cdef Term term = Term(self)
1203 term.cterm = self.csolver.mkPi()
1206 def mkInteger(self, val):
1208 Create an integer constant.
1210 :param val: Representation of the constant: either a string or
1212 :return: A constant of sort Integer.
1214 cdef Term term = Term(self)
1215 if isinstance(val, str):
1216 term.cterm = self.csolver.mkInteger(
1217 <const string &> str(val).encode())
1219 assert(isinstance(val, int))
1220 term.cterm = self.csolver.mkInteger((<int?> val))
1223 def mkReal(self, val, den=None):
1225 Create a real constant.
1227 :param val: The value of the term. Can be an integer, float, or
1228 string. It will be formatted as a string before the
1230 :param den: If not None, the value is ``val``/``den``.
1231 :return: A real term with literal value.
1233 Can be used in various forms:
1235 - Given a string ``"N/D"`` constructs the corresponding rational.
1236 - Given a string ``"W.D"`` constructs the reduction of
1237 ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
1238 - Given a float ``f``, constructs the rational matching ``f``'s
1239 string representation. This means that ``mkReal(0.3)`` gives
1240 ``3/10`` and not the IEEE-754 approximation of ``3/10``.
1241 - Given a string ``"W"`` or an integer, constructs that integer.
1242 - Given two strings and/or integers ``N`` and ``D``, constructs
1245 cdef Term term = Term(self)
1247 term.cterm = self.csolver.mkReal(str(val).encode())
1249 if not isinstance(val, int) or not isinstance(den, int):
1250 raise ValueError("Expecting integers when"
1251 " constructing a rational"
1252 " but got: {}".format((val, den)))
1253 term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
1256 def mkRegexpAll(self):
1258 Create a regular expression all (``re.all``) term.
1260 :return: The all term.
1262 cdef Term term = Term(self)
1263 term.cterm = self.csolver.mkRegexpAll()
1266 def mkRegexpAllchar(self):
1268 Create a regular expression allchar (``re.allchar``) term.
1270 :return: The allchar term.
1272 cdef Term term = Term(self)
1273 term.cterm = self.csolver.mkRegexpAllchar()
1276 def mkRegexpNone(self):
1278 Create a regular expression none (``re.none``) term.
1280 :return: The none term.
1282 cdef Term term = Term(self)
1283 term.cterm = self.csolver.mkRegexpNone()
1286 def mkEmptySet(self, Sort s):
1288 Create a constant representing an empty set of the given sort.
1290 :param sort: The sort of the set elements.
1291 :return: The empty set constant.
1293 cdef Term term = Term(self)
1294 term.cterm = self.csolver.mkEmptySet(s.csort)
1297 def mkEmptyBag(self, Sort s):
1299 Create a constant representing an empty bag of the given sort.
1301 :param sort: The sort of the bag elements.
1302 :return: The empty bag constant.
1304 cdef Term term = Term(self)
1305 term.cterm = self.csolver.mkEmptyBag(s.csort)
1310 Create a separation logic empty term.
1312 .. warning:: This method is experimental and may change in future
1315 :return: The separation logic empty term.
1317 cdef Term term = Term(self)
1318 term.cterm = self.csolver.mkSepEmp()
1321 def mkSepNil(self, Sort sort):
1323 Create a separation logic nil term.
1325 .. warning:: This method is experimental and may change in future
1328 :param sort: The sort of the nil term.
1329 :return: The separation logic nil term.
1331 cdef Term term = Term(self)
1332 term.cterm = self.csolver.mkSepNil(sort.csort)
1335 def mkString(self, str s, useEscSequences = None):
1337 Create a String constant from a ``str`` which may contain SMT-LIB
1338 compatible escape sequences like ``\\u1234`` to encode unicode
1341 :param s: The string this constant represents.
1342 :param useEscSequences: Determines whether escape sequences in `s`
1343 should be converted to the corresponding
1345 :return: The String constant.
1347 cdef Term term = Term(self)
1348 cdef Py_ssize_t size
1349 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1350 if isinstance(useEscSequences, bool):
1351 term.cterm = self.csolver.mkString(
1352 s.encode(), <bint> useEscSequences)
1354 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1358 def mkEmptySequence(self, Sort sort):
1360 Create an empty sequence of the given element sort.
1362 :param sort: The element sort of the sequence.
1363 :return: The empty sequence with given element sort.
1365 cdef Term term = Term(self)
1366 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1369 def mkUniverseSet(self, Sort sort):
1371 Create a universe set of the given sort.
1373 :param sort: The sort of the set elements
1374 :return: The universe set constant
1376 cdef Term term = Term(self)
1377 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1380 @expand_list_arg(num_req_args=0)
1381 def mkBitVector(self, *args):
1383 Create bit-vector value.
1385 Supports the following arguments:
1387 - ``Term mkBitVector(int size, int val=0)``
1388 - ``Term mkBitVector(int size, string val, int base)``
1390 :return: A Term representing a bit-vector value.
1391 :param size: The bit-width.
1392 :param val: An integer representating the value, in the first form.
1393 In the second form, a string representing the value.
1394 :param base: The base of the string representation (second form
1397 cdef Term term = Term(self)
1399 raise ValueError("Missing arguments to mkBitVector")
1401 if not isinstance(size, int):
1403 "Invalid first argument to mkBitVector '{}', "
1404 "expected bit-vector size".format(size))
1406 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1407 elif len(args) == 2:
1409 if not isinstance(val, int):
1411 "Invalid second argument to mkBitVector '{}', "
1412 "expected integer value".format(size))
1413 term.cterm = self.csolver.mkBitVector(
1414 <uint32_t> size, <uint32_t> val)
1415 elif len(args) == 3:
1418 if not isinstance(val, str):
1420 "Invalid second argument to mkBitVector '{}', "
1421 "expected value string".format(size))
1422 if not isinstance(base, int):
1424 "Invalid third argument to mkBitVector '{}', "
1425 "expected base given as integer".format(size))
1426 term.cterm = self.csolver.mkBitVector(
1428 <const string&> str(val).encode(),
1431 raise ValueError("Unexpected inputs to mkBitVector")
1434 def mkConstArray(self, Sort sort, Term val):
1436 Create a constant array with the provided constant value stored at
1439 :param sort: The sort of the constant array (must be an array sort).
1440 :param val: The constant value to store (must match the sort's
1442 :return: The constant array term.
1444 cdef Term term = Term(self)
1445 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1448 def mkFloatingPointPosInf(self, int exp, int sig):
1450 Create a positive infinity floating-point constant.
1452 :param exp: Number of bits in the exponent.
1453 :param sig: Number of bits in the significand.
1454 :return: The floating-point constant.
1456 cdef Term term = Term(self)
1457 term.cterm = self.csolver.mkFloatingPointPosInf(exp, sig)
1460 def mkFloatingPointNegInf(self, int exp, int sig):
1462 Create a negative infinity floating-point constant.
1464 :param exp: Number of bits in the exponent.
1465 :param sig: Number of bits in the significand.
1466 :return: The floating-point constant.
1468 cdef Term term = Term(self)
1469 term.cterm = self.csolver.mkFloatingPointNegInf(exp, sig)
1472 def mkFloatingPointNaN(self, int exp, int sig):
1474 Create a not-a-number (NaN) floating-point constant.
1476 :param exp: Number of bits in the exponent.
1477 :param sig: Number of bits in the significand.
1478 :return: The floating-point constant.
1480 cdef Term term = Term(self)
1481 term.cterm = self.csolver.mkFloatingPointNaN(exp, sig)
1484 def mkFloatingPointPosZero(self, int exp, int sig):
1486 Create a positive zero (+0.0) floating-point constant.
1488 :param exp: Number of bits in the exponent.
1489 :param sig: Number of bits in the significand.
1490 :return: The floating-point constant.
1492 cdef Term term = Term(self)
1493 term.cterm = self.csolver.mkFloatingPointPosZero(exp, sig)
1496 def mkFloatingPointNegZero(self, int exp, int sig):
1498 Create a negative zero (+0.0) floating-point constant.
1500 :param exp: Number of bits in the exponent.
1501 :param sig: Number of bits in the significand.
1502 :return: The floating-point constant.
1504 cdef Term term = Term(self)
1505 term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig)
1508 def mkRoundingMode(self, rm):
1510 Create a roundingmode constant.
1512 :param rm: The floating point rounding mode this constant
1515 cdef Term term = Term(self)
1516 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.value)
1519 def mkFloatingPoint(self, int exp, int sig, Term val):
1521 Create a floating-point constant.
1523 :param exp: Size of the exponent.
1524 :param sig: Size of the significand.
1525 :param val: Value of the floating-point constant as a bit-vector
1528 cdef Term term = Term(self)
1529 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1532 def mkCardinalityConstraint(self, Sort sort, int index):
1534 Create cardinality constraint.
1536 .. warning:: This method is experimental and may change in future
1539 :param sort: Sort of the constraint.
1540 :param index: The upper bound for the cardinality of the sort.
1542 cdef Term term = Term(self)
1543 term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
1546 def mkConst(self, Sort sort, symbol=None):
1548 Create (first-order) constant (0-arity function symbol).
1552 .. code-block:: smtlib
1554 ( declare-const <symbol> <sort> )
1555 ( declare-fun <symbol> ( ) <sort> )
1557 :param sort: The sort of the constant.
1558 :param symbol: The name of the constant. If None, a default symbol
1560 :return: The first-order constant.
1562 cdef Term term = Term(self)
1564 term.cterm = self.csolver.mkConst(sort.csort)
1566 term.cterm = self.csolver.mkConst(sort.csort,
1567 (<str?> symbol).encode())
1570 def mkVar(self, Sort sort, symbol=None):
1572 Create a bound variable to be used in a binder (i.e. a quantifier,
1573 a lambda, or a witness binder).
1575 :param sort: The sort of the variable.
1576 :param symbol: The name of the variable.
1577 :return: The variable.
1579 cdef Term term = Term(self)
1581 term.cterm = self.csolver.mkVar(sort.csort)
1583 term.cterm = self.csolver.mkVar(sort.csort,
1584 (<str?> symbol).encode())
1587 def mkDatatypeConstructorDecl(self, str name):
1589 Create datatype constructor declaration.
1591 :param name: The name of the constructor.
1592 :return: The datatype constructor declaration.
1594 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1595 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1598 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1600 Create a datatype declaration.
1602 :param name: The name of the datatype.
1603 :param isCoDatatype: True if a codatatype is to be constructed.
1604 :return: The datatype declaration.
1606 cdef DatatypeDecl dd = DatatypeDecl(self)
1607 cdef vector[c_Sort] v
1610 if sorts_or_bool is None and isCoDatatype is None:
1611 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1612 elif sorts_or_bool is not None and isCoDatatype is None:
1613 if isinstance(sorts_or_bool, bool):
1614 dd.cdd = self.csolver.mkDatatypeDecl(
1615 <const string &> name.encode(), <bint> sorts_or_bool)
1616 elif isinstance(sorts_or_bool, Sort):
1617 dd.cdd = self.csolver.mkDatatypeDecl(
1618 <const string &> name.encode(),
1619 (<Sort> sorts_or_bool).csort)
1620 elif isinstance(sorts_or_bool, list):
1621 for s in sorts_or_bool:
1622 v.push_back((<Sort?> s).csort)
1623 dd.cdd = self.csolver.mkDatatypeDecl(
1624 <const string &> name.encode(),
1625 <const vector[c_Sort]&> v)
1627 raise ValueError("Unhandled second argument type {}"
1628 .format(type(sorts_or_bool)))
1629 elif sorts_or_bool is not None and isCoDatatype is not None:
1630 if isinstance(sorts_or_bool, Sort):
1631 dd.cdd = self.csolver.mkDatatypeDecl(
1632 <const string &> name.encode(),
1633 (<Sort> sorts_or_bool).csort,
1634 <bint> isCoDatatype)
1635 elif isinstance(sorts_or_bool, list):
1636 for s in sorts_or_bool:
1637 v.push_back((<Sort?> s).csort)
1638 dd.cdd = self.csolver.mkDatatypeDecl(
1639 <const string &> name.encode(),
1640 <const vector[c_Sort]&> v,
1641 <bint> isCoDatatype)
1643 raise ValueError("Unhandled second argument type {}"
1644 .format(type(sorts_or_bool)))
1646 raise ValueError("Can't create DatatypeDecl with {}".format(
1647 [type(a) for a in [name, sorts_or_bool, isCoDatatype]]))
1651 def simplify(self, Term t):
1653 Simplify a formula without doing "much" work. Does not involve the
1654 SAT Engine in the simplification, but uses the current definitions,
1655 assertions, and the current partial model, if one has been
1656 constructed. It also involves theory normalization.
1658 .. warning:: This method is experimental and may change in future
1661 :param t: The formula to simplify.
1662 :return: The simplified formula.
1664 cdef Term term = Term(self)
1665 term.cterm = self.csolver.simplify(t.cterm)
1668 def assertFormula(self, Term term):
1674 .. code-block:: smtlib
1678 :param term: The formula to assert.
1680 self.csolver.assertFormula(term.cterm)
1684 Check satisfiability.
1688 .. code-block:: smtlib
1692 :return: The result of the satisfiability check.
1694 cdef Result r = Result()
1695 r.cr = self.csolver.checkSat()
1698 def mkSygusGrammar(self, boundVars, ntSymbols):
1700 Create a SyGuS grammar. The first non-terminal is treated as the
1701 starting non-terminal, so the order of non-terminals matters.
1703 :param boundVars: The parameters to corresponding
1704 synth-fun/synth-inv.
1705 :param ntSymbols: The pre-declaration of the non-terminal symbols.
1706 :return: The grammar.
1708 cdef Grammar grammar = Grammar(self)
1709 cdef vector[c_Term] bvc
1710 cdef vector[c_Term] ntc
1711 for bv in boundVars:
1712 bvc.push_back((<Term?> bv).cterm)
1713 for nt in ntSymbols:
1714 ntc.push_back((<Term?> nt).cterm)
1715 grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1718 def declareSygusVar(self, str symbol, Sort sort):
1720 Append symbol to the current list of universal variables.
1724 .. code-block:: smtlib
1726 ( declare-var <symbol> <sort> )
1728 :param sort: The sort of the universal variable.
1729 :param symbol: The name of the universal variable.
1730 :return: The universal variable.
1732 cdef Term term = Term(self)
1733 term.cterm = self.csolver.declareSygusVar(symbol.encode(), sort.csort)
1736 def addSygusConstraint(self, Term t):
1738 Add a formula to the set of SyGuS constraints.
1742 .. code-block:: smtlib
1744 ( constraint <term> )
1746 :param term: The formula to add as a constraint.
1748 self.csolver.addSygusConstraint(t.cterm)
1750 def addSygusAssume(self, Term t):
1752 Add a formula to the set of Sygus assumptions.
1756 .. code-block:: smtlib
1760 :param term: The formuula to add as an assumption.
1762 self.csolver.addSygusAssume(t.cterm)
1764 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1766 Add a set of SyGuS constraints to the current state that correspond
1767 to an invariant synthesis problem.
1771 .. code-block:: smtlib
1773 ( inv-constraint <inv> <pre> <trans> <post> )
1775 :param inv: The function-to-synthesize.
1776 :param pre: The pre-condition.
1777 :param trans: The transition relation.
1778 :param post: The post-condition.
1780 self.csolver.addSygusInvConstraint(
1781 inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1783 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1785 Synthesize n-ary function following specified syntactic constraints.
1789 .. code-block:: smtlib
1791 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1793 :param symbol: The name of the function.
1794 :param boundVars: The parameters to this function.
1795 :param sort: The sort of the return value of this function.
1796 :param grammar: The syntactic constraints.
1797 :return: The function.
1799 cdef Term term = Term(self)
1800 cdef vector[c_Term] v
1801 for bv in bound_vars:
1802 v.push_back((<Term?> bv).cterm)
1804 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1806 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1809 def checkSynth(self):
1811 Try to find a solution for the synthesis conjecture corresponding
1812 to the current list of functions-to-synthesize, universal variables
1817 .. code-block:: smtlib
1821 :return: The result of the check, which is "solution" if the check
1822 found a solution in which case solutions are available via
1823 getSynthSolutions, "no solution" if it was determined
1824 there is no solution, or "unknown" otherwise.
1826 cdef SynthResult r = SynthResult()
1827 r.cr = self.csolver.checkSynth()
1830 def checkSynthNext(self):
1832 Try to find a next solution for the synthesis conjecture
1833 corresponding to the current list of functions-to-synthesize,
1834 universal variables and constraints. Must be called immediately
1835 after a successful call to check-synth or check-synth-next.
1836 Requires incremental mode.
1840 .. code-block:: smtlib
1844 :return: The result of the check, which is "solution" if the check
1845 found a solution in which case solutions are available via
1846 getSynthSolutions, "no solution" if it was determined
1847 there is no solution, or "unknown" otherwise.
1849 cdef SynthResult r = SynthResult()
1850 r.cr = self.csolver.checkSynthNext()
1853 def getSynthSolution(self, Term term):
1855 Get the synthesis solution of the given term. This method should be
1856 called immediately after the solver answers unsat for sygus input.
1858 :param term: The term for which the synthesis solution is queried.
1859 :return: The synthesis solution of the given term.
1861 cdef Term t = Term(self)
1862 t.cterm = self.csolver.getSynthSolution(term.cterm)
1865 def getSynthSolutions(self, list terms):
1867 Get the synthesis solutions of the given terms. This method should
1868 be called immediately after the solver answers unsat for sygus
1871 :param terms: The terms for which the synthesis solutions is
1873 :return: The synthesis solutions of the given terms.
1876 cdef vector[c_Term] vec
1878 vec.push_back((<Term?> t).cterm)
1879 cresult = self.csolver.getSynthSolutions(vec)
1887 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1889 Synthesize invariant.
1893 .. code-block:: smtlib
1895 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1897 :param symbol: The name of the invariant.
1898 :param boundVars: The parameters to this invariant.
1899 :param grammar: The syntactic constraints.
1900 :return: The invariant.
1902 cdef Term term = Term(self)
1903 cdef vector[c_Term] v
1904 for bv in bound_vars:
1905 v.push_back((<Term?> bv).cterm)
1907 term.cterm = self.csolver.synthInv(
1908 symbol.encode(), <const vector[c_Term]&> v)
1910 term.cterm = self.csolver.synthInv(
1912 <const vector[c_Term]&> v,
1916 @expand_list_arg(num_req_args=0)
1917 def checkSatAssuming(self, *assumptions):
1919 Check satisfiability assuming the given formula.
1923 .. code-block:: smtlib
1925 ( check-sat-assuming ( <prop_literal> ) )
1927 :param assumptions: The formulas to assume, as a list or as
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 @expand_list_arg(num_req_args=1)
1940 def declareDatatype(self, str symbol, *ctors):
1942 Create datatype sort.
1946 .. code-block:: smtlib
1948 ( declare-datatype <symbol> <datatype_decl> )
1950 :param symbol: The name of the datatype sort.
1951 :param ctors: The constructor declarations of the datatype sort, as
1952 a list or as distinct arguments.
1953 :return: The datatype sort.
1955 cdef Sort sort = Sort(self)
1956 cdef vector[c_DatatypeConstructorDecl] v
1959 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1960 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1963 def declareFun(self, str symbol, list sorts, Sort sort):
1965 Declare n-ary function symbol.
1969 .. code-block:: smtlib
1971 ( declare-fun <symbol> ( <sort>* ) <sort> )
1973 :param symbol: The name of the function.
1974 :param sorts: The sorts of the parameters to this function.
1975 :param sort: The sort of the return value of this function.
1976 :return: The function.
1978 cdef Term term = Term(self)
1979 cdef vector[c_Sort] v
1981 v.push_back((<Sort?> s).csort)
1982 term.cterm = self.csolver.declareFun(symbol.encode(),
1983 <const vector[c_Sort]&> v,
1987 def declareSort(self, str symbol, int arity):
1989 Declare uninterpreted sort.
1993 .. code-block:: smtlib
1995 ( declare-sort <symbol> <numeral> )
1999 This corresponds to :py:meth:`Solver.mkUninterpretedSort()` if
2001 :py:meth:`Solver.mkUninterpretedSortConstructorSort()` if
2004 :param symbol: The name of the sort.
2005 :param arity: The arity of the sort.
2008 cdef Sort sort = Sort(self)
2009 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
2012 def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
2014 Define n-ary function.
2018 .. code-block:: smtlib
2020 ( define-fun <function_def> )
2022 :param symbol: The name of the function.
2023 :param bound_vars: The parameters to this function.
2024 :param sort: The sort of the return value of this function.
2025 :param term: The function body.
2026 :param glbl: Determines whether this definition is global (i.e.
2027 persists when popping the context).
2028 :return: The function.
2030 cdef Term fun = Term(self)
2031 cdef vector[c_Term] v
2032 for bv in bound_vars:
2033 v.push_back((<Term?> bv).cterm)
2035 fun.cterm = self.csolver.defineFun(symbol.encode(),
2036 <const vector[c_Term] &> v,
2042 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
2044 Define recursive functions.
2046 Supports the following arguments:
2048 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
2049 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
2053 .. code-block:: smtlib
2055 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
2057 Create elements of parameter ``funs`` with :py:meth:`mkConst() <cvc5.Solver.mkConst()>`.
2059 :param funs: The sorted functions.
2060 :param bound_vars: The list of parameters to the functions.
2061 :param terms: The list of function bodies of the functions.
2062 :param global: Determines whether this definition is global (i.e.
2063 persists when popping the context).
2064 :return: The function.
2066 cdef Term term = Term(self)
2067 cdef vector[c_Term] v
2068 for bv in bound_vars:
2069 v.push_back((<Term?> bv).cterm)
2072 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
2073 <const vector[c_Term] &> v,
2074 (<Sort?> sort_or_term).csort,
2078 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
2079 <const vector[c_Term]&> v,
2080 (<Term?> sort_or_term).cterm,
2085 def defineFunsRec(self, funs, bound_vars, terms):
2087 Define recursive functions.
2091 .. code-block:: smtlib
2093 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
2095 Create elements of parameter ``funs`` with :py:meth:`mkConst() <cvc5.Solver.mkConst()>`.
2097 :param funs: The sorted functions.
2098 :param bound_vars: The list of parameters to the functions.
2099 :param terms: The list of function bodies of the functions.
2100 :param global: Determines whether this definition is global (i.e.
2101 persists when popping the context).
2102 :return: The function.
2104 cdef vector[c_Term] vf
2105 cdef vector[vector[c_Term]] vbv
2106 cdef vector[c_Term] vt
2109 vf.push_back((<Term?> f).cterm)
2111 cdef vector[c_Term] temp
2112 for v in bound_vars:
2114 temp.push_back((<Term?> t).cterm)
2119 vf.push_back((<Term?> t).cterm)
2123 Get the refutation proof
2127 .. code-block:: smtlib
2131 Requires to enable option
2132 :ref:`produce-proofs <lbl-option-produce-proofs>`.
2134 .. warning:: This method is experimental and may change in future
2137 :return: A string representing the proof, according to the value of
2138 :ref:`proof-format-mode <lbl-option-proof-format-mode>`.
2140 return self.csolver.getProof()
2142 def getLearnedLiterals(self):
2144 Get a list of literals that are entailed by the current set of assertions
2148 .. code-block:: smtlib
2150 ( get-learned-literals )
2152 .. warning:: This method is experimental and may change in future
2155 :return: The list of literals.
2158 for a in self.csolver.getLearnedLiterals():
2164 def getAssertions(self):
2166 Get the list of asserted formulas.
2170 .. code-block:: smtlib
2174 :return: The list of asserted formulas.
2177 for a in self.csolver.getAssertions():
2180 assertions.append(term)
2183 def getInfo(self, str flag):
2185 Get info from the solver.
2189 .. code-block:: smtlib
2191 ( get-info <info_flag> )
2193 :param flag: The info flag.
2196 return self.csolver.getInfo(flag.encode())
2198 def getOption(self, str option):
2200 Get the value of a given option.
2204 .. code-block:: smtlib
2206 ( get-option <keyword> )
2208 :param option: The option for which the value is queried.
2209 :return: A string representation of the option value.
2211 return self.csolver.getOption(option.encode()).decode()
2213 def getOptionNames(self):
2215 Get all option names that can be used with
2216 :py:meth:`Solver.setOption()`, :py:meth:`Solver.getOption()`
2217 and :py:meth:`Solver.getOptionInfo()`.
2219 :return: All option names.
2221 return [s.decode() for s in self.csolver.getOptionNames()]
2223 def getOptionInfo(self, str option):
2225 Get some information about the given option.
2226 Returns the information provided by the C++
2227 :cpp:func:`OptionInfo <cvc5::OptionInfo>` as a dictionary.
2229 :return: Information about the given option.
2231 # declare all the variables we may need later
2232 cdef c_OptionInfo.ValueInfo[c_bool] vib
2233 cdef c_OptionInfo.ValueInfo[string] vis
2234 cdef c_OptionInfo.NumberInfo[int64_t] nii
2235 cdef c_OptionInfo.NumberInfo[uint64_t] niu
2236 cdef c_OptionInfo.NumberInfo[double] nid
2237 cdef c_OptionInfo.ModeInfo mi
2239 oi = self.csolver.getOptionInfo(option.encode())
2240 # generic information
2242 'name': oi.name.decode(),
2243 'aliases': [s.decode() for s in oi.aliases],
2244 'setByUser': oi.setByUser,
2247 # now check which type is actually in the variant
2248 if c_holds[c_OptionInfo.VoidInfo](oi.valueInfo):
2251 elif c_holds[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo):
2254 vib = c_getVariant[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo)
2255 res['current'] = vib.currentValue
2256 res['default'] = vib.defaultValue
2257 elif c_holds[c_OptionInfo.ValueInfo[string]](oi.valueInfo):
2260 vis = c_getVariant[c_OptionInfo.ValueInfo[string]](oi.valueInfo)
2261 res['current'] = vis.currentValue.decode()
2262 res['default'] = vis.defaultValue.decode()
2263 elif c_holds[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo):
2266 nii = c_getVariant[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo)
2267 res['current'] = nii.currentValue
2268 res['default'] = nii.defaultValue
2269 res['minimum'] = nii.minimum.value() \
2270 if nii.minimum.has_value() else None
2271 res['maximum'] = nii.maximum.value() \
2272 if nii.maximum.has_value() else None
2273 elif c_holds[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo):
2276 niu = c_getVariant[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo)
2277 res['current'] = niu.currentValue
2278 res['default'] = niu.defaultValue
2279 res['minimum'] = niu.minimum.value() \
2280 if niu.minimum.has_value() else None
2281 res['maximum'] = niu.maximum.value() \
2282 if niu.maximum.has_value() else None
2283 elif c_holds[c_OptionInfo.NumberInfo[double]](oi.valueInfo):
2286 nid = c_getVariant[c_OptionInfo.NumberInfo[double]](oi.valueInfo)
2287 res['current'] = nid.currentValue
2288 res['default'] = nid.defaultValue
2289 res['minimum'] = nid.minimum.value() \
2290 if nid.minimum.has_value() else None
2291 res['maximum'] = nid.maximum.value() \
2292 if nid.maximum.has_value() else None
2293 elif c_holds[c_OptionInfo.ModeInfo](oi.valueInfo):
2295 res['type'] = 'mode'
2296 mi = c_getVariant[c_OptionInfo.ModeInfo](oi.valueInfo)
2297 res['current'] = mi.currentValue.decode()
2298 res['default'] = mi.defaultValue.decode()
2299 res['modes'] = [s.decode() for s in mi.modes]
2302 def getOptionNames(self):
2304 Get all option names that can be used with
2305 :py:meth:`Solver.setOption()`, :py:meth:`Solver.getOption()` and
2306 :py:meth:`Solver.getOptionInfo()`.
2307 :return: All option names.
2310 for n in self.csolver.getOptionNames():
2311 result += [n.decode()]
2314 def getUnsatAssumptions(self):
2316 Get the set of unsat ("failed") assumptions.
2320 .. code-block:: smtlib
2322 ( get-unsat-assumptions )
2324 Requires to enable option :ref:`produce-unsat-assumptions
2325 <lbl-option-produce-unsat-assumptions>`.
2327 :return: The set of unsat assumptions.
2330 for a in self.csolver.getUnsatAssumptions():
2333 assumptions.append(term)
2336 def getUnsatCore(self):
2338 Get the unsatisfiable core.
2342 .. code-block:: smtlib
2346 Requires to enable option :ref:`produce-unsat-cores
2347 <lbl-option-produce-unsat-cores>`.
2351 In contrast to SMT-LIB, the API does not distinguish between
2352 named and unnamed assertions when producing an unsatisfiable
2353 core. Additionally, the API allows this option to be called after
2354 a check with assumptions. A subset of those assumptions may be
2355 included in the unsatisfiable core returned by this method.
2357 :return: A set of terms representing the unsatisfiable core.
2360 for a in self.csolver.getUnsatCore():
2366 def getDifficulty(self):
2368 Get a difficulty estimate for an asserted formula. This method is
2369 intended to be called immediately after any response to a
2370 :py:meth:`Solver.checkSat()` call.
2372 .. warning:: This method is experimental and may change in future
2375 :return: A map from (a subset of) the input assertions to a real
2376 value that is an estimate of how difficult each assertion
2377 was to solver. Unmentioned assertions can be assumed to
2378 have zero difficulty.
2381 for p in self.csolver.getDifficulty():
2391 diffi[termk] = termv
2394 def getValue(self, Term t):
2396 Get the value of the given term in the current model.
2400 .. code-block:: smtlib
2402 ( get-value ( <term> ) )
2404 :param term: The term for which the value is queried.
2405 :return: The value of the given term.
2407 cdef Term term = Term(self)
2408 term.cterm = self.csolver.getValue(t.cterm)
2411 def getModelDomainElements(self, Sort s):
2413 Get the domain elements of uninterpreted sort s in the current
2414 model. The current model interprets s as the finite sort whose
2415 domain elements are given in the return value of this method.
2417 :param s: The uninterpreted sort in question.
2418 :return: The domain elements of s in the current model.
2421 cresult = self.csolver.getModelDomainElements(s.csort)
2428 def isModelCoreSymbol(self, Term v):
2430 This returns False if the model value of free constant v was not
2431 essential for showing the satisfiability of the last call to
2432 checkSat using the current model. This method will only return
2433 false (for any v) if the model-cores option has been set.
2435 .. warning:: This method is experimental and may change in future
2438 :param v: The term in question.
2439 :return: True if v is a model core symbol.
2441 return self.csolver.isModelCoreSymbol(v.cterm)
2443 def getQuantifierElimination(self, Term term):
2445 Do quantifier elimination.
2449 .. code-block:: smtlib
2453 Requires a logic that supports quantifier elimination.
2454 Currently, the only logics supported by quantifier elimination
2457 .. warning:: This method is experimental and may change in future
2460 :param q: A quantified formula of the form
2461 :math:`Q\\bar{x_1}\\dots Q\\bar{x}_n. P( x_1 \\dots x_i, y_1 \\dots y_j)`
2463 :math:`Q\\bar{x}` is a set of quantified variables of the
2464 form :math:`Q x_1...x_k` and
2465 :math:`P( x_1...x_i, y_1...y_j )` is a quantifier-free
2467 :return: A formula :math:`\\phi` such that, given the current set
2468 of formulas :math:`A` asserted to this solver:
2470 - :math:`(A \\wedge q)` :math:`(A \\wedge \\phi)` are
2472 - :math:`\\phi` is quantifier-free formula containing only
2473 free variables in :math:`y_1...y_n`.
2475 cdef Term result = Term(self)
2476 result.cterm = self.csolver.getQuantifierElimination(term.cterm)
2479 def getQuantifierEliminationDisjunct(self, Term term):
2481 Do partial quantifier elimination, which can be used for
2482 incrementally computing the result of a quantifier elimination.
2486 .. code-block:: smtlib
2488 ( get-qe-disjunct <q> )
2490 Requires a logic that supports quantifier elimination.
2491 Currently, the only logics supported by quantifier elimination
2494 .. warning:: This method is experimental and may change in future
2497 :param q: A quantified formula of the form
2498 :math:`Q\\bar{x_1} ... Q\\bar{x_n}. P( x_1...x_i, y_1...y_j)`
2499 where :math:`Q\\bar{x}` is a set of quantified variables of
2500 the form :math:`Q x_1...x_k` and
2501 :math:`P( x_1...x_i, y_1...y_j )` is a quantifier-free formula.
2503 :return: A formula :math:`\\phi` such that, given the current set
2504 of formulas :math:`A` asserted to this solver:
2506 - :math:`(A \\wedge q \\implies A \\wedge \\phi)` if :math:`Q`
2507 is :math:`\\forall`, and
2508 :math:`(A \\wedge \\phi \\implies A \\wedge q)` if
2509 :math:`Q` is :math:`\\exists`
2510 - :math:`\\phi` is quantifier-free formula containing only
2511 free variables in :math:`y_1...y_n`
2512 - If :math:`Q` is :math:`\\exists`, let :math:`(A \\wedge Q_n)`
2514 :math:`(A \\wedge \\neg (\\phi \wedge Q_1) \\wedge ... \\wedge \\neg (\\phi \\wedge Q_n))`
2515 where for each :math:`i = 1...n`, formula
2516 :math:`(\\phi \\wedge Q_i)` is the result of calling
2517 :py:meth:`getQuantifierEliminationDisjunct()`
2518 for :math:`q` with the set of assertions
2519 :math:`(A \\wedge Q_{i-1})`.
2520 Similarly, if :math:`Q` is :math:`\\forall`, then let
2521 :math:`(A \\wedge Q_n)` be
2522 :math:`(A \\wedge (\\phi \\wedge Q_1) \\wedge ... \\wedge (\\phi \\wedge Q_n))`
2523 where :math:`(\\phi \\wedge Q_i)` is the same as above.
2524 In either case, we have that :math:`(\\phi \\wedge Q_j)`
2525 will eventually be true or false, for some finite :math:`j`.
2527 cdef Term result = Term(self)
2528 result.cterm = self.csolver.getQuantifierEliminationDisjunct(term.cterm)
2531 def getModel(self, sorts, consts):
2541 Requires to enable option
2542 :ref:`produce-models <lbl-option-produce-models>`.
2544 .. warning:: This method is experimental and may change in future
2547 :param sorts: The list of uninterpreted sorts that should be
2548 printed in the model.
2549 :param vars: The list of free constants that should be printed in
2550 the model. A subset of these may be printed based on
2551 :py:meth:`Solver.isModelCoreSymbol()`.
2552 :return: A string representing the model.
2555 cdef vector[c_Sort] csorts
2557 csorts.push_back((<Sort?> sort).csort)
2559 cdef vector[c_Term] cconsts
2560 for const in consts:
2561 cconsts.push_back((<Term?> const).cterm)
2563 return self.csolver.getModel(csorts, cconsts)
2565 def getValueSepHeap(self):
2567 When using separation logic, obtain the term for the heap.
2569 .. warning:: This method is experimental and may change in future
2572 :return: The term for the heap.
2574 cdef Term term = Term(self)
2575 term.cterm = self.csolver.getValueSepHeap()
2578 def getValueSepNil(self):
2580 When using separation logic, obtain the term for nil.
2582 .. warning:: This method is experimental and may change in future
2585 :return: The term for nil.
2587 cdef Term term = Term(self)
2588 term.cterm = self.csolver.getValueSepNil()
2591 def declareSepHeap(self, Sort locType, Sort dataType):
2593 When using separation logic, this sets the location sort and the
2594 datatype sort to the given ones. This method should be invoked
2595 exactly once, before any separation logic constraints are provided.
2597 .. warning:: This method is experimental and may change in future
2600 :param locSort: The location sort of the heap.
2601 :param dataSort: The data sort of the heap.
2603 self.csolver.declareSepHeap(locType.csort, dataType.csort)
2605 def declarePool(self, str symbol, Sort sort, initValue):
2607 Declare a symbolic pool of terms with the given initial value.
2611 .. code-block:: smtlib
2613 ( declare-pool <symbol> <sort> ( <term>* ) )
2615 .. warning:: This method is experimental and may change in future
2618 :param symbol: The name of the pool.
2619 :param sort: The sort of the elements of the pool.
2620 :param initValue: The initial value of the pool.
2622 cdef Term term = Term(self)
2623 cdef vector[c_Term] niv
2625 niv.push_back((<Term?> v).cterm)
2626 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
2629 def pop(self, nscopes=1):
2631 Pop ``nscopes`` level(s) from the assertion stack.
2635 .. code-block:: smtlib
2639 :param nscopes: The number of levels to pop.
2641 self.csolver.pop(nscopes)
2643 def push(self, nscopes=1):
2645 Push ``nscopes`` level(s) to the assertion stack.
2649 .. code-block:: smtlib
2653 :param nscopes: The number of levels to push.
2655 self.csolver.push(nscopes)
2657 def resetAssertions(self):
2659 Remove all assertions.
2663 .. code-block:: smtlib
2665 ( reset-assertions )
2668 self.csolver.resetAssertions()
2670 def setInfo(self, str keyword, str value):
2676 .. code-block:: smtlib
2678 ( set-info <attribute> )
2680 :param keyword: The info flag.
2681 :param value: The value of the info flag.
2683 self.csolver.setInfo(keyword.encode(), value.encode())
2685 def setLogic(self, str logic):
2691 .. code-block:: smtlib
2693 ( set-logic <symbol> )
2695 :param logic: The logic to set.
2697 self.csolver.setLogic(logic.encode())
2699 def setOption(self, str option, str value):
2705 .. code-block:: smtlib
2707 ( set-option <option> )
2709 :param option: The option name.
2710 :param value: The option value.
2712 self.csolver.setOption(option.encode(), value.encode())
2715 def getInterpolant(self, Term conj, *args):
2721 .. code-block:: smtlib
2723 ( get-interpolant <conj> )
2724 ( get-interpolant <conj> <grammar> )
2726 Requires option :ref:`produce-interpolants
2727 <lbl-option-produce-interpolants>` to be set to a mode different
2730 Supports the following variants:
2732 - ``Term getInterpolant(Term conj)``
2733 - ``Term getInterpolant(Term conj, Grammar grammar)``
2735 .. warning:: This method is experimental and may change in future
2738 :param conj: The conjecture term.
2739 :param output: The term where the result will be stored.
2740 :param grammar: A grammar for the inteprolant.
2741 :return: True iff an interpolant was found.
2743 cdef Term result = Term(self)
2745 result.cterm = self.csolver.getInterpolant(conj.cterm)
2747 assert len(args) == 1
2748 assert isinstance(args[0], Grammar)
2749 result.cterm = self.csolver.getInterpolant(
2750 conj.cterm, (<Grammar ?> args[0]).cgrammar)
2754 def getInterpolantNext(self):
2756 Get the next interpolant. Can only be called immediately after
2757 a successful call to :py:func:`Solver.getInterpolant()` or
2758 :py:func:`Solver.getInterpolantNext()`.
2759 Is guaranteed to produce a syntactically different interpolant wrt
2760 the last returned interpolant if successful.
2764 .. code-block:: smtlib
2766 ( get-interpolant-next )
2768 Requires to enable incremental mode, and option
2769 :ref:`produce-interpolants <lbl-option-produce-interpolants>` to be
2770 set to a mode different from ``none``.
2772 .. warning:: This method is experimental and may change in future
2775 :param output: The term where the result will be stored.
2776 :return: True iff an interpolant was found.
2778 cdef Term result = Term(self)
2779 result.cterm = self.csolver.getInterpolantNext()
2782 def getAbduct(self, Term conj, *args):
2788 .. code-block:: smtlib
2790 ( get-abduct <conj> )
2791 ( get-abduct <conj> <grammar> )
2793 Requires to enable option :ref:`produce-abducts
2794 <lbl-option-produce-abducts>`.
2796 Supports the following variants:
2798 - ``Term getAbduct(Term conj)``
2799 - ``Term getAbduct(Term conj, Grammar grammar)``
2801 .. warning:: This method is experimental and may change in future
2804 :param conj: The conjecture term.
2805 :param output: The term where the result will be stored.
2806 :param grammar: A grammar for the abduct.
2807 :return: True iff an abduct was found.
2809 cdef Term result = Term(self)
2811 result.cterm = self.csolver.getAbduct(conj.cterm)
2813 assert len(args) == 1
2814 assert isinstance(args[0], Grammar)
2815 result.cterm = self.csolver.getAbduct(
2816 conj.cterm, (<Grammar ?> args[0]).cgrammar)
2819 def getAbductNext(self):
2821 Get the next abduct. Can only be called immediately after
2822 a succesful call to :py:func:`Solver.getAbduct()` or
2823 :py:func:`Solver.getAbductNext()`.
2824 Is guaranteed to produce a syntactically different abduct wrt the
2825 last returned abduct if successful.
2829 .. code-block:: smtlib
2833 Requires to enable incremental mode, and
2834 option :ref:`produce-abducts <lbl-option-produce-abducts>`.
2836 .. warning:: This method is experimental and may change in future
2839 :param output: The term where the result will be stored.
2840 :return: True iff an abduct was found.
2842 cdef Term result = Term(self)
2843 result.cterm = self.csolver.getAbductNext()
2846 def blockModel(self):
2848 Block the current model. Can be called only if immediately preceded
2849 by a SAT or INVALID query.
2853 .. code-block:: smtlib
2857 Requires enabling option
2858 :ref:`produce-models <lbl-option-produce-models>`
2860 :ref:`block-models <lbl-option-block-models>`
2861 to a mode other than ``none``.
2863 .. warning:: This method is experimental and may change in future
2866 self.csolver.blockModel()
2868 def blockModelValues(self, terms):
2870 Block the current model values of (at least) the values in terms.
2871 Can be called only if immediately preceded by a SAT or NOT_ENTAILED
2876 .. code-block:: smtlib
2878 (block-model-values ( <terms>+ ))
2880 Requires enabling option
2881 :ref:`produce-models <lbl-option-produce-models>`.
2883 .. warning:: This method is experimental and may change in future
2886 cdef vector[c_Term] nts
2888 nts.push_back((<Term?> t).cterm)
2889 self.csolver.blockModelValues(nts)
2891 def getInstantiations(self):
2893 Return a string that contains information about all instantiations
2894 made by the quantifiers module.
2896 .. warning:: This method is experimental and may change in future
2899 return self.csolver.getInstantiations()
2901 def getStatistics(self):
2903 Returns a snapshot of the current state of the statistic values of
2904 this solver. The returned object is completely decoupled from the
2905 solver and will not change when the solver is used again.
2908 res.cstats = self.csolver.getStatistics()
2914 The sort of a cvc5 term.
2916 Wrapper class for :cpp:class:`cvc5::Sort`.
2920 def __cinit__(self, Solver solver):
2921 # csort always set by Solver
2922 self.solver = solver
2924 def __eq__(self, Sort other):
2925 return self.csort == other.csort
2927 def __ne__(self, Sort other):
2928 return self.csort != other.csort
2930 def __lt__(self, Sort other):
2931 return self.csort < other.csort
2933 def __gt__(self, Sort other):
2934 return self.csort > other.csort
2936 def __le__(self, Sort other):
2937 return self.csort <= other.csort
2939 def __ge__(self, Sort other):
2940 return self.csort >= other.csort
2943 return self.csort.toString().decode()
2946 return self.csort.toString().decode()
2949 return csorthash(self.csort)
2951 def hasSymbol(self):
2953 :return: True iff this sort has a symbol.
2955 return self.csort.hasSymbol()
2957 def getSymbol(self):
2959 Asserts :py:meth:`hasSymbol()`.
2961 :return: The raw symbol of the sort.
2963 return self.csort.getSymbol().decode()
2967 :return: True if this Sort is a null sort.
2969 return self.csort.isNull()
2971 def isBoolean(self):
2973 Is this a Boolean sort?
2975 :return: True if the sort is the Boolean sort.
2977 return self.csort.isBoolean()
2979 def isInteger(self):
2981 Is this an integer sort?
2983 :return: True if the sort is the integer sort.
2985 return self.csort.isInteger()
2989 Is this a real sort?
2991 :return: True if the sort is the real sort.
2993 return self.csort.isReal()
2997 Is this a string sort?
2999 :return: True if the sort is the string sort.
3001 return self.csort.isString()
3005 Is this a regexp sort?
3007 :return: True if the sort is the regexp sort.
3009 return self.csort.isRegExp()
3011 def isRoundingMode(self):
3013 Is this a rounding mode sort?
3015 :return: True if the sort is the rounding mode sort.
3017 return self.csort.isRoundingMode()
3019 def isBitVector(self):
3021 Is this a bit-vector sort?
3023 :return: True if the sort is a bit-vector sort.
3025 return self.csort.isBitVector()
3027 def isFloatingPoint(self):
3029 Is this a floating-point sort?
3031 :return: True if the sort is a bit-vector sort.
3033 return self.csort.isFloatingPoint()
3035 def isDatatype(self):
3037 Is this a datatype sort?
3039 :return: True if the sort is a datatype sort.
3041 return self.csort.isDatatype()
3043 def isDatatypeConstructor(self):
3045 Is this a datatype constructor sort?
3047 :return: True if the sort is a datatype constructor sort.
3049 return self.csort.isDatatypeConstructor()
3051 def isDatatypeSelector(self):
3053 Is this a datatype selector sort?
3055 :return: True if the sort is a datatype selector sort.
3057 return self.csort.isDatatypeSelector()
3059 def isDatatypeTester(self):
3061 Is this a tester sort?
3063 :return: True if the sort is a selector sort.
3065 return self.csort.isDatatypeTester()
3067 def isDatatypeUpdater(self):
3069 Is this a datatype updater sort?
3071 :return: True if the sort is a datatype updater sort.
3073 return self.csort.isDatatypeUpdater()
3075 def isFunction(self):
3077 Is this a function sort?
3079 :return: True if the sort is a function sort.
3081 return self.csort.isFunction()
3083 def isPredicate(self):
3085 Is this a predicate sort?
3086 That is, is this a function sort mapping to Boolean? All predicate
3087 sorts are also function sorts.
3089 :return: True if the sort is a predicate sort.
3091 return self.csort.isPredicate()
3095 Is this a tuple sort?
3097 :return: True if the sort is a tuple sort.
3099 return self.csort.isTuple()
3103 Is this a record sort?
3105 .. warning:: This method is experimental and may change in future
3108 :return: True if the sort is a record sort.
3110 return self.csort.isRecord()
3114 Is this an array sort?
3116 :return: True if the sort is an array sort.
3118 return self.csort.isArray()
3124 :return: True if the sort is a set sort.
3126 return self.csort.isSet()
3132 :return: True if the sort is a bag sort.
3134 return self.csort.isBag()
3136 def isSequence(self):
3138 Is this a sequence sort?
3140 :return: True if the sort is a sequence sort.
3142 return self.csort.isSequence()
3144 def isUninterpretedSort(self):
3146 Is this a sort uninterpreted?
3148 :return: True if the sort is uninterpreted.
3150 return self.csort.isUninterpretedSort()
3152 def isUninterpretedSortConstructor(self):
3154 Is this a sort constructor kind?
3156 An uninterpreted sort constructor is an uninterpreted sort with
3159 :return: True if this a sort constructor kind.
3161 return self.csort.isUninterpretedSortConstructor()
3163 def isInstantiated(self):
3165 Is this an instantiated (parametric datatype or uninterpreted sort
3168 An instantiated sort is a sort that has been constructed from
3169 instantiating a sort parameters with sort arguments
3170 (see :py:meth:`instantiate()`).
3172 :return: True if this is an instantiated sort.
3174 return self.csort.isInstantiated()
3176 def getUninterpretedSortConstructor(self):
3178 Get the associated uninterpreted sort constructor of an
3179 instantiated uninterpreted sort.
3181 :return: The uninterpreted sort constructor sort
3183 cdef Sort sort = Sort(self.solver)
3184 sort.csort = self.csort.getUninterpretedSortConstructor()
3187 def getDatatype(self):
3189 :return: The underlying datatype of a datatype sort
3191 cdef Datatype d = Datatype(self.solver)
3192 d.cd = self.csort.getDatatype()
3195 def instantiate(self, params):
3197 Instantiate a parameterized datatype sort or uninterpreted sort
3200 Create sorts parameter with :py:meth:`Solver.mkParamSort()`
3202 .. warning:: This method is experimental and may change in future
3205 :param params: The list of sort parameters to instantiate with
3206 :return: The instantiated sort
3208 cdef Sort sort = Sort(self.solver)
3209 cdef vector[c_Sort] v
3211 v.push_back((<Sort?> s).csort)
3212 sort.csort = self.csort.instantiate(v)
3215 def getInstantiatedParameters(self):
3217 Get the sorts used to instantiate the sort parameters of a
3218 parametric sort (parametric datatype or uninterpreted sort
3219 constructor sort, see :py:meth:`instantiate()`).
3221 :return: The sorts used to instantiate the sort parameters of a
3224 instantiated_sorts = []
3225 for s in self.csort.getInstantiatedParameters():
3226 sort = Sort(self.solver)
3228 instantiated_sorts.append(sort)
3229 return instantiated_sorts
3231 def substitute(self, sort_or_list_1, sort_or_list_2):
3233 Substitution of Sorts.
3235 Note that this replacement is applied during a pre-order traversal
3236 and only once to the sort. It is not run until fix point. In the
3237 case that sort_or_list_1 contains duplicates, the replacement
3238 earliest in the list takes priority.
3241 ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])``
3242 will return ``(Array (Array C D) B)``.
3244 .. warning:: This method is experimental and may change in future
3247 :param sort_or_list_1: The subsort or subsorts to be substituted
3249 :param sort_or_list_2: The sort or list of sorts replacing the
3250 substituted subsort.
3253 # The resulting sort after substitution
3254 cdef Sort sort = Sort(self.solver)
3255 # lists for substitutions
3256 cdef vector[c_Sort] ces
3257 cdef vector[c_Sort] creplacements
3259 # normalize the input parameters to be lists
3260 if isinstance(sort_or_list_1, list):
3261 assert isinstance(sort_or_list_2, list)
3263 replacements = sort_or_list_2
3264 if len(es) != len(replacements):
3265 raise RuntimeError("Expecting list inputs to substitute to "
3266 "have the same length but got: "
3268 len(es), len(replacements)))
3270 for e, r in zip(es, replacements):
3271 ces.push_back((<Sort?> e).csort)
3272 creplacements.push_back((<Sort?> r).csort)
3275 # add the single elements to the vectors
3276 ces.push_back((<Sort?> sort_or_list_1).csort)
3277 creplacements.push_back((<Sort?> sort_or_list_2).csort)
3279 # call the API substitute method with lists
3280 sort.csort = self.csort.substitute(ces, creplacements)
3284 def getDatatypeConstructorArity(self):
3286 :return: The arity of a datatype constructor sort.
3288 return self.csort.getDatatypeConstructorArity()
3290 def getDatatypeConstructorDomainSorts(self):
3292 :return: The domain sorts of a datatype constructor sort.
3295 for s in self.csort.getDatatypeConstructorDomainSorts():
3296 sort = Sort(self.solver)
3298 domain_sorts.append(sort)
3301 def getDatatypeConstructorCodomainSort(self):
3303 :return: The codomain sort of a datatype constructor sort.
3305 cdef Sort sort = Sort(self.solver)
3306 sort.csort = self.csort.getDatatypeConstructorCodomainSort()
3309 def getDatatypeSelectorDomainSort(self):
3311 :return: The domain sort of a datatype selector sort.
3313 cdef Sort sort = Sort(self.solver)
3314 sort.csort = self.csort.getDatatypeSelectorDomainSort()
3317 def getDatatypeSelectorCodomainSort(self):
3319 :return: The codomain sort of a datatype selector sort.
3321 cdef Sort sort = Sort(self.solver)
3322 sort.csort = self.csort.getDatatypeSelectorCodomainSort()
3325 def getDatatypeTesterDomainSort(self):
3327 :return: The domain sort of a datatype tester sort.
3329 cdef Sort sort = Sort(self.solver)
3330 sort.csort = self.csort.getDatatypeTesterDomainSort()
3333 def getDatatypeTesterCodomainSort(self):
3335 :return: the codomain sort of a datatype tester sort, which is the
3338 cdef Sort sort = Sort(self.solver)
3339 sort.csort = self.csort.getDatatypeTesterCodomainSort()
3342 def getFunctionArity(self):
3344 :return: The arity of a function sort.
3346 return self.csort.getFunctionArity()
3348 def getFunctionDomainSorts(self):
3350 :return: The domain sorts of a function sort.
3353 for s in self.csort.getFunctionDomainSorts():
3354 sort = Sort(self.solver)
3356 domain_sorts.append(sort)
3359 def getFunctionCodomainSort(self):
3361 :return: The codomain sort of a function sort.
3363 cdef Sort sort = Sort(self.solver)
3364 sort.csort = self.csort.getFunctionCodomainSort()
3367 def getArrayIndexSort(self):
3369 :return: The array index sort of an array sort.
3371 cdef Sort sort = Sort(self.solver)
3372 sort.csort = self.csort.getArrayIndexSort()
3375 def getArrayElementSort(self):
3377 :return: The array element sort of an array sort.
3379 cdef Sort sort = Sort(self.solver)
3380 sort.csort = self.csort.getArrayElementSort()
3383 def getSetElementSort(self):
3385 :return: The element sort of a set sort.
3387 cdef Sort sort = Sort(self.solver)
3388 sort.csort = self.csort.getSetElementSort()
3391 def getBagElementSort(self):
3393 :return: The element sort of a bag sort.
3395 cdef Sort sort = Sort(self.solver)
3396 sort.csort = self.csort.getBagElementSort()
3399 def getSequenceElementSort(self):
3401 :return: The element sort of a sequence sort.
3403 cdef Sort sort = Sort(self.solver)
3404 sort.csort = self.csort.getSequenceElementSort()
3407 def getUninterpretedSortConstructorArity(self):
3409 :return: The arity of a sort constructor sort.
3411 return self.csort.getUninterpretedSortConstructorArity()
3413 def getBitVectorSize(self):
3415 :return: The bit-width of the bit-vector sort.
3417 return self.csort.getBitVectorSize()
3419 def getFloatingPointExponentSize(self):
3421 :return: The bit-width of the exponent of the floating-point sort.
3423 return self.csort.getFloatingPointExponentSize()
3425 def getFloatingPointSignificandSize(self):
3427 :return: The width of the significand of the floating-point sort.
3429 return self.csort.getFloatingPointSignificandSize()
3431 def getDatatypeArity(self):
3433 :return: The arity of a datatype sort.
3435 return self.csort.getDatatypeArity()
3437 def getTupleLength(self):
3439 :return: The length of a tuple sort.
3441 return self.csort.getTupleLength()
3443 def getTupleSorts(self):
3445 :return: The element sorts of a tuple sort.
3448 for s in self.csort.getTupleSorts():
3449 sort = Sort(self.solver)
3451 tuple_sorts.append(sort)
3455 cdef class Statistics:
3457 The cvc5 Statistics.
3459 Wrapper class for :cpp:class:`cvc5::Statistics`.
3460 Obtain a single statistic value using ``stats["name"]`` and a dictionary
3461 with all (visible) statistics using
3462 ``stats.get(internal=False, defaulted=False)``.
3464 cdef c_Statistics cstats
3466 cdef __stat_to_dict(self, const c_Stat& s):
3473 res = s.getString().decode()
3474 elif s.isHistogram():
3475 res = { h.first.decode(): h.second for h in s.getHistogram() }
3477 'defaulted': s.isDefault(),
3478 'internal': s.isInternal(),
3482 def __getitem__(self, str name):
3484 Get the statistics information for the statistic called ``name``.
3486 return self.__stat_to_dict(self.cstats.get(name.encode()))
3488 def get(self, bint internal = False, bint defaulted = False):
3490 Get all statistics as a dictionary. See :cpp:func:`cvc5::Statistics::begin()`
3491 for more information on which statistics are included based on the parameters.
3493 :return: A dictionary with all available statistics.
3495 cdef c_Statistics.iterator it = self.cstats.begin(internal, defaulted)
3496 cdef pair[string,c_Stat]* s
3498 while it != self.cstats.end():
3499 s = &dereference(it)
3500 res[s.first.decode()] = self.__stat_to_dict(s.second)
3509 Wrapper class for :cpp:class:`cvc5::Term`.
3513 def __cinit__(self, Solver solver):
3514 # cterm always set in the Solver object
3515 self.solver = solver
3517 def __eq__(self, Term other):
3518 return self.cterm == other.cterm
3520 def __ne__(self, Term other):
3521 return self.cterm != other.cterm
3523 def __lt__(self, Term other):
3524 return self.cterm < other.cterm
3526 def __gt__(self, Term other):
3527 return self.cterm > other.cterm
3529 def __le__(self, Term other):
3530 return self.cterm <= other.cterm
3532 def __ge__(self, Term other):
3533 return self.cterm >= other.cterm
3535 def __getitem__(self, int index):
3536 cdef Term term = Term(self.solver)
3538 term.cterm = self.cterm[index]
3540 raise ValueError("Expecting a non-negative integer or string")
3544 return self.cterm.toString().decode()
3547 return self.cterm.toString().decode()
3550 for ci in self.cterm:
3551 term = Term(self.solver)
3556 return ctermhash(self.cterm)
3558 def getNumChildren(self):
3560 :return: The number of children of this term.
3562 return self.cterm.getNumChildren()
3566 :return: The id of this term.
3568 return self.cterm.getId()
3572 :return: The :py:class:`cvc5.Kind` of this term.
3574 return Kind(<int> self.cterm.getKind())
3578 :return: The :py:class:`cvc5.Sort` of this term.
3580 cdef Sort sort = Sort(self.solver)
3581 sort.csort = self.cterm.getSort()
3584 def substitute(self, term_or_list_1, term_or_list_2):
3586 :return: The result of simultaneously replacing the term(s) stored
3587 in ``term_or_list_1`` by the term(s) stored in
3588 ``term_or_list_2`` in this term.
3592 This replacement is applied during a pre-order traversal and
3593 only once to the term. It is not run until fix point. In the
3594 case that terms contains duplicates, the replacement earliest
3595 in the list takes priority. For example, calling substitute on
3600 term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ]
3602 results in the term ``f(g(z),y)``.
3604 # The resulting term after substitution
3605 cdef Term term = Term(self.solver)
3606 # lists for substitutions
3607 cdef vector[c_Term] ces
3608 cdef vector[c_Term] creplacements
3610 # normalize the input parameters to be lists
3611 if isinstance(term_or_list_1, list):
3612 assert isinstance(term_or_list_2, list)
3614 replacements = term_or_list_2
3615 if len(es) != len(replacements):
3616 raise RuntimeError("Expecting list inputs to substitute to "
3617 "have the same length but got: "
3618 "{} and {}".format(len(es), len(replacements)))
3620 for e, r in zip(es, replacements):
3621 ces.push_back((<Term?> e).cterm)
3622 creplacements.push_back((<Term?> r).cterm)
3625 # add the single elements to the vectors
3626 ces.push_back((<Term?> term_or_list_1).cterm)
3627 creplacements.push_back((<Term?> term_or_list_2).cterm)
3629 # call the API substitute method with lists
3630 term.cterm = self.cterm.substitute(ces, creplacements)
3635 :return: True iff this term has an operator.
3637 return self.cterm.hasOp()
3641 :return: The :py:class:`cvc5.Op` used to create this Term.
3645 This is safe to call when :py:meth:`hasOp()` returns True.
3648 cdef Op op = Op(self.solver)
3649 op.cop = self.cterm.getOp()
3652 def hasSymbol(self):
3654 :return: True iff this term has a symbol.
3656 return self.cterm.hasSymbol()
3658 def getSymbol(self):
3660 Asserts :py:meth:`hasSymbol()`.
3662 :return: The raw symbol of the term.
3664 return self.cterm.getSymbol().decode()
3668 :return: True iff this term is a null term.
3670 return self.cterm.isNull()
3676 :return: The Boolean negation of this term.
3678 cdef Term term = Term(self.solver)
3679 term.cterm = self.cterm.notTerm()
3682 def andTerm(self, Term t):
3686 :param t: A Boolean term.
3687 :return: The conjunction of this term and the given term.
3689 cdef Term term = Term(self.solver)
3690 term.cterm = self.cterm.andTerm((<Term> t).cterm)
3693 def orTerm(self, Term t):
3697 :param t: A Boolean term.
3698 :return: The disjunction of this term and the given term.
3700 cdef Term term = Term(self.solver)
3701 term.cterm = self.cterm.orTerm(t.cterm)
3704 def xorTerm(self, Term t):
3706 Boolean exclusive or.
3708 :param t: A Boolean term.
3709 :return: The exclusive disjunction of this term and the given term.
3711 cdef Term term = Term(self.solver)
3712 term.cterm = self.cterm.xorTerm(t.cterm)
3715 def eqTerm(self, Term t):
3719 :param t: A Boolean term.
3720 :return: The Boolean equivalence of this term and the given term.
3722 cdef Term term = Term(self.solver)
3723 term.cterm = self.cterm.eqTerm(t.cterm)
3726 def impTerm(self, Term t):
3728 Boolean Implication.
3730 :param t: A Boolean term.
3731 :return: The implication of this term and the given term.
3733 cdef Term term = Term(self.solver)
3734 term.cterm = self.cterm.impTerm(t.cterm)
3737 def iteTerm(self, Term then_t, Term else_t):
3739 If-then-else with this term as the Boolean condition.
3741 :param then_t: The `then` term.
3742 :param else_t: The `else` term.
3743 :return: The if-then-else term with this term as the Boolean
3746 cdef Term term = Term(self.solver)
3747 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
3750 def isConstArray(self):
3752 :return: True iff this term is a constant array.
3754 return self.cterm.isConstArray()
3756 def getConstArrayBase(self):
3758 Asserts :py:meth:`isConstArray()`.
3760 :return: The base (element stored at all indicies) of this constant
3763 cdef Term term = Term(self.solver)
3764 term.cterm = self.cterm.getConstArrayBase()
3767 def isBooleanValue(self):
3769 :return: True iff this term is a Boolean value.
3771 return self.cterm.isBooleanValue()
3773 def getBooleanValue(self):
3775 Asserts :py:meth:`isBooleanValue()`
3777 :return: The representation of a Boolean value as a native Boolean
3780 return self.cterm.getBooleanValue()
3782 def isStringValue(self):
3784 :return: True iff this term is a string value.
3786 return self.cterm.isStringValue()
3788 def getStringValue(self):
3790 Asserts :py:meth:`isStringValue()`.
3793 This method is not to be confused with :py:meth:`__str__()`
3794 which returns the term in some string representation, whatever
3797 :return: The string term as a native string value.
3799 cdef Py_ssize_t size
3800 cdef c_wstring s = self.cterm.getStringValue()
3801 return PyUnicode_FromWideChar(s.data(), s.size())
3803 def getRealOrIntegerValueSign(self):
3805 Get integer or real value sign. Must be called on integer or real
3806 values, or otherwise an exception is thrown.
3808 :return: 0 if this term is zero, -1 if this term is a negative real
3809 or integer value, 1 if this term is a positive real or
3812 return self.cterm.getRealOrIntegerValueSign()
3814 def isIntegerValue(self):
3816 :return: True iff this term is an integer value.
3818 return self.cterm.isIntegerValue()
3820 def getIntegerValue(self):
3822 Asserts :py:meth:`isIntegerValue()`.
3824 :return: The integer term as a native python integer.
3826 return int(self.cterm.getIntegerValue().decode())
3828 def isFloatingPointPosZero(self):
3830 :return: True iff the term is the floating-point value for positive
3833 return self.cterm.isFloatingPointPosZero()
3835 def isFloatingPointNegZero(self):
3837 :return: True iff the term is the floating-point value for negative
3840 return self.cterm.isFloatingPointNegZero()
3842 def isFloatingPointPosInf(self):
3844 :return: True iff the term is the floating-point value for positive
3847 return self.cterm.isFloatingPointPosInf()
3849 def isFloatingPointNegInf(self):
3851 :return: True iff the term is the floating-point value for negative
3854 return self.cterm.isFloatingPointNegInf()
3856 def isFloatingPointNaN(self):
3858 :return: True iff the term is the floating-point value for not a
3861 return self.cterm.isFloatingPointNaN()
3863 def isFloatingPointValue(self):
3865 :return: True iff this term is a floating-point value.
3867 return self.cterm.isFloatingPointValue()
3869 def getFloatingPointValue(self):
3871 Asserts :py:meth:`isFloatingPointValue()`.
3873 :return: The representation of a floating-point value as a tuple of
3874 the exponent width, the significand width and a bit-vector
3877 cdef c_tuple[uint32_t, uint32_t, c_Term] t = \
3878 self.cterm.getFloatingPointValue()
3879 cdef Term term = Term(self.solver)
3880 term.cterm = get2(t)
3881 return (get0(t), get1(t), term)
3883 def isSetValue(self):
3885 A term is a set value if it is considered to be a (canonical)
3886 constant set value. A canonical set value is one whose AST is:
3891 (set.singleton c1) ...
3892 (set.union (set.singleton c_{n-1}) (set.singleton c_n))))
3894 where :math:`c_1 \dots c_n` are values ordered by id such that
3895 :math:`c_1 > \cdots > c_n`.
3898 A universe set term ``(kind SET_UNIVERSE)`` is not considered
3901 :return: True if the term is a set value.
3903 return self.cterm.isSetValue()
3905 def getSetValue(self):
3907 Asserts :py:meth:`isSetValue()`.
3909 :return: The representation of a set value as a set of terms.
3912 for e in self.cterm.getSetValue():
3913 term = Term(self.solver)
3918 def isSequenceValue(self):
3920 :return: True iff this term is a sequence value.
3922 return self.cterm.isSequenceValue()
3924 def getSequenceValue(self):
3926 Asserts :py:meth:`isSequenceValue()`.
3930 It is usually necessary for sequences to call
3931 :py:meth:`Solver.simplify()` to turn a sequence that is
3932 constructed by, e.g., concatenation of unit sequences, into a
3935 :return: The representation of a sequence value as a vector of
3939 for e in self.cterm.getSequenceValue():
3940 term = Term(self.solver)
3945 def isCardinalityConstraint(self):
3947 :return: True if the term is a cardinality constraint.
3949 .. warning:: This method is experimental and may change in future
3952 return self.cterm.isCardinalityConstraint()
3954 def getCardinalityConstraint(self):
3956 :return: The sort the cardinality constraint is for and its upper
3958 .. warning:: This method is experimental and may change in future
3961 cdef pair[c_Sort, uint32_t] p
3962 p = self.cterm.getCardinalityConstraint()
3963 cdef Sort sort = Sort(self.solver)
3964 sort.csort = p.first
3965 return (sort, p.second)
3968 def isUninterpretedSortValue(self):
3970 :return: True iff this term is a value from an uninterpreted sort.
3972 return self.cterm.isUninterpretedSortValue()
3974 def getUninterpretedSortValue(self):
3976 Asserts :py:meth:`isUninterpretedSortValue()`.
3978 :return: The representation of an uninterpreted value as a pair of
3979 its sort and its index.
3981 return self.cterm.getUninterpretedSortValue()
3983 def isTupleValue(self):
3985 :return: True iff this term is a tuple value.
3987 return self.cterm.isTupleValue()
3989 def isRoundingModeValue(self):
3991 :return: True if the term is a floating-point rounding mode
3994 return self.cterm.isRoundingModeValue()
3996 def getRoundingModeValue(self):
3998 Asserts :py:meth:`isRoundingModeValue()`.
3999 :return: The floating-point rounding mode value held by the term.
4001 return RoundingMode(<int> self.cterm.getRoundingModeValue())
4003 def getTupleValue(self):
4005 Asserts :py:meth:`isTupleValue()`.
4007 :return: The representation of a tuple value as a vector of terms.
4010 for e in self.cterm.getTupleValue():
4011 term = Term(self.solver)
4016 def isRealValue(self):
4018 :return: True iff this term is a rational value.
4022 A term of kind :py:obj:`Pi <cvc5.Kind.Pi>` is not considered
4026 return self.cterm.isRealValue()
4028 def getRealValue(self):
4030 Asserts :py:meth:`isRealValue()`.
4032 :return: The representation of a rational value as a python Fraction.
4034 return Fraction(self.cterm.getRealValue().decode())
4036 def isBitVectorValue(self):
4038 :return: True iff this term is a bit-vector value.
4040 return self.cterm.isBitVectorValue()
4042 def getBitVectorValue(self, base = 2):
4044 Asserts :py:meth:`isBitVectorValue()`.
4045 Supported bases are 2 (bit string), 10 (decimal string) or 16
4046 (hexdecimal string).
4048 :return: The representation of a bit-vector value in string
4051 return self.cterm.getBitVectorValue(base).decode()
4053 def toPythonObj(self):
4055 Converts a constant value Term to a Python object.
4059 - **Boolean:** Returns a Python bool
4060 - **Int :** Returns a Python int
4061 - **Real :** Returns a Python Fraction
4062 - **BV :** Returns a Python int (treats BV as unsigned)
4063 - **String :** Returns a Python Unicode string
4064 - **Array :** Returns a Python dict mapping indices to values. The constant base is returned as the default value.
4068 if self.isBooleanValue():
4069 return self.getBooleanValue()
4070 elif self.isIntegerValue():
4071 return self.getIntegerValue()
4072 elif self.isRealValue():
4073 return self.getRealValue()
4074 elif self.isBitVectorValue():
4075 return int(self.getBitVectorValue(), 2)
4076 elif self.isStringValue():
4077 return self.getStringValue()
4078 elif self.getSort().isArray():
4084 # Array models are represented as a series of store operations
4085 # on a constant array
4088 if t.getKind().value == c_Kind.STORE:
4090 keys.append(t[1].toPythonObj())
4091 values.append(t[2].toPythonObj())
4092 to_visit.append(t[0])
4094 assert t.getKind().value == c_Kind.CONST_ARRAY
4095 base_value = t.getConstArrayBase().toPythonObj()
4097 assert len(keys) == len(values)
4098 assert base_value is not None
4100 # put everything in a dictionary with the constant
4101 # base as the result for any index not included in the stores
4102 res = defaultdict(lambda : base_value)
4103 for k, v in zip(keys, values):