1 from collections import defaultdict, Set
2 from fractions import Fraction
3 from functools import wraps
6 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
7 from libc.stddef cimport wchar_t
9 from libcpp.pair cimport pair
10 from libcpp.set cimport set as c_set
11 from libcpp.string cimport string
12 from libcpp.vector cimport vector
14 from cvc5 cimport cout
15 from cvc5 cimport Datatype as c_Datatype
16 from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
17 from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
18 from cvc5 cimport DatatypeDecl as c_DatatypeDecl
19 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
20 from cvc5 cimport Result as c_Result
21 from cvc5 cimport RoundingMode as c_RoundingMode
22 from cvc5 cimport UnknownExplanation as c_UnknownExplanation
23 from cvc5 cimport Op as c_Op
24 from cvc5 cimport Solver as c_Solver
25 from cvc5 cimport Grammar as c_Grammar
26 from cvc5 cimport Sort as c_Sort
27 from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
28 from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
29 from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
30 from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT
31 from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED
32 from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON
33 from cvc5 cimport OTHER
34 from cvc5 cimport Term as c_Term
35 from cvc5 cimport hash as c_hash
36 from cvc5 cimport wstring as c_wstring
37 from cvc5 cimport tuple as c_tuple
38 from cvc5 cimport get0, get1, get2
39 from cvc5kinds cimport Kind as c_Kind
41 cdef extern from "Python.h":
42 wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
43 object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
44 void PyMem_Free(void*)
46 ################################## DECORATORS #################################
47 def expand_list_arg(num_req_args=0):
49 Creates a decorator that looks at index num_req_args of the args,
50 if it's a list, it expands it before calling the function.
54 def wrapper(owner, *args):
55 if len(args) == num_req_args + 1 and \
56 isinstance(args[num_req_args], list):
57 args = list(args[:num_req_args]) + args[num_req_args]
58 return func(owner, *args)
61 ###############################################################################
64 ### Using PEP-8 spacing recommendations
65 ### Limit linewidth to 79 characters
66 ### Break before binary operators
67 ### surround top level functions and classes with two spaces
68 ### separate methods by one space
69 ### use spaces in functions sparingly to separate logical blocks
70 ### can omit spaces between unrelated oneliners
71 ### always use c++ default arguments
72 #### only use default args of None at python level
74 # References and pointers
75 # The Solver object holds a pointer to a c_Solver.
76 # This is because the assignment operator is deleted in the C++ API for solvers.
77 # Cython has a limitation where you can't stack allocate objects
78 # that have constructors with arguments:
79 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
80 # To get around that you can either have a nullary constructor and assignment
81 # or, use a pointer (which is what we chose).
82 # An additional complication of this is that to free up resources, you must
83 # know when to delete the object.
84 # Python will not follow the same scoping rules as in C++, so it must be
85 # able to reference count. To do this correctly, the solver must be a
86 # reference in the Python class for any class that keeps a pointer to
87 # the solver in C++ (to ensure the solver is not deleted before something
88 # that depends on it).
91 ## Objects for hashing
92 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
93 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
94 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
98 """Wrapper class for :cpp:class:`cvc5::api::Datatype`."""
101 def __cinit__(self, Solver solver):
104 def __getitem__(self, index):
105 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
106 if isinstance(index, int) and index >= 0:
107 dc.cdc = self.cd[(<int?> index)]
108 elif isinstance(index, str):
109 dc.cdc = self.cd[(<const string &> index.encode())]
111 raise ValueError("Expecting a non-negative integer or string")
114 def getConstructor(self, str name):
116 :param name: the name of the constructor.
117 :return: a constructor by name.
119 cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
120 dc.cdc = self.cd.getConstructor(name.encode())
123 def getConstructorTerm(self, str name):
125 :param name: the name of the constructor.
126 :return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`).
128 cdef Term term = Term(self.solver)
129 term.cterm = self.cd.getConstructorTerm(name.encode())
132 def getSelector(self, str name):
134 :param name: the name of the selector..
135 :return: a selector by name.
137 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
138 ds.cds = self.cd.getSelector(name.encode())
143 :return: the name of the datatype.
145 return self.cd.getName().decode()
147 def getNumConstructors(self):
149 :return: number of constructors in this datatype.
151 return self.cd.getNumConstructors()
153 def isParametric(self):
154 """:return: whether this datatype is parametric."""
155 return self.cd.isParametric()
157 def isCodatatype(self):
158 """:return: whether this datatype corresponds to a co-datatype."""
159 return self.cd.isCodatatype()
162 """:return: whether this datatype corresponds to a tuple."""
163 return self.cd.isTuple()
166 """:return: whether this datatype corresponds to a record."""
167 return self.cd.isRecord()
170 """:return: whether this datatype is finite."""
171 return self.cd.isFinite()
173 def isWellFounded(self):
174 """:return: whether this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
175 return self.cd.isWellFounded()
177 def hasNestedRecursion(self):
178 """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
179 return self.cd.hasNestedRecursion()
182 return self.cd.isNull()
185 return self.cd.toString().decode()
188 return self.cd.toString().decode()
192 dc = DatatypeConstructor(self.solver)
197 cdef class DatatypeConstructor:
198 """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`."""
199 cdef c_DatatypeConstructor cdc
201 def __cinit__(self, Solver solver):
202 self.cdc = c_DatatypeConstructor()
205 def __getitem__(self, index):
206 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
207 if isinstance(index, int) and index >= 0:
208 ds.cds = self.cdc[(<int?> index)]
209 elif isinstance(index, str):
210 ds.cds = self.cdc[(<const string &> index.encode())]
212 raise ValueError("Expecting a non-negative integer or string")
217 :return: the name of the constructor.
219 return self.cdc.getName().decode()
221 def getConstructorTerm(self):
223 :return: the constructor operator as a term.
225 cdef Term term = Term(self.solver)
226 term.cterm = self.cdc.getConstructorTerm()
229 def getSpecializedConstructorTerm(self, Sort retSort):
231 Specialized method for parametric datatypes (see :cpp:func:`DatatypeConstructor::getSpecializedConstructorTerm() <cvc5::api::DatatypeConstructor::getSpecializedConstructorTerm>`).
233 :param retSort: the desired return sort of the constructor
234 :return: the constructor operator as a term.
236 cdef Term term = Term(self.solver)
237 term.cterm = self.cdc.getSpecializedConstructorTerm(retSort.csort)
240 def getTesterTerm(self):
242 :return: the tester operator that is related to this constructor, as a term.
244 cdef Term term = Term(self.solver)
245 term.cterm = self.cdc.getTesterTerm()
248 def getNumSelectors(self):
250 :return: the number of selecters (so far) of this Datatype constructor.
252 return self.cdc.getNumSelectors()
254 def getSelector(self, str name):
256 :param name: the name of the datatype selector.
257 :return: the first datatype selector with the given name
259 cdef DatatypeSelector ds = DatatypeSelector(self.solver)
260 ds.cds = self.cdc.getSelector(name.encode())
263 def getSelectorTerm(self, str name):
265 :param name: the name of the datatype selector.
266 :return: a term representing the firstdatatype selector with the given name.
268 cdef Term term = Term(self.solver)
269 term.cterm = self.cdc.getSelectorTerm(name.encode())
273 return self.cdc.isNull()
276 return self.cdc.toString().decode()
279 return self.cdc.toString().decode()
283 ds = DatatypeSelector(self.solver)
288 cdef class DatatypeConstructorDecl:
289 """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`."""
290 cdef c_DatatypeConstructorDecl cddc
293 def __cinit__(self, Solver solver):
296 def addSelector(self, str name, Sort sort):
298 Add datatype selector declaration.
300 :param name: the name of the datatype selector declaration to add.
301 :param sort: the range sort of the datatype selector declaration to add.
303 self.cddc.addSelector(name.encode(), sort.csort)
305 def addSelectorSelf(self, str name):
307 Add datatype selector declaration whose range sort is the datatype itself.
309 :param name: the name of the datatype selector declaration to add.
311 self.cddc.addSelectorSelf(name.encode())
314 return self.cddc.isNull()
317 return self.cddc.toString().decode()
320 return self.cddc.toString().decode()
323 cdef class DatatypeDecl:
324 """Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`."""
325 cdef c_DatatypeDecl cdd
327 def __cinit__(self, Solver solver):
330 def addConstructor(self, DatatypeConstructorDecl ctor):
332 Add a datatype constructor declaration.
334 :param ctor: the datatype constructor declaration to add.
336 self.cdd.addConstructor(ctor.cddc)
338 def getNumConstructors(self):
340 :return: number of constructors (so far) for this datatype declaration.
342 return self.cdd.getNumConstructors()
344 def isParametric(self):
346 :return: is this datatype declaration parametric?
348 return self.cdd.isParametric()
352 :return: the name of this datatype declaration.
354 return self.cdd.getName().decode()
357 return self.cdd.isNull()
360 return self.cdd.toString().decode()
363 return self.cdd.toString().decode()
366 cdef class DatatypeSelector:
367 """Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`."""
368 cdef c_DatatypeSelector cds
370 def __cinit__(self, Solver solver):
371 self.cds = c_DatatypeSelector()
376 :return: the name of this datatype selector.
378 return self.cds.getName().decode()
380 def getSelectorTerm(self):
382 :return: the selector opeartor of this datatype selector as a term.
384 cdef Term term = Term(self.solver)
385 term.cterm = self.cds.getSelectorTerm()
388 def getUpdaterTerm(self):
390 :return: the updater opeartor of this datatype selector as a term.
392 cdef Term term = Term(self.solver)
393 term.cterm = self.cds.getUpdaterTerm()
396 def getRangeSort(self):
398 :return: the range sort of this selector.
400 cdef Sort sort = Sort(self.solver)
401 sort.csort = self.cds.getRangeSort()
405 return self.cds.isNull()
408 return self.cds.toString().decode()
411 return self.cds.toString().decode()
417 def __cinit__(self, Solver solver):
421 def __eq__(self, Op other):
422 return self.cop == other.cop
424 def __ne__(self, Op other):
425 return self.cop != other.cop
428 return self.cop.toString().decode()
431 return self.cop.toString().decode()
434 return cophash(self.cop)
437 return kind(<int> self.cop.getKind())
440 return self.cop.isIndexed()
443 return self.cop.isNull()
445 def getNumIndices(self):
446 return self.cop.getNumIndices()
448 def getIndices(self):
451 indices = self.cop.getIndices[string]().decode()
456 indices = self.cop.getIndices[uint32_t]()
461 indices = self.cop.getIndices[pair[uint32_t, uint32_t]]()
466 raise RuntimeError("Unable to retrieve indices from {}".format(self))
471 cdef c_Grammar cgrammar
473 def __cinit__(self, Solver solver):
475 self.cgrammar = c_Grammar()
477 def addRule(self, Term ntSymbol, Term rule):
478 self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
480 def addAnyConstant(self, Term ntSymbol):
481 self.cgrammar.addAnyConstant(ntSymbol.cterm)
483 def addAnyVariable(self, Term ntSymbol):
484 self.cgrammar.addAnyVariable(ntSymbol.cterm)
486 def addRules(self, Term ntSymbol, rules):
487 cdef vector[c_Term] crules
489 crules.push_back((<Term?> r).cterm)
490 self.cgrammar.addRules(ntSymbol.cterm, crules)
495 # gets populated by solver
499 return self.cr.isNull()
502 return self.cr.isSat()
505 return self.cr.isUnsat()
507 def isSatUnknown(self):
508 return self.cr.isSatUnknown()
510 def isEntailed(self):
511 return self.cr.isEntailed()
513 def isNotEntailed(self):
514 return self.cr.isNotEntailed()
516 def isEntailmentUnknown(self):
517 return self.cr.isEntailmentUnknown()
519 def __eq__(self, Result other):
520 return self.cr == other.cr
522 def __ne__(self, Result other):
523 return self.cr != other.cr
525 def getUnknownExplanation(self):
526 return UnknownExplanation(<int> self.cr.getUnknownExplanation())
529 return self.cr.toString().decode()
532 return self.cr.toString().decode()
535 cdef class RoundingMode:
536 cdef c_RoundingMode crm
538 def __cinit__(self, int rm):
539 # crm always assigned externally
540 self.crm = <c_RoundingMode> rm
541 self.name = __rounding_modes[rm]
543 def __eq__(self, RoundingMode other):
544 return (<int> self.crm) == (<int> other.crm)
546 def __ne__(self, RoundingMode other):
547 return not self.__eq__(other)
550 return hash((<int> self.crm, self.name))
559 cdef class UnknownExplanation:
560 cdef c_UnknownExplanation cue
562 def __cinit__(self, int ue):
563 # crm always assigned externally
564 self.cue = <c_UnknownExplanation> ue
565 self.name = __unknown_explanations[ue]
567 def __eq__(self, UnknownExplanation other):
568 return (<int> self.cue) == (<int> other.cue)
570 def __ne__(self, UnknownExplanation other):
571 return not self.__eq__(other)
574 return hash((<int> self.crm, self.name))
584 """Wrapper class for :cpp:class:`cvc5::api::Solver`."""
585 cdef c_Solver* csolver
588 self.csolver = new c_Solver()
590 def __dealloc__(self):
593 def getBooleanSort(self):
594 """:return: sort Boolean
596 cdef Sort sort = Sort(self)
597 sort.csort = self.csolver.getBooleanSort()
600 def getIntegerSort(self):
601 """:return: sort Integer
603 cdef Sort sort = Sort(self)
604 sort.csort = self.csolver.getIntegerSort()
607 def getNullSort(self):
608 """:return: sort null
610 cdef Sort sort = Sort(self)
611 sort.csort = self.csolver.getNullSort()
614 def getRealSort(self):
615 """:return: sort Real
617 cdef Sort sort = Sort(self)
618 sort.csort = self.csolver.getRealSort()
621 def getRegExpSort(self):
622 """:return: sort of RegExp
624 cdef Sort sort = Sort(self)
625 sort.csort = self.csolver.getRegExpSort()
628 def getRoundingModeSort(self):
629 """:return: sort RoundingMode
631 cdef Sort sort = Sort(self)
632 sort.csort = self.csolver.getRoundingModeSort()
635 def getStringSort(self):
636 """:return: sort String
638 cdef Sort sort = Sort(self)
639 sort.csort = self.csolver.getStringSort()
642 def mkArraySort(self, Sort indexSort, Sort elemSort):
643 """Create an array sort.
645 :param indexSort: the array index sort
646 :param elemSort: the array element sort
647 :return: the array sort
649 cdef Sort sort = Sort(self)
650 sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
653 def mkBitVectorSort(self, uint32_t size):
654 """Create a bit-vector sort.
656 :param size: the bit-width of the bit-vector sort
657 :return: the bit-vector sort
659 cdef Sort sort = Sort(self)
660 sort.csort = self.csolver.mkBitVectorSort(size)
663 def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
664 """Create a floating-point sort.
666 :param exp: the bit-width of the exponent of the floating-point sort.
667 :param sig: the bit-width of the significand of the floating-point sort.
669 cdef Sort sort = Sort(self)
670 sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
673 def mkDatatypeSort(self, DatatypeDecl dtypedecl):
674 """Create a datatype sort.
676 :param dtypedecl: the datatype declaration from which the sort is created
677 :return: the datatype sort
679 cdef Sort sort = Sort(self)
680 sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
683 def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
685 Create a vector of datatype sorts using unresolved sorts. The names of
686 the datatype declarations in dtypedecls must be distinct.
688 This method is called when the DatatypeDecl objects dtypedecls have been
689 built using "unresolved" sorts.
691 We associate each sort in unresolvedSorts with exacly one datatype from
692 dtypedecls. In particular, it must have the same name as exactly one
693 datatype declaration in dtypedecls.
695 When constructing datatypes, unresolved sorts are replaced by the datatype
696 sort constructed for the datatype declaration it is associated with.
698 :param dtypedecls: the datatype declarations from which the sort is created
699 :param unresolvedSorts: the list of unresolved sorts
700 :return: the datatype sorts
702 if unresolvedSorts == None:
703 unresolvedSorts = set([])
705 assert isinstance(unresolvedSorts, Set)
708 cdef vector[c_DatatypeDecl] decls
709 for decl in dtypedecls:
710 decls.push_back((<DatatypeDecl?> decl).cdd)
712 cdef c_set[c_Sort] usorts
713 for usort in unresolvedSorts:
714 usorts.insert((<Sort?> usort).csort)
716 csorts = self.csolver.mkDatatypeSorts(
717 <const vector[c_DatatypeDecl]&> decls, <const c_set[c_Sort]&> usorts)
725 def mkFunctionSort(self, sorts, Sort codomain):
726 """ Create function sort.
728 :param sorts: the sort of the function arguments
729 :param codomain: the sort of the function return value
730 :return: the function sort
733 cdef Sort sort = Sort(self)
734 # populate a vector with dereferenced c_Sorts
735 cdef vector[c_Sort] v
737 if isinstance(sorts, Sort):
738 sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
740 elif isinstance(sorts, list):
742 v.push_back((<Sort?>s).csort)
744 sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
748 def mkParamSort(self, symbolname):
749 """ Create a sort parameter.
751 :param symbol: the name of the sort
752 :return: the sort parameter
754 cdef Sort sort = Sort(self)
755 sort.csort = self.csolver.mkParamSort(symbolname.encode())
758 @expand_list_arg(num_req_args=0)
759 def mkPredicateSort(self, *sorts):
760 """Create a predicate sort.
762 :param sorts: the list of sorts of the predicate, as a list or as distinct arguments.
763 :return: the predicate sort
765 cdef Sort sort = Sort(self)
766 cdef vector[c_Sort] v
768 v.push_back((<Sort?> s).csort)
769 sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
772 @expand_list_arg(num_req_args=0)
773 def mkRecordSort(self, *fields):
774 """Create a record sort
776 :param fields: the list of fields of the record, as a list or as distinct arguments
777 :return: the record sort
779 cdef Sort sort = Sort(self)
780 cdef vector[pair[string, c_Sort]] v
781 cdef pair[string, c_Sort] p
785 p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
787 sort.csort = self.csolver.mkRecordSort(
788 <const vector[pair[string, c_Sort]] &> v)
791 def mkSetSort(self, Sort elemSort):
792 """Create a set sort.
794 :param elemSort: the sort of the set elements
795 :return: the set sort
797 cdef Sort sort = Sort(self)
798 sort.csort = self.csolver.mkSetSort(elemSort.csort)
801 def mkBagSort(self, Sort elemSort):
802 """Create a bag sort.
804 :param elemSort: the sort of the bag elements
805 :return: the bag sort
807 cdef Sort sort = Sort(self)
808 sort.csort = self.csolver.mkBagSort(elemSort.csort)
811 def mkSequenceSort(self, Sort elemSort):
812 """Create a sequence sort.
814 :param elemSort: the sort of the sequence elements
815 :return: the sequence sort
817 cdef Sort sort = Sort(self)
818 sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
821 def mkUninterpretedSort(self, str name):
822 """Create an uninterpreted sort.
824 :param symbol: the name of the sort
825 :return: the uninterpreted sort
827 cdef Sort sort = Sort(self)
828 sort.csort = self.csolver.mkUninterpretedSort(name.encode())
831 def mkSortConstructorSort(self, str symbol, size_t arity):
832 """Create a sort constructor sort.
834 :param symbol: the symbol of the sort
835 :param arity: the arity of the sort
836 :return: the sort constructor sort
838 cdef Sort sort = Sort(self)
839 sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
842 @expand_list_arg(num_req_args=0)
843 def mkTupleSort(self, *sorts):
844 """Create a tuple sort.
846 :param sorts: of the elements of the tuple, as a list or as distinct arguments
847 :return: the tuple sort
849 cdef Sort sort = Sort(self)
850 cdef vector[c_Sort] v
852 v.push_back((<Sort?> s).csort)
853 sort.csort = self.csolver.mkTupleSort(v)
856 @expand_list_arg(num_req_args=1)
857 def mkTerm(self, kind_or_op, *args):
859 Supports the following arguments:
861 - ``Term mkTerm(Kind kind)``
862 - ``Term mkTerm(Kind kind, Op child1, List[Term] children)``
863 - ``Term mkTerm(Kind kind, List[Term] children)``
865 where ``List[Term]`` can also be comma-separated arguments
867 cdef Term term = Term(self)
868 cdef vector[c_Term] v
871 if isinstance(kind_or_op, kind):
872 op = self.mkOp(kind_or_op)
875 term.cterm = self.csolver.mkTerm((<Op?> op).cop)
878 v.push_back((<Term?> a).cterm)
879 term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
882 def mkTuple(self, sorts, terms):
883 """Create a tuple term. Terms are automatically converted if sorts are compatible.
885 :param sorts: The sorts of the elements in the tuple
886 :param terms: The elements in the tuple
887 :return: the tuple Term
889 cdef vector[c_Sort] csorts
890 cdef vector[c_Term] cterms
893 csorts.push_back((<Sort?> s).csort)
895 cterms.push_back((<Term?> s).cterm)
896 cdef Term result = Term(self)
897 result.cterm = self.csolver.mkTuple(csorts, cterms)
900 @expand_list_arg(num_req_args=0)
901 def mkOp(self, kind k, *args):
903 Supports the following uses:
905 - ``Op mkOp(Kind kind)``
906 - ``Op mkOp(Kind kind, Kind k)``
907 - ``Op mkOp(Kind kind, const string& arg)``
908 - ``Op mkOp(Kind kind, uint32_t arg)``
909 - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
911 cdef Op op = Op(self)
915 op.cop = self.csolver.mkOp(k.k)
917 if isinstance(args[0], str):
918 op.cop = self.csolver.mkOp(k.k,
921 elif isinstance(args[0], int):
922 op.cop = self.csolver.mkOp(k.k, <int?> args[0])
923 elif isinstance(args[0], list):
925 v.push_back((<int?> a))
926 op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v)
928 raise ValueError("Unsupported signature"
929 " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
931 if isinstance(args[0], int) and isinstance(args[1], int):
932 op.cop = self.csolver.mkOp(k.k, <int> args[0], <int> args[1])
934 raise ValueError("Unsupported signature"
935 " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
939 """Create a Boolean true constant.
941 :return: the true constant
943 cdef Term term = Term(self)
944 term.cterm = self.csolver.mkTrue()
948 """Create a Boolean false constant.
950 :return: the false constant
952 cdef Term term = Term(self)
953 term.cterm = self.csolver.mkFalse()
956 def mkBoolean(self, bint val):
957 """Create a Boolean constant.
959 :return: the Boolean constant
960 :param val: the value of the constant
962 cdef Term term = Term(self)
963 term.cterm = self.csolver.mkBoolean(val)
967 """Create a constant representing the number Pi.
969 :return: a constant representing Pi
971 cdef Term term = Term(self)
972 term.cterm = self.csolver.mkPi()
975 def mkInteger(self, val):
976 """Create an integer constant.
978 :param val: representation of the constant: either a string or integer
979 :return: a constant of sort Integer
981 cdef Term term = Term(self)
982 if isinstance(val, str):
983 term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
985 assert(isinstance(val, int))
986 term.cterm = self.csolver.mkInteger((<int?> val))
989 def mkReal(self, val, den=None):
990 """Create a real constant.
992 :param: `val` the value of the term. Can be an integer, float, or string. It will be formatted as a string before the term is built.
993 :param: `den` if not None, the value is `val`/`den`
994 :return: a real term with literal value
996 Can be used in various forms:
998 - Given a string ``"N/D"`` constructs the corresponding rational.
999 - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10.
1000 - Given a float ``f``, constructs the rational matching ``f``'s string representation. This means that ``mkReal(0.3)`` gives ``3/10`` and not the IEEE-754 approximation of ``3/10``.
1001 - Given a string ``"W"`` or an integer, constructs that integer.
1002 - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``.
1004 cdef Term term = Term(self)
1006 term.cterm = self.csolver.mkReal(str(val).encode())
1008 if not isinstance(val, int) or not isinstance(den, int):
1009 raise ValueError("Expecting integers when"
1010 " constructing a rational"
1011 " but got: {}".format((val, den)))
1012 term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
1015 def mkRegexpEmpty(self):
1016 """Create a regular expression empty term.
1018 :return: the empty term
1020 cdef Term term = Term(self)
1021 term.cterm = self.csolver.mkRegexpEmpty()
1024 def mkRegexpSigma(self):
1025 """Create a regular expression sigma term.
1027 :return: the sigma term
1029 cdef Term term = Term(self)
1030 term.cterm = self.csolver.mkRegexpSigma()
1033 def mkEmptySet(self, Sort s):
1034 """Create a constant representing an empty set of the given sort.
1036 :param sort: the sort of the set elements.
1037 :return: the empty set constant
1039 cdef Term term = Term(self)
1040 term.cterm = self.csolver.mkEmptySet(s.csort)
1043 def mkEmptyBag(self, Sort s):
1044 """Create a constant representing an empty bag of the given sort.
1046 :param sort: the sort of the bag elements.
1047 :return: the empty bag constant
1049 cdef Term term = Term(self)
1050 term.cterm = self.csolver.mkEmptyBag(s.csort)
1053 def mkSepNil(self, Sort sort):
1054 """Create a separation logic nil term.
1056 :param sort: the sort of the nil term
1057 :return: the separation logic nil term
1059 cdef Term term = Term(self)
1060 term.cterm = self.csolver.mkSepNil(sort.csort)
1063 def mkString(self, str s, useEscSequences = None):
1065 Create a String constant from a `str` which may contain SMT-LIB
1066 compatible escape sequences like ``\\u1234`` to encode unicode characters.
1068 :param s: the string this constant represents
1069 :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character
1070 :return: the String constant
1072 cdef Term term = Term(self)
1073 cdef Py_ssize_t size
1074 cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
1075 if isinstance(useEscSequences, bool):
1076 term.cterm = self.csolver.mkString(
1077 s.encode(), <bint> useEscSequences)
1079 term.cterm = self.csolver.mkString(c_wstring(tmp, size))
1083 def mkEmptySequence(self, Sort sort):
1084 """Create an empty sequence of the given element sort.
1086 :param sort: The element sort of the sequence.
1087 :return: the empty sequence with given element sort.
1089 cdef Term term = Term(self)
1090 term.cterm = self.csolver.mkEmptySequence(sort.csort)
1093 def mkUniverseSet(self, Sort sort):
1094 """Create a universe set of the given sort.
1096 :param sort: the sort of the set elements
1097 :return: the universe set constant
1099 cdef Term term = Term(self)
1100 term.cterm = self.csolver.mkUniverseSet(sort.csort)
1103 @expand_list_arg(num_req_args=0)
1104 def mkBitVector(self, *args):
1106 Supports the following arguments:
1108 - ``Term mkBitVector(int size, int val=0)``
1109 - ``Term mkBitVector(int size, string val, int base)``
1111 :return: a bit-vector literal term
1112 :param: `size` an integer size.
1113 :param: `val` an integer representating the value, in the first form. In the second form, a string representing the value.
1114 :param: `base` the base of the string representation (second form only)
1116 cdef Term term = Term(self)
1118 raise ValueError("Missing arguments to mkBitVector")
1120 if not isinstance(size, int):
1122 "Invalid first argument to mkBitVector '{}', "
1123 "expected bit-vector size".format(size))
1125 term.cterm = self.csolver.mkBitVector(<uint32_t> size)
1126 elif len(args) == 2:
1128 if not isinstance(val, int):
1130 "Invalid second argument to mkBitVector '{}', "
1131 "expected integer value".format(size))
1132 term.cterm = self.csolver.mkBitVector(
1133 <uint32_t> size, <uint32_t> val)
1134 elif len(args) == 3:
1137 if not isinstance(val, str):
1139 "Invalid second argument to mkBitVector '{}', "
1140 "expected value string".format(size))
1141 if not isinstance(base, int):
1143 "Invalid third argument to mkBitVector '{}', "
1144 "expected base given as integer".format(size))
1145 term.cterm = self.csolver.mkBitVector(
1147 <const string&> str(val).encode(),
1150 raise ValueError("Unexpected inputs to mkBitVector")
1153 def mkConstArray(self, Sort sort, Term val):
1155 Create a constant array with the provided constant value stored at every
1158 :param sort: the sort of the constant array (must be an array sort)
1159 :param val: the constant value to store (must match the sort's element sort)
1160 :return: the constant array term
1162 cdef Term term = Term(self)
1163 term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
1166 def mkPosInf(self, int exp, int sig):
1167 """Create a positive infinity floating-point constant.
1169 :param exp: Number of bits in the exponent
1170 :param sig: Number of bits in the significand
1171 :return: the floating-point constant
1173 cdef Term term = Term(self)
1174 term.cterm = self.csolver.mkPosInf(exp, sig)
1177 def mkNegInf(self, int exp, int sig):
1178 """Create a negative infinity floating-point constant.
1180 :param exp: Number of bits in the exponent
1181 :param sig: Number of bits in the significand
1182 :return: the floating-point constant
1184 cdef Term term = Term(self)
1185 term.cterm = self.csolver.mkNegInf(exp, sig)
1188 def mkNaN(self, int exp, int sig):
1189 """Create a not-a-number (NaN) floating-point constant.
1191 :param exp: Number of bits in the exponent
1192 :param sig: Number of bits in the significand
1193 :return: the floating-point constant
1195 cdef Term term = Term(self)
1196 term.cterm = self.csolver.mkNaN(exp, sig)
1199 def mkPosZero(self, int exp, int sig):
1200 """Create a positive zero (+0.0) floating-point constant.
1202 :param exp: Number of bits in the exponent
1203 :param sig: Number of bits in the significand
1204 :return: the floating-point constant
1206 cdef Term term = Term(self)
1207 term.cterm = self.csolver.mkPosZero(exp, sig)
1210 def mkNegZero(self, int exp, int sig):
1211 """Create a negative zero (+0.0) floating-point constant.
1213 :param exp: Number of bits in the exponent
1214 :param sig: Number of bits in the significand
1215 :return: the floating-point constant
1217 cdef Term term = Term(self)
1218 term.cterm = self.csolver.mkNegZero(exp, sig)
1221 def mkRoundingMode(self, RoundingMode rm):
1222 """Create a roundingmode constant.
1224 :param rm: the floating point rounding mode this constant represents
1226 cdef Term term = Term(self)
1227 term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
1230 def mkUninterpretedConst(self, Sort sort, int index):
1231 """Create uninterpreted constant.
1233 :param sort: Sort of the constant
1234 :param index: Index of the constant
1236 cdef Term term = Term(self)
1237 term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index)
1240 def mkAbstractValue(self, index):
1242 Create an abstract value constant.
1243 The given index needs to be positive.
1245 :param index: Index of the abstract value
1247 cdef Term term = Term(self)
1249 term.cterm = self.csolver.mkAbstractValue(str(index).encode())
1252 "mkAbstractValue expects a str representing a number"
1253 " or an int, but got{}".format(index))
1256 def mkFloatingPoint(self, int exp, int sig, Term val):
1257 """Create a floating-point constant.
1259 :param exp: Size of the exponent
1260 :param sig: Size of the significand
1261 :param val: Value of the floating-point constant as a bit-vector term
1263 cdef Term term = Term(self)
1264 term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
1267 def mkConst(self, Sort sort, symbol=None):
1269 Create (first-order) constant (0-arity function symbol).
1273 .. code-block:: smtlib
1275 ( declare-const <symbol> <sort> )
1276 ( declare-fun <symbol> ( ) <sort> )
1278 :param sort: the sort of the constant
1279 :param symbol: the name of the constant. If None, a default symbol is used.
1280 :return: the first-order constant
1282 cdef Term term = Term(self)
1284 term.cterm = self.csolver.mkConst(sort.csort)
1286 term.cterm = self.csolver.mkConst(sort.csort,
1287 (<str?> symbol).encode())
1290 def mkVar(self, Sort sort, symbol=None):
1292 Create a bound variable to be used in a binder (i.e. a quantifier, a
1293 lambda, or a witness binder).
1295 :param sort: the sort of the variable
1296 :param symbol: the name of the variable
1297 :return: the variable
1299 cdef Term term = Term(self)
1301 term.cterm = self.csolver.mkVar(sort.csort)
1303 term.cterm = self.csolver.mkVar(sort.csort,
1304 (<str?> symbol).encode())
1307 def mkDatatypeConstructorDecl(self, str name):
1309 :return: a datatype constructor declaration
1310 :param: `name` the constructor's name
1312 cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
1313 ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
1316 def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
1317 """Create a datatype declaration.
1319 :param name: the name of the datatype
1320 :param isCoDatatype: true if a codatatype is to be constructed
1321 :return: the DatatypeDecl
1323 cdef DatatypeDecl dd = DatatypeDecl(self)
1324 cdef vector[c_Sort] v
1327 if sorts_or_bool is None and isCoDatatype is None:
1328 dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
1329 elif sorts_or_bool is not None and isCoDatatype is None:
1330 if isinstance(sorts_or_bool, bool):
1331 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1332 <bint> sorts_or_bool)
1333 elif isinstance(sorts_or_bool, Sort):
1334 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1335 (<Sort> sorts_or_bool).csort)
1336 elif isinstance(sorts_or_bool, list):
1337 for s in sorts_or_bool:
1338 v.push_back((<Sort?> s).csort)
1339 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1340 <const vector[c_Sort]&> v)
1342 raise ValueError("Unhandled second argument type {}"
1343 .format(type(sorts_or_bool)))
1344 elif sorts_or_bool is not None and isCoDatatype is not None:
1345 if isinstance(sorts_or_bool, Sort):
1346 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1347 (<Sort> sorts_or_bool).csort,
1348 <bint> isCoDatatype)
1349 elif isinstance(sorts_or_bool, list):
1350 for s in sorts_or_bool:
1351 v.push_back((<Sort?> s).csort)
1352 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
1353 <const vector[c_Sort]&> v,
1354 <bint> isCoDatatype)
1356 raise ValueError("Unhandled second argument type {}"
1357 .format(type(sorts_or_bool)))
1359 raise ValueError("Can't create DatatypeDecl with {}".format([type(a)
1366 def simplify(self, Term t):
1368 Simplify a formula without doing "much" work. Does not involve the
1369 SAT Engine in the simplification, but uses the current definitions,
1370 assertions, and the current partial model, if one has been constructed.
1371 It also involves theory normalization.
1373 :param t: the formula to simplify
1374 :return: the simplified formula
1376 cdef Term term = Term(self)
1377 term.cterm = self.csolver.simplify(t.cterm)
1380 def assertFormula(self, Term term):
1381 """ Assert a formula
1385 .. code-block:: smtlib
1389 :param term: the formula to assert
1391 self.csolver.assertFormula(term.cterm)
1395 Check satisfiability.
1399 .. code-block:: smtlib
1403 :return: the result of the satisfiability check.
1405 cdef Result r = Result()
1406 r.cr = self.csolver.checkSat()
1409 def mkSygusGrammar(self, boundVars, ntSymbols):
1411 Create a SyGuS grammar. The first non-terminal is treated as the
1412 starting non-terminal, so the order of non-terminals matters.
1414 :param boundVars: the parameters to corresponding synth-fun/synth-inv
1415 :param ntSymbols: the pre-declaration of the non-terminal symbols
1416 :return: the grammar
1418 cdef Grammar grammar = Grammar(self)
1419 cdef vector[c_Term] bvc
1420 cdef vector[c_Term] ntc
1421 for bv in boundVars:
1422 bvc.push_back((<Term?> bv).cterm)
1423 for nt in ntSymbols:
1424 ntc.push_back((<Term?> nt).cterm)
1425 grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
1428 def mkSygusVar(self, Sort sort, str symbol=""):
1429 """Append symbol to the current list of universal variables.
1433 .. code-block:: smtlib
1435 ( declare-var <symbol> <sort> )
1437 :param sort: the sort of the universal variable
1438 :param symbol: the name of the universal variable
1439 :return: the universal variable
1441 cdef Term term = Term(self)
1442 term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode())
1445 def addSygusConstraint(self, Term t):
1447 Add a formula to the set of SyGuS constraints.
1451 .. code-block:: smtlib
1453 ( constraint <term> )
1455 :param term: the formula to add as a constraint
1457 self.csolver.addSygusConstraint(t.cterm)
1459 def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
1461 Add a set of SyGuS constraints to the current state that correspond to an
1462 invariant synthesis problem.
1466 .. code-block:: smtlib
1468 ( inv-constraint <inv> <pre> <trans> <post> )
1470 :param inv: the function-to-synthesize
1471 :param pre: the pre-condition
1472 :param trans: the transition relation
1473 :param post: the post-condition
1475 self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
1477 def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
1479 Synthesize n-ary function following specified syntactic constraints.
1483 .. code-block:: smtlib
1485 ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
1487 :param symbol: the name of the function
1488 :param boundVars: the parameters to this function
1489 :param sort: the sort of the return value of this function
1490 :param grammar: the syntactic constraints
1491 :return: the function
1493 cdef Term term = Term(self)
1494 cdef vector[c_Term] v
1495 for bv in bound_vars:
1496 v.push_back((<Term?> bv).cterm)
1498 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
1500 term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
1503 def checkSynth(self):
1505 Try to find a solution for the synthesis conjecture corresponding to the
1506 current list of functions-to-synthesize, universal variables and
1511 .. code-block:: smtlib
1515 :return: the result of the synthesis conjecture.
1517 cdef Result r = Result()
1518 r.cr = self.csolver.checkSynth()
1521 def getSynthSolution(self, Term term):
1523 Get the synthesis solution of the given term. This method should be
1524 called immediately after the solver answers unsat for sygus input.
1526 :param term: the term for which the synthesis solution is queried
1527 :return: the synthesis solution of the given term
1529 cdef Term t = Term(self)
1530 t.cterm = self.csolver.getSynthSolution(term.cterm)
1533 def getSynthSolutions(self, list terms):
1535 Get the synthesis solutions of the given terms. This method should be
1536 called immediately after the solver answers unsat for sygus input.
1538 :param terms: the terms for which the synthesis solutions is queried
1539 :return: the synthesis solutions of the given terms
1542 cdef vector[c_Term] vec
1544 vec.push_back((<Term?> t).cterm)
1545 cresult = self.csolver.getSynthSolutions(vec)
1553 def synthInv(self, symbol, bound_vars, Grammar grammar=None):
1555 Synthesize invariant.
1559 .. code-block:: smtlib
1561 ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
1563 :param symbol: the name of the invariant
1564 :param boundVars: the parameters to this invariant
1565 :param grammar: the syntactic constraints
1566 :return: the invariant
1568 cdef Term term = Term(self)
1569 cdef vector[c_Term] v
1570 for bv in bound_vars:
1571 v.push_back((<Term?> bv).cterm)
1573 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
1575 term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
1578 @expand_list_arg(num_req_args=0)
1579 def checkSatAssuming(self, *assumptions):
1580 """ Check satisfiability assuming the given formula.
1584 .. code-block:: smtlib
1586 ( check-sat-assuming ( <prop_literal> ) )
1588 :param assumptions: the formulas to assume, as a list or as distinct arguments
1589 :return: the result of the satisfiability check.
1591 cdef Result r = Result()
1592 # used if assumptions is a list of terms
1593 cdef vector[c_Term] v
1594 for a in assumptions:
1595 v.push_back((<Term?> a).cterm)
1596 r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
1599 @expand_list_arg(num_req_args=0)
1600 def checkEntailed(self, *assumptions):
1601 """Check entailment of the given formula w.r.t. the current set of assertions.
1603 :param terms: the formulas to check entailment for, as a list or as distinct arguments
1604 :return: the result of the entailment check.
1606 cdef Result r = Result()
1607 # used if assumptions is a list of terms
1608 cdef vector[c_Term] v
1609 for a in assumptions:
1610 v.push_back((<Term?> a).cterm)
1611 r.cr = self.csolver.checkEntailed(<const vector[c_Term]&> v)
1614 @expand_list_arg(num_req_args=1)
1615 def declareDatatype(self, str symbol, *ctors):
1617 Create datatype sort.
1621 .. code-block:: smtlib
1623 ( declare-datatype <symbol> <datatype_decl> )
1625 :param symbol: the name of the datatype sort
1626 :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
1627 :return: the datatype sort
1629 cdef Sort sort = Sort(self)
1630 cdef vector[c_DatatypeConstructorDecl] v
1633 v.push_back((<DatatypeConstructorDecl?> c).cddc)
1634 sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1637 def declareFun(self, str symbol, list sorts, Sort sort):
1638 """Declare n-ary function symbol.
1642 .. code-block:: smtlib
1644 ( declare-fun <symbol> ( <sort>* ) <sort> )
1646 :param symbol: the name of the function
1647 :param sorts: the sorts of the parameters to this function
1648 :param sort: the sort of the return value of this function
1649 :return: the function
1651 cdef Term term = Term(self)
1652 cdef vector[c_Sort] v
1654 v.push_back((<Sort?> s).csort)
1655 term.cterm = self.csolver.declareFun(symbol.encode(),
1656 <const vector[c_Sort]&> v,
1660 def declareSort(self, str symbol, int arity):
1661 """Declare uninterpreted sort.
1665 .. code-block:: smtlib
1667 ( declare-sort <symbol> <numeral> )
1669 :param symbol: the name of the sort
1670 :param arity: the arity of the sort
1673 cdef Sort sort = Sort(self)
1674 sort.csort = self.csolver.declareSort(symbol.encode(), arity)
1677 def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1679 Define n-ary function.
1682 - ``Term defineFun(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1683 - ``Term defineFun(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1688 .. code-block:: smtlib
1690 ( define-fun <function_def> )
1692 :param symbol: the name of the function
1693 :param bound_vars: the parameters to this function
1694 :param sort: the sort of the return value of this function
1695 :param term: the function body
1696 :param global: determines whether this definition is global (i.e. persists when popping the context)
1697 :return: the function
1699 cdef Term term = Term(self)
1700 cdef vector[c_Term] v
1701 for bv in bound_vars:
1702 v.push_back((<Term?> bv).cterm)
1705 term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(),
1706 <const vector[c_Term] &> v,
1707 (<Sort?> sort_or_term).csort,
1711 term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm,
1712 <const vector[c_Term]&> v,
1713 (<Term?> sort_or_term).cterm,
1718 def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1719 """Define recursive functions.
1723 - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
1724 - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
1729 .. code-block:: smtlib
1731 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1733 Create elements of parameter ``funs`` with mkConst().
1735 :param funs: the sorted functions
1736 :param bound_vars: the list of parameters to the functions
1737 :param terms: the list of function bodies of the functions
1738 :param global: determines whether this definition is global (i.e. persists when popping the context)
1739 :return: the function
1741 cdef Term term = Term(self)
1742 cdef vector[c_Term] v
1743 for bv in bound_vars:
1744 v.push_back((<Term?> bv).cterm)
1747 term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
1748 <const vector[c_Term] &> v,
1749 (<Sort?> sort_or_term).csort,
1753 term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
1754 <const vector[c_Term]&> v,
1755 (<Term?> sort_or_term).cterm,
1760 def defineFunsRec(self, funs, bound_vars, terms):
1761 """Define recursive functions.
1765 .. code-block:: smtlib
1767 ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
1769 Create elements of parameter ``funs`` with mkConst().
1771 :param funs: the sorted functions
1772 :param bound_vars: the list of parameters to the functions
1773 :param terms: the list of function bodies of the functions
1774 :param global: determines whether this definition is global (i.e. persists when popping the context)
1775 :return: the function
1777 cdef vector[c_Term] vf
1778 cdef vector[vector[c_Term]] vbv
1779 cdef vector[c_Term] vt
1782 vf.push_back((<Term?> f).cterm)
1784 cdef vector[c_Term] temp
1785 for v in bound_vars:
1787 temp.push_back((<Term?> t).cterm)
1792 vf.push_back((<Term?> t).cterm)
1794 def getAssertions(self):
1795 """Get the list of asserted formulas.
1799 .. code-block:: smtlib
1803 :return: the list of asserted formulas
1806 for a in self.csolver.getAssertions():
1809 assertions.append(term)
1812 def getInfo(self, str flag):
1813 """Get info from the solver.
1817 .. code-block:: smtlib
1819 ( get-info <info_flag> )
1821 :param flag: the info flag
1824 return self.csolver.getInfo(flag.encode())
1826 def getOption(self, str option):
1827 """Get the value of a given option.
1831 .. code-block:: smtlib
1833 ( get-option <keyword> )
1835 :param option: the option for which the value is queried
1836 :return: a string representation of the option value
1838 return self.csolver.getOption(option.encode())
1840 def getUnsatAssumptions(self):
1842 Get the set of unsat ("failed") assumptions.
1846 .. code-block:: smtlib
1848 ( get-unsat-assumptions )
1850 Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
1852 :return: the set of unsat assumptions.
1855 for a in self.csolver.getUnsatAssumptions():
1858 assumptions.append(term)
1861 def getUnsatCore(self):
1862 """Get the unsatisfiable core.
1866 .. code-block:: smtlib
1870 Requires to enable option :ref:`produce-unsat-cores <lbl-produce-unsat-cores>`.
1872 :return: a set of terms representing the unsatisfiable core
1875 for a in self.csolver.getUnsatCore():
1881 def getValue(self, Term t):
1882 """Get the value of the given term in the current model.
1886 .. code-block:: smtlib
1888 ( get-value ( <term> ) )
1890 :param term: the term for which the value is queried
1891 :return: the value of the given term
1893 cdef Term term = Term(self)
1894 term.cterm = self.csolver.getValue(t.cterm)
1897 def getModelDomainElements(self, Sort s):
1899 Get the domain elements of uninterpreted sort s in the current model. The
1900 current model interprets s as the finite sort whose domain elements are
1901 given in the return value of this method.
1903 :param s: The uninterpreted sort in question
1904 :return: the domain elements of s in the current model
1907 cresult = self.csolver.getModelDomainElements(s.csort)
1914 def isModelCoreSymbol(self, Term v):
1916 This returns false if the model value of free constant v was not
1917 essential for showing the satisfiability of the last call to checkSat
1918 using the current model. This method will only return false (for any v)
1919 if the model-cores option has been set.
1921 :param v: The term in question
1922 :return: true if v is a model core symbol
1924 return self.csolver.isModelCoreSymbol(v.cterm)
1926 def getSeparationHeap(self):
1927 """When using separation logic, obtain the term for the heap.
1929 :return: The term for the heap
1931 cdef Term term = Term(self)
1932 term.cterm = self.csolver.getSeparationHeap()
1935 def getSeparationNilTerm(self):
1936 """When using separation logic, obtain the term for nil.
1938 :return: The term for nil
1940 cdef Term term = Term(self)
1941 term.cterm = self.csolver.getSeparationNilTerm()
1944 def declareSeparationHeap(self, Sort locType, Sort dataType):
1946 When using separation logic, this sets the location sort and the
1947 datatype sort to the given ones. This method should be invoked exactly
1948 once, before any separation logic constraints are provided.
1950 :param locSort: The location sort of the heap
1951 :param dataSort: The data sort of the heap
1953 self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
1955 def declarePool(self, str symbol, Sort sort, initValue):
1956 """Declare a symbolic pool of terms with the given initial value.
1960 .. code-block:: smtlib
1962 ( declare-pool <symbol> <sort> ( <term>* ) )
1964 :param symbol: The name of the pool
1965 :param sort: The sort of the elements of the pool.
1966 :param initValue: The initial value of the pool
1968 cdef Term term = Term(self)
1969 cdef vector[c_Term] niv
1971 niv.push_back((<Term?> v).cterm)
1972 term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
1975 def pop(self, nscopes=1):
1976 """Pop ``nscopes`` level(s) from the assertion stack.
1980 .. code-block:: smtlib
1984 :param nscopes: the number of levels to pop
1986 self.csolver.pop(nscopes)
1988 def push(self, nscopes=1):
1989 """ Push ``nscopes`` level(s) to the assertion stack.
1993 .. code-block:: smtlib
1997 :param nscopes: the number of levels to push
1999 self.csolver.push(nscopes)
2001 def resetAssertions(self):
2003 Remove all assertions.
2007 .. code-block:: smtlib
2009 ( reset-assertions )
2012 self.csolver.resetAssertions()
2014 def setInfo(self, str keyword, str value):
2019 .. code-block:: smtlib
2021 ( set-info <attribute> )
2023 :param keyword: the info flag
2024 :param value: the value of the info flag
2026 self.csolver.setInfo(keyword.encode(), value.encode())
2028 def setLogic(self, str logic):
2033 .. code-block:: smtlib
2035 ( set-logic <symbol> )
2037 :param logic: the logic to set
2039 self.csolver.setLogic(logic.encode())
2041 def setOption(self, str option, str value):
2046 .. code-block:: smtlib
2048 ( set-option <option> )
2050 :param option: the option name
2051 :param value: the option value
2053 self.csolver.setOption(option.encode(), value.encode())
2059 def __cinit__(self, Solver solver):
2060 # csort always set by Solver
2061 self.solver = solver
2063 def __eq__(self, Sort other):
2064 return self.csort == other.csort
2066 def __ne__(self, Sort other):
2067 return self.csort != other.csort
2069 def __lt__(self, Sort other):
2070 return self.csort < other.csort
2072 def __gt__(self, Sort other):
2073 return self.csort > other.csort
2075 def __le__(self, Sort other):
2076 return self.csort <= other.csort
2078 def __ge__(self, Sort other):
2079 return self.csort >= other.csort
2082 return self.csort.toString().decode()
2085 return self.csort.toString().decode()
2088 return csorthash(self.csort)
2090 def isBoolean(self):
2091 return self.csort.isBoolean()
2093 def isInteger(self):
2094 return self.csort.isInteger()
2097 return self.csort.isReal()
2100 return self.csort.isString()
2103 return self.csort.isRegExp()
2105 def isRoundingMode(self):
2106 return self.csort.isRoundingMode()
2108 def isBitVector(self):
2109 return self.csort.isBitVector()
2111 def isFloatingPoint(self):
2112 return self.csort.isFloatingPoint()
2114 def isDatatype(self):
2115 return self.csort.isDatatype()
2117 def isParametricDatatype(self):
2118 return self.csort.isParametricDatatype()
2120 def isConstructor(self):
2121 return self.csort.isConstructor()
2123 def isSelector(self):
2124 return self.csort.isSelector()
2127 return self.csort.isTester()
2129 def isFunction(self):
2130 return self.csort.isFunction()
2132 def isPredicate(self):
2133 return self.csort.isPredicate()
2136 return self.csort.isTuple()
2139 return self.csort.isRecord()
2142 return self.csort.isArray()
2145 return self.csort.isSet()
2148 return self.csort.isBag()
2150 def isSequence(self):
2151 return self.csort.isSequence()
2153 def isUninterpretedSort(self):
2154 return self.csort.isUninterpretedSort()
2156 def isSortConstructor(self):
2157 return self.csort.isSortConstructor()
2159 def isFirstClass(self):
2160 return self.csort.isFirstClass()
2162 def isFunctionLike(self):
2163 return self.csort.isFunctionLike()
2165 def isSubsortOf(self, Sort sort):
2166 return self.csort.isSubsortOf(sort.csort)
2168 def isComparableTo(self, Sort sort):
2169 return self.csort.isComparableTo(sort.csort)
2171 def getDatatype(self):
2172 cdef Datatype d = Datatype(self.solver)
2173 d.cd = self.csort.getDatatype()
2176 def instantiate(self, params):
2177 cdef Sort sort = Sort(self.solver)
2178 cdef vector[c_Sort] v
2180 v.push_back((<Sort?> s).csort)
2181 sort.csort = self.csort.instantiate(v)
2184 def getConstructorArity(self):
2185 return self.csort.getConstructorArity()
2187 def getConstructorDomainSorts(self):
2189 for s in self.csort.getConstructorDomainSorts():
2190 sort = Sort(self.solver)
2192 domain_sorts.append(sort)
2195 def getConstructorCodomainSort(self):
2196 cdef Sort sort = Sort(self.solver)
2197 sort.csort = self.csort.getConstructorCodomainSort()
2200 def getSelectorDomainSort(self):
2201 cdef Sort sort = Sort(self.solver)
2202 sort.csort = self.csort.getSelectorDomainSort()
2205 def getSelectorCodomainSort(self):
2206 cdef Sort sort = Sort(self.solver)
2207 sort.csort = self.csort.getSelectorCodomainSort()
2210 def getTesterDomainSort(self):
2211 cdef Sort sort = Sort(self.solver)
2212 sort.csort = self.csort.getTesterDomainSort()
2215 def getTesterCodomainSort(self):
2216 cdef Sort sort = Sort(self.solver)
2217 sort.csort = self.csort.getTesterCodomainSort()
2220 def getFunctionArity(self):
2221 return self.csort.getFunctionArity()
2223 def getFunctionDomainSorts(self):
2225 for s in self.csort.getFunctionDomainSorts():
2226 sort = Sort(self.solver)
2228 domain_sorts.append(sort)
2231 def getFunctionCodomainSort(self):
2232 cdef Sort sort = Sort(self.solver)
2233 sort.csort = self.csort.getFunctionCodomainSort()
2236 def getArrayIndexSort(self):
2237 cdef Sort sort = Sort(self.solver)
2238 sort.csort = self.csort.getArrayIndexSort()
2241 def getArrayElementSort(self):
2242 cdef Sort sort = Sort(self.solver)
2243 sort.csort = self.csort.getArrayElementSort()
2246 def getSetElementSort(self):
2247 cdef Sort sort = Sort(self.solver)
2248 sort.csort = self.csort.getSetElementSort()
2251 def getBagElementSort(self):
2252 cdef Sort sort = Sort(self.solver)
2253 sort.csort = self.csort.getBagElementSort()
2256 def getSequenceElementSort(self):
2257 cdef Sort sort = Sort(self.solver)
2258 sort.csort = self.csort.getSequenceElementSort()
2261 def getUninterpretedSortName(self):
2262 return self.csort.getUninterpretedSortName().decode()
2264 def isUninterpretedSortParameterized(self):
2265 return self.csort.isUninterpretedSortParameterized()
2267 def getUninterpretedSortParamSorts(self):
2269 for s in self.csort.getUninterpretedSortParamSorts():
2270 sort = Sort(self.solver)
2272 param_sorts.append(sort)
2275 def getSortConstructorName(self):
2276 return self.csort.getSortConstructorName().decode()
2278 def getSortConstructorArity(self):
2279 return self.csort.getSortConstructorArity()
2281 def getBVSize(self):
2282 return self.csort.getBVSize()
2284 def getFPExponentSize(self):
2285 return self.csort.getFPExponentSize()
2287 def getFPSignificandSize(self):
2288 return self.csort.getFPSignificandSize()
2290 def getDatatypeParamSorts(self):
2292 for s in self.csort.getDatatypeParamSorts():
2293 sort = Sort(self.solver)
2295 param_sorts.append(sort)
2298 def getDatatypeArity(self):
2299 return self.csort.getDatatypeArity()
2301 def getTupleLength(self):
2302 return self.csort.getTupleLength()
2304 def getTupleSorts(self):
2306 for s in self.csort.getTupleSorts():
2307 sort = Sort(self.solver)
2309 tuple_sorts.append(sort)
2316 def __cinit__(self, Solver solver):
2317 # cterm always set in the Solver object
2318 self.solver = solver
2320 def __eq__(self, Term other):
2321 return self.cterm == other.cterm
2323 def __ne__(self, Term other):
2324 return self.cterm != other.cterm
2326 def __lt__(self, Term other):
2327 return self.cterm < other.cterm
2329 def __gt__(self, Term other):
2330 return self.cterm > other.cterm
2332 def __le__(self, Term other):
2333 return self.cterm <= other.cterm
2335 def __ge__(self, Term other):
2336 return self.cterm >= other.cterm
2338 def __getitem__(self, int index):
2339 cdef Term term = Term(self.solver)
2341 term.cterm = self.cterm[index]
2343 raise ValueError("Expecting a non-negative integer or string")
2347 return self.cterm.toString().decode()
2350 return self.cterm.toString().decode()
2353 for ci in self.cterm:
2354 term = Term(self.solver)
2359 return ctermhash(self.cterm)
2361 def getNumChildren(self):
2362 return self.cterm.getNumChildren()
2365 return self.cterm.getId()
2368 return kind(<int> self.cterm.getKind())
2371 cdef Sort sort = Sort(self.solver)
2372 sort.csort = self.cterm.getSort()
2375 def substitute(self, term_or_list_1, term_or_list_2):
2376 # The resulting term after substitution
2377 cdef Term term = Term(self.solver)
2378 # lists for substitutions
2379 cdef vector[c_Term] ces
2380 cdef vector[c_Term] creplacements
2382 # normalize the input parameters to be lists
2383 if isinstance(term_or_list_1, list):
2384 assert isinstance(term_or_list_2, list)
2386 replacements = term_or_list_2
2387 if len(es) != len(replacements):
2388 raise RuntimeError("Expecting list inputs to substitute to "
2389 "have the same length but got: "
2390 "{} and {}".format(len(es), len(replacements)))
2392 for e, r in zip(es, replacements):
2393 ces.push_back((<Term?> e).cterm)
2394 creplacements.push_back((<Term?> r).cterm)
2397 # add the single elements to the vectors
2398 ces.push_back((<Term?> term_or_list_1).cterm)
2399 creplacements.push_back((<Term?> term_or_list_2).cterm)
2401 # call the API substitute method with lists
2402 term.cterm = self.cterm.substitute(ces, creplacements)
2406 return self.cterm.hasOp()
2409 cdef Op op = Op(self.solver)
2410 op.cop = self.cterm.getOp()
2414 return self.cterm.isNull()
2417 cdef Term term = Term(self.solver)
2418 term.cterm = self.cterm.notTerm()
2421 def andTerm(self, Term t):
2422 cdef Term term = Term(self.solver)
2423 term.cterm = self.cterm.andTerm((<Term> t).cterm)
2426 def orTerm(self, Term t):
2427 cdef Term term = Term(self.solver)
2428 term.cterm = self.cterm.orTerm(t.cterm)
2431 def xorTerm(self, Term t):
2432 cdef Term term = Term(self.solver)
2433 term.cterm = self.cterm.xorTerm(t.cterm)
2436 def eqTerm(self, Term t):
2437 cdef Term term = Term(self.solver)
2438 term.cterm = self.cterm.eqTerm(t.cterm)
2441 def impTerm(self, Term t):
2442 cdef Term term = Term(self.solver)
2443 term.cterm = self.cterm.impTerm(t.cterm)
2446 def iteTerm(self, Term then_t, Term else_t):
2447 cdef Term term = Term(self.solver)
2448 term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
2451 def isConstArray(self):
2452 return self.cterm.isConstArray()
2454 def getConstArrayBase(self):
2455 cdef Term term = Term(self.solver)
2456 term.cterm = self.cterm.getConstArrayBase()
2459 def isBooleanValue(self):
2460 return self.cterm.isBooleanValue()
2462 def getBooleanValue(self):
2463 return self.cterm.getBooleanValue()
2465 def isStringValue(self):
2466 return self.cterm.isStringValue()
2468 def getStringValue(self):
2469 cdef Py_ssize_t size
2470 cdef c_wstring s = self.cterm.getStringValue()
2471 return PyUnicode_FromWideChar(s.data(), s.size())
2473 def isIntegerValue(self):
2474 return self.cterm.isIntegerValue()
2475 def isAbstractValue(self):
2476 return self.cterm.isAbstractValue()
2478 def getAbstractValue(self):
2479 return self.cterm.getAbstractValue().decode()
2481 def isFloatingPointPosZero(self):
2482 return self.cterm.isFloatingPointPosZero()
2484 def isFloatingPointNegZero(self):
2485 return self.cterm.isFloatingPointNegZero()
2487 def isFloatingPointPosInf(self):
2488 return self.cterm.isFloatingPointPosInf()
2490 def isFloatingPointNegInf(self):
2491 return self.cterm.isFloatingPointNegInf()
2493 def isFloatingPointNaN(self):
2494 return self.cterm.isFloatingPointNaN()
2496 def isFloatingPointValue(self):
2497 return self.cterm.isFloatingPointValue()
2499 def getFloatingPointValue(self):
2500 cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
2501 cdef Term term = Term(self.solver)
2502 term.cterm = get2(t)
2503 return (get0(t), get1(t), term)
2505 def isSetValue(self):
2506 return self.cterm.isSetValue()
2508 def getSetValue(self):
2510 for e in self.cterm.getSetValue():
2511 term = Term(self.solver)
2516 def isSequenceValue(self):
2517 return self.cterm.isSequenceValue()
2519 def getSequenceValue(self):
2521 for e in self.cterm.getSequenceValue():
2522 term = Term(self.solver)
2527 def isUninterpretedValue(self):
2528 return self.cterm.isUninterpretedValue()
2530 def getUninterpretedValue(self):
2531 cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue()
2532 cdef Sort sort = Sort(self.solver)
2533 sort.csort = p.first
2537 def isTupleValue(self):
2538 return self.cterm.isTupleValue()
2540 def getTupleValue(self):
2542 for e in self.cterm.getTupleValue():
2543 term = Term(self.solver)
2548 def getIntegerValue(self):
2549 return int(self.cterm.getIntegerValue().decode())
2551 def isRealValue(self):
2552 return self.cterm.isRealValue()
2554 def getRealValue(self):
2555 """Returns the value of a real term as a Fraction"""
2556 return Fraction(self.cterm.getRealValue().decode())
2558 def isBitVectorValue(self):
2559 return self.cterm.isBitVectorValue()
2561 def getBitVectorValue(self, base = 2):
2562 """Returns the value of a bit-vector term as a 0/1 string"""
2563 return self.cterm.getBitVectorValue(base).decode()
2565 def toPythonObj(self):
2567 Converts a constant value Term to a Python object.
2570 Boolean -- returns a Python bool
2571 Int -- returns a Python int
2572 Real -- returns a Python Fraction
2573 BV -- returns a Python int (treats BV as unsigned)
2574 String -- returns a Python Unicode string
2575 Array -- returns a Python dict mapping indices to values
2576 -- the constant base is returned as the default value
2579 if self.isBooleanValue():
2580 return self.getBooleanValue()
2581 elif self.isIntegerValue():
2582 return self.getIntegerValue()
2583 elif self.isRealValue():
2584 return self.getRealValue()
2585 elif self.isBitVectorValue():
2586 return int(self.getBitVectorValue(), 2)
2587 elif self.isStringValue():
2588 return self.getStringValue()
2589 elif self.getSort().isArray():
2595 # Array models are represented as a series of store operations
2596 # on a constant array
2599 if t.getKind() == kinds.Store:
2601 keys.append(t[1].toPythonObj())
2602 values.append(t[2].toPythonObj())
2603 to_visit.append(t[0])
2605 assert t.getKind() == kinds.ConstArray
2606 base_value = t.getConstArrayBase().toPythonObj()
2608 assert len(keys) == len(values)
2609 assert base_value is not None
2611 # put everything in a dictionary with the constant
2612 # base as the result for any index not included in the stores
2613 res = defaultdict(lambda : base_value)
2614 for k, v in zip(keys, values):
2620 # Generate rounding modes
2621 cdef __rounding_modes = {
2622 <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
2623 <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
2624 <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
2625 <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
2626 <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway"
2629 mod_ref = sys.modules[__name__]
2630 for rm_int, name in __rounding_modes.items():
2631 r = RoundingMode(rm_int)
2633 if name in dir(mod_ref):
2634 raise RuntimeError("Redefinition of Python RoundingMode %s."%name)
2636 setattr(mod_ref, name, r)
2643 # Generate unknown explanations
2644 cdef __unknown_explanations = {
2645 <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
2646 <int> INCOMPLETE: "Incomplete",
2647 <int> TIMEOUT: "Timeout",
2648 <int> RESOURCEOUT: "Resourceout",
2649 <int> MEMOUT: "Memout",
2650 <int> INTERRUPTED: "Interrupted",
2651 <int> NO_STATUS: "NoStatus",
2652 <int> UNSUPPORTED: "Unsupported",
2653 <int> OTHER: "Other",
2654 <int> UNKNOWN_REASON: "UnknownReason"
2657 for ue_int, name in __unknown_explanations.items():
2658 u = UnknownExplanation(ue_int)
2660 if name in dir(mod_ref):
2661 raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
2663 setattr(mod_ref, name, u)