CODEWITHSUNDEEP
z3smt
buggymcbugfix
buggymcbugfix

Reputation: 321

Z3/SMT-LIB Evaluating function and collecting results

I'm trying to get some values out of Z3 in a way that it queries all available values automatically:

(define-fun-rec out ((p Pkg) (t Time)) (List Bool)
  (ite (< t 0) (as nil (List Bool)) (insert (eval (installed p t)) (out p (- t 1)))))

(eval (out a t-final))

Unfortunately this gives me the error unknown function/constant eval

I also tried doing the eval side effect within the function instead of building a list, but that didn't work either, because I can't sequence statements (eval and the recursive call).

Anybody have any ideas?

Upvotes: 1

Views: 749

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

At this page, I found the following quote:

The command eval evaluates an expression in the last model produced by Z3. It is essentially executing the "function program" produced by Z3.

Since eval is a <command>, it follows that it cannot be used within a <term> expression.

I believe model-enumeration should be easier using some API interface instead of the SmtLibv2 format, as one can easily write a loop that alternates satisfiability checks with learning of a blocking clause that removes previously find solutions from the search space.

Upvotes: 1

Related Questions