Add RecAddDefinition and AddDefinition

[caioraposo]

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

[caioraposo]

Marked as draft as the curent implementation doesn't work due to #93.

[daniel-larraz]

According to Z3, a recursive function must be declared using RecFunction instead of Function. If you try to add a definition using RecAddDefinition to a function declared with Function, Z3 will trigger an error.

[caioraposo]

I had an implementation of RecFunction but it turned out exactly the same as Function. The reason for this distinction in z3 is because they have Z3_mk_func_decl and Z3_mk_rec_func_decl, here I believe we just need mkConst to declare a function, recursive or not.

[caioraposo]

I could add RecFunction to maintain compatibility, but do you think we should restrict the usage of RecAddDefinition like z3 does?

[HanielB]

We have discussed this in the cvc5 team and the conclusion is:

• we should support the same functionality that z3 does, so to have a RecFunction method
• we can also have extra functionality, so it's OK to support the case where we use Function

[allan-mercari]

@caioraposo @daniel-larraz I would be interested in picking this PR up because my project uses this functionality and I'm trying to add a cvc5 backend in addition to z3. However I've reviewed the code and I'm stumped on Caio's comment here: #108 (comment)

Potential solutions I see:

1.Context could be extended to include the Solver, but this seems suboptimal as Caio previously noted.
2. TermManager could be extended to support defineFunRec such that when these functions are used the definition is injected into the solver.

I believe that #2 is closer to what Z3 does however, are there other parts of the cvc5 pythonic API that already do anything similar?

[caioraposo]

2. TermManager could be extended to support defineFunRec such that when these functions are used the definition is injected into the solver.

This would simplify things here but would change the other cvc5 APIs as well. I'll push some changes shortly with a solution.

[daniel-larraz]

@caioraposo Your current implementation (399bd09) doesn't seem to behave correctly. Consider the following example:

ctx = Context()
s1 = Solver(ctx=ctx)
s2 = Solver(ctx=ctx)

x = Int('x', ctx)
s1.add(x > 0)
s2.add(x < 0)
print(s1.check())

Z3 returns sat, but your version returns unsat.

[daniel-larraz]

What about storing the recursive definition in the Context object associated with the function body, and adding the definition to the Solver as soon as it is created?

[allan-mercari]

@caioraposo @daniel-larraz You can find a working snippet for using the "configure solver on creation" strategy here: https://github.com/mercari/cel-smt/blob/8c6fbf987c309c22d1d0da25bec9a382e9dec8c3/src/cel_smt/backend.py#L23

Please let me know if you'd like me to create a separate PR, I'm happy to do so.

[caioraposo]

@caioraposo @daniel-larraz You can find a working snippet for using the "configure solver on creation" strategy here: https://github.com/mercari/cel-smt/blob/8c6fbf987c309c22d1d0da25bec9a382e9dec8c3/src/cel_smt/backend.py#L23

Please let me know if you'd like me to create a separate PR, I'm happy to do so.

Can you confirm this works if you define a function after creating a solver? For example:

s = SolverFor("UFLIA")
fact = Function('fact', IntSort(), IntSort())
n = Int('n')
RecAddDefinition(fact, n, If(n == 0, 1, n * fact(n - 1)))

s.add(Not(fact(5) == 120))
print(s.check())

I don't know how I could test your code.

[caioraposo]

I think you can open a PR or point to your working branch, just to make it easier to review and test. It's difficult to know just based on the snippet you provided.