Start python API Solver documentation (#7064)

4 files changed, 740 insertions, 104 deletions

diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst
index 3944d60ea..d815f837a 100644
--- a/docs/api/python/python.rst
+++ b/docs/api/python/python.rst
@@ -13,6 +13,7 @@ Python API Documentation
     :maxdepth: 1
 
     quickstart
+    solver
     datatype
     datatypeconstructor
     datatypeconstructordecl
diff --git a/docs/api/python/solver.rst b/docs/api/python/solver.rst
new file mode 100644
index 000000000..2147a1f76
--- /dev/null
+++ b/docs/api/python/solver.rst
@@ -0,0 +1,6 @@
+Solver
+========
+
+.. autoclass:: pycvc5.Solver
+    :members:
+    :undoc-members:
diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py
index a7b8405be..54441ca25 100644
--- a/docs/ext/smtliblexer.py
+++ b/docs/ext/smtliblexer.py
@@ -23,6 +23,9 @@ class SmtLibLexer(RegexLexer):
         'get-assignment', 'get-info', 'get-model', 'get-option', 'get-proof',
         'get-unsat-assumptions', 'get-unsat-core', 'get-value', 'pop', 'push',
         'reset', 'reset-assertions', 'set-info', 'set-logic', 'set-option',
+        # SyGuS v2
+        'declare-var', 'constraint', 'inv-constraint', 'synth-fun',
+        'check-synth', 'synth-inv', 'declare-pool',
     ]
     SORTS = [
         'Array', 'BitVec', 'Bool', 'FloatingPoint', 'Float[0-9]+', 'Int',
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 865e51cb1..91daa4883 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1,5 +1,6 @@
 from collections import defaultdict, Set
 from fractions import Fraction
+from functools import wraps
 import sys
 
 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
@@ -44,11 +45,12 @@ 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.
-    '''
+    """
     def decorator(func):
+        @wraps(func)
         def wrapper(owner, *args):
             if len(args) == num_req_args + 1 and \
                isinstance(args[num_req_args], list):
@@ -433,7 +435,7 @@ cdef class Op:
 
     def getKind(self):
         return kind(<int> self.cop.getKind())
-    
+
     def isIndexed(self):
         return self.cop.isIndexed()
 
@@ -579,6 +581,7 @@ cdef class UnknownExplanation:
 
 
 cdef class Solver:
+    """Wrapper class for :cpp:class:`cvc5::api::Solver`."""
     cdef c_Solver* csolver
 
     def __cinit__(self):
@@ -588,62 +591,113 @@ cdef class Solver:
         del self.csolver
 
     def getBooleanSort(self):
+        """:return: sort Boolean
+        """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getBooleanSort()
         return sort
 
     def getIntegerSort(self):
+        """:return: sort Integer
+        """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getIntegerSort()
         return sort
 
     def getNullSort(self):
+        """:return: sort null
+        """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getNullSort()
         return sort
 
     def getRealSort(self):
+        """:return: sort Real
+        """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getRealSort()
         return sort
 
     def getRegExpSort(self):
+        """:return: sort of RegExp
+        """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getRegExpSort()
         return sort
 
     def getRoundingModeSort(self):
+        """:return: sort RoundingMode
+        """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getRoundingModeSort()
         return sort
 
     def getStringSort(self):
+        """: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.
+
+        :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.
+
+        :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.
+
+        :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.
+
+        :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)
         return sort
 
     def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None):
-        """:return: A list of datatype sorts that correspond to dtypedecls and unresolvedSorts"""
+        """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.
+
+        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.
+
+        :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([])
         else:
@@ -668,6 +722,12 @@ cdef class Solver:
         return sorts
 
     def mkFunctionSort(self, sorts, Sort codomain):
+        """ Create 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)
         # populate a vector with dereferenced c_Sorts
@@ -685,19 +745,22 @@ cdef class Solver:
         return sort
 
     def mkParamSort(self, symbolname):
+        """ Create a sort parameter.
+
+        :param symbol: the name of the sort
+        :return: the sort parameter
+        """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.mkParamSort(symbolname.encode())
         return sort
 
     @expand_list_arg(num_req_args=0)
     def mkPredicateSort(self, *sorts):
-        '''
-        Supports the following arguments:
-                 Sort mkPredicateSort(List[Sort] sorts)
+        """Create a predicate sort.
 
-                 where sorts can also be comma-separated arguments of
-                  type 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
         for s in sorts:
@@ -707,13 +770,11 @@ cdef class Solver:
 
     @expand_list_arg(num_req_args=0)
     def mkRecordSort(self, *fields):
-        '''
-        Supports the following arguments:
-                Sort mkRecordSort(List[Tuple[str, Sort]] fields)
+        """Create a record sort
 
-                  where fields can also be comma-separated arguments of
-          type Tuple[str, 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
         cdef pair[string, c_Sort] p
@@ -727,39 +788,63 @@ cdef class Solver:
         return sort
 
     def mkSetSort(self, Sort elemSort):
+        """Create a 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.
+
+        :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.
+
+        :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):
+        """Create an uninterpreted sort.
+
+        :param symbol: the name of the sort
+        :return: the uninterpreted sort
+        """
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.mkUninterpretedSort(name.encode())
         return sort
 
     def mkSortConstructorSort(self, str symbol, size_t arity):
+        """Create a sort constructor sort.
+
+        :param symbol: the symbol of the sort
+        :param arity: the arity of the sort
+        :return: the sort constructor sort
+        """
         cdef Sort sort = Sort(self)
         sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
         return sort
 
     @expand_list_arg(num_req_args=0)
     def mkTupleSort(self, *sorts):
-        '''
-           Supports the following arguments:
-                Sort mkTupleSort(List[Sort] sorts)
+        """Create a tuple sort.
 
-                 where sorts can also be comma-separated arguments of
-                 type 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
         for s in sorts:
@@ -769,14 +854,15 @@ cdef class Solver:
 
     @expand_list_arg(num_req_args=1)
     def mkTerm(self, kind_or_op, *args):
-        '''
-            Supports the following arguments:
-                    Term mkTerm(Kind kind)
-                    Term mkTerm(Kind kind, Op child1, List[Term] children)
-                    Term mkTerm(Kind kind, List[Term] children)
-
-                where List[Term] can also be comma-separated arguments
-        '''
+        """
+        Supports the following arguments:
+
+        - ``Term mkTerm(Kind kind)``
+        - ``Term mkTerm(Kind kind, Op child1, List[Term] children)``
+        - ``Term mkTerm(Kind kind, List[Term] children)``
+
+        where ``List[Term]`` can also be comma-separated arguments
+        """
         cdef Term term = Term(self)
         cdef vector[c_Term] v
 
@@ -793,6 +879,12 @@ cdef class Solver:
         return term
 
     def mkTuple(self, sorts, terms):
+        """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
+        """
         cdef vector[c_Sort] csorts
         cdef vector[c_Term] cterms
 
@@ -806,14 +898,15 @@ cdef class Solver:
 
     @expand_list_arg(num_req_args=0)
     def mkOp(self, kind k, *args):
-        '''
+        """
         Supports the following uses:
-                Op mkOp(Kind kind)
-                Op mkOp(Kind kind, Kind k)
-                Op mkOp(Kind kind, const string& arg)
-                Op mkOp(Kind kind, uint32_t arg)
-                Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)
-        '''
+
+        - ``Op mkOp(Kind kind)``
+        - ``Op mkOp(Kind kind, Kind k)``
+        - ``Op mkOp(Kind kind, const string& arg)``
+        - ``Op mkOp(Kind kind, uint32_t arg)``
+        - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
+        """
         cdef Op op = Op(self)
         cdef vector[int] v
 
@@ -842,26 +935,48 @@ cdef class Solver:
         return op
 
     def mkTrue(self):
+        """Create a Boolean 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.
+
+        :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.
+
+        :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.
+
+        :return: a constant representing Pi
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkPi()
         return term
 
     def mkInteger(self, val):
+        """Create an integer constant.
+
+        :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(<const string &> str(val).encode())
@@ -871,21 +986,20 @@ cdef class Solver:
         return term
 
     def mkReal(self, val, den=None):
-        '''
-        Make a real number term.
-
-        Really, makes a rational term.
-
-        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.
-        '''
+        """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
+
+        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``.
+        """
         cdef Term term = Term(self)
         if den is None:
             term.cterm = self.csolver.mkReal(str(val).encode())
@@ -898,31 +1012,61 @@ cdef class Solver:
         return term
 
     def mkRegexpEmpty(self):
+        """Create a regular expression empty term.
+
+        :return: the empty term
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkRegexpEmpty()
         return term
 
     def mkRegexpSigma(self):
+        """Create a regular expression sigma term.
+
+        :return: the sigma term
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkRegexpSigma()
         return term
 
     def mkEmptySet(self, Sort s):
+        """Create a constant representing an empty set of the given sort.
+
+        :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.
+
+        :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 mkSepNil(self, Sort sort):
+        """Create a 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)
         return term
 
     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.
+
+        :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
         cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
@@ -935,22 +1079,38 @@ cdef class Solver:
         return term
 
     def mkEmptySequence(self, Sort 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.
+        """
         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.
+
+        :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)
         return term
 
     @expand_list_arg(num_req_args=0)
     def mkBitVector(self, *args):
-        '''
-            Supports the following arguments:
-            Term mkBitVector(int size, int val=0)
-            Term mkBitVector(int size, string val, int base)
-         '''
+        """
+        Supports the following arguments:
+
+        - ``Term mkBitVector(int size, int val=0)``
+        - ``Term mkBitVector(int size, string val, int base)``
+
+        :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)
+        """
         cdef Term term = Term(self)
         if len(args) == 0:
             raise ValueError("Missing arguments to mkBitVector")
@@ -989,46 +1149,97 @@ cdef class Solver:
         return term
 
     def mkConstArray(self, Sort sort, Term val):
+        """ 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
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
         return term
 
     def mkPosInf(self, int exp, int sig):
+        """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
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkPosInf(exp, sig)
         return term
 
     def mkNegInf(self, int exp, int sig):
+        """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
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkNegInf(exp, sig)
         return term
 
     def mkNaN(self, int exp, int sig):
+        """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
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkNaN(exp, sig)
         return term
 
     def mkPosZero(self, int exp, int sig):
+        """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
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkPosZero(exp, sig)
         return term
 
     def mkNegZero(self, int exp, int sig):
+        """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
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkNegZero(exp, sig)
         return term
 
     def mkRoundingMode(self, RoundingMode rm):
+        """Create a roundingmode constant.
+        
+        :param rm: the floating point rounding mode this constant represents
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
         return term
 
     def mkUninterpretedConst(self, Sort sort, int index):
+        """Create uninterpreted constant.
+
+        :param sort: Sort of the constant
+        :param index: Index of the constant
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index)
         return term
 
     def mkAbstractValue(self, index):
+        """Create an abstract value constant.
+        The given index needs to be positive.
+
+        :param index: Index of the abstract value
+        """
         cdef Term term = Term(self)
         try:
             term.cterm = self.csolver.mkAbstractValue(str(index).encode())
@@ -1039,11 +1250,31 @@ cdef class Solver:
         return term
 
     def mkFloatingPoint(self, int exp, int sig, Term val):
+        """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
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
         return term
 
     def mkConst(self, Sort sort, symbol=None):
+        """
+        Create (first-order) constant (0-arity function symbol).
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( declare-const <symbol> <sort> )
+            ( declare-fun <symbol> ( ) <sort> )
+
+        :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:
             term.cterm = self.csolver.mkConst(sort.csort)
@@ -1053,6 +1284,13 @@ cdef class Solver:
         return term
 
     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).
+
+        :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:
             term.cterm = self.csolver.mkVar(sort.csort)
@@ -1062,11 +1300,20 @@ cdef class Solver:
         return term
 
     def mkDatatypeConstructorDecl(self, str name):
+        """ :return: a datatype constructor declaration
+        :param: `name` the constructor's name
+        """
         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.
+
+        :param name: the name of the datatype
+        :param isCoDatatype: true if a codatatype is to be constructed
+        :return: the DatatypeDecl
+        """
         cdef DatatypeDecl dd = DatatypeDecl(self)
         cdef vector[c_Sort] v
 
@@ -1111,19 +1358,55 @@ cdef class Solver:
         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.
+
+        :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
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( assert <term> )
+
+        :param term: the formula to assert
+        """
         self.csolver.assertFormula(term.cterm)
 
     def checkSat(self):
+        """
+        Check satisfiability.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( check-sat )
+
+        :return: the result of the satisfiability check.
+        """
         cdef Result r = Result()
         r.cr = self.csolver.checkSat()
         return r
 
     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.
+
+        :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
         cdef vector[c_Term] ntc
@@ -1135,17 +1418,69 @@ cdef class Solver:
         return grammar
 
     def mkSygusVar(self, Sort sort, str symbol=""):
+        """Append symbol to the current list of universal variables.
+
+        SyGuS v2:
+
+        .. code-block:: smtlib
+
+            ( declare-var <symbol> <sort> )
+
+        :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.mkSygusVar(sort.csort, symbol.encode())
         return term
 
     def addSygusConstraint(self, Term t):
+        """
+        Add a formula to the set of SyGuS constraints.
+
+        SyGuS v2:
+
+        .. code-block:: smtlib
+
+            ( constraint <term> )
+
+        :param term: the formula to add as a constraint
+        """
         self.csolver.addSygusConstraint(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.
+
+        SyGuS v2:
+
+        .. code-block:: smtlib
+
+            ( inv-constraint <inv> <pre> <trans> <post> )
+
+        :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)
 
     def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
+        """
+        Synthesize n-ary function following specified syntactic constraints.
+
+        SyGuS v2:
+
+        .. code-block:: smtlib
+
+            ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
+
+        :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
         for bv in bound_vars:
@@ -1157,16 +1492,41 @@ cdef class Solver:
         return term
 
     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.
+
+        SyGuS v2:
+
+        .. code-block:: smtlib
+
+            ( check-synth )
+
+        :return: the result of the synthesis conjecture.
+        """
         cdef Result r = Result()
         r.cr = self.csolver.checkSynth()
         return r
 
     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.
+
+        :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)
         return t
 
     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.
+
+        :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
         for t in terms:
@@ -1180,6 +1540,20 @@ cdef class Solver:
 
 
     def synthInv(self, symbol, bound_vars, Grammar grammar=None):
+        """
+        Synthesize invariant.
+
+        SyGuS v2:
+
+        .. code-block:: smtlib
+
+            ( synth-inv <symbol> ( <boundVars>* ) <grammar> )
+
+        :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:
@@ -1192,13 +1566,17 @@ cdef class Solver:
 
     @expand_list_arg(num_req_args=0)
     def checkSatAssuming(self, *assumptions):
-        '''
-            Supports the following arguments:
-                 Result checkSatAssuming(List[Term] assumptions)
+        """ Check satisfiability assuming the given formula.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( check-sat-assuming ( <prop_literal> ) )
 
-                 where assumptions can also be comma-separated arguments of
-                 type (boolean) Term
-        '''
+        :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
         cdef vector[c_Term] v
@@ -1209,13 +1587,11 @@ cdef class Solver:
 
     @expand_list_arg(num_req_args=0)
     def checkEntailed(self, *assumptions):
-        '''
-            Supports the following arguments:
-                 Result checkEntailed(List[Term] assumptions)
+        """Check entailment of the given formula w.r.t. the current set of assertions.
 
-                 where assumptions can also be comma-separated arguments of
-                 type (boolean) Term
-        '''
+        :param terms: the formulas to check entailment for, as a list or as distinct arguments
+        :return: the result of the entailment check.
+        """
         cdef Result r = Result()
         # used if assumptions is a list of terms
         cdef vector[c_Term] v
@@ -1226,13 +1602,19 @@ cdef class Solver:
 
     @expand_list_arg(num_req_args=1)
     def declareDatatype(self, str symbol, *ctors):
-        '''
-            Supports the following arguments:
-                 Sort declareDatatype(str symbol, List[Term] ctors)
+        """
+        Create datatype sort.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
 
-                 where ctors can also be comma-separated arguments of
-                  type DatatypeConstructorDecl
-        '''
+            ( declare-datatype <symbol> <datatype_decl> )
+
+        :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
 
@@ -1242,6 +1624,19 @@ cdef class Solver:
         return sort
 
     def declareFun(self, str symbol, list sorts, Sort sort):
+        """Declare n-ary function symbol.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( declare-fun <symbol> ( <sort>* ) <sort> )
+
+        :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
         for s in sorts:
@@ -1252,18 +1647,44 @@ cdef class Solver:
         return term
 
     def declareSort(self, str symbol, int arity):
+        """Declare uninterpreted sort.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( declare-sort <symbol> <numeral> )
+
+        :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, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
-        '''
+        """
+        Define n-ary function.
         Supports two uses:
-                Term defineFun(str symbol, List[Term] bound_vars,
-                               Sort sort, Term term, bool glbl)
-                Term defineFun(Term fun, List[Term] bound_vars,
-                               Term term, bool glbl)
-        '''
+
+        - ``Term defineFun(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
+        - ``Term defineFun(Term fun, List[Term] bound_vars, Term term, bool glbl)``
+
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( define-fun <function_def> )
+
+        :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 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
         for bv in bound_vars:
@@ -1284,13 +1705,28 @@ cdef class Solver:
         return term
 
     def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
-        '''
+        """Define recursive functions.
+
         Supports two uses:
-                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)
-        '''
+
+        - ``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:
+
+        .. code-block:: smtlib
+
+            ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
+
+        Create elements of parameter ``funs`` with 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
+        """
         cdef Term term = Term(self)
         cdef vector[c_Term] v
         for bv in bound_vars:
@@ -1311,6 +1747,22 @@ cdef class Solver:
         return term
 
     def defineFunsRec(self, funs, bound_vars, terms):
+        """Define recursive functions.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )
+
+        Create elements of parameter ``funs`` with 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
+        """
         cdef vector[c_Term] vf
         cdef vector[vector[c_Term]] vbv
         cdef vector[c_Term] vt
@@ -1329,6 +1781,16 @@ cdef class Solver:
             vf.push_back((<Term?> t).cterm)
 
     def getAssertions(self):
+        """Get the list of asserted formulas.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-assertions )
+
+        :return: the list of asserted formulas
+        """
         assertions = []
         for a in self.csolver.getAssertions():
             term = Term(self)
@@ -1337,12 +1799,47 @@ cdef class Solver:
         return assertions
 
     def getInfo(self, str flag):
+        """Get info from the solver.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-info <info_flag> )
+
+        :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.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-option <keyword> )
+
+        :param option: the option for which the value is queried
+        :return: a string representation of the option value
+        """
         return self.csolver.getOption(option.encode())
 
     def getUnsatAssumptions(self):
+        """
+        Get the set of unsat ("failed") assumptions.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-unsat-assumptions )
+
+        Requires to enable option :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
+
+        :return: the set of unsat assumptions.
+        """
         assumptions = []
         for a in self.csolver.getUnsatAssumptions():
             term = Term(self)
@@ -1351,6 +1848,18 @@ cdef class Solver:
         return assumptions
 
     def getUnsatCore(self):
+        """Get the unsatisfiable core.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-unsat-core )
+
+        Requires to enable option :ref:`produce-unsat-cores <lbl-produce-unsat-cores>`.
+
+        :return: a set of terms representing the unsatisfiable core
+        """
         core = []
         for a in self.csolver.getUnsatCore():
             term = Term(self)
@@ -1359,11 +1868,30 @@ cdef class Solver:
         return core
 
     def getValue(self, Term t):
+        """Get the value of the given term in the current model.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-value ( <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)
         return term
 
     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.
+
+        :param s: The uninterpreted sort in question
+        :return: the domain elements of s in the current model
+        """
         result = []
         cresult = self.csolver.getModelDomainElements(s.csort)
         for e in cresult:
@@ -1373,22 +1901,58 @@ cdef class Solver:
         return result
 
     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.
+
+        :param v: The term in question
+        :return: true if v is a model core symbol
+        """
         return self.csolver.isModelCoreSymbol(v.cterm)
 
     def getSeparationHeap(self):
+        """When using separation logic, obtain the term for the heap.
+
+        :return: The term for the heap
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.getSeparationHeap()
         return term
 
-    def declareSeparationHeap(self, Sort locType, Sort dataType):
-        self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
-
     def getSeparationNilTerm(self):
+        """When using separation logic, obtain the term for nil.
+
+        :return: The term for nil
+        """
         cdef Term term = Term(self)
         term.cterm = self.csolver.getSeparationNilTerm()
         return term
 
+    def declareSeparationHeap(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.
+
+        :param locSort: The location sort of the heap
+        :param dataSort: The data sort of the heap
+        """
+        self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
+
     def declarePool(self, str symbol, Sort sort, initValue):
+        """Declare a symbolic pool of terms with the given initial value.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( declare-pool <symbol> <sort> ( <term>* ) )
+
+        :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
         for v in initValue:
@@ -1397,21 +1961,83 @@ cdef class Solver:
         return term
 
     def pop(self, nscopes=1):
+        """Pop ``nscopes`` level(s) from the assertion stack.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( pop <numeral> )
+
+        :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.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( push <numeral> )
+
+        :param nscopes: the number of levels to push
+        """
         self.csolver.push(nscopes)
 
     def resetAssertions(self):
+        """
+        Remove all assertions.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( reset-assertions )
+
+        """
         self.csolver.resetAssertions()
 
     def setInfo(self, str keyword, str value):
+        """Set info.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( set-info <attribute> )
+
+        :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.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( set-logic <symbol> )
+
+        :param logic: the logic to set
+        """
         self.csolver.setLogic(logic.encode())
 
     def setOption(self, str option, str value):
+        """Set option.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( set-option <option> )
+
+        :param option: the option name
+        :param value: the option value
+        """
         self.csolver.setOption(option.encode(), value.encode())
 
 
@@ -1508,7 +2134,7 @@ cdef class Sort:
 
     def isBag(self):
         return self.csort.isBag()
-    
+
     def isSequence(self):
         return self.csort.isSequence()
 
@@ -1578,7 +2204,7 @@ cdef class Sort:
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getTesterCodomainSort()
         return sort
-    
+
     def getFunctionArity(self):
         return self.csort.getFunctionArity()
 
@@ -1740,7 +2366,7 @@ cdef class Term:
         # lists for substitutions
         cdef vector[c_Term] ces
         cdef vector[c_Term] creplacements
-        
+
         # normalize the input parameters to be lists
         if isinstance(term_or_list_1, list):
             assert isinstance(term_or_list_2, list)
@@ -1759,7 +2385,7 @@ cdef class Term:
             # add the single elements to the vectors
             ces.push_back((<Term?> term_or_list_1).cterm)
             creplacements.push_back((<Term?> term_or_list_2).cterm)
-        
+
         # call the API substitute method with lists
         term.cterm = self.cterm.substitute(ces, creplacements)
         return term
@@ -1842,19 +2468,19 @@ cdef class Term:
 
     def isFloatingPointPosZero(self):
         return self.cterm.isFloatingPointPosZero()
-    
+
     def isFloatingPointNegZero(self):
         return self.cterm.isFloatingPointNegZero()
-    
+
     def isFloatingPointPosInf(self):
         return self.cterm.isFloatingPointPosInf()
-    
+
     def isFloatingPointNegInf(self):
         return self.cterm.isFloatingPointNegInf()
-    
+
     def isFloatingPointNaN(self):
         return self.cterm.isFloatingPointNaN()
-    
+
     def isFloatingPointValue(self):
         return self.cterm.isFloatingPointValue()
 
@@ -1888,7 +2514,7 @@ cdef class Term:
 
     def isUninterpretedValue(self):
         return self.cterm.isUninterpretedValue()
- 
+
     def getUninterpretedValue(self):
         cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue()
         cdef Sort sort = Sort(self.solver)
@@ -1914,18 +2540,18 @@ cdef class Term:
         return self.cterm.isRealValue()
 
     def getRealValue(self):
-        '''Returns the value of a real term as a Fraction'''
+        """Returns the value of a real term as a Fraction"""
         return Fraction(self.cterm.getRealValue().decode())
 
     def isBitVectorValue(self):
         return self.cterm.isBitVectorValue()
 
     def getBitVectorValue(self, base = 2):
-        '''Returns the value of a bit-vector term as a 0/1 string'''
+        """Returns the value of a bit-vector term as a 0/1 string"""
         return self.cterm.getBitVectorValue(base).decode()
 
     def toPythonObj(self):
-        '''
+        """
         Converts a constant value Term to a Python object.
 
         Currently supports:
@@ -1936,7 +2562,7 @@ cdef class Term:
           String  -- returns a Python Unicode string
           Array   -- returns a Python dict mapping indices to values
                   -- the constant base is returned as the default value
-        '''
+        """
 
         if self.isBooleanValue():
             return self.getBooleanValue()