CODEWITHSUNDEEP
z3smtcvc4
Bill
Bill

Reputation: 493

Using define-fun-rec in SMT

I'm currently trying to write an SMT script using define-fun-rec. I've tested with both Z3, version 4.4.2, and CVC4, version 1.4. As far as I can tell, these are the most recent versions of both, and both support the feature*. However, both do not seem to recognize the command.

(I made some changes to this based on Nikolaj's reply. It still gives the error messages.) Specifically, given:

(define-fun-rec 
    fac ((x Int)) Int
    (
        ite (<= x 1) 
            1 
            (* x (fac (- x 1)))
    )
)

(assert (= (fac 4) 24))

(check-sat)

Z3 outputs:

unsupported
; define-fun-rec
(error "line 10 column 17: unknown function/constant fac")
sat

And CVC4 outputs:

(error "Parse Error: fac.smt2:1.15: expected SMT-LIBv2 command, got `define-fun-rec'.

  (define-fun-rec 
   ^
")

My best guess is that there is some sort of flag I need to set or I need to be using some specific logic, but I've had a lot of trouble finding any sort of detailed instructions or examples with define-fun-rec. Any advice would be appreciated. Thanks!

*Z3 has support: How to deal with recursive function in Z3?

CVC4 has support: http://lara.epfl.ch/~reynolds/pres-smt15.pdf

Upvotes: 1

Views: 1564

Answers (2)

Andrew Reynolds
Andrew Reynolds

Reputation: 21

The latest version of CVC4 can be downloaded under "Development versions" (on the right hand side) of: http://cvc4.cs.nyu.edu/downloads/

The latest development version has support for recursive function definitions. You can use the cvc4 command line option "--fmf-fun" to enable a technique that finds small models for problems involving recursive function applications, assuming definitions are admissible.

(Although, unfortunately your example with factorial also requires non-linear arithmetic, which CVC4 does not yet support.)

Upvotes: 2

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

  1. Don't set the logic to LIA. This is not in the LIA fragment and Z3 will use the wrong tactic to solve the problem.Just remove the set-logic line.
  2. It helps to not use an undefined function "f" inside the definition of "fib".
  3. I would suggest that you call the function "fac" and not "fib" since you are defining a factorial function.

Thus,

(define-fun-rec 
   fac ((x Int)) Int
   (
    ite (<= x 1) 
        1 
        (* x (fac (- x 1)))
   )
)

(assert (= (fac 4) 24))

(check-sat)

z3 -version

Z3 version 4.4.2

z3 fac.smt2

sat

If you change 24 to 25 you get unsat.

Upvotes: 1

Related Questions