From 8ef22792d24afa6e80a92fccd84292a8533fd49f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 31 Mar 2022 22:45:33 -0700 Subject: [PATCH] Python api: Various fixes in docs. (#8480) --- docs/api/python/base/python.rst | 1 + docs/api/python/base/statistics.rst | 7 + src/api/python/cvc5.pxi | 2273 +++++++++++++++------------ 3 files changed, 1316 insertions(+), 965 deletions(-) create mode 100644 docs/api/python/base/statistics.rst diff --git a/docs/api/python/base/python.rst b/docs/api/python/base/python.rst index cf2122b12..d0692b062 100644 --- a/docs/api/python/base/python.rst +++ b/docs/api/python/base/python.rst @@ -28,6 +28,7 @@ See the :doc:`pythonic API <../pythonic/pythonic>` for a higher-level programmin roundingmode solver sort + statistics synthresult term unknownexplanation diff --git a/docs/api/python/base/statistics.rst b/docs/api/python/base/statistics.rst new file mode 100644 index 000000000..175633bc4 --- /dev/null +++ b/docs/api/python/base/statistics.rst @@ -0,0 +1,7 @@ +Statistics +========== + +.. autoclass:: cvc5.Statistics + :members: + :special-members: __getitem__ + :undoc-members: diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 91b949854..1b227e504 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -48,8 +48,8 @@ cdef extern from "Python.h": ################################## DECORATORS ################################# def expand_list_arg(num_req_args=0): """ - Creates a decorator that looks at index num_req_args of the args, - if it's a list, it expands it before calling the function. + Creates a decorator that looks at index num_req_args of the args, + if it's a list, it expands it before calling the function. """ def decorator(func): @wraps(func) @@ -99,7 +99,8 @@ cdef c_hash[c_Term] ctermhash = c_hash[c_Term]() cdef class Datatype: """ A cvc5 datatype. - Wrapper class for :cpp:class:`cvc5::Datatype`. + + Wrapper class for the C++ class :cpp:class:`cvc5::Datatype`. """ cdef c_Datatype cd cdef Solver solver @@ -118,8 +119,8 @@ cdef class Datatype: def getConstructor(self, str name): """ - :param name: the name of the constructor. - :return: a constructor by name. + :param name: The name of the constructor. + :return: A constructor by name. """ cdef DatatypeConstructor dc = DatatypeConstructor(self.solver) dc.cdc = self.cd.getConstructor(name.encode()) @@ -127,8 +128,9 @@ cdef class Datatype: def getConstructorTerm(self, str name): """ - :param name: the name of the constructor. - :return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() `). + :param name: The name of the constructor. + :return: The term representing the datatype constructor with the + given name. """ cdef Term term = Term(self.solver) term.cterm = self.cd.getConstructorTerm(name.encode()) @@ -136,8 +138,8 @@ cdef class Datatype: def getSelector(self, str name): """ - :param name: the name of the selector.. - :return: a selector by name. + :param name: The name of the selector.. + :return: A selector by name. """ cdef DatatypeSelector ds = DatatypeSelector(self.solver) ds.cds = self.cd.getSelector(name.encode()) @@ -145,19 +147,20 @@ cdef class Datatype: def getName(self): """ - :return: the name of the datatype. + :return: The name of the datatype. """ return self.cd.getName().decode() def getNumConstructors(self): """ - :return: number of constructors in this datatype. + :return: The number of constructors in this datatype. """ return self.cd.getNumConstructors() def getParameters(self): """ - :return: the parameters of this datatype, if it is parametric. An exception is thrown if this datatype is not parametric. + :return: The parameters of this datatype, if it is parametric. An + exception is thrown if this datatype is not parametric. """ param_sorts = [] for s in self.cd.getParameters(): @@ -175,11 +178,15 @@ cdef class Datatype: return self.cd.isParametric() def isCodatatype(self): - """:return: True if this datatype corresponds to a co-datatype.""" + """ + :return: True if this datatype corresponds to a co-datatype. + """ return self.cd.isCodatatype() def isTuple(self): - """:return: True if this datatype corresponds to a tuple.""" + """ + :return: True if this datatype corresponds to a tuple. + """ return self.cd.isTuple() def isRecord(self): @@ -191,15 +198,26 @@ cdef class Datatype: return self.cd.isRecord() def isFinite(self): - """:return: True if this datatype is finite.""" + """ + :return: True if this datatype is finite. + """ return self.cd.isFinite() def isWellFounded(self): - """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() `).""" + """ + Is this datatype well-founded? + + If this datatype is not a codatatype, this returns false if there + are no values of this datatype that are of finite size. + + :return: True if this datatype is well-founded + """ return self.cd.isWellFounded() def isNull(self): - """:return: True if this Datatype is a null object.""" + """ + :return: True if this Datatype is a null object. + """ return self.cd.isNull() def __str__(self): @@ -218,6 +236,7 @@ cdef class Datatype: cdef class DatatypeConstructor: """ A cvc5 datatype constructor. + Wrapper class for :cpp:class:`cvc5::DatatypeConstructor`. """ cdef c_DatatypeConstructor cdc @@ -238,13 +257,13 @@ cdef class DatatypeConstructor: def getName(self): """ - :return: the name of the constructor. + :return: The name of the constructor. """ return self.cdc.getName().decode() def getConstructorTerm(self): """ - :return: the constructor operator as a term. + :return: The constructor operator as a term. """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getConstructorTerm() @@ -252,15 +271,43 @@ cdef class DatatypeConstructor: def getInstantiatedConstructorTerm(self, Sort retSort): """ - Specialized method for parametric datatypes (see - :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm() - `). + Get the constructor operator of this datatype constructor whose + return type is retSort. This method is intended to be used on + constructors of parametric datatypes and can be seen as returning + the constructor term that has been explicitly cast to the given + sort. + + This method is required for constructors of parametric datatypes + whose return type cannot be determined by type inference. For + example, given: + + .. code:: smtlib + + (declare-datatype List + (par (T) ((nil) (cons (head T) (tail (List T)))))) + + The type of nil terms must be provided by the user. In SMT version + 2.6, this is done via the syntax for qualified identifiers: + + .. code:: smtlib + + (as nil (List Int)) + + This method is equivalent of applying the above, where this + DatatypeConstructor is the one corresponding to nil, and retSort is + ``(List Int)``. + + .. note:: + + The returned constructor term ``t`` is an operator, while + ``Solver.mkTerm(APPLY_CONSTRUCTOR, [t])`` is used to construct + the above (nullary) application of nil. .. warning:: This method is experimental and may change in future versions. - :param retSort: the desired return sort of the constructor - :return: the constructor operator as a term. + :param retSort: The desired return sort of the constructor. + :return: The constructor operator as a term. """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort) @@ -268,7 +315,8 @@ cdef class DatatypeConstructor: def getTesterTerm(self): """ - :return: the tester operator that is related to this constructor, as a term. + :return: The tester operator that is related to this constructor, + as a term. """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getTesterTerm() @@ -276,14 +324,15 @@ cdef class DatatypeConstructor: def getNumSelectors(self): """ - :return: the number of selecters (so far) of this Datatype constructor. + :return: The number of selecters (so far) of this Datatype + constructor. """ return self.cdc.getNumSelectors() def getSelector(self, str name): """ - :param name: the name of the datatype selector. - :return: the first datatype selector with the given name + :param name: The name of the datatype selector. + :return: The first datatype selector with the given name. """ cdef DatatypeSelector ds = DatatypeSelector(self.solver) ds.cds = self.cdc.getSelector(name.encode()) @@ -291,15 +340,18 @@ cdef class DatatypeConstructor: def getSelectorTerm(self, str name): """ - :param name: the name of the datatype selector. - :return: a term representing the firstdatatype selector with the given name. + :param name: The name of the datatype selector. + :return: A term representing the firstdatatype selector with the + given name. """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getSelectorTerm(name.encode()) return term def isNull(self): - """:return: True if this DatatypeConstructor is a null object.""" + """ + :return: True if this DatatypeConstructor is a null object. + """ return self.cdc.isNull() def __str__(self): @@ -318,6 +370,7 @@ cdef class DatatypeConstructor: cdef class DatatypeConstructorDecl: """ A cvc5 datatype constructor declaration. + Wrapper class for :cpp:class:`cvc5::DatatypeConstructorDecl`. """ cdef c_DatatypeConstructorDecl cddc @@ -330,8 +383,8 @@ cdef class DatatypeConstructorDecl: """ Add datatype selector declaration. - :param name: the name of the datatype selector declaration to add. - :param sort: the codomain sort of the datatype selector declaration + :param name: The name of the datatype selector declaration to add. + :param sort: The codomain sort of the datatype selector declaration to add. """ self.cddc.addSelector(name.encode(), sort.csort) @@ -341,12 +394,14 @@ cdef class DatatypeConstructorDecl: Add datatype selector declaration whose codomain sort is the datatype itself. - :param name: the name of the datatype selector declaration to add. + :param name: The name of the datatype selector declaration to add. """ self.cddc.addSelectorSelf(name.encode()) def isNull(self): - """:return: True if this DatatypeConstructorDecl is a null object.""" + """ + :return: True if this DatatypeConstructorDecl is a null object. + """ return self.cddc.isNull() def __str__(self): @@ -359,6 +414,7 @@ cdef class DatatypeConstructorDecl: cdef class DatatypeDecl: """ A cvc5 datatype declaration. + Wrapper class for :cpp:class:`cvc5::DatatypeDecl`. """ cdef c_DatatypeDecl cdd @@ -370,30 +426,33 @@ cdef class DatatypeDecl: """ Add a datatype constructor declaration. - :param ctor: the datatype constructor declaration to add. + :param ctor: The datatype constructor declaration to add. """ self.cdd.addConstructor(ctor.cddc) def getNumConstructors(self): """ - :return: number of constructors (so far) for this datatype declaration. + :return: The number of constructors (so far) for this datatype + declaration. """ return self.cdd.getNumConstructors() def isParametric(self): """ - :return: is this datatype declaration parametric? + :return: True if this datatype declaration is parametric. """ return self.cdd.isParametric() def getName(self): """ - :return: the name of this datatype declaration. + :return: The name of this datatype declaration. """ return self.cdd.getName().decode() def isNull(self): - """:return: True if this DatatypeDecl is a null object.""" + """ + :return: True if this DatatypeDecl is a null object. + """ return self.cdd.isNull() def __str__(self): @@ -406,6 +465,7 @@ cdef class DatatypeDecl: cdef class DatatypeSelector: """ A cvc5 datatype selector. + Wrapper class for :cpp:class:`cvc5::DatatypeSelector`. """ cdef c_DatatypeSelector cds @@ -416,13 +476,13 @@ cdef class DatatypeSelector: def getName(self): """ - :return: the name of this datatype selector. + :return: The name of this datatype selector. """ return self.cds.getName().decode() def getSelectorTerm(self): """ - :return: the selector opeartor of this datatype selector as a term. + :return: The selector opeartor of this datatype selector as a term. """ cdef Term term = Term(self.solver) term.cterm = self.cds.getSelectorTerm() @@ -430,7 +490,7 @@ cdef class DatatypeSelector: def getUpdaterTerm(self): """ - :return: the updater opeartor of this datatype selector as a term. + :return: The updater opeartor of this datatype selector as a term. """ cdef Term term = Term(self.solver) term.cterm = self.cds.getUpdaterTerm() @@ -438,14 +498,16 @@ cdef class DatatypeSelector: def getCodomainSort(self): """ - :return: the codomain sort of this selector. + :return: The codomain sort of this selector. """ cdef Sort sort = Sort(self.solver) sort.csort = self.cds.getCodomainSort() return sort def isNull(self): - """:return: True if this DatatypeSelector is a null object.""" + """ + :return: True if this DatatypeSelector is a null object. + """ return self.cds.isNull() def __str__(self): @@ -458,9 +520,11 @@ cdef class DatatypeSelector: cdef class Op: """ A cvc5 operator. + An operator is a term that represents certain operators, instantiated with its required parameters, e.g., - a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`. + a term of kind :py:obj:`BVExtract `. + Wrapper class for :cpp:class:`cvc5::Op`. """ cdef c_Op cop @@ -486,7 +550,7 @@ cdef class Op: def getKind(self): """ - :return: the kind of this operator. + :return: The kind of this operator. """ return Kind( self.cop.getKind()) @@ -504,15 +568,16 @@ cdef class Op: def getNumIndices(self): """ - :return: number of indices of this op. + :return: The number of indices of this op. """ return self.cop.getNumIndices() def __getitem__(self, i): """ - Get the index at position i. - :param i: the position of the index to return - :return: the index at position i + Get the index at position ``i``. + + :param i: The position of the index to return. + :return: The index at position ``i``. """ cdef Term term = Term(self.solver) term.cterm = self.cop[i] @@ -522,6 +587,7 @@ cdef class Op: cdef class Grammar: """ A Sygus Grammar. + Wrapper class for :cpp:class:`cvc5::Grammar`. """ cdef c_Grammar cgrammar @@ -534,8 +600,8 @@ cdef class Grammar: """ Add ``rule`` to the set of rules corresponding to ``ntSymbol``. - :param ntSymbol: the non-terminal to which the rule is added. - :param rule: the rule to add. + :param ntSymbol: The non-terminal to which the rule is added. + :param rule: The rule to add. """ self.cgrammar.addRule(ntSymbol.cterm, rule.cterm) @@ -543,15 +609,16 @@ cdef class Grammar: """ Allow ``ntSymbol`` to be an arbitrary constant. - :param ntSymbol: the non-terminal allowed to be constant. + :param ntSymbol: The non-terminal allowed to be constant. """ self.cgrammar.addAnyConstant(ntSymbol.cterm) def addAnyVariable(self, Term ntSymbol): """ - Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``. + Allow ``ntSymbol`` to be any input variable to corresponding + synth-fun/synth-inv with the same sort as ``ntSymbol``. - :param ntSymbol: the non-terminal allowed to be any input variable. + :param ntSymbol: The non-terminal allowed to be any input variable. """ self.cgrammar.addAnyVariable(ntSymbol.cterm) @@ -559,8 +626,8 @@ cdef class Grammar: """ Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``. - :param ntSymbol: the non-terminal to which the rules are added. - :param rules: the rules to add. + :param ntSymbol: The non-terminal to which the rules are added. + :param rules: The rules to add. """ cdef vector[c_Term] crules for r in rules: @@ -570,6 +637,7 @@ cdef class Grammar: cdef class Result: """ Encapsulation of a three-valued solver result, with explanations. + Wrapper class for :cpp:class:`cvc5::Result`. """ cdef c_Result cr @@ -579,32 +647,39 @@ cdef class Result: def isNull(self): """ - :return: True if Result is empty, i.e., a nullary Result, and not an actual result returned from a - :cpp:func:`Solver::checkSat() ` (and friends) query. + :return: True if Result is empty, i.e., a nullary Result, and not + an actual result returned from a + :py:meth:`Solver.checkSat()` (and friends) query. """ return self.cr.isNull() def isSat(self): """ - :return: True if query was a satisfiable :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query. + :return: True if query was a satisfiable + :py:meth:`Solver.checkSat()` or + :py:meth:`Solver.checkSatAssuming()` query. """ return self.cr.isSat() def isUnsat(self): """ - :return: True if query was an usatisfiable :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query. + :return: True if query was an usatisfiable + :py:meth:`Solver.checkSat()` or + :py:meth:`Solver.checkSatAssuming()` query. """ return self.cr.isUnsat() def isUnknown(self): """ - :return: True if query was a :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query and cvc5 was not able to determine (un)satisfiability. + :return: True if query was a :py:meth:`Solver.checkSat()` or + :py:meth:`Solver.checkSatAssuming()` query and cvc5 was + not able to determine (un)satisfiability. """ return self.cr.isUnknown() def getUnknownExplanation(self): """ - :return: an explanation for an unknown query result. + :return: An explanation for an unknown query result. """ return UnknownExplanation( self.cr.getUnknownExplanation()) @@ -622,10 +697,13 @@ cdef class Result: cdef class SynthResult: """ - Encapsulation of a solver synth result. This is the return value of the - API methods: + Encapsulation of a solver synth result. + + This is the return value of the API methods: + - :py:meth:`Solver.checkSynth()` - :py:meth:`Solver.checkSynthNext()` + which we call synthesis queries. This class indicates whether the synthesis query has a solution, has no solution, or is unknown. """ @@ -636,7 +714,8 @@ cdef class SynthResult: def isNull(self): """ - :return: True if SynthResult is null, i.e. not a SynthResult returned from a synthesis query. + :return: True if SynthResult is null, i.e., not a SynthResult + returned from a synthesis query. """ return self.cr.isNull() @@ -649,13 +728,14 @@ cdef class SynthResult: def hasNoSolution(self): """ :return: True if the synthesis query has no solution. - In this case, then it was determined there was no solution. + In this case, it was determined that there was no solution. """ return self.cr.hasNoSolution() def isUnknown(self): """ - :return: True if the result of the synthesis query could not be determined. + :return: True if the result of the synthesis query could not be + determined. """ return self.cr.isUnknown() @@ -667,7 +747,11 @@ cdef class SynthResult: cdef class Solver: - """Wrapper class for :cpp:class:`cvc5::Solver`.""" + """ + A cvc5 solver. + + Wrapper class for :cpp:class:`cvc5::Solver`. + """ cdef c_Solver* csolver def __cinit__(self): @@ -677,90 +761,101 @@ cdef class Solver: del self.csolver def getBooleanSort(self): - """:return: sort Boolean + """ + :return: Sort Boolean. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.getBooleanSort() return sort def getIntegerSort(self): - """:return: sort Integer + """ + :return: Sort Integer. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.getIntegerSort() return sort def getNullSort(self): - """:return: sort null + """ + :return: A null sort object. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.getNullSort() return sort def getRealSort(self): - """:return: sort Real + """ + :return: Sort Real. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.getRealSort() return sort def getRegExpSort(self): - """:return: sort of RegExp + """:return: The sort of regular expressions. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.getRegExpSort() return sort def getRoundingModeSort(self): - """:return: sort RoundingMode + """:return: Sort RoundingMode. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.getRoundingModeSort() return sort def getStringSort(self): - """:return: sort String + """:return: Sort String. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.getStringSort() return sort def mkArraySort(self, Sort indexSort, Sort elemSort): - """Create an array sort. + """ + Create an array sort. - :param indexSort: the array index sort - :param elemSort: the array element sort - :return: the array sort + :param indexSort: The array index sort. + :param elemSort: The array element sort. + :return: The array sort. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort) return sort def mkBitVectorSort(self, uint32_t size): - """Create a bit-vector sort. + """ + Create a bit-vector sort. - :param size: the bit-width of the bit-vector sort - :return: the bit-vector sort + :param size: The bit-width of the bit-vector sort + :return: The bit-vector sort """ cdef Sort sort = Sort(self) sort.csort = self.csolver.mkBitVectorSort(size) return sort def mkFloatingPointSort(self, uint32_t exp, uint32_t sig): - """Create a floating-point sort. + """ + Create a floating-point sort. - :param exp: the bit-width of the exponent of the floating-point sort. - :param sig: the bit-width of the significand of the floating-point sort. + :param exp: The bit-width of the exponent of the floating-point + sort. + :param sig: The bit-width of the significand of the floating-point + sort. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.mkFloatingPointSort(exp, sig) return sort def mkDatatypeSort(self, DatatypeDecl dtypedecl): - """Create a datatype sort. + """ + Create a datatype sort. - :param dtypedecl: the datatype declaration from which the sort is created - :return: the datatype sort + :param dtypedecl: The datatype declaration from which the sort is + created. + :return: The datatype sort. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd) @@ -768,22 +863,24 @@ cdef class Solver: def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None): """ - Create a vector of datatype sorts using unresolved sorts. The names of - the datatype declarations in dtypedecls must be distinct. + Create a vector of datatype sorts using unresolved sorts. The names + of the datatype declarations in dtypedecls must be distinct. - This method is called when the DatatypeDecl objects dtypedecls have been - built using "unresolved" sorts. + This method is called when the DatatypeDecl objects dtypedecls have + been built using "unresolved" sorts. - We associate each sort in unresolvedSorts with exacly one datatype from - dtypedecls. In particular, it must have the same name as exactly one - datatype declaration in dtypedecls. + We associate each sort in unresolvedSorts with exacly one datatype + from dtypedecls. In particular, it must have the same name as + exactly one datatype declaration in dtypedecls. - When constructing datatypes, unresolved sorts are replaced by the datatype - sort constructed for the datatype declaration it is associated with. + When constructing datatypes, unresolved sorts are replaced by the + datatype sort constructed for the datatype declaration it is + associated with. - :param dtypedecls: the datatype declarations from which the sort is created - :param unresolvedSorts: the list of unresolved sorts - :return: the datatype sorts + :param dtypedecls: The datatype declarations from which the sort is + created. + :param unresolvedSorts: The list of unresolved sorts. + :return: The datatype sorts. """ if unresolvedSorts == None: unresolvedSorts = set([]) @@ -809,11 +906,12 @@ cdef class Solver: return sorts def mkFunctionSort(self, sorts, Sort codomain): - """ Create function sort. + """ + Create function sort. - :param sorts: the sort of the function arguments - :param codomain: the sort of the function return value - :return: the function sort + :param sorts: The sort of the function arguments. + :param codomain: The sort of the function return value. + :return: The function sort. """ cdef Sort sort = Sort(self) @@ -830,13 +928,14 @@ cdef class Solver: return sort def mkParamSort(self, str symbolname = None): - """ Create a sort parameter. + """ + Create a sort parameter. - .. warning:: This method is experimental and may change in future - versions. + .. warning:: This method is experimental and may change in future + versions. - :param symbol: the name of the sort - :return: the sort parameter + :param symbol: The name of the sort. + :return: The sort parameter. """ cdef Sort sort = Sort(self) if symbolname is None: @@ -847,10 +946,12 @@ cdef class Solver: @expand_list_arg(num_req_args=0) def mkPredicateSort(self, *sorts): - """Create a predicate sort. + """ + Create a predicate sort. - :param sorts: the list of sorts of the predicate, as a list or as distinct arguments. - :return: the predicate sort + :param sorts: The list of sorts of the predicate, as a list or as + distinct arguments. + :return: The predicate sort. """ cdef Sort sort = Sort(self) cdef vector[c_Sort] v @@ -861,13 +962,15 @@ cdef class Solver: @expand_list_arg(num_req_args=0) def mkRecordSort(self, *fields): - """Create a record sort + """ + Create a record sort - .. warning:: This method is experimental and may change in future - versions. + .. warning:: This method is experimental and may change in future + versions. - :param fields: the list of fields of the record, as a list or as distinct arguments - :return: the record sort + :param fields: The list of fields of the record, as a list or as + distinct arguments. + :return: The record sort. """ cdef Sort sort = Sort(self) cdef vector[pair[string, c_Sort]] v @@ -882,40 +985,44 @@ cdef class Solver: return sort def mkSetSort(self, Sort elemSort): - """Create a set sort. + """ + Create a set sort. - :param elemSort: the sort of the set elements - :return: the set sort + :param elemSort: The sort of the set elements. + :return: The set sort. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.mkSetSort(elemSort.csort) return sort def mkBagSort(self, Sort elemSort): - """Create a bag sort. + """ + Create a bag sort. - :param elemSort: the sort of the bag elements - :return: the bag sort + :param elemSort: The sort of the bag elements. + :return: The bag sort. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.mkBagSort(elemSort.csort) return sort def mkSequenceSort(self, Sort elemSort): - """Create a sequence sort. + """ + Create a sequence sort. - :param elemSort: the sort of the sequence elements - :return: the sequence sort + :param elemSort: The sort of the sequence elements + :return: The sequence sort. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.mkSequenceSort(elemSort.csort) return sort def mkUninterpretedSort(self, str name = None): - """Create an uninterpreted sort. + """ + Create an uninterpreted sort. - :param symbol: the name of the sort - :return: the uninterpreted sort + :param symbol: The name of the sort. + :return: The uninterpreted sort. """ cdef Sort sort = Sort(self) if name is None: @@ -925,28 +1032,30 @@ cdef class Solver: return sort def mkUnresolvedSort(self, str name, size_t arity = 0): - """Create an unresolved sort. + """ + Create an unresolved sort. - This is for creating yet unresolved sort placeholders for mutually - recursive datatypes. + This is for creating yet unresolved sort placeholders for mutually + recursive datatypes. - :param symbol: the name of the sort - :param arity: the number of sort parameters of the sort - :return: the unresolved sort + :param symbol: The name of the sort. + :param arity: The number of sort parameters of the sort. + :return: The unresolved sort. """ cdef Sort sort = Sort(self) sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity) return sort def mkUninterpretedSortConstructorSort(self, size_t arity, str symbol = None): - """Create a sort constructor sort. + """ + Create a sort constructor sort. - An uninterpreted sort constructor is an uninterpreted sort with - arity > 0. + An uninterpreted sort constructor is an uninterpreted sort with + arity > 0. - :param symbol: the symbol of the sort - :param arity: the arity of the sort (must be > 0) - :return: the sort constructor sort + :param symbol: The symbol of the sort. + :param arity: The arity of the sort (must be > 0). + :return: The sort constructor sort. """ cdef Sort sort = Sort(self) if symbol is None: @@ -958,10 +1067,12 @@ cdef class Solver: @expand_list_arg(num_req_args=0) def mkTupleSort(self, *sorts): - """Create a tuple sort. + """ + Create a tuple sort. - :param sorts: of the elements of the tuple, as a list or as distinct arguments - :return: the tuple sort + :param sorts: Of the elements of the tuple, as a list or as + distinct arguments. + :return: The tuple sort. """ cdef Sort sort = Sort(self) cdef vector[c_Sort] v @@ -973,13 +1084,16 @@ cdef class Solver: @expand_list_arg(num_req_args=1) def mkTerm(self, kind_or_op, *args): """ - Supports the following arguments: + Create a term. + + Supports the following arguments: - - ``Term mkTerm(Kind kind)`` - - ``Term mkTerm(Kind kind, Op child1, List[Term] children)`` - - ``Term mkTerm(Kind kind, List[Term] children)`` + - ``Term mkTerm(Kind kind)`` + - ``Term mkTerm(Kind kind, List[Term] children)`` + - ``Term mkTerm(Op op)`` + - ``Term mkTerm(Op op, List[Term] children)`` - where ``List[Term]`` can also be comma-separated arguments + where ``List[Term]`` can also be comma-separated arguments """ cdef Term term = Term(self) cdef vector[c_Term] v @@ -997,11 +1111,13 @@ cdef class Solver: return term def mkTuple(self, sorts, terms): - """Create a tuple term. Terms are automatically converted if sorts are compatible. + """ + Create a tuple term. Terms are automatically converted if sorts are + compatible. - :param sorts: The sorts of the elements in the tuple - :param terms: The elements in the tuple - :return: the tuple Term + :param sorts: The sorts of the elements in the tuple. + :param terms: The elements in the tuple. + :return: The tuple Term. """ cdef vector[c_Sort] csorts cdef vector[c_Term] cterms @@ -1017,11 +1133,13 @@ cdef class Solver: @expand_list_arg(num_req_args=0) def mkOp(self, k, *args): """ - Supports the following uses: + Create operator. + + Supports the following arguments: - - ``Op mkOp(Kind kind)`` - - ``Op mkOp(Kind kind, const string& arg)`` - - ``Op mkOp(Kind kind, uint32_t arg0, ...)`` + - ``Op mkOp(Kind kind)`` + - ``Op mkOp(Kind kind, const string& arg)`` + - ``Op mkOp(Kind kind, uint32_t arg0, ...)`` """ cdef Op op = Op(self) cdef vector[uint32_t] v @@ -1045,70 +1163,84 @@ cdef class Solver: return op def mkTrue(self): - """Create a Boolean true constant. + """ + Create a Boolean true constant. - :return: the true constant + :return: The true constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkTrue() return term def mkFalse(self): - """Create a Boolean false constant. + """ + Create a Boolean false constant. - :return: the false constant + :return: The false constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkFalse() return term def mkBoolean(self, bint val): - """Create a Boolean constant. + """ + Create a Boolean constant. - :return: the Boolean constant - :param val: the value of the constant + :return: The Boolean constant. + :param val: The value of the constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkBoolean(val) return term def mkPi(self): - """Create a constant representing the number Pi. + """ + Create a constant representing the number Pi. - :return: a constant representing Pi + :return: A constant representing :py:obj:`Pi `. """ cdef Term term = Term(self) term.cterm = self.csolver.mkPi() return term def mkInteger(self, val): - """Create an integer constant. + """ + Create an integer constant. - :param val: representation of the constant: either a string or integer - :return: a constant of sort Integer + :param val: Representation of the constant: either a string or + integer. + :return: A constant of sort Integer. """ cdef Term term = Term(self) if isinstance(val, str): - term.cterm = self.csolver.mkInteger( str(val).encode()) + term.cterm = self.csolver.mkInteger( + str(val).encode()) else: assert(isinstance(val, int)) term.cterm = self.csolver.mkInteger(( val)) return term def mkReal(self, val, den=None): - """Create a real constant. + """ + Create a real constant. - :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. - :param den: if not None, the value is `val`/`den` - :return: a real term with literal value + :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. + :param den: If not None, the value is ``val``/``den``. + :return: A real term with literal value. - Can be used in various forms: + Can be used in various forms: - - Given a string ``"N/D"`` constructs the corresponding rational. - - Given a string ``"W.D"`` constructs the reduction of ``(W * P + D)/P``, where ``P`` is the appropriate power of 10. - - 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``. - - Given a string ``"W"`` or an integer, constructs that integer. - - Given two strings and/or integers ``N`` and ``D``, constructs ``N/D``. + - Given a string ``"N/D"`` constructs the corresponding rational. + - Given a string ``"W.D"`` constructs the reduction of + ``(W * P + D)/P``, where ``P`` is the appropriate power of 10. + - 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``. + - Given a string ``"W"`` or an integer, constructs that integer. + - Given two strings and/or integers ``N`` and ``D``, constructs + ``N/D``. """ cdef Term term = Term(self) if den is None: @@ -1122,72 +1254,79 @@ cdef class Solver: return term def mkRegexpAll(self): - """Create a regular expression all (re.all) term. + """ + Create a regular expression all (``re.all``) term. - :return: the all term + :return: The all term. """ cdef Term term = Term(self) term.cterm = self.csolver.mkRegexpAll() return term def mkRegexpAllchar(self): - """Create a regular expression allchar (re.allchar) term. + """ + Create a regular expression allchar (``re.allchar``) term. - :return: the allchar term + :return: The allchar term. """ cdef Term term = Term(self) term.cterm = self.csolver.mkRegexpAllchar() return term def mkRegexpNone(self): - """Create a regular expression none (re.none) term. + """ + Create a regular expression none (``re.none``) term. - :return: the none term + :return: The none term. """ cdef Term term = Term(self) term.cterm = self.csolver.mkRegexpNone() return term def mkEmptySet(self, Sort s): - """Create a constant representing an empty set of the given sort. + """ + Create a constant representing an empty set of the given sort. - :param sort: the sort of the set elements. - :return: the empty set constant + :param sort: The sort of the set elements. + :return: The empty set constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkEmptySet(s.csort) return term def mkEmptyBag(self, Sort s): - """Create a constant representing an empty bag of the given sort. + """ + Create a constant representing an empty bag of the given sort. - :param sort: the sort of the bag elements. - :return: the empty bag constant + :param sort: The sort of the bag elements. + :return: The empty bag constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkEmptyBag(s.csort) return term def mkSepEmp(self): - """Create a separation logic empty term. + """ + Create a separation logic empty term. - .. warning:: This method is experimental and may change in future - versions. + .. warning:: This method is experimental and may change in future + versions. - :return: the separation logic empty term + :return: The separation logic empty term. """ cdef Term term = Term(self) term.cterm = self.csolver.mkSepEmp() return term def mkSepNil(self, Sort sort): - """Create a separation logic nil term. + """ + Create a separation logic nil term. - .. warning:: This method is experimental and may change in future - versions. + .. warning:: This method is experimental and may change in future + versions. - :param sort: the sort of the nil term - :return: the separation logic nil term + :param sort: The sort of the nil term. + :return: The separation logic nil term. """ cdef Term term = Term(self) term.cterm = self.csolver.mkSepNil(sort.csort) @@ -1195,12 +1334,15 @@ cdef class Solver: def mkString(self, str s, useEscSequences = None): """ - Create a String constant from a `str` which may contain SMT-LIB - compatible escape sequences like ``\\u1234`` to encode unicode characters. + Create a String constant from a ``str`` which may contain SMT-LIB + compatible escape sequences like ``\\u1234`` to encode unicode + characters. - :param s: the string this constant represents - :param useEscSequences: determines whether escape sequences in `s` should be converted to the corresponding unicode character - :return: the String constant + :param s: The string this constant represents. + :param useEscSequences: Determines whether escape sequences in `s` + should be converted to the corresponding + unicode character + :return: The String constant. """ cdef Term term = Term(self) cdef Py_ssize_t size @@ -1214,20 +1356,22 @@ cdef class Solver: return term def mkEmptySequence(self, Sort sort): - """Create an empty sequence of the given element sort. + """ + Create an empty sequence of the given element sort. - :param sort: The element sort of the sequence. - :return: the empty sequence with given element sort. + :param sort: The element sort of the sequence. + :return: The empty sequence with given element sort. """ cdef Term term = Term(self) term.cterm = self.csolver.mkEmptySequence(sort.csort) return term def mkUniverseSet(self, Sort sort): - """Create a universe set of the given sort. + """ + Create a universe set of the given sort. - :param sort: the sort of the set elements - :return: the universe set constant + :param sort: The sort of the set elements + :return: The universe set constant """ cdef Term term = Term(self) term.cterm = self.csolver.mkUniverseSet(sort.csort) @@ -1236,15 +1380,19 @@ cdef class Solver: @expand_list_arg(num_req_args=0) def mkBitVector(self, *args): """ - Supports the following arguments: + Create bit-vector value. - - ``Term mkBitVector(int size, int val=0)`` - - ``Term mkBitVector(int size, string val, int base)`` + Supports the following arguments: - :return: a bit-vector literal term - :param size: an integer size. - :param val: an integer representating the value, in the first form. In the second form, a string representing the value. - :param base: the base of the string representation (second form only) + - ``Term mkBitVector(int size, int val=0)`` + - ``Term mkBitVector(int size, string val, int base)`` + + :return: A Term representing a bit-vector value. + :param size: The bit-width. + :param val: An integer representating the value, in the first form. + In the second form, a string representing the value. + :param base: The base of the string representation (second form + only). """ cdef Term term = Term(self) if len(args) == 0: @@ -1285,100 +1433,111 @@ cdef class Solver: def mkConstArray(self, Sort sort, Term val): """ - Create a constant array with the provided constant value stored at every - index + Create a constant array with the provided constant value stored at + every index - :param sort: the sort of the constant array (must be an array sort) - :param val: the constant value to store (must match the sort's element sort) - :return: the constant array term - """ + :param sort: The sort of the constant array (must be an array sort). + :param val: The constant value to store (must match the sort's + element sort). + :return: The constant array term. + """ cdef Term term = Term(self) term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm) return term def mkFloatingPointPosInf(self, int exp, int sig): - """Create a positive infinity floating-point constant. + """ + Create a positive infinity floating-point constant. - :param exp: Number of bits in the exponent - :param sig: Number of bits in the significand - :return: the floating-point constant + :param exp: Number of bits in the exponent. + :param sig: Number of bits in the significand. + :return: The floating-point constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkFloatingPointPosInf(exp, sig) return term def mkFloatingPointNegInf(self, int exp, int sig): - """Create a negative infinity floating-point constant. + """ + Create a negative infinity floating-point constant. - :param exp: Number of bits in the exponent - :param sig: Number of bits in the significand - :return: the floating-point constant + :param exp: Number of bits in the exponent. + :param sig: Number of bits in the significand. + :return: The floating-point constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkFloatingPointNegInf(exp, sig) return term def mkFloatingPointNaN(self, int exp, int sig): - """Create a not-a-number (NaN) floating-point constant. + """ + Create a not-a-number (NaN) floating-point constant. - :param exp: Number of bits in the exponent - :param sig: Number of bits in the significand - :return: the floating-point constant + :param exp: Number of bits in the exponent. + :param sig: Number of bits in the significand. + :return: The floating-point constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkFloatingPointNaN(exp, sig) return term def mkFloatingPointPosZero(self, int exp, int sig): - """Create a positive zero (+0.0) floating-point constant. + """ + Create a positive zero (+0.0) floating-point constant. - :param exp: Number of bits in the exponent - :param sig: Number of bits in the significand - :return: the floating-point constant + :param exp: Number of bits in the exponent. + :param sig: Number of bits in the significand. + :return: The floating-point constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkFloatingPointPosZero(exp, sig) return term def mkFloatingPointNegZero(self, int exp, int sig): - """Create a negative zero (+0.0) floating-point constant. + """ + Create a negative zero (+0.0) floating-point constant. - :param exp: Number of bits in the exponent - :param sig: Number of bits in the significand - :return: the floating-point constant + :param exp: Number of bits in the exponent. + :param sig: Number of bits in the significand. + :return: The floating-point constant. """ cdef Term term = Term(self) term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig) return term def mkRoundingMode(self, rm): - """Create a roundingmode constant. + """ + Create a roundingmode constant. - :param rm: the floating point rounding mode this constant represents + :param rm: The floating point rounding mode this constant + represents. """ cdef Term term = Term(self) term.cterm = self.csolver.mkRoundingMode( rm.value) return term def mkFloatingPoint(self, int exp, int sig, Term val): - """Create a floating-point constant. + """ + Create a floating-point constant. - :param exp: Size of the exponent - :param sig: Size of the significand - :param val: Value of the floating-point constant as a bit-vector term + :param exp: Size of the exponent. + :param sig: Size of the significand. + :param val: Value of the floating-point constant as a bit-vector + term. """ cdef Term term = Term(self) term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm) return term def mkCardinalityConstraint(self, Sort sort, int index): - """Create cardinality constraint. + """ + Create cardinality constraint. - .. warning:: This method is experimental and may change in future - versions. + .. warning:: This method is experimental and may change in future + versions. - :param sort: Sort of the constraint - :param index: The upper bound for the cardinality of the sort + :param sort: Sort of the constraint. + :param index: The upper bound for the cardinality of the sort. """ cdef Term term = Term(self) term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index) @@ -1386,18 +1545,19 @@ cdef class Solver: def mkConst(self, Sort sort, symbol=None): """ - Create (first-order) constant (0-arity function symbol). + Create (first-order) constant (0-arity function symbol). - SMT-LIB: + SMT-LIB: - .. code-block:: smtlib + .. code-block:: smtlib - ( declare-const ) - ( declare-fun ( ) ) + ( declare-const ) + ( declare-fun ( ) ) - :param sort: the sort of the constant - :param symbol: the name of the constant. If None, a default symbol is used. - :return: the first-order constant + :param sort: The sort of the constant. + :param symbol: The name of the constant. If None, a default symbol + is used. + :return: The first-order constant. """ cdef Term term = Term(self) if symbol is None: @@ -1409,12 +1569,12 @@ cdef class Solver: def mkVar(self, Sort sort, symbol=None): """ - Create a bound variable to be used in a binder (i.e. a quantifier, a - lambda, or a witness binder). + Create a bound variable to be used in a binder (i.e. a quantifier, + a lambda, or a witness binder). - :param sort: the sort of the variable - :param symbol: the name of the variable - :return: the variable + :param sort: The sort of the variable. + :param symbol: The name of the variable. + :return: The variable. """ cdef Term term = Term(self) if symbol is None: @@ -1426,19 +1586,22 @@ cdef class Solver: def mkDatatypeConstructorDecl(self, str name): """ - :param name: the constructor's name - :return: the DatatypeConstructorDecl + Create datatype constructor declaration. + + :param name: The name of the constructor. + :return: The datatype constructor declaration. """ cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self) ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode()) return ddc def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None): - """Create a datatype declaration. + """ + Create a datatype declaration. - :param name: the name of the datatype - :param isCoDatatype: true if a codatatype is to be constructed - :return: the DatatypeDecl + :param name: The name of the datatype. + :param isCoDatatype: True if a codatatype is to be constructed. + :return: The datatype declaration. """ cdef DatatypeDecl dd = DatatypeDecl(self) cdef vector[c_Sort] v @@ -1448,82 +1611,85 @@ cdef class Solver: dd.cdd = self.csolver.mkDatatypeDecl(name.encode()) elif sorts_or_bool is not None and isCoDatatype is None: if isinstance(sorts_or_bool, bool): - dd.cdd = self.csolver.mkDatatypeDecl( name.encode(), - sorts_or_bool) + dd.cdd = self.csolver.mkDatatypeDecl( + name.encode(), sorts_or_bool) elif isinstance(sorts_or_bool, Sort): - dd.cdd = self.csolver.mkDatatypeDecl( name.encode(), - ( sorts_or_bool).csort) + dd.cdd = self.csolver.mkDatatypeDecl( + name.encode(), + ( sorts_or_bool).csort) elif isinstance(sorts_or_bool, list): for s in sorts_or_bool: v.push_back(( s).csort) - dd.cdd = self.csolver.mkDatatypeDecl( name.encode(), - v) + dd.cdd = self.csolver.mkDatatypeDecl( + name.encode(), + v) else: raise ValueError("Unhandled second argument type {}" .format(type(sorts_or_bool))) elif sorts_or_bool is not None and isCoDatatype is not None: if isinstance(sorts_or_bool, Sort): - dd.cdd = self.csolver.mkDatatypeDecl( name.encode(), - ( sorts_or_bool).csort, - isCoDatatype) + dd.cdd = self.csolver.mkDatatypeDecl( + name.encode(), + ( sorts_or_bool).csort, + isCoDatatype) elif isinstance(sorts_or_bool, list): for s in sorts_or_bool: v.push_back(( s).csort) - dd.cdd = self.csolver.mkDatatypeDecl( name.encode(), - v, - isCoDatatype) + dd.cdd = self.csolver.mkDatatypeDecl( + name.encode(), + v, + isCoDatatype) else: raise ValueError("Unhandled second argument type {}" .format(type(sorts_or_bool))) else: - raise ValueError("Can't create DatatypeDecl with {}".format([type(a) - for a in [name, - sorts_or_bool, - isCoDatatype]])) + raise ValueError("Can't create DatatypeDecl with {}".format( + [type(a) for a in [name, sorts_or_bool, isCoDatatype]])) return dd def simplify(self, Term t): """ - Simplify a formula without doing "much" work. Does not involve the - SAT Engine in the simplification, but uses the current definitions, - assertions, and the current partial model, if one has been constructed. - It also involves theory normalization. + Simplify a formula without doing "much" work. Does not involve the + SAT Engine in the simplification, but uses the current definitions, + assertions, and the current partial model, if one has been + constructed. It also involves theory normalization. - .. warning:: This method is experimental and may change in future - versions. + .. warning:: This method is experimental and may change in future + versions. - :param t: the formula to simplify - :return: the simplified formula + :param t: The formula to simplify. + :return: The simplified formula. """ cdef Term term = Term(self) term.cterm = self.csolver.simplify(t.cterm) return term def assertFormula(self, Term term): - """ Assert a formula + """ + Assert a formula - SMT-LIB: + SMT-LIB: - .. code-block:: smtlib + .. code-block:: smtlib - ( assert ) + ( assert ) - :param term: the formula to assert + :param term: The formula to assert. """ self.csolver.assertFormula(term.cterm) def checkSat(self): """ - Check satisfiability. + Check satisfiability. - SMT-LIB: + SMT-LIB: - .. code-block:: smtlib + .. code-block:: smtlib - ( check-sat ) + ( check-sat ) - :return: the result of the satisfiability check. + :return: The result of the satisfiability check. """ cdef Result r = Result() r.cr = self.csolver.checkSat() @@ -1531,12 +1697,13 @@ cdef class Solver: def mkSygusGrammar(self, boundVars, ntSymbols): """ - Create a SyGuS grammar. The first non-terminal is treated as the - starting non-terminal, so the order of non-terminals matters. + Create a SyGuS grammar. The first non-terminal is treated as the + starting non-terminal, so the order of non-terminals matters. - :param boundVars: the parameters to corresponding synth-fun/synth-inv - :param ntSymbols: the pre-declaration of the non-terminal symbols - :return: the grammar + :param boundVars: The parameters to corresponding + synth-fun/synth-inv. + :param ntSymbols: The pre-declaration of the non-terminal symbols. + :return: The grammar. """ cdef Grammar grammar = Grammar(self) cdef vector[c_Term] bvc @@ -1549,17 +1716,18 @@ cdef class Solver: return grammar def declareSygusVar(self, str symbol, Sort sort): - """Append symbol to the current list of universal variables. + """ + Append symbol to the current list of universal variables. - SyGuS v2: + SyGuS v2: - .. code-block:: smtlib + .. code-block:: smtlib - ( declare-var ) + ( declare-var ) - :param sort: the sort of the universal variable - :param symbol: the name of the universal variable - :return: the universal variable + :param sort: The sort of the universal variable. + :param symbol: The name of the universal variable. + :return: The universal variable. """ cdef Term term = Term(self) term.cterm = self.csolver.declareSygusVar(symbol.encode(), sort.csort) @@ -1567,65 +1735,66 @@ cdef class Solver: def addSygusConstraint(self, Term t): """ - Add a formula to the set of SyGuS constraints. + Add a formula to the set of SyGuS constraints. - SyGuS v2: + SyGuS v2: - .. code-block:: smtlib + .. code-block:: smtlib - ( constraint ) + ( constraint ) - :param term: the formula to add as a constraint + :param term: The formula to add as a constraint. """ self.csolver.addSygusConstraint(t.cterm) def addSygusAssume(self, Term t): """ - Add a formula to the set of Sygus assumptions. + Add a formula to the set of Sygus assumptions. - SyGuS v2: + SyGuS v2: - .. code-block:: smtlib + .. code-block:: smtlib - ( assume ) + ( assume ) - :param term: the formuula to add as an assumption + :param term: The formuula to add as an assumption. """ self.csolver.addSygusAssume(t.cterm) def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f): """ - Add a set of SyGuS constraints to the current state that correspond to an - invariant synthesis problem. + Add a set of SyGuS constraints to the current state that correspond + to an invariant synthesis problem. - SyGuS v2: + SyGuS v2: - .. code-block:: smtlib + .. code-block:: smtlib - ( inv-constraint 
   )
+                ( inv-constraint  
   )
 
-        :param inv: the function-to-synthesize
-        :param pre: the pre-condition
-        :param trans: the transition relation
-        :param post: the post-condition
+            :param inv: The function-to-synthesize.
+            :param pre: The pre-condition.
+            :param trans: The transition relation.
+            :param post: The post-condition.
         """
-        self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
+        self.csolver.addSygusInvConstraint(
+                inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
 
     def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
         """
-        Synthesize n-ary function following specified syntactic constraints.
+            Synthesize n-ary function following specified syntactic constraints.
 
-        SyGuS v2:
+            SyGuS v2:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( synth-fun  ( * )   )
+                ( synth-fun  ( * )   )
 
-        :param symbol: the name of the function
-        :param boundVars: the parameters to this function
-        :param sort: the sort of the return value of this function
-        :param grammar: the syntactic constraints
-        :return: the function
+            :param symbol: The name of the function.
+            :param boundVars: The parameters to this function.
+            :param sort: The sort of the return value of this function.
+            :param grammar: The syntactic constraints.
+            :return: The function.
         """
         cdef Term term = Term(self)
         cdef vector[c_Term] v
@@ -1639,20 +1808,20 @@ cdef class Solver:
 
     def checkSynth(self):
         """
-        Try to find a solution for the synthesis conjecture corresponding to the
-        current list of functions-to-synthesize, universal variables and
-        constraints.
+            Try to find a solution for the synthesis conjecture corresponding
+            to the current list of functions-to-synthesize, universal variables
+            and constraints.
 
-        SyGuS v2:
+            SyGuS v2:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( check-synth )
+                ( check-synth )
 
-        :return: the result of the check, which is "solution" if the check
-                 found a solution in which case solutions are available via
-                 getSynthSolutions, "no solution" if it was determined there is
-                 no solution, or "unknown" otherwise.
+            :return: The result of the check, which is "solution" if the check
+                     found a solution in which case solutions are available via
+                     getSynthSolutions, "no solution" if it was determined
+                     there is no solution, or "unknown" otherwise.
         """
         cdef SynthResult r = SynthResult()
         r.cr = self.csolver.checkSynth()
@@ -1660,21 +1829,22 @@ cdef class Solver:
 
     def checkSynthNext(self):
         """
-        Try to find a next solution for the synthesis conjecture corresponding
-        to the current list of functions-to-synthesize, universal variables and
-        constraints. Must be called immediately after a successful call to
-        check-synth or check-synth-next. Requires incremental mode.
+            Try to find a next solution for the synthesis conjecture
+            corresponding to the current list of functions-to-synthesize,
+            universal variables and constraints. Must be called immediately
+            after a successful call to check-synth or check-synth-next.
+            Requires incremental mode.
 
-        SyGuS v2:
+            SyGuS v2:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( check-synth )
+                ( check-synth )
 
-        :return: the result of the check, which is "solution" if the check
-                 found a solution in which case solutions are available via
-                 getSynthSolutions, "no solution" if it was determined there is
-                 no solution, or "unknown" otherwise.
+            :return: The result of the check, which is "solution" if the check
+                     found a solution in which case solutions are available via
+                     getSynthSolutions, "no solution" if it was determined
+                     there is no solution, or "unknown" otherwise.
         """
         cdef SynthResult r = SynthResult()
         r.cr = self.csolver.checkSynthNext()
@@ -1682,11 +1852,11 @@ cdef class Solver:
 
     def getSynthSolution(self, Term term):
         """
-        Get the synthesis solution of the given term. This method should be
-        called immediately after the solver answers unsat for sygus input.
+            Get the synthesis solution of the given term. This method should be
+            called immediately after the solver answers unsat for sygus input.
 
-        :param term: the term for which the synthesis solution is queried
-        :return: the synthesis solution of the given term
+            :param term: The term for which the synthesis solution is queried.
+            :return: The synthesis solution of the given term.
         """
         cdef Term t = Term(self)
         t.cterm = self.csolver.getSynthSolution(term.cterm)
@@ -1694,11 +1864,13 @@ cdef class Solver:
 
     def getSynthSolutions(self, list terms):
         """
-        Get the synthesis solutions of the given terms. This method should be
-        called immediately after the solver answers unsat for sygus input.
+            Get the synthesis solutions of the given terms. This method should
+            be called immediately after the solver answers unsat for sygus
+            input.
 
-        :param terms: the terms for which the synthesis solutions is queried
-        :return: the synthesis solutions of the given terms
+            :param terms: The terms for which the synthesis solutions is
+                          queried.
+            :return: The synthesis solutions of the given terms.
         """
         result = []
         cdef vector[c_Term] vec
@@ -1714,41 +1886,47 @@ cdef class Solver:
 
     def synthInv(self, symbol, bound_vars, Grammar grammar=None):
         """
-        Synthesize invariant.
+            Synthesize invariant.
 
-        SyGuS v2:
+            SyGuS v2:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( synth-inv  ( * )  )
+                ( synth-inv  ( * )  )
 
-        :param symbol: the name of the invariant
-        :param boundVars: the parameters to this invariant
-        :param grammar: the syntactic constraints
-        :return: the invariant
+            :param symbol: The name of the invariant.
+            :param boundVars: The parameters to this invariant.
+            :param grammar: The syntactic constraints.
+            :return: The invariant.
         """
         cdef Term term = Term(self)
         cdef vector[c_Term] v
         for bv in bound_vars:
             v.push_back(( bv).cterm)
         if grammar is None:
-            term.cterm = self.csolver.synthInv(symbol.encode(),  v)
+            term.cterm = self.csolver.synthInv(
+                    symbol.encode(),  v)
         else:
-            term.cterm = self.csolver.synthInv(symbol.encode(),  v, grammar.cgrammar)
+            term.cterm = self.csolver.synthInv(
+                    symbol.encode(),
+                     v,
+                    grammar.cgrammar)
         return term
 
     @expand_list_arg(num_req_args=0)
     def checkSatAssuming(self, *assumptions):
-        """ Check satisfiability assuming the given formula.
+        """
+            Check satisfiability assuming the given formula.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( check-sat-assuming (  ) )
+                ( check-sat-assuming (  ) )
 
-        :param assumptions: the formulas to assume, as a list or as distinct arguments
-        :return: the result of the satisfiability check.
+            :param assumptions: The formulas to assume, as a list or as
+                                distinct arguments.
+            :return: The result of the satisfiability check.
         """
         cdef Result r = Result()
         # used if assumptions is a list of terms
@@ -1761,17 +1939,18 @@ cdef class Solver:
     @expand_list_arg(num_req_args=1)
     def declareDatatype(self, str symbol, *ctors):
         """
-        Create datatype sort.
+            Create datatype sort.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( declare-datatype   )
+                ( declare-datatype   )
 
-        :param symbol: the name of the datatype sort
-        :param ctors: the constructor declarations of the datatype sort, as a list or as distinct arguments
-        :return: the datatype sort
+            :param symbol: The name of the datatype sort.
+            :param ctors: The constructor declarations of the datatype sort, as
+                          a list or as distinct arguments.
+            :return: The datatype sort.
         """
         cdef Sort sort = Sort(self)
         cdef vector[c_DatatypeConstructorDecl] v
@@ -1782,18 +1961,19 @@ cdef class Solver:
         return sort
 
     def declareFun(self, str symbol, list sorts, Sort sort):
-        """Declare n-ary function symbol.
+        """
+            Declare n-ary function symbol.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( declare-fun  ( * )  )
+                ( declare-fun  ( * )  )
 
-        :param symbol: the name of the function
-        :param sorts: the sorts of the parameters to this function
-        :param sort: the sort of the return value of this function
-        :return: the function
+            :param symbol: The name of the function.
+            :param sorts: The sorts of the parameters to this function.
+            :param sort: The sort of the return value of this function.
+            :return: The function.
         """
         cdef Term term = Term(self)
         cdef vector[c_Sort] v
@@ -1805,42 +1985,47 @@ cdef class Solver:
         return term
 
     def declareSort(self, str symbol, int arity):
-        """Declare uninterpreted sort.
+        """
+            Declare uninterpreted sort.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( declare-sort   )
+                ( declare-sort   )
 
-        .. note::
-          This corresponds to :py:meth:`Solver.mkUninterpretedSort()` if
-          arity = 0, and to
-          :py:meth:`Solver.mkUninterpretedSortConstructorSort()` if arity > 0.
+            .. note::
 
-        :param symbol: the name of the sort
-        :param arity: the arity of the sort
-        :return: the sort
+              This corresponds to :py:meth:`Solver.mkUninterpretedSort()` if
+              arity = 0, and to
+              :py:meth:`Solver.mkUninterpretedSortConstructorSort()` if
+              arity > 0.
+
+            :param symbol: The name of the sort.
+            :param arity: The arity of the sort.
+            :return: The sort.
         """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.declareSort(symbol.encode(), arity)
         return sort
 
     def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
-        """Define n-ary function.
+        """
+            Define n-ary function.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( define-fun  )
+                ( define-fun  )
 
-        :param symbol: the name of the function
-        :param bound_vars: the parameters to this function
-        :param sort: the sort of the return value of this function
-        :param term: the function body
-        :param glbl: determines whether this definition is global (i.e. persists when popping the context)
-        :return: the function
+            :param symbol: The name of the function.
+            :param bound_vars: The parameters to this function.
+            :param sort: The sort of the return value of this function.
+            :param term: The function body.
+            :param glbl: Determines whether this definition is global (i.e.
+                         persists when popping the context).
+            :return: The function.
         """
         cdef Term fun = Term(self)
         cdef vector[c_Term] v
@@ -1855,27 +2040,28 @@ cdef class Solver:
         return fun
 
     def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
-        """Define recursive functions.
-
-        Supports two uses:
+        """
+            Define recursive functions.
 
-        - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
-        - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
+            Supports the following arguments:
 
+            - ``Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
+            - ``Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)``
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( define-funs-rec ( ^n ) ( ^n ) )
+                ( define-funs-rec ( ^n ) ( ^n ) )
 
-        Create elements of parameter ``funs`` with mkConst().
+            Create elements of parameter ``funs`` with :py:meth:`mkConst() `.
 
-        :param funs: the sorted functions
-        :param bound_vars: the list of parameters to the functions
-        :param terms: the list of function bodies of the functions
-        :param global: determines whether this definition is global (i.e. persists when popping the context)
-        :return: the function
+            :param funs: The sorted functions.
+            :param bound_vars: The list of parameters to the functions.
+            :param terms: The list of function bodies of the functions.
+            :param global: Determines whether this definition is global (i.e.
+                           persists when popping the context).
+            :return: The function.
         """
         cdef Term term = Term(self)
         cdef vector[c_Term] v
@@ -1897,21 +2083,23 @@ cdef class Solver:
         return term
 
     def defineFunsRec(self, funs, bound_vars, terms):
-        """Define recursive functions.
+        """
+            Define recursive functions.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( define-funs-rec ( ^n ) ( ^n ) )
+                ( define-funs-rec ( ^n ) ( ^n ) )
 
-        Create elements of parameter ``funs`` with mkConst().
+            Create elements of parameter ``funs`` with :py:meth:`mkConst() `.
 
-        :param funs: the sorted functions
-        :param bound_vars: the list of parameters to the functions
-        :param terms: the list of function bodies of the functions
-        :param global: determines whether this definition is global (i.e. persists when popping the context)
-        :return: the function
+            :param funs: The sorted functions.
+            :param bound_vars: The list of parameters to the functions.
+            :param terms: The list of function bodies of the functions.
+            :param global: Determines whether this definition is global (i.e.
+                           persists when popping the context).
+            :return: The function.
         """
         cdef vector[c_Term] vf
         cdef vector[vector[c_Term]] vbv
@@ -1931,38 +2119,40 @@ cdef class Solver:
             vf.push_back(( t).cterm)
 
     def getProof(self):
-        """Get the refutation proof
+        """
+            Get the refutation proof
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
-        
-           (get-proof)
+            .. code-block:: smtlib
 
-        Requires to enable option
-        :ref:`produce-proofs `.
+               (get-proof)
 
-        .. warning:: This method is experimental and may change in future
-                     versions.
+            Requires to enable option
+            :ref:`produce-proofs `.
 
-        :return: a string representing the proof, according to the value of
-                 proof-format-mode.
+            .. warning:: This method is experimental and may change in future
+                         versions.
+
+            :return: A string representing the proof, according to the value of
+                     :ref:`proof-format-mode `.
         """
         return self.csolver.getProof()
 
     def getLearnedLiterals(self):
-        """Get a list of literals that are entailed by the current set of assertions
+        """
+            Get a list of literals that are entailed by the current set of assertions
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( get-learned-literals )
+                ( get-learned-literals )
 
-        .. warning:: This method is experimental and may change in future
-                     versions.
+            .. warning:: This method is experimental and may change in future
+                         versions.
 
-        :return: the list of literals
+            :return: The list of literals.
         """
         lits = []
         for a in self.csolver.getLearnedLiterals():
@@ -1972,15 +2162,16 @@ cdef class Solver:
         return lits
 
     def getAssertions(self):
-        """Get the list of asserted formulas.
+        """
+            Get the list of asserted formulas.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( get-assertions )
+                ( get-assertions )
 
-        :return: the list of asserted formulas
+            :return: The list of asserted formulas.
         """
         assertions = []
         for a in self.csolver.getAssertions():
@@ -1991,45 +2182,51 @@ cdef class Solver:
 
     def getInfo(self, str flag):
         """
-        Get info from the solver.
+            Get info from the solver.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( get-info  )
+                ( get-info  )
 
-        :param flag: the info flag
-        :return: the info
+            :param flag: The info flag.
+            :return: The info.
         """
         return self.csolver.getInfo(flag.encode())
 
     def getOption(self, str option):
-        """Get the value of a given option.
+        """
+            Get the value of a given option.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( get-option  )
+                ( get-option  )
 
-        :param option: the option for which the value is queried
-        :return: a string representation of the option value
+            :param option: The option for which the value is queried.
+            :return: A string representation of the option value.
         """
         return self.csolver.getOption(option.encode()).decode()
 
     def getOptionNames(self):
-        """Get all option names that can be used with `setOption`, `getOption` and `getOptionInfo`.
+        """
+            Get all option names that can be used with
+            :py:meth:`Solver.setOption()`, :py:meth:`Solver.getOption()`
+            and :py:meth:`Solver.getOptionInfo()`.
 
-        :return: all option names
+        :return: All option names.
         """
         return [s.decode() for s in self.csolver.getOptionNames()]
 
     def getOptionInfo(self, str option):
-        """Get some information about the given option. Check the `OptionInfo`
-        class for more details on which information is available.
+        """
+            Get some information about the given option.
+            Returns the information provided by the C++
+            :cpp:func:`OptionInfo ` as a dictionary.
 
-        :return: information about the given option
+            :return: Information about the given option.
         """
         # declare all the variables we may need later
         cdef c_OptionInfo.ValueInfo[c_bool] vib
@@ -2069,24 +2266,30 @@ cdef class Solver:
             nii = c_getVariant[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo)
             res['current'] = nii.currentValue
             res['default'] = nii.defaultValue
-            res['minimum'] = nii.minimum.value() if nii.minimum.has_value() else None
-            res['maximum'] = nii.maximum.value() if nii.maximum.has_value() else None
+            res['minimum'] = nii.minimum.value() \
+                if nii.minimum.has_value() else None
+            res['maximum'] = nii.maximum.value() \
+                if nii.maximum.has_value() else None
         elif c_holds[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo):
             # it's a uint64_t
             res['type'] = int
             niu = c_getVariant[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo)
             res['current'] = niu.currentValue
             res['default'] = niu.defaultValue
-            res['minimum'] = niu.minimum.value() if niu.minimum.has_value() else None
-            res['maximum'] = niu.maximum.value() if niu.maximum.has_value() else None
+            res['minimum'] = niu.minimum.value() \
+                if niu.minimum.has_value() else None
+            res['maximum'] = niu.maximum.value() \
+                if niu.maximum.has_value() else None
         elif c_holds[c_OptionInfo.NumberInfo[double]](oi.valueInfo):
             # it's a double
             res['type'] = float
             nid = c_getVariant[c_OptionInfo.NumberInfo[double]](oi.valueInfo)
             res['current'] = nid.currentValue
             res['default'] = nid.defaultValue
-            res['minimum'] = nid.minimum.value() if nid.minimum.has_value() else None
-            res['maximum'] = nid.maximum.value() if nid.maximum.has_value() else None
+            res['minimum'] = nid.minimum.value() \
+                if nid.minimum.has_value() else None
+            res['maximum'] = nid.maximum.value() \
+                if nid.maximum.has_value() else None
         elif c_holds[c_OptionInfo.ModeInfo](oi.valueInfo):
             # it's a mode
             res['type'] = 'mode'
@@ -2097,8 +2300,11 @@ cdef class Solver:
         return res
 
     def getOptionNames(self):
-       """Get all option names that can be used with `setOption`, `getOption` and `getOptionInfo`.
-       :return: all option names
+       """
+           Get all option names that can be used with
+           :py:meth:`Solver.setOption()`, :py:meth:`Solver.getOption()` and
+           :py:meth:`Solver.getOptionInfo()`.
+           :return: All option names.
        """
        result = []
        for n in self.csolver.getOptionNames():
@@ -2107,17 +2313,18 @@ cdef class Solver:
 
     def getUnsatAssumptions(self):
         """
-        Get the set of unsat ("failed") assumptions.
+            Get the set of unsat ("failed") assumptions.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( get-unsat-assumptions )
+                ( get-unsat-assumptions )
 
-        Requires to enable option :ref:`produce-unsat-assumptions `.
+            Requires to enable option :ref:`produce-unsat-assumptions
+            `.
 
-        :return: the set of unsat assumptions.
+            :return: The set of unsat assumptions.
         """
         assumptions = []
         for a in self.csolver.getUnsatAssumptions():
@@ -2127,24 +2334,27 @@ cdef class Solver:
         return assumptions
 
     def getUnsatCore(self):
-        """Get the unsatisfiable core.
+        """
+            Get the unsatisfiable core.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-          (get-unsat-core)
+              (get-unsat-core)
 
-        Requires to enable option :ref:`produce-unsat-cores `.
+            Requires to enable option :ref:`produce-unsat-cores
+            `.
 
-        .. note::
-          In contrast to SMT-LIB, the API does not distinguish between named and
-          unnamed assertions when producing an unsatisfiable core. Additionally,
-          the API allows this option to be called after a check with assumptions.
-          A subset of those assumptions may be included in the unsatisfiable core
-          returned by this method.
+            .. note::
 
-        :return: a set of terms representing the unsatisfiable core
+              In contrast to SMT-LIB, the API does not distinguish between
+              named and unnamed assertions when producing an unsatisfiable
+              core. Additionally, the API allows this option to be called after
+              a check with assumptions. A subset of those assumptions may be
+              included in the unsatisfiable core returned by this method.
+
+            :return: A set of terms representing the unsatisfiable core.
         """
         core = []
         for a in self.csolver.getUnsatCore():
@@ -2155,13 +2365,17 @@ cdef class Solver:
 
     def getDifficulty(self):
         """
-            Get a difficulty estimate for an asserted formula. This method is intended to be called immediately after 
-            any response to a checkSat.
+            Get a difficulty estimate for an asserted formula. This method is
+            intended to be called immediately after any response to a
+            :py:meth:`Solver.checkSat()` call.
 
             .. warning:: This method is experimental and may change in future
                          versions.
 
-            :return: a map from (a subset of) the input assertions to a real value that is an estimate of how difficult each assertion was to solver. Unmentioned assertions can be assumed to have zero difficulty.
+            :return: A map from (a subset of) the input assertions to a real
+                     value that is an estimate of how difficult each assertion
+                     was to solver. Unmentioned assertions can be assumed to
+                     have zero difficulty.
         """
         diffi = {}
         for p in self.csolver.getDifficulty():
@@ -2178,16 +2392,17 @@ cdef class Solver:
         return diffi
 
     def getValue(self, Term t):
-        """Get the value of the given term in the current model.
+        """
+            Get the value of the given term in the current model.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( get-value (  ) )
+                ( get-value (  ) )
 
-        :param term: the term for which the value is queried
-        :return: the value of the given term
+            :param term: The term for which the value is queried.
+            :return: The value of the given term.
         """
         cdef Term term = Term(self)
         term.cterm = self.csolver.getValue(t.cterm)
@@ -2195,12 +2410,12 @@ cdef class Solver:
 
     def getModelDomainElements(self, Sort s):
         """
-        Get the domain elements of uninterpreted sort s in the current model. The
-        current model interprets s as the finite sort whose domain elements are
-        given in the return value of this method.
+            Get the domain elements of uninterpreted sort s in the current
+            model. The current model interprets s as the finite sort whose
+            domain elements are given in the return value of this method.
 
-        :param s: The uninterpreted sort in question
-        :return: the domain elements of s in the current model
+            :param s: The uninterpreted sort in question.
+            :return: The domain elements of s in the current model.
         """
         result = []
         cresult = self.csolver.getModelDomainElements(s.csort)
@@ -2212,122 +2427,129 @@ cdef class Solver:
 
     def isModelCoreSymbol(self, Term v):
         """
-        This returns false if the model value of free constant v was not
-        essential for showing the satisfiability of the last call to checkSat
-        using the current model. This method will only return false (for any v)
-        if the model-cores option has been set.
+            This returns False if the model value of free constant v was not
+            essential for showing the satisfiability of the last call to
+            checkSat using the current model. This method will only return
+            false (for any v) if the model-cores option has been set.
 
-        .. warning:: This method is experimental and may change in future
-                     versions.
+            .. warning:: This method is experimental and may change in future
+                         versions.
 
-        :param v: The term in question
-        :return: true if v is a model core symbol
+            :param v: The term in question.
+            :return: True if v is a model core symbol.
         """
         return self.csolver.isModelCoreSymbol(v.cterm)
 
     def getQuantifierElimination(self, Term term):
-        """Do quantifier elimination.
+        """
+            Do quantifier elimination.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( get-qe  )
+                ( get-qe  )
 
-        Requires a logic that supports quantifier elimination.
-        Currently, the only logics supported by quantifier elimination
-        are LRA and LIA.
+            Requires a logic that supports quantifier elimination.
+            Currently, the only logics supported by quantifier elimination
+            are LRA and LIA.
 
-        .. warning:: This method is experimental and may change in future
+            .. warning:: This method is experimental and may change in future
                          versions.
 
-        :param q: a quantified formula of the form
-                :math:`Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)'
-                where
-                :math:'Q\bar{x}' is a set of quantified variables of the form
-                :math:'Q x_1...x_k' and
-                :math:'P( x_1...x_i, y_1...y_j )' is a quantifier-free formula
-        :return: a formula :math:'\phi'  such that, given the current set of formulas
-               :math:'A asserted to this solver:
-               - :math:'(A \wedge q)' :math:'(A \wedge \phi)' are equivalent
-               - :math:'\phi' is quantifier-free formula containing only free
-                 variables in :math:'y_1...y_n'.
+            :param q: A quantified formula of the form
+                      :math:`Q\\bar{x_1}\\dots Q\\bar{x}_n. P( x_1 \\dots x_i, y_1 \\dots y_j)`
+                      where
+                      :math:`Q\\bar{x}` is a set of quantified variables of the
+                      form :math:`Q x_1...x_k` and
+                      :math:`P( x_1...x_i, y_1...y_j )` is a quantifier-free
+                      formula
+            :return: A formula :math:`\\phi` such that, given the current set
+                     of formulas :math:`A` asserted to this solver:
+
+                     - :math:`(A \\wedge q)` :math:`(A \\wedge \\phi)` are
+                       equivalent
+                     - :math:`\\phi` is quantifier-free formula containing only
+                       free variables in :math:`y_1...y_n`.
         """
         cdef Term result = Term(self)
         result.cterm = self.csolver.getQuantifierElimination(term.cterm)
         return result
 
     def getQuantifierEliminationDisjunct(self, Term term):
-        """Do partial quantifier elimination, which can be used for incrementally computing
-        the result of a quantifier elimination.
+        """
+            Do partial quantifier elimination, which can be used for
+            incrementally computing the result of a quantifier elimination.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( get-qe-disjunct  )
+                ( get-qe-disjunct  )
 
-        Requires a logic that supports quantifier elimination.
-        Currently, the only logics supported by quantifier elimination
-        are LRA and LIA.
-            
-	.. warning:: This method is experimental and may change in future
+            Requires a logic that supports quantifier elimination.
+            Currently, the only logics supported by quantifier elimination
+            are LRA and LIA.
+
+	        .. warning:: This method is experimental and may change in future
                          versions.
-        
-           :param q: a quantified formula of the form
-                   @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
-                   where
-                   @f$Q\bar{x}@f$ is a set of quantified variables of the form
-                   @f$Q x_1...x_k@f$ and
-                   @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
-           :return: a formula @f$\phi@f$ such that, given the current set of formulas
-                  @f$A@f$ asserted to this solver:
-                  - @f$(A \wedge q \implies A \wedge \phi)@f$ if @f$Q@f$ is
-                    @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if
-                    @f$Q@f$ is @f$\exists@f$
-                  - @f$\phi@f$ is quantifier-free formula containing only free
-                    variables in @f$y_1...y_n@f$
-                  - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the
-                    formula
-                    @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge
-                    \neg (\phi \wedge Q_n))@f$
-                    where for each @f$i = 1...n@f$,
-                    formula @f$(\phi \wedge Q_i)@f$ is the result of calling
-                    Solver::getQuantifierEliminationDisjunct() for @f$q@f$ with the
-                    set of assertions @f$(A \wedge Q_{i-1})@f$.
-                    Similarly, if @f$Q@f$ is @f$\forall@f$, then let
-                    @f$(A \wedge Q_n)@f$ be
-                    @f$(A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge
-                    Q_n))@f$
-                    where @f$(\phi \wedge Q_i)@f$ is the same as above.
-                    In either case, we have that @f$(\phi \wedge Q_j)@f$ will
-                    eventually be true or false, for some finite j.
+
+            :param q: A quantified formula of the form
+                 :math:`Q\\bar{x_1} ... Q\\bar{x_n}. P( x_1...x_i, y_1...y_j)`
+                 where :math:`Q\\bar{x}` is a set of quantified variables of
+                 the form :math:`Q x_1...x_k` and
+                 :math:`P( x_1...x_i, y_1...y_j )` is a quantifier-free formula.
+
+            :return: A formula :math:`\\phi` such that, given the current set
+                 of formulas :math:`A` asserted to this solver:
+
+                 - :math:`(A \\wedge q \\implies A \\wedge \\phi)` if :math:`Q`
+                   is :math:`\\forall`, and
+                   :math:`(A \\wedge \\phi \\implies A \\wedge q)` if
+                   :math:`Q` is :math:`\\exists`
+                 - :math:`\\phi` is quantifier-free formula containing only
+                   free variables in :math:`y_1...y_n`
+                 - If :math:`Q` is :math:`\\exists`, let :math:`(A \\wedge Q_n)`
+                   be the formula
+                   :math:`(A \\wedge \\neg (\\phi \wedge Q_1) \\wedge ... \\wedge \\neg (\\phi \\wedge Q_n))`
+                   where for each :math:`i = 1...n`, formula
+                   :math:`(\\phi \\wedge Q_i)` is the result of calling
+                   :py:meth:`getQuantifierEliminationDisjunct()`
+                   for :math:`q` with the set of assertions
+                   :math:`(A \\wedge Q_{i-1})`.
+                   Similarly, if :math:`Q` is :math:`\\forall`, then let
+                   :math:`(A \\wedge Q_n)` be
+                   :math:`(A \\wedge (\\phi \\wedge Q_1) \\wedge ... \\wedge (\\phi \\wedge Q_n))`
+                   where :math:`(\\phi \\wedge Q_i)` is the same as above.
+                   In either case, we have that :math:`(\\phi \\wedge Q_j)`
+                   will eventually be true or false, for some finite :math:`j`.
         """
         cdef Term result = Term(self)
         result.cterm = self.csolver.getQuantifierEliminationDisjunct(term.cterm)
         return result
-    
+
     def getModel(self, sorts, consts):
-        """Get the model
+        """
+            Get the model
+
+            SMT-LIB:
 
-        SMT-LIB:
+            .. code:: smtlib
 
-        .. code:: smtlib
-        
-            (get-model)
+                (get-model)
 
-        Requires to enable option
-        :ref:`produce-models `.
+            Requires to enable option
+            :ref:`produce-models `.
 
-        .. warning:: This method is experimental and may change in future
-                     versions.
-   
-        :param sorts: The list of uninterpreted sorts that should be printed in
-                      the model.
-        :param vars: The list of free constants that should be printed in the
-                     model. A subset of these may be printed based on
-                     isModelCoreSymbol.
-        :return: a string representing the model.
+            .. warning:: This method is experimental and may change in future
+                         versions.
+
+            :param sorts: The list of uninterpreted sorts that should be
+                          printed in the model.
+            :param vars: The list of free constants that should be printed in
+                         the model. A subset of these may be printed based on
+                         :py:meth:`Solver.isModelCoreSymbol()`.
+            :return: A string representing the model.
         """
 
         cdef vector[c_Sort] csorts
@@ -2341,24 +2563,26 @@ cdef class Solver:
         return self.csolver.getModel(csorts, cconsts)
 
     def getValueSepHeap(self):
-        """When using separation logic, obtain the term for the heap.
+        """
+            When using separation logic, obtain the term for the heap.
 
-        .. warning:: This method is experimental and may change in future
-                     versions.
+            .. warning:: This method is experimental and may change in future
+                         versions.
 
-        :return: The term for the heap
+            :return: The term for the heap.
         """
         cdef Term term = Term(self)
         term.cterm = self.csolver.getValueSepHeap()
         return term
 
     def getValueSepNil(self):
-        """When using separation logic, obtain the term for nil.
+        """
+            When using separation logic, obtain the term for nil.
 
-        .. warning:: This method is experimental and may change in future
-                     versions.
+            .. warning:: This method is experimental and may change in future
+                         versions.
 
-        :return: The term for nil
+            :return: The term for nil.
         """
         cdef Term term = Term(self)
         term.cterm = self.csolver.getValueSepNil()
@@ -2366,33 +2590,34 @@ cdef class Solver:
 
     def declareSepHeap(self, Sort locType, Sort dataType):
         """
-        When using separation logic, this sets the location sort and the
-        datatype sort to the given ones. This method should be invoked exactly
-        once, before any separation logic constraints are provided.
+            When using separation logic, this sets the location sort and the
+            datatype sort to the given ones. This method should be invoked
+            exactly once, before any separation logic constraints are provided.
 
-        .. warning:: This method is experimental and may change in future
-                     versions.
+            .. warning:: This method is experimental and may change in future
+                         versions.
 
-        :param locSort: The location sort of the heap
-        :param dataSort: The data sort of the heap
+            :param locSort: The location sort of the heap.
+            :param dataSort: The data sort of the heap.
         """
         self.csolver.declareSepHeap(locType.csort, dataType.csort)
 
     def declarePool(self, str symbol, Sort sort, initValue):
-        """Declare a symbolic pool of terms with the given initial value.
+        """
+            Declare a symbolic pool of terms with the given initial value.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( declare-pool   ( * ) )
+                ( declare-pool   ( * ) )
 
-        .. warning:: This method is experimental and may change in future
-                     versions.
+            .. warning:: This method is experimental and may change in future
+                         versions.
 
-        :param symbol: The name of the pool
-        :param sort: The sort of the elements of the pool.
-        :param initValue: The initial value of the pool
+            :param symbol: The name of the pool.
+            :param sort: The sort of the elements of the pool.
+            :param initValue: The initial value of the pool.
         """
         cdef Term term = Term(self)
         cdef vector[c_Term] niv
@@ -2402,171 +2627,184 @@ cdef class Solver:
         return term
 
     def pop(self, nscopes=1):
-        """Pop ``nscopes`` level(s) from the assertion stack.
+        """
+            Pop ``nscopes`` level(s) from the assertion stack.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( pop  )
+                ( pop  )
 
-        :param nscopes: the number of levels to pop
+            :param nscopes: The number of levels to pop.
         """
         self.csolver.pop(nscopes)
 
     def push(self, nscopes=1):
-        """ Push ``nscopes`` level(s) to the assertion stack.
+        """
+            Push ``nscopes`` level(s) to the assertion stack.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( push  )
+                ( push  )
 
-        :param nscopes: the number of levels to push
+            :param nscopes: The number of levels to push.
         """
         self.csolver.push(nscopes)
 
     def resetAssertions(self):
         """
-        Remove all assertions.
+            Remove all assertions.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( reset-assertions )
+                ( reset-assertions )
 
         """
         self.csolver.resetAssertions()
 
     def setInfo(self, str keyword, str value):
-        """Set info.
+        """
+            Set info.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( set-info  )
+                ( set-info  )
 
-        :param keyword: the info flag
-        :param value: the value of the info flag
+            :param keyword: The info flag.
+            :param value: The value of the info flag.
         """
         self.csolver.setInfo(keyword.encode(), value.encode())
 
     def setLogic(self, str logic):
-        """Set logic.
+        """
+            Set logic.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( set-logic  )
+                ( set-logic  )
 
-        :param logic: the logic to set
+            :param logic: The logic to set.
         """
         self.csolver.setLogic(logic.encode())
 
     def setOption(self, str option, str value):
-        """Set option.
+        """
+            Set option.
 
-        SMT-LIB:
+            SMT-LIB:
 
-        .. code-block:: smtlib
+            .. code-block:: smtlib
 
-            ( set-option