Z3 Java API - ignoring an expression like a max-function

Question

last time I asked how to define a function in the Z3 Java API. The reason was that there is no command to define a function in the Java API. The answer was to substitute the argument values of the function for the input values (Z3 Java API defining a function).

Example (what I need):

1. without API (normal smt-file)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(define-fun max2 ((x Int) (y Int)) Int (ite (<= x y) y x))

(assert (< (max2 a b) c))
(assert (>= (max2 a b) c))

(check-sat)

What I do now is something like this:

2. with Java API

Context ctx = new Context();

ArithExpr a = (ArithExpr) ctx.mkConst(ctx.mkSymbol("a"), ctx.getIntSort());
ArithExpr b = (ArithExpr) ctx.mkConst(ctx.mkSymbol("b"), ctx.getIntSort());
ArithExpr c = (ArithExpr) ctx.mkConst(ctx.mkSymbol("c"), ctx.getIntSort());

ArithExpr max2 = (ArithExpr) ctx.mkITE(ctx.mkLe(a, b), b, a);
BoolExpr one = (BoolExpr) ctx.mkLt(max2, c);
BoolExpr two = (BoolExpr) ctx.mkGe(max2, c);

I wonder, if this makes a difference?

I assume that the max2-function in the smt-file (1) is correct and does not have to be re-solved again. But if I do it as in the above java code (2), the solver has to solve the expression of the max2-function ctx.mkITE(ctx.mkLe(a, b), b, a) every time again. Or am I completely wrong and it is not possible, to ignore the expression of the max2-function?

Does anyone have an idea?

Answer 1

The define-fun construct behaves like a macro, so all occurrences of max2 will be replaced with the function definition. Alternatively, we could use quantifiers and the macro-finder (see e.g., Equivalent of define-fun in Z3 API), or we can just replace all occurrences of the function ourselves.

In general it is not possible to "ignore" anything and Z3 will not attempt to "solve" one function before another one; it only knows one problem in which the same sub-expression can appear multiple times (and it has hash-consing, so it knows about equal sub-expressions). If you know that it's possible to solve the problem without knowing about the semantics of the function, then you could just replace it with a new variable to represent the return value for some particular arguments, that will likely make it possible to solve the problem much quicker.