Geek Answers Handbook

Z3 Java API Defining Function

I need your help in defining a function using the Java API Z3. I am trying to solve something like this (which works 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)

Result of this smt file:

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

Now the problem is this: there is no option to define a function using the java API. In another post ( Equivalent to define-fun in the Z3 API ), I noticed using the following statement in the java interface:

(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 (<= xy) yx)) in my smt file and started z3. exe again. The result is the following:

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

So, as you can see, there is no longer a satisfactory result. Translating this into java will produce the same UNKNOWN result .

, ?

+4
2

, , define-fun. API , , , Expr.Substitute.

, , , unknown, , . (. ), .

+2

​​:

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

, , :

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))))));
+1

More articles:


All Articles