Add RecAddDefinition and AddDefinition

This commit adds support for defining functions (recursive or not)
through defineFun and defineFunRec from the base API.

Author: caioraposo

cvc5_pythonic_api/cvc5_pythonic.py

@@ -64,7 +64,6 @@
   * FiniteDomainSort
   * Fixedpoint API
   * SMT2 file support
-  * recursive functions
 * Not missing, but different
   * Options
     * as expected
@@ -938,6 +937,44 @@ def FreshFunction(*sig):
     return Function(name, *sig)
 
 
+def RecAddDefinition(func, args, body):
+    """Define a new SMT recursive function with the given function declaration.
+    Replaces constants in `args` with bound variables.
+
+    >>> fact = Function('fact', IntSort(), IntSort())
+    >>> n = Int('n')
+    >>> RecAddDefinition(fact, n, If(n == 0, 1, n * fact(n - 1)))
+    >>> solve(Not(fact(5) == 120))
+    unsat
+    """
+    if is_app(args):
+        args = [args]
+    ctx = func.ctx
+    consts = [a.ast for a in args]
+    vars_ = [ctx.solver.mkVar(a.sort().ast, str(a)) for a in args]
+    subbed_body = body.ast.substitute(consts, vars_)
+    ctx.solver.defineFunRec(func.ast, vars_, subbed_body)
+
+
+def AddDefinition(name, args, body):
+    """Define a new SMT function with the given function declaration.
+    Replaces constants in `args` with bound variables.
+
+    >>> x, y = Ints('x y')
+    >>> minus = AddDefinition(minus, [x, y], x - y)
+    >>> solve(Not(minus(10, 5) == 5))
+    unsat
+    """
+    if is_app(args):
+        args = [args]
+    ctx = body.ctx
+    consts = [a.ast for a in args]
+    vars_ = [ctx.solver.mkVar(a.sort().ast, str(a)) for a in args]
+    subbed_body = body.ast.substitute(consts, vars_)
+    func = ctx.solver.defineFun(name, vars_, subbed_body.getSort(), subbed_body)
+    return FuncDeclRef(func, ctx)
+
+
 #########################################
 #
 # Expressions