Z3 Java API defining a function

Question

I need your help defining a function with the Z3 Java API. I try to solve something like this (which is working fine with the z3.exe process):

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Bool)

(define-fun max2 ((x Real) (y Real)) Real (ite (<= x y) y x))

(assert (and (>= a 0.0) (<= a 100.0)))
(assert (or (= (max2 (+ 100.0 (* (- 1.0) a)) (/ 1.0 1000.0)) 0.0) c (not (= b 0.0))))

(check-sat-using (then simplify bit-blast qfnra))
(get-model)

The result of this smt-file is:

sat
(model
  (define-fun a () Real
    1.0)
  (define-fun c () Bool
    false)
  (define-fun b () Real
    1.0)
)

The problem now is: There is no option, to define a function with the java API. In another post (Equivalent of define-fun in Z3 API), i noticed to use the following statement in the java API:

(declare-fun max2 (Real Real) Real)
(assert (forall ((y Real) (x Real)) (= (max2 y x) (ite (<= x y) y x))))

So i replaced (define-fun max2 ((x Real) (y Real)) Real (ite (<= x y) y x)) in my smt-file and started the z3.exe process again. The result was the following:

unknown
(model
  (define-fun b () Real
    0.0)
)

So, as you can see, there is no satisfiable result any more. Translating this in java, will get the same result UNKNOWN.

Any ideas, what i can do?

Answer 1

There is no equivalent to function definitions because they aren't necessary, just like the define-fun macro. The equivalent thing to do in the API is to build an expression for the function and then for every application of the function, just substitute the argument values for the input values, e.g., by using Expr.Substitute.

Like Leo mentioned in the post you cited, the use of quantifiers is possible for this purpose, but the solver will often just give up and return unknown because it thinks the formula is too hard to solve. We can get around that by using the macro finder (see cited post), which will recognize exactly this kind of macro.

Answer 2

How about declaring a function like this:

private static RealExpr max2(Context ctx, ArithExpr x, ArithExpr y) 
        throws Z3Exception {
    return (RealExpr) ctx.mkITE(ctx.mkLe(x, y), y, x);
}

And probably use it like this:

Context ctx = new Context();

ArithExpr a = (ArithExpr) ctx.mkConst(ctx.mkSymbol("a"), ctx.getRealSort());
ArithExpr b = (ArithExpr) ctx.mkConst(ctx.mkSymbol("b"), ctx.getRealSort());
BoolExpr c = (BoolExpr) ctx.mkConst(ctx.mkSymbol("c"), ctx.getBoolSort());

Goal g = ctx.mkGoal(true, true, false);
g.add(ctx.mkAnd(ctx.mkGe(a, ctx.mkReal(0)), ctx.mkLe(a, ctx.mkReal(100))));
g.add(ctx.mkOr(
    ctx.mkEq(
        max2(ctx, 
            ctx.mkAdd(ctx.mkReal(100), ctx.mkMul(ctx.mkReal(-1), a)), 
            ctx.mkDiv(ctx.mkReal(1), ctx.mkReal(1000))), 
        ctx.mkReal(0)),
    c,
    (ctx.mkNot(ctx.mkEq(b, ctx.mkReal(0))))));