How to define recursive function in CVC5?

I am having trouble using recursive functions in cvc5. I am trying to declare the following function:

f(x) = if x <= 0 then 0 else f( x - 1 )

Then I try to assert f(3) = 0. My issue is I keep getting unknown (incomplete) when checking for sat

#include <iostream>
#include <cvc5/cvc5.h>

int main()
{

    cvc5::TermManager tm = cvc5::TermManager();
    cvc5::Solver slv     = cvc5::Solver(tm);

    slv.setLogic("ALL");
    slv.setOption("produce-models", "true");


    auto x = tm.mkVar( tm.getIntegerSort() );

    auto fn = tm.mkConst(
        tm.mkFunctionSort( { tm.getIntegerSort() }, tm.getIntegerSort() )
    );

    // construct f(x) = if x <= 0 then 0 else f( x - 1 )
    auto rec_fn = slv.defineFunRec(
        fn ,
        { x } ,
        tm.mkTerm(
            cvc5::Kind::ITE,
            { tm.mkTerm(cvc5::Kind::LEQ,{ x, tm.mkInteger(0) }),
              tm.mkInteger(0),
              tm.mkTerm(cvc5::Kind::APPLY_UF, {
                  fn ,
                  tm.mkTerm(cvc5::Kind::SUB, { x, tm.mkInteger(1) })
              })
            }
        )
    );

    // adding or removing this assertion does not change the outcome
    slv.assertFormula(
      tm.mkTerm(
          cvc5::Kind::EQUAL,
          { rec_fn, fn }
      )
    );
    
    // f(3) 
    auto fn_3 = tm.mkTerm(
        cvc5::Kind::APPLY_UF,
        { rec_fn, tm.mkInteger(3) }
    );

    // assert f(3) == 0
    slv.assertFormula(
        tm.mkTerm(
            cvc5::Kind::EQUAL,
            { fn_3 , tm.mkInteger(0) }
        )
    );

    auto res = slv.checkSat();
    std::cout << "res: " << res << std::endl;
    // output: res: unknown (INCOMPLETE)
}

Alternatively if someone can provide an example of a "loop" in cvc5 then that's also acceptable.

Any help would be greatly appreciated. Thank you for your time

Solution

I think the encoding here is a bit of a red-herring. The programmable API of solvers for C/C++ tend to be really hairy and hide the underlying issues. So, let's code your function in good old SMTLib:

$ cat a.smt2
(set-logic ALL)

; f(x) = if x <= 0 then 0 else f( x - 1 )
(define-fun-rec f ((x Int)) Int (ite (<= x 0) 0 (f (- x 1))))

(assert (= 0 (f 3)))
(check-sat)

Let's try z3 and cvc5 on it:

$ z3 a.smt2
sat
$ cvc5 a.smt2
unknown

So, z3 can handle this problem, but cvc5 produces unknown. Before opining on why this might be, let's also try asserting the negation (which is the typical proof strategy to prove that f(3) = 0):

$ cat a.smt2
(set-logic ALL)

; f(x) = if x <= 0 then 0 else f( x - 1 )
(define-fun-rec f ((x Int)) Int (ite (<= x 0) 0 (f (- x 1))))

(assert (not (= 0 (f 3))))
(check-sat)

We now get:

$ z3 a.smt2
unsat
$ cvc5 a.smt2
unsat

So, both solvers can deduce unsat.

Why is this?

Well, the problem is that finding a "model" in the presence of recursive definitions is a really hard problem, compared to determining unsat. SMT solvers typically only generate finite models (i.e., one that can be fully specified with a finite number of "points"), so if your recursive definition requires an infinite model (typically the case when the definition has infinitely many differing input/output pairs), then they have a harder time. It looks like z3 is doing much better here compared to cvc5.

There might be various flags/settings that can CVC5 to return sat for your problem; but these tend to be brittle. I think you'll find z3 to be the most powerful as of today, i.e., late 2024; but of course CVC5 might get better, or other solvers might come into play eventually.

I'd recommend sticking to SMTLib or some other higher level interface (there are various bindings from Python, Haskell, Rust that tend to be much easier to use compared to C/C++) to sort out the issues before delving into more low level programming.

If you're so inclined, you can post the above SMTLib encoding to CVC5 GitHub issues page and see if the developers recommend any ideas. Please do share what you find if you do so.