Defining a function in Z3 by its Java implementation?

Question

So here's what I am trying to do.

Let's say that I want to find the value of op using Z3 (and its Java binding) in an expression similar to this:

((exists (op Int)) (= (foo op) 2)

So I want to call a function foo on the op variable and check for which values of op will the function return 2. I want to define a function foo in Java and thought that there exists a way for Z3 to access these function definitions. I want to do it like this because the functions are actually look-ups in a HashMap which was easy to implement in Java.

Since I am a beginner to SMT solvers in general it might be possible that I want to do something which cannot be done. So I am open to all suggestions regarding the topic.

Thanks in advance for your time and answers!

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2016-05-22T14:04:14

That would be very nice to have, but at the moment Z3 can't use function definitions from other languages/APIs. For the case of lookup-tables it should be easy though, because they can easily be encoded as if-then-else cascades, for instance as follows:

;; define foo
(define-fun foo ((x Int)) Int
    (ite (= x 1) 42
    (ite (= x 2) 43
    ;; ...
                 78)))

;; use foo
(assert (exists ((op Int)) (= (foo op) 43)))
(apply skip)

produces

(goal
  (exists ((op Int)) (= (ite (= op 1) 42 (ite (= op 2) 43 78)) 43))
  :precision precise :depth 0)
)

(and it is solved quickly, too.)

The easiest way to do this via the API is to set up the problem with the function declaration and then to provide a macro definition via a universal quantifier that is recognized by the macro-finder tactic:

;; declare foo
(declare-fun foo ((Int)) Int)

;; define foo
(assert (forall ((x Int)) (= (foo x)
    (ite (= x 1) 42
    (ite (= x 2) 43
    ;; ...
                 78)))))

;; use foo
(assert (exists ((op Int)) (= (foo op) 43)))
(apply macro-finder) ;; replaces foo with it's definition

For the macro-finder to pick up the function definition, the quantifier has to have the form

(forall ((x ...)) (= (foo x) (... definition ...))

Defining a function in Z3 by its Java implementation?

1 Answers