diff options
author | 2021-08-03 18:42:39 +0900 | |
---|---|---|
committer | 2021-08-06 19:32:38 +0900 | |
commit | be4f78978faba3d3ceb88df02a7f93a2e09ff1e0 (patch) | |
tree | 1f3f1a96251ac4f655c8a96fc33d5d4ee779cd06 /rba.tool.core/lib/z3/JavaExample.java | |
parent | 71ca7c6cab863767ef30c8bd05b2bbfda8731cb5 (diff) |
Initial commit
Bug-AGL: SPEC-4033
Signed-off-by: Kenji Hosokawa <khosokawa@jp.adit-jv.com>
Diffstat (limited to 'rba.tool.core/lib/z3/JavaExample.java')
-rw-r--r-- | rba.tool.core/lib/z3/JavaExample.java | 2400 |
1 files changed, 2400 insertions, 0 deletions
diff --git a/rba.tool.core/lib/z3/JavaExample.java b/rba.tool.core/lib/z3/JavaExample.java new file mode 100644 index 0000000..8faa94c --- /dev/null +++ b/rba.tool.core/lib/z3/JavaExample.java @@ -0,0 +1,2400 @@ +/*++ + Copyright (c) 2012 Microsoft Corporation +Module Name: + Program.java +Abstract: + Z3 Java API: Example program +Author: + Christoph Wintersteiger (cwinter) 2012-11-27 +Notes: + +--*/ + +package rba.tool.simulator.constraint.handlers; + +import java.util.*; + +import com.microsoft.z3.*; + +class JavaExample +{ + @SuppressWarnings("serial") + class TestFailedException extends Exception + { + public TestFailedException() + { + super("Check FAILED"); + } + }; + + // / Create axiom: function f is injective in the i-th argument. + + // / <remarks> + // / The following axiom is produced: + // / <code> + // / forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i + // / </code> + // / Where, <code>finv</code>is a fresh function declaration. + + public BoolExpr injAxiom(Context ctx, FuncDecl f, int i) + { + Sort[] domain = f.getDomain(); + int sz = f.getDomainSize(); + + if (i >= sz) + { + System.out.println("failed to create inj axiom"); + return null; + } + + /* declare the i-th inverse of f: finv */ + Sort finv_domain = f.getRange(); + Sort finv_range = domain[i]; + FuncDecl finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range); + + /* allocate temporary arrays */ + Expr[] xs = new Expr[sz]; + Symbol[] names = new Symbol[sz]; + Sort[] types = new Sort[sz]; + + /* fill types, names and xs */ + + for (int j = 0; j < sz; j++) + { + types[j] = domain[j]; + names[j] = ctx.mkSymbol("x_" + Integer.toString(j)); + xs[j] = ctx.mkBound(j, types[j]); + } + Expr x_i = xs[i]; + + /* create f(x_0, ..., x_i, ..., x_{n-1}) */ + Expr fxs = f.apply(xs); + + /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */ + Expr finv_fxs = finv.apply(fxs); + + /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */ + Expr eq = ctx.mkEq(finv_fxs, x_i); + + /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */ + Pattern p = ctx.mkPattern(fxs); + + /* create & assert quantifier */ + BoolExpr q = ctx.mkForall(types, /* types of quantified variables */ + names, /* names of quantified variables */ + eq, 1, new Pattern[] { p } /* patterns */, null, null, null); + + return q; + } + + // / Create axiom: function f is injective in the i-th argument. + + // / <remarks> + // / The following axiom is produced: + // / <code> + // / forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i + // / </code> + // / Where, <code>finv</code>is a fresh function declaration. + + public BoolExpr injAxiomAbs(Context ctx, FuncDecl f, int i) + { + Sort[] domain = f.getDomain(); + int sz = f.getDomainSize(); + + if (i >= sz) + { + System.out.println("failed to create inj axiom"); + return null; + } + + /* declare the i-th inverse of f: finv */ + Sort finv_domain = f.getRange(); + Sort finv_range = domain[i]; + FuncDecl finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range); + + /* allocate temporary arrays */ + Expr[] xs = new Expr[sz]; + + /* fill types, names and xs */ + for (int j = 0; j < sz; j++) + { + xs[j] = ctx.mkConst("x_" + Integer.toString(j), domain[j]); + } + Expr x_i = xs[i]; + + /* create f(x_0, ..., x_i, ..., x_{n-1}) */ + Expr fxs = f.apply(xs); + + /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */ + Expr finv_fxs = finv.apply(fxs); + + /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */ + Expr eq = ctx.mkEq(finv_fxs, x_i); + + /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */ + Pattern p = ctx.mkPattern(fxs); + + /* create & assert quantifier */ + BoolExpr q = ctx.mkForall(xs, /* types of quantified variables */ + eq, /* names of quantified variables */ + 1, new Pattern[] { p } /* patterns */, null, null, null); + + return q; + } + + // / Assert the axiom: function f is commutative. + + // / <remarks> + // / This example uses the SMT-LIB parser to simplify the axiom + // construction. + // / </remarks> + private BoolExpr commAxiom(Context ctx, FuncDecl f) throws Exception + { + Sort t = f.getRange(); + Sort[] dom = f.getDomain(); + + if (dom.length != 2 || !t.equals(dom[0]) || !t.equals(dom[1])) + { + System.out.println(Integer.toString(dom.length) + " " + + dom[0].toString() + " " + dom[1].toString() + " " + + t.toString()); + throw new Exception( + "function must be binary, and argument types must be equal to return type"); + } + + String bench = "(benchmark comm :formula (forall (x " + t.getName() + + ") (y " + t.getName() + ") (= (" + f.getName() + " x y) (" + + f.getName() + " y x))))"; + ctx.parseSMTLIBString(bench, new Symbol[] { t.getName() }, + new Sort[] { t }, new Symbol[] { f.getName() }, + new FuncDecl[] { f }); + return ctx.getSMTLIBFormulas()[0]; + } + + // / "Hello world" example: create a Z3 logical context, and delete it. + + public void simpleExample() + { + System.out.println("SimpleExample"); + Log.append("SimpleExample"); + + { + Context ctx = new Context(); + /* do something with the context */ + + /* be kind to dispose manually and not wait for the GC. */ + ctx.close(); + } + } + + Model check(Context ctx, BoolExpr f, Status sat) throws TestFailedException + { + Solver s = ctx.mkSolver(); + s.add(f); + if (s.check() != sat) + throw new TestFailedException(); + if (sat == Status.SATISFIABLE) + return s.getModel(); + else + return null; + } + + void solveTactical(Context ctx, Tactic t, Goal g, Status sat) + throws TestFailedException + { + Solver s = ctx.mkSolver(t); + System.out.println("\nTactical solver: " + s); + + for (BoolExpr a : g.getFormulas()) + s.add(a); + System.out.println("Solver: " + s); + + if (s.check() != sat) + throw new TestFailedException(); + } + + ApplyResult applyTactic(Context ctx, Tactic t, Goal g) + { + System.out.println("\nGoal: " + g); + + ApplyResult res = t.apply(g); + System.out.println("Application result: " + res); + + Status q = Status.UNKNOWN; + for (Goal sg : res.getSubgoals()) + if (sg.isDecidedSat()) + q = Status.SATISFIABLE; + else if (sg.isDecidedUnsat()) + q = Status.UNSATISFIABLE; + + switch (q) + { + case UNKNOWN: + System.out.println("Tactic result: Undecided"); + break; + case SATISFIABLE: + System.out.println("Tactic result: SAT"); + break; + case UNSATISFIABLE: + System.out.println("Tactic result: UNSAT"); + break; + } + + return res; + } + + void prove(Context ctx, BoolExpr f, boolean useMBQI) throws TestFailedException + { + BoolExpr[] assumptions = new BoolExpr[0]; + prove(ctx, f, useMBQI, assumptions); + } + + void prove(Context ctx, BoolExpr f, boolean useMBQI, + BoolExpr... assumptions) throws TestFailedException + { + System.out.println("Proving: " + f); + Solver s = ctx.mkSolver(); + Params p = ctx.mkParams(); + p.add("mbqi", useMBQI); + s.setParameters(p); + for (BoolExpr a : assumptions) + s.add(a); + s.add(ctx.mkNot(f)); + Status q = s.check(); + + switch (q) + { + case UNKNOWN: + System.out.println("Unknown because: " + s.getReasonUnknown()); + break; + case SATISFIABLE: + throw new TestFailedException(); + case UNSATISFIABLE: + System.out.println("OK, proof: " + s.getProof()); + break; + } + } + + void disprove(Context ctx, BoolExpr f, boolean useMBQI) + throws TestFailedException + { + BoolExpr[] a = {}; + disprove(ctx, f, useMBQI, a); + } + + void disprove(Context ctx, BoolExpr f, boolean useMBQI, + BoolExpr... assumptions) throws TestFailedException + { + System.out.println("Disproving: " + f); + Solver s = ctx.mkSolver(); + Params p = ctx.mkParams(); + p.add("mbqi", useMBQI); + s.setParameters(p); + for (BoolExpr a : assumptions) + s.add(a); + s.add(ctx.mkNot(f)); + Status q = s.check(); + + switch (q) + { + case UNKNOWN: + System.out.println("Unknown because: " + s.getReasonUnknown()); + break; + case SATISFIABLE: + System.out.println("OK, model: " + s.getModel()); + break; + case UNSATISFIABLE: + throw new TestFailedException(); + } + } + + void modelConverterTest(Context ctx) throws TestFailedException + { + System.out.println("ModelConverterTest"); + + ArithExpr xr = (ArithExpr) ctx.mkConst(ctx.mkSymbol("x"), + ctx.mkRealSort()); + ArithExpr yr = (ArithExpr) ctx.mkConst(ctx.mkSymbol("y"), + ctx.mkRealSort()); + Goal g4 = ctx.mkGoal(true, false, false); + g4.add(ctx.mkGt(xr, ctx.mkReal(10, 1))); + g4.add(ctx.mkEq(yr, ctx.mkAdd(xr, ctx.mkReal(1, 1)))); + g4.add(ctx.mkGt(yr, ctx.mkReal(1, 1))); + + ApplyResult ar = applyTactic(ctx, ctx.mkTactic("simplify"), g4); + if (ar.getNumSubgoals() == 1 + && (ar.getSubgoals()[0].isDecidedSat() || ar.getSubgoals()[0] + .isDecidedUnsat())) + throw new TestFailedException(); + + ar = applyTactic(ctx, ctx.andThen(ctx.mkTactic("simplify"), + ctx.mkTactic("solve-eqs")), g4); + if (ar.getNumSubgoals() == 1 + && (ar.getSubgoals()[0].isDecidedSat() || ar.getSubgoals()[0] + .isDecidedUnsat())) + throw new TestFailedException(); + + Solver s = ctx.mkSolver(); + for (BoolExpr e : ar.getSubgoals()[0].getFormulas()) + s.add(e); + Status q = s.check(); + System.out.println("Solver says: " + q); + System.out.println("Model: \n" + s.getModel()); + System.out.println("Converted Model: \n" + + ar.convertModel(0, s.getModel())); + if (q != Status.SATISFIABLE) + throw new TestFailedException(); + } + + // / A simple array example. + + void arrayExample1(Context ctx) throws TestFailedException + { + System.out.println("ArrayExample1"); + Log.append("ArrayExample1"); + + Goal g = ctx.mkGoal(true, false, false); + ArraySort asort = ctx.mkArraySort(ctx.getIntSort(), + ctx.mkBitVecSort(32)); + ArrayExpr aex = (ArrayExpr) ctx.mkConst(ctx.mkSymbol("MyArray"), asort); + Expr sel = ctx.mkSelect(aex, ctx.mkInt(0)); + g.add(ctx.mkEq(sel, ctx.mkBV(42, 32))); + Symbol xs = ctx.mkSymbol("x"); + IntExpr xc = (IntExpr) ctx.mkConst(xs, ctx.getIntSort()); + + Symbol fname = ctx.mkSymbol("f"); + Sort[] domain = { ctx.getIntSort() }; + FuncDecl fd = ctx.mkFuncDecl(fname, domain, ctx.getIntSort()); + Expr[] fargs = { ctx.mkConst(xs, ctx.getIntSort()) }; + IntExpr fapp = (IntExpr) ctx.mkApp(fd, fargs); + + g.add(ctx.mkEq(ctx.mkAdd(xc, fapp), ctx.mkInt(123))); + + Solver s = ctx.mkSolver(); + for (BoolExpr a : g.getFormulas()) + s.add(a); + System.out.println("Solver: " + s); + + Status q = s.check(); + System.out.println("Status: " + q); + + if (q != Status.SATISFIABLE) + throw new TestFailedException(); + + System.out.println("Model = " + s.getModel()); + + System.out.println("Interpretation of MyArray:\n" + + s.getModel().getFuncInterp(aex.getFuncDecl())); + System.out.println("Interpretation of x:\n" + + s.getModel().getConstInterp(xc)); + System.out.println("Interpretation of f:\n" + + s.getModel().getFuncInterp(fd)); + System.out.println("Interpretation of MyArray as Term:\n" + + s.getModel().getFuncInterp(aex.getFuncDecl())); + } + + // / Prove <tt>store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 + // = i3 or select(a1, i3) = select(a2, i3))</tt>. + + // / <remarks>This example demonstrates how to use the array + // theory.</remarks> + public void arrayExample2(Context ctx) throws TestFailedException + { + System.out.println("ArrayExample2"); + Log.append("ArrayExample2"); + + Sort int_type = ctx.getIntSort(); + Sort array_type = ctx.mkArraySort(int_type, int_type); + + ArrayExpr a1 = (ArrayExpr) ctx.mkConst("a1", array_type); + ArrayExpr a2 = ctx.mkArrayConst("a2", int_type, int_type); + Expr i1 = ctx.mkConst("i1", int_type); + Expr i2 = ctx.mkConst("i2", int_type); + Expr i3 = ctx.mkConst("i3", int_type); + Expr v1 = ctx.mkConst("v1", int_type); + Expr v2 = ctx.mkConst("v2", int_type); + + Expr st1 = ctx.mkStore(a1, i1, v1); + Expr st2 = ctx.mkStore(a2, i2, v2); + + Expr sel1 = ctx.mkSelect(a1, i3); + Expr sel2 = ctx.mkSelect(a2, i3); + + /* create antecedent */ + BoolExpr antecedent = ctx.mkEq(st1, st2); + + /* + * create consequent: i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, + * i3) + */ + BoolExpr consequent = ctx.mkOr(ctx.mkEq(i1, i3), ctx.mkEq(i2, i3), + ctx.mkEq(sel1, sel2)); + + /* + * prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = + * i3 or select(a1, i3) = select(a2, i3)) + */ + BoolExpr thm = ctx.mkImplies(antecedent, consequent); + System.out + .println("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))"); + System.out.println(thm); + prove(ctx, thm, false); + } + + // / Show that <code>distinct(a_0, ... , a_n)</code> is + // / unsatisfiable when <code>a_i</code>'s are arrays from boolean to + // / boolean and n > 4. + + // / <remarks>This example also shows how to use the <code>distinct</code> + // construct.</remarks> + public void arrayExample3(Context ctx) throws TestFailedException + { + System.out.println("ArrayExample3"); + Log.append("ArrayExample2"); + + for (int n = 2; n <= 5; n++) + { + System.out.println("n = " + Integer.toString(n)); + + Sort bool_type = ctx.mkBoolSort(); + Sort array_type = ctx.mkArraySort(bool_type, bool_type); + Expr[] a = new Expr[n]; + + /* create arrays */ + for (int i = 0; i < n; i++) + { + a[i] = ctx.mkConst("array_" + Integer.toString(i), array_type); + } + + /* assert distinct(a[0], ..., a[n]) */ + BoolExpr d = ctx.mkDistinct(a); + System.out.println(d); + + /* context is satisfiable if n < 5 */ + Model model = check(ctx, d, n < 5 ? Status.SATISFIABLE + : Status.UNSATISFIABLE); + if (n < 5) + { + for (int i = 0; i < n; i++) + { + System.out.println(a[i].toString() + " = " + + model.evaluate(a[i], false)); + } + } + } + } + + // / Sudoku solving example. + + void sudokuExample(Context ctx) throws TestFailedException + { + System.out.println("SudokuExample"); + Log.append("SudokuExample"); + + // 9x9 matrix of integer variables + IntExpr[][] X = new IntExpr[9][]; + for (int i = 0; i < 9; i++) + { + X[i] = new IntExpr[9]; + for (int j = 0; j < 9; j++) + X[i][j] = (IntExpr) ctx.mkConst( + ctx.mkSymbol("x_" + (i + 1) + "_" + (j + 1)), + ctx.getIntSort()); + } + + // each cell contains a value in {1, ..., 9} + BoolExpr[][] cells_c = new BoolExpr[9][]; + for (int i = 0; i < 9; i++) + { + cells_c[i] = new BoolExpr[9]; + for (int j = 0; j < 9; j++) + cells_c[i][j] = ctx.mkAnd(ctx.mkLe(ctx.mkInt(1), X[i][j]), + ctx.mkLe(X[i][j], ctx.mkInt(9))); + } + + // each row contains a digit at most once + BoolExpr[] rows_c = new BoolExpr[9]; + for (int i = 0; i < 9; i++) + rows_c[i] = ctx.mkDistinct(X[i]); + + // each column contains a digit at most once + BoolExpr[] cols_c = new BoolExpr[9]; + for (int j = 0; j < 9; j++) + cols_c[j] = ctx.mkDistinct(X[j]); + + // each 3x3 square contains a digit at most once + BoolExpr[][] sq_c = new BoolExpr[3][]; + for (int i0 = 0; i0 < 3; i0++) + { + sq_c[i0] = new BoolExpr[3]; + for (int j0 = 0; j0 < 3; j0++) + { + IntExpr[] square = new IntExpr[9]; + for (int i = 0; i < 3; i++) + for (int j = 0; j < 3; j++) + square[3 * i + j] = X[3 * i0 + i][3 * j0 + j]; + sq_c[i0][j0] = ctx.mkDistinct(square); + } + } + + BoolExpr sudoku_c = ctx.mkTrue(); + for (BoolExpr[] t : cells_c) + sudoku_c = ctx.mkAnd(ctx.mkAnd(t), sudoku_c); + sudoku_c = ctx.mkAnd(ctx.mkAnd(rows_c), sudoku_c); + sudoku_c = ctx.mkAnd(ctx.mkAnd(cols_c), sudoku_c); + for (BoolExpr[] t : sq_c) + sudoku_c = ctx.mkAnd(ctx.mkAnd(t), sudoku_c); + + // sudoku instance, we use '0' for empty cells + int[][] instance = { { 0, 0, 0, 0, 9, 4, 0, 3, 0 }, + { 0, 0, 0, 5, 1, 0, 0, 0, 7 }, { 0, 8, 9, 0, 0, 0, 0, 4, 0 }, + { 0, 0, 0, 0, 0, 0, 2, 0, 8 }, { 0, 6, 0, 2, 0, 1, 0, 5, 0 }, + { 1, 0, 2, 0, 0, 0, 0, 0, 0 }, { 0, 7, 0, 0, 0, 0, 5, 2, 0 }, + { 9, 0, 0, 0, 6, 5, 0, 0, 0 }, { 0, 4, 0, 9, 7, 0, 0, 0, 0 } }; + + BoolExpr instance_c = ctx.mkTrue(); + for (int i = 0; i < 9; i++) + for (int j = 0; j < 9; j++) + instance_c = ctx.mkAnd( + instance_c, + (BoolExpr) ctx.mkITE( + ctx.mkEq(ctx.mkInt(instance[i][j]), + ctx.mkInt(0)), ctx.mkTrue(), + ctx.mkEq(X[i][j], ctx.mkInt(instance[i][j])))); + + Solver s = ctx.mkSolver(); + s.add(sudoku_c); + s.add(instance_c); + + if (s.check() == Status.SATISFIABLE) + { + Model m = s.getModel(); + Expr[][] R = new Expr[9][9]; + for (int i = 0; i < 9; i++) + for (int j = 0; j < 9; j++) + R[i][j] = m.evaluate(X[i][j], false); + System.out.println("Sudoku solution:"); + for (int i = 0; i < 9; i++) + { + for (int j = 0; j < 9; j++) + System.out.print(" " + R[i][j]); + System.out.println(); + } + } else + { + System.out.println("Failed to solve sudoku"); + throw new TestFailedException(); + } + } + + // / A basic example of how to use quantifiers. + + void quantifierExample1(Context ctx) + { + System.out.println("QuantifierExample"); + Log.append("QuantifierExample"); + + Sort[] types = new Sort[3]; + IntExpr[] xs = new IntExpr[3]; + Symbol[] names = new Symbol[3]; + IntExpr[] vars = new IntExpr[3]; + + for (int j = 0; j < 3; j++) + { + types[j] = ctx.getIntSort(); + names[j] = ctx.mkSymbol("x_" + Integer.toString(j)); + xs[j] = (IntExpr) ctx.mkConst(names[j], types[j]); + vars[j] = (IntExpr) ctx.mkBound(2 - j, types[j]); // <-- vars + // reversed! + } + + Expr body_vars = ctx.mkAnd( + ctx.mkEq(ctx.mkAdd(vars[0], ctx.mkInt(1)), ctx.mkInt(2)), + ctx.mkEq(ctx.mkAdd(vars[1], ctx.mkInt(2)), + ctx.mkAdd(vars[2], ctx.mkInt(3)))); + + Expr body_const = ctx.mkAnd( + ctx.mkEq(ctx.mkAdd(xs[0], ctx.mkInt(1)), ctx.mkInt(2)), + ctx.mkEq(ctx.mkAdd(xs[1], ctx.mkInt(2)), + ctx.mkAdd(xs[2], ctx.mkInt(3)))); + + Expr x = ctx.mkForall(types, names, body_vars, 1, null, null, + ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1")); + System.out.println("Quantifier X: " + x.toString()); + + Expr y = ctx.mkForall(xs, body_const, 1, null, null, + ctx.mkSymbol("Q2"), ctx.mkSymbol("skid2")); + System.out.println("Quantifier Y: " + y.toString()); + } + + void quantifierExample2(Context ctx) + { + + System.out.println("QuantifierExample2"); + Log.append("QuantifierExample2"); + + Expr q1, q2; + FuncDecl f = ctx.mkFuncDecl("f", ctx.getIntSort(), ctx.getIntSort()); + FuncDecl g = ctx.mkFuncDecl("g", ctx.getIntSort(), ctx.getIntSort()); + + // Quantifier with Exprs as the bound variables. + { + Expr x = ctx.mkConst("x", ctx.getIntSort()); + Expr y = ctx.mkConst("y", ctx.getIntSort()); + Expr f_x = ctx.mkApp(f, x); + Expr f_y = ctx.mkApp(f, y); + Expr g_y = ctx.mkApp(g, y); + @SuppressWarnings("unused") + Pattern[] pats = new Pattern[] { ctx.mkPattern(f_x, g_y) }; + Expr[] no_pats = new Expr[] { f_y }; + Expr[] bound = new Expr[] { x, y }; + Expr body = ctx.mkAnd(ctx.mkEq(f_x, f_y), ctx.mkEq(f_y, g_y)); + + q1 = ctx.mkForall(bound, body, 1, null, no_pats, ctx.mkSymbol("q"), + ctx.mkSymbol("sk")); + + System.out.println(q1); + } + + // Quantifier with de-Brujin indices. + { + Expr x = ctx.mkBound(1, ctx.getIntSort()); + Expr y = ctx.mkBound(0, ctx.getIntSort()); + Expr f_x = ctx.mkApp(f, x); + Expr f_y = ctx.mkApp(f, y); + Expr g_y = ctx.mkApp(g, y); + @SuppressWarnings("unused") + Pattern[] pats = new Pattern[] { ctx.mkPattern(f_x, g_y) }; + Expr[] no_pats = new Expr[] { f_y }; + Symbol[] names = new Symbol[] { ctx.mkSymbol("x"), + ctx.mkSymbol("y") }; + Sort[] sorts = new Sort[] { ctx.getIntSort(), ctx.getIntSort() }; + Expr body = ctx.mkAnd(ctx.mkEq(f_x, f_y), ctx.mkEq(f_y, g_y)); + + q2 = ctx.mkForall(sorts, names, body, 1, null, // pats, + no_pats, ctx.mkSymbol("q"), ctx.mkSymbol("sk")); + System.out.println(q2); + } + + System.out.println(q1.equals(q2)); + } + + // / Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when + // / <code>f</code> is injective in the second argument. <seealso + // cref="inj_axiom"/> + + public void quantifierExample3(Context ctx) throws TestFailedException + { + System.out.println("QuantifierExample3"); + Log.append("QuantifierExample3"); + + /* + * If quantified formulas are asserted in a logical context, then the + * model produced by Z3 should be viewed as a potential model. + */ + + /* declare function f */ + Sort I = ctx.getIntSort(); + FuncDecl f = ctx.mkFuncDecl("f", new Sort[] { I, I }, I); + + /* f is injective in the second argument. */ + BoolExpr inj = injAxiom(ctx, f, 1); + + /* create x, y, v, w, fxy, fwv */ + Expr x = ctx.mkIntConst("x"); + Expr y = ctx.mkIntConst("y"); + Expr v = ctx.mkIntConst("v"); + Expr w = ctx.mkIntConst("w"); + Expr fxy = ctx.mkApp(f, x, y); + Expr fwv = ctx.mkApp(f, w, v); + + /* f(x, y) = f(w, v) */ + BoolExpr p1 = ctx.mkEq(fxy, fwv); + + /* prove f(x, y) = f(w, v) implies y = v */ + BoolExpr p2 = ctx.mkEq(y, v); + prove(ctx, p2, false, inj, p1); + + /* disprove f(x, y) = f(w, v) implies x = w */ + BoolExpr p3 = ctx.mkEq(x, w); + disprove(ctx, p3, false, inj, p1); + } + + // / Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when + // / <code>f</code> is injective in the second argument. <seealso + // cref="inj_axiom"/> + + public void quantifierExample4(Context ctx) throws TestFailedException + { + System.out.println("QuantifierExample4"); + Log.append("QuantifierExample4"); + + /* + * If quantified formulas are asserted in a logical context, then the + * model produced by Z3 should be viewed as a potential model. + */ + + /* declare function f */ + Sort I = ctx.getIntSort(); + FuncDecl f = ctx.mkFuncDecl("f", new Sort[] { I, I }, I); + + /* f is injective in the second argument. */ + BoolExpr inj = injAxiomAbs(ctx, f, 1); + + /* create x, y, v, w, fxy, fwv */ + Expr x = ctx.mkIntConst("x"); + Expr y = ctx.mkIntConst("y"); + Expr v = ctx.mkIntConst("v"); + Expr w = ctx.mkIntConst("w"); + Expr fxy = ctx.mkApp(f, x, y); + Expr fwv = ctx.mkApp(f, w, v); + + /* f(x, y) = f(w, v) */ + BoolExpr p1 = ctx.mkEq(fxy, fwv); + + /* prove f(x, y) = f(w, v) implies y = v */ + BoolExpr p2 = ctx.mkEq(y, v); + prove(ctx, p2, false, inj, p1); + + /* disprove f(x, y) = f(w, v) implies x = w */ + BoolExpr p3 = ctx.mkEq(x, w); + disprove(ctx, p3, false, inj, p1); + } + + // / Some basic tests. + + void basicTests(Context ctx) throws TestFailedException + { + System.out.println("BasicTests"); + + Symbol fname = ctx.mkSymbol("f"); + Symbol x = ctx.mkSymbol("x"); + Symbol y = ctx.mkSymbol("y"); + + Sort bs = ctx.mkBoolSort(); + + Sort[] domain = { bs, bs }; + FuncDecl f = ctx.mkFuncDecl(fname, domain, bs); + Expr fapp = ctx.mkApp(f, ctx.mkConst(x, bs), ctx.mkConst(y, bs)); + + Expr[] fargs2 = { ctx.mkFreshConst("cp", bs) }; + Sort[] domain2 = { bs }; + Expr fapp2 = ctx.mkApp(ctx.mkFreshFuncDecl("fp", domain2, bs), fargs2); + + BoolExpr trivial_eq = ctx.mkEq(fapp, fapp); + BoolExpr nontrivial_eq = ctx.mkEq(fapp, fapp2); + + Goal g = ctx.mkGoal(true, false, false); + g.add(trivial_eq); + g.add(nontrivial_eq); + System.out.println("Goal: " + g); + + Solver solver = ctx.mkSolver(); + + for (BoolExpr a : g.getFormulas()) + solver.add(a); + + if (solver.check() != Status.SATISFIABLE) + throw new TestFailedException(); + + ApplyResult ar = applyTactic(ctx, ctx.mkTactic("simplify"), g); + if (ar.getNumSubgoals() == 1 + && (ar.getSubgoals()[0].isDecidedSat() || ar.getSubgoals()[0] + .isDecidedUnsat())) + throw new TestFailedException(); + + ar = applyTactic(ctx, ctx.mkTactic("smt"), g); + if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat()) + throw new TestFailedException(); + + g.add(ctx.mkEq(ctx.mkNumeral(1, ctx.mkBitVecSort(32)), + ctx.mkNumeral(2, ctx.mkBitVecSort(32)))); + ar = applyTactic(ctx, ctx.mkTactic("smt"), g); + if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat()) + throw new TestFailedException(); + + Goal g2 = ctx.mkGoal(true, true, false); + ar = applyTactic(ctx, ctx.mkTactic("smt"), g2); + if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat()) + throw new TestFailedException(); + + g2 = ctx.mkGoal(true, true, false); + g2.add(ctx.mkFalse()); + ar = applyTactic(ctx, ctx.mkTactic("smt"), g2); + if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat()) + throw new TestFailedException(); + + Goal g3 = ctx.mkGoal(true, true, false); + Expr xc = ctx.mkConst(ctx.mkSymbol("x"), ctx.getIntSort()); + Expr yc = ctx.mkConst(ctx.mkSymbol("y"), ctx.getIntSort()); + g3.add(ctx.mkEq(xc, ctx.mkNumeral(1, ctx.getIntSort()))); + g3.add(ctx.mkEq(yc, ctx.mkNumeral(2, ctx.getIntSort()))); + BoolExpr constr = ctx.mkEq(xc, yc); + g3.add(constr); + ar = applyTactic(ctx, ctx.mkTactic("smt"), g3); + if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat()) + throw new TestFailedException(); + + modelConverterTest(ctx); + + // Real num/den test. + RatNum rn = ctx.mkReal(42, 43); + Expr inum = rn.getNumerator(); + Expr iden = rn.getDenominator(); + System.out.println("Numerator: " + inum + " Denominator: " + iden); + if (!inum.toString().equals("42") || !iden.toString().equals("43")) + throw new TestFailedException(); + + if (!rn.toDecimalString(3).toString().equals("0.976?")) + throw new TestFailedException(); + + bigIntCheck(ctx, ctx.mkReal("-1231231232/234234333")); + bigIntCheck(ctx, ctx.mkReal("-123123234234234234231232/234234333")); + bigIntCheck(ctx, ctx.mkReal("-234234333")); + bigIntCheck(ctx, ctx.mkReal("234234333/2")); + + String bn = "1234567890987654321"; + + if (!ctx.mkInt(bn).getBigInteger().toString().equals(bn)) + throw new TestFailedException(); + + if (!ctx.mkBV(bn, 128).getBigInteger().toString().equals(bn)) + throw new TestFailedException(); + + if (ctx.mkBV(bn, 32).getBigInteger().toString().equals(bn)) + throw new TestFailedException(); + + // Error handling test. + try + { + @SuppressWarnings("unused") + IntExpr i = ctx.mkInt("1/2"); + throw new TestFailedException(); // unreachable + } catch (Z3Exception e) + { + } + } + + // / Some basic expression casting tests. + + void castingTest(Context ctx) throws TestFailedException + { + System.out.println("CastingTest"); + + Sort[] domain = { ctx.getBoolSort(), ctx.getBoolSort() }; + FuncDecl f = ctx.mkFuncDecl("f", domain, ctx.getBoolSort()); + + AST upcast = ctx.mkFuncDecl(ctx.mkSymbol("q"), domain, + ctx.getBoolSort()); + + try + { + @SuppressWarnings("unused") + FuncDecl downcast = (FuncDecl) f; // OK + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + + try + { + @SuppressWarnings("unused") + Expr uc = (Expr) upcast; + throw new TestFailedException(); // should not be reachable! + } catch (ClassCastException e) + { + } + + Symbol s = ctx.mkSymbol(42); + IntSymbol si = (s.getClass() == IntSymbol.class) ? (IntSymbol) s : null; + if (si == null) + throw new TestFailedException(); + try + { + @SuppressWarnings("unused") + IntSymbol si2 = (IntSymbol) s; + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + + s = ctx.mkSymbol("abc"); + StringSymbol ss = (s.getClass() == StringSymbol.class) ? (StringSymbol) s + : null; + if (ss == null) + throw new TestFailedException(); + try + { + @SuppressWarnings("unused") + StringSymbol ss2 = (StringSymbol) s; + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + try + { + @SuppressWarnings("unused") + IntSymbol si2 = (IntSymbol) s; + throw new TestFailedException(); // unreachable + } catch (Exception e) + { + } + + Sort srt = ctx.mkBitVecSort(32); + BitVecSort bvs = null; + try + { + bvs = (BitVecSort) srt; + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + + if (bvs.getSize() != 32) + throw new TestFailedException(); + + Expr q = ctx.mkAdd(ctx.mkInt(1), ctx.mkInt(2)); + Expr q2 = q.getArgs()[1]; + Sort qs = q2.getSort(); + if (qs.getClass() != IntSort.class) + throw new TestFailedException(); + try + { + @SuppressWarnings("unused") + IntSort isrt = (IntSort) qs; + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + + AST a = ctx.mkInt(42); + + try + { + Expr.class.cast(a); + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + + try + { + ArithExpr.class.cast(a); + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + + try + { + IntExpr.class.cast(a); + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + + try + { + IntNum.class.cast(a); + } catch (ClassCastException e) + { + throw new TestFailedException(); + } + + Expr[][] earr = new Expr[2][]; + earr[0] = new Expr[2]; + earr[1] = new Expr[2]; + earr[0][0] = ctx.mkTrue(); + earr[0][1] = ctx.mkTrue(); + earr[1][0] = ctx.mkFalse(); + earr[1][1] = ctx.mkFalse(); + for (Expr[] ea : earr) + for (Expr e : ea) + { + try + { + Expr ns = ctx.mkNot((BoolExpr) e); + @SuppressWarnings("unused") + BoolExpr ens = (BoolExpr) ns; + } catch (ClassCastException ex) + { + throw new TestFailedException(); + } + } + } + + // / Shows how to read an SMT1 file. + + void smt1FileTest(String filename) + { + System.out.print("SMT File test "); + + { + HashMap<String, String> cfg = new HashMap<String, String>(); + Context ctx = new Context(cfg); + ctx.parseSMTLIBFile(filename, null, null, null, null); + + BoolExpr a = ctx.mkAnd(ctx.getSMTLIBFormulas()); + System.out.println("read formula: " + a); + } + } + + // / Shows how to read an SMT2 file. + + void smt2FileTest(String filename) + { + Date before = new Date(); + + System.out.println("SMT2 File test "); + System.gc(); + + { + HashMap<String, String> cfg = new HashMap<String, String>(); + cfg.put("model", "true"); + Context ctx = new Context(cfg); + Expr a = ctx.parseSMTLIB2File(filename, null, null, null, null); + + long t_diff = ((new Date()).getTime() - before.getTime()) / 1000; + + System.out.println("SMT2 file read time: " + t_diff + " sec"); + + // Iterate over the formula. + + LinkedList<Expr> q = new LinkedList<Expr>(); + q.add(a); + int cnt = 0; + while (q.size() > 0) + { + AST cur = (AST) q.removeFirst(); + cnt++; + + if (cur.getClass() == Expr.class) + if (!(cur.isVar())) + for (Expr c : ((Expr) cur).getArgs()) + q.add(c); + } + System.out.println(cnt + " ASTs"); + } + + long t_diff = ((new Date()).getTime() - before.getTime()) / 1000; + System.out.println("SMT2 file test took " + t_diff + " sec"); + } + + // / Shows how to use Solver(logic) + + // / @param ctx + void logicExample(Context ctx) throws TestFailedException + { + System.out.println("LogicTest"); + Log.append("LogicTest"); + + com.microsoft.z3.Global.ToggleWarningMessages(true); + + BitVecSort bvs = ctx.mkBitVecSort(32); + Expr x = ctx.mkConst("x", bvs); + Expr y = ctx.mkConst("y", bvs); + BoolExpr eq = ctx.mkEq(x, y); + + // Use a solver for QF_BV + Solver s = ctx.mkSolver("QF_BV"); + s.add(eq); + Status res = s.check(); + System.out.println("solver result: " + res); + + // Or perhaps a tactic for QF_BV + Goal g = ctx.mkGoal(true, false, false); + g.add(eq); + + Tactic t = ctx.mkTactic("qfbv"); + ApplyResult ar = t.apply(g); + System.out.println("tactic result: " + ar); + + if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat()) + throw new TestFailedException(); + } + + // / Demonstrates how to use the ParOr tactic. + + void parOrExample(Context ctx) throws TestFailedException + { + System.out.println("ParOrExample"); + Log.append("ParOrExample"); + + BitVecSort bvs = ctx.mkBitVecSort(32); + Expr x = ctx.mkConst("x", bvs); + Expr y = ctx.mkConst("y", bvs); + BoolExpr q = ctx.mkEq(x, y); + + Goal g = ctx.mkGoal(true, false, false); + g.add(q); + + Tactic t1 = ctx.mkTactic("qfbv"); + Tactic t2 = ctx.mkTactic("qfbv"); + Tactic p = ctx.parOr(t1, t2); + + ApplyResult ar = p.apply(g); + + if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat()) + throw new TestFailedException(); + } + + void bigIntCheck(Context ctx, RatNum r) + { + System.out.println("Num: " + r.getBigIntNumerator()); + System.out.println("Den: " + r.getBigIntDenominator()); + } + + // / Find a model for <code>x xor y</code>. + + public void findModelExample1(Context ctx) throws TestFailedException + { + System.out.println("FindModelExample1"); + Log.append("FindModelExample1"); + + BoolExpr x = ctx.mkBoolConst("x"); + BoolExpr y = ctx.mkBoolConst("y"); + BoolExpr x_xor_y = ctx.mkXor(x, y); + + Model model = check(ctx, x_xor_y, Status.SATISFIABLE); + System.out.println("x = " + model.evaluate(x, false) + ", y = " + + model.evaluate(y, false)); + } + + // / Find a model for <tt>x < y + 1, x > 2</tt>. + // / Then, assert <tt>not(x = y)</tt>, and find another model. + + public void findModelExample2(Context ctx) throws TestFailedException + { + System.out.println("FindModelExample2"); + Log.append("FindModelExample2"); + + IntExpr x = ctx.mkIntConst("x"); + IntExpr y = ctx.mkIntConst("y"); + IntExpr one = ctx.mkInt(1); + IntExpr two = ctx.mkInt(2); + + ArithExpr y_plus_one = ctx.mkAdd(y, one); + + BoolExpr c1 = ctx.mkLt(x, y_plus_one); + BoolExpr c2 = ctx.mkGt(x, two); + + BoolExpr q = ctx.mkAnd(c1, c2); + + System.out.println("model for: x < y + 1, x > 2"); + Model model = check(ctx, q, Status.SATISFIABLE); + System.out.println("x = " + model.evaluate(x, false) + ", y =" + + model.evaluate(y, false)); + + /* assert not(x = y) */ + BoolExpr x_eq_y = ctx.mkEq(x, y); + BoolExpr c3 = ctx.mkNot(x_eq_y); + + q = ctx.mkAnd(q, c3); + + System.out.println("model for: x < y + 1, x > 2, not(x = y)"); + model = check(ctx, q, Status.SATISFIABLE); + System.out.println("x = " + model.evaluate(x, false) + ", y = " + + model.evaluate(y, false)); + } + + // / Prove <tt>x = y implies g(x) = g(y)</tt>, and + // / disprove <tt>x = y implies g(g(x)) = g(y)</tt>. + + // / <remarks>This function demonstrates how to create uninterpreted + // / types and functions.</remarks> + public void proveExample1(Context ctx) throws TestFailedException + { + System.out.println("ProveExample1"); + Log.append("ProveExample1"); + + /* create uninterpreted type. */ + Sort U = ctx.mkUninterpretedSort(ctx.mkSymbol("U")); + + /* declare function g */ + FuncDecl g = ctx.mkFuncDecl("g", U, U); + + /* create x and y */ + Expr x = ctx.mkConst("x", U); + Expr y = ctx.mkConst("y", U); + /* create g(x), g(y) */ + Expr gx = g.apply(x); + Expr gy = g.apply(y); + + /* assert x = y */ + BoolExpr eq = ctx.mkEq(x, y); + + /* prove g(x) = g(y) */ + BoolExpr f = ctx.mkEq(gx, gy); + System.out.println("prove: x = y implies g(x) = g(y)"); + prove(ctx, ctx.mkImplies(eq, f), false); + + /* create g(g(x)) */ + Expr ggx = g.apply(gx); + + /* disprove g(g(x)) = g(y) */ + f = ctx.mkEq(ggx, gy); + System.out.println("disprove: x = y implies g(g(x)) = g(y)"); + disprove(ctx, ctx.mkImplies(eq, f), false); + + /* Print the model using the custom model printer */ + Model m = check(ctx, ctx.mkNot(f), Status.SATISFIABLE); + System.out.println(m); + } + + // / Prove <tt>not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 + // </tt>. + // / Then, show that <tt>z < -1</tt> is not implied. + + // / <remarks>This example demonstrates how to combine uninterpreted + // functions + // / and arithmetic.</remarks> + public void proveExample2(Context ctx) throws TestFailedException + { + System.out.println("ProveExample2"); + Log.append("ProveExample2"); + + /* declare function g */ + Sort I = ctx.getIntSort(); + + FuncDecl g = ctx.mkFuncDecl("g", I, I); + + /* create x, y, and z */ + IntExpr x = ctx.mkIntConst("x"); + IntExpr y = ctx.mkIntConst("y"); + IntExpr z = ctx.mkIntConst("z"); + + /* create gx, gy, gz */ + Expr gx = ctx.mkApp(g, x); + Expr gy = ctx.mkApp(g, y); + Expr gz = ctx.mkApp(g, z); + + /* create zero */ + IntExpr zero = ctx.mkInt(0); + + /* assert not(g(g(x) - g(y)) = g(z)) */ + ArithExpr gx_gy = ctx.mkSub((IntExpr) gx, (IntExpr) gy); + Expr ggx_gy = ctx.mkApp(g, gx_gy); + BoolExpr eq = ctx.mkEq(ggx_gy, gz); + BoolExpr c1 = ctx.mkNot(eq); + + /* assert x + z <= y */ + ArithExpr x_plus_z = ctx.mkAdd(x, z); + BoolExpr c2 = ctx.mkLe(x_plus_z, y); + + /* assert y <= x */ + BoolExpr c3 = ctx.mkLe(y, x); + + /* prove z < 0 */ + BoolExpr f = ctx.mkLt(z, zero); + System.out + .println("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0"); + prove(ctx, f, false, c1, c2, c3); + + /* disprove z < -1 */ + IntExpr minus_one = ctx.mkInt(-1); + f = ctx.mkLt(z, minus_one); + System.out + .println("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1"); + disprove(ctx, f, false, c1, c2, c3); + } + + // / Show how push & pop can be used to create "backtracking" points. + + // / <remarks>This example also demonstrates how big numbers can be + // / created in ctx.</remarks> + public void pushPopExample1(Context ctx) throws TestFailedException + { + System.out.println("PushPopExample1"); + Log.append("PushPopExample1"); + + /* create a big number */ + IntSort int_type = ctx.getIntSort(); + IntExpr big_number = ctx + .mkInt("1000000000000000000000000000000000000000000000000000000"); + + /* create number 3 */ + IntExpr three = (IntExpr) ctx.mkNumeral("3", int_type); + + /* create x */ + IntExpr x = ctx.mkIntConst("x"); + + Solver solver = ctx.mkSolver(); + + /* assert x >= "big number" */ + BoolExpr c1 = ctx.mkGe(x, big_number); + System.out.println("assert: x >= 'big number'"); + solver.add(c1); + + /* create a backtracking point */ + System.out.println("push"); + solver.push(); + + /* assert x <= 3 */ + BoolExpr c2 = ctx.mkLe(x, three); + System.out.println("assert: x <= 3"); + solver.add(c2); + + /* context is inconsistent at this point */ + if (solver.check() != Status.UNSATISFIABLE) + throw new TestFailedException(); + + /* + * backtrack: the constraint x <= 3 will be removed, since it was + * asserted after the last ctx.Push. + */ + System.out.println("pop"); + solver.pop(1); + + /* the context is consistent again. */ + if (solver.check() != Status.SATISFIABLE) + throw new TestFailedException(); + + /* new constraints can be asserted... */ + + /* create y */ + IntExpr y = ctx.mkIntConst("y"); + + /* assert y > x */ + BoolExpr c3 = ctx.mkGt(y, x); + System.out.println("assert: y > x"); + solver.add(c3); + + /* the context is still consistent. */ + if (solver.check() != Status.SATISFIABLE) + throw new TestFailedException(); + } + + // / Tuples. + + // / <remarks>Check that the projection of a tuple + // / returns the corresponding element.</remarks> + public void tupleExample(Context ctx) throws TestFailedException + { + System.out.println("TupleExample"); + Log.append("TupleExample"); + + Sort int_type = ctx.getIntSort(); + TupleSort tuple = ctx.mkTupleSort(ctx.mkSymbol("mk_tuple"), // name of + // tuple + // constructor + new Symbol[] { ctx.mkSymbol("first"), ctx.mkSymbol("second") }, // names + // of + // projection + // operators + new Sort[] { int_type, int_type } // types of projection + // operators + ); + FuncDecl first = tuple.getFieldDecls()[0]; // declarations are for + // projections + @SuppressWarnings("unused") + FuncDecl second = tuple.getFieldDecls()[1]; + Expr x = ctx.mkConst("x", int_type); + Expr y = ctx.mkConst("y", int_type); + Expr n1 = tuple.mkDecl().apply(x, y); + Expr n2 = first.apply(n1); + BoolExpr n3 = ctx.mkEq(x, n2); + System.out.println("Tuple example: " + n3); + prove(ctx, n3, false); + } + + // / Simple bit-vector example. + + // / <remarks> + // / This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) + // machine integers + // / </remarks> + public void bitvectorExample1(Context ctx) throws TestFailedException + { + System.out.println("BitvectorExample1"); + Log.append("BitvectorExample1"); + + Sort bv_type = ctx.mkBitVecSort(32); + BitVecExpr x = (BitVecExpr) ctx.mkConst("x", bv_type); + BitVecNum zero = (BitVecNum) ctx.mkNumeral("0", bv_type); + BitVecNum ten = ctx.mkBV(10, 32); + BitVecExpr x_minus_ten = ctx.mkBVSub(x, ten); + /* bvsle is signed less than or equal to */ + BoolExpr c1 = ctx.mkBVSLE(x, ten); + BoolExpr c2 = ctx.mkBVSLE(x_minus_ten, zero); + BoolExpr thm = ctx.mkIff(c1, c2); + System.out + .println("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers"); + disprove(ctx, thm, false); + } + + // / Find x and y such that: x ^ y - 103 == x * y + + public void bitvectorExample2(Context ctx) throws TestFailedException + { + System.out.println("BitvectorExample2"); + Log.append("BitvectorExample2"); + + /* construct x ^ y - 103 == x * y */ + Sort bv_type = ctx.mkBitVecSort(32); + BitVecExpr x = ctx.mkBVConst("x", 32); + BitVecExpr y = ctx.mkBVConst("y", 32); + BitVecExpr x_xor_y = ctx.mkBVXOR(x, y); + BitVecExpr c103 = (BitVecNum) ctx.mkNumeral("103", bv_type); + BitVecExpr lhs = ctx.mkBVSub(x_xor_y, c103); + BitVecExpr rhs = ctx.mkBVMul(x, y); + BoolExpr ctr = ctx.mkEq(lhs, rhs); + + System.out + .println("find values of x and y, such that x ^ y - 103 == x * y"); + + /* find a model (i.e., values for x an y that satisfy the constraint */ + Model m = check(ctx, ctr, Status.SATISFIABLE); + System.out.println(m); + } + + // / Demonstrates how to use the SMTLIB parser. + + public void parserExample1(Context ctx) throws TestFailedException + { + System.out.println("ParserExample1"); + Log.append("ParserExample1"); + + ctx.parseSMTLIBString( + "(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))", + null, null, null, null); + for (BoolExpr f : ctx.getSMTLIBFormulas()) + System.out.println("formula " + f); + + @SuppressWarnings("unused") + Model m = check(ctx, ctx.mkAnd(ctx.getSMTLIBFormulas()), + Status.SATISFIABLE); + } + + // / Demonstrates how to initialize the parser symbol table. + + public void parserExample2(Context ctx) throws TestFailedException + { + System.out.println("ParserExample2"); + Log.append("ParserExample2"); + + Symbol[] declNames = { ctx.mkSymbol("a"), ctx.mkSymbol("b") }; + FuncDecl a = ctx.mkConstDecl(declNames[0], ctx.mkIntSort()); + FuncDecl b = ctx.mkConstDecl(declNames[1], ctx.mkIntSort()); + FuncDecl[] decls = new FuncDecl[] { a, b }; + + ctx.parseSMTLIBString("(benchmark tst :formula (> a b))", null, null, + declNames, decls); + BoolExpr f = ctx.getSMTLIBFormulas()[0]; + System.out.println("formula: " + f); + check(ctx, f, Status.SATISFIABLE); + } + + // / Demonstrates how to initialize the parser symbol table. + + public void parserExample3(Context ctx) throws Exception + { + System.out.println("ParserExample3"); + Log.append("ParserExample3"); + + /* declare function g */ + Sort I = ctx.mkIntSort(); + FuncDecl g = ctx.mkFuncDecl("g", new Sort[] { I, I }, I); + + BoolExpr ca = commAxiom(ctx, g); + + ctx.parseSMTLIBString( + "(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (gg x 0) (gg 0 y)))))", + null, null, new Symbol[] { ctx.mkSymbol("gg") }, + new FuncDecl[] { g }); + + BoolExpr thm = ctx.getSMTLIBFormulas()[0]; + System.out.println("formula: " + thm); + prove(ctx, thm, false, ca); + } + + // / Display the declarations, assumptions and formulas in a SMT-LIB string. + + public void parserExample4(Context ctx) + { + System.out.println("ParserExample4"); + Log.append("ParserExample4"); + + ctx.parseSMTLIBString( + "(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))", + null, null, null, null); + for (FuncDecl decl : ctx.getSMTLIBDecls()) + { + System.out.println("Declaration: " + decl); + } + for (BoolExpr f : ctx.getSMTLIBAssumptions()) + { + System.out.println("Assumption: " + f); + } + for (BoolExpr f : ctx.getSMTLIBFormulas()) + { + System.out.println("Formula: " + f); + } + } + + // / Demonstrates how to handle parser errors using Z3 error handling + // support. + + // / <remarks></remarks> + public void parserExample5(Context ctx) + { + System.out.println("ParserExample5"); + + try + { + ctx.parseSMTLIBString( + /* + * the following string has a parsing error: missing + * parenthesis + */ + "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))", + null, null, null, null); + } catch (Z3Exception e) + { + System.out.println("Z3 error: " + e); + } + } + + // / Create an ite-Expr (if-then-else Exprs). + + public void iteExample(Context ctx) + { + System.out.println("ITEExample"); + Log.append("ITEExample"); + + BoolExpr f = ctx.mkFalse(); + Expr one = ctx.mkInt(1); + Expr zero = ctx.mkInt(0); + Expr ite = ctx.mkITE(f, one, zero); + + System.out.println("Expr: " + ite); + } + + // / Create an enumeration data type. + + public void enumExample(Context ctx) throws TestFailedException + { + System.out.println("EnumExample"); + Log.append("EnumExample"); + + Symbol name = ctx.mkSymbol("fruit"); + + EnumSort fruit = ctx.mkEnumSort(name, ctx.mkSymbol("apple"), + ctx.mkSymbol("banana"), ctx.mkSymbol("orange")); + + System.out.println((fruit.getConsts()[0])); + System.out.println((fruit.getConsts()[1])); + System.out.println((fruit.getConsts()[2])); + + System.out.println((fruit.getTesterDecls()[0])); + System.out.println((fruit.getTesterDecls()[1])); + System.out.println((fruit.getTesterDecls()[2])); + + Expr apple = fruit.getConsts()[0]; + Expr banana = fruit.getConsts()[1]; + Expr orange = fruit.getConsts()[2]; + + /* Apples are different from oranges */ + prove(ctx, ctx.mkNot(ctx.mkEq(apple, orange)), false); + + /* Apples pass the apple test */ + prove(ctx, (BoolExpr) ctx.mkApp(fruit.getTesterDecls()[0], apple), + false); + + /* Oranges fail the apple test */ + disprove(ctx, (BoolExpr) ctx.mkApp(fruit.getTesterDecls()[0], orange), + false); + prove(ctx, + (BoolExpr) ctx.mkNot((BoolExpr) ctx.mkApp( + fruit.getTesterDecls()[0], orange)), false); + + Expr fruity = ctx.mkConst("fruity", fruit); + + /* If something is fruity, then it is an apple, banana, or orange */ + + prove(ctx, + ctx.mkOr(ctx.mkEq(fruity, apple), ctx.mkEq(fruity, banana), + ctx.mkEq(fruity, orange)), false); + } + + // / Create a list datatype. + + public void listExample(Context ctx) throws TestFailedException + { + System.out.println("ListExample"); + Log.append("ListExample"); + + Sort int_ty; + ListSort int_list; + Expr nil, l1, l2, x, y, u, v; + BoolExpr fml, fml1; + + int_ty = ctx.mkIntSort(); + + int_list = ctx.mkListSort(ctx.mkSymbol("int_list"), int_ty); + + nil = ctx.mkConst(int_list.getNilDecl()); + l1 = ctx.mkApp(int_list.getConsDecl(), ctx.mkInt(1), nil); + l2 = ctx.mkApp(int_list.getConsDecl(), ctx.mkInt(2), nil); + + /* nil != cons(1, nil) */ + prove(ctx, ctx.mkNot(ctx.mkEq(nil, l1)), false); + + /* cons(2,nil) != cons(1, nil) */ + prove(ctx, ctx.mkNot(ctx.mkEq(l1, l2)), false); + + /* cons(x,nil) = cons(y, nil) => x = y */ + x = ctx.mkConst("x", int_ty); + y = ctx.mkConst("y", int_ty); + l1 = ctx.mkApp(int_list.getConsDecl(), x, nil); + l2 = ctx.mkApp(int_list.getConsDecl(), y, nil); + prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false); + + /* cons(x,u) = cons(x, v) => u = v */ + u = ctx.mkConst("u", int_list); + v = ctx.mkConst("v", int_list); + l1 = ctx.mkApp(int_list.getConsDecl(), x, u); + l2 = ctx.mkApp(int_list.getConsDecl(), y, v); + prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(u, v)), false); + prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false); + + /* is_nil(u) or is_cons(u) */ + prove(ctx, ctx.mkOr((BoolExpr) ctx.mkApp(int_list.getIsNilDecl(), u), + (BoolExpr) ctx.mkApp(int_list.getIsConsDecl(), u)), false); + + /* occurs check u != cons(x,u) */ + prove(ctx, ctx.mkNot(ctx.mkEq(u, l1)), false); + + /* destructors: is_cons(u) => u = cons(head(u),tail(u)) */ + fml1 = ctx.mkEq( + u, + ctx.mkApp(int_list.getConsDecl(), + ctx.mkApp(int_list.getHeadDecl(), u), + ctx.mkApp(int_list.getTailDecl(), u))); + fml = ctx.mkImplies((BoolExpr) ctx.mkApp(int_list.getIsConsDecl(), u), + fml1); + System.out.println("Formula " + fml); + + prove(ctx, fml, false); + + disprove(ctx, fml1, false); + } + + // / Create a binary tree datatype. + + public void treeExample(Context ctx) throws TestFailedException + { + System.out.println("TreeExample"); + Log.append("TreeExample"); + + Sort cell; + FuncDecl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl; + Expr nil, l1, l2, x, y, u, v; + BoolExpr fml, fml1; + String[] head_tail = new String[] { "car", "cdr" }; + Sort[] sorts = new Sort[] { null, null }; + int[] sort_refs = new int[] { 0, 0 }; + Constructor nil_con, cons_con; + + nil_con = ctx.mkConstructor("nil", "is_nil", null, null, null); + cons_con = ctx.mkConstructor("cons", "is_cons", head_tail, sorts, + sort_refs); + Constructor[] constructors = new Constructor[] { nil_con, cons_con }; + + cell = ctx.mkDatatypeSort("cell", constructors); + + nil_decl = nil_con.ConstructorDecl(); + is_nil_decl = nil_con.getTesterDecl(); + cons_decl = cons_con.ConstructorDecl(); + is_cons_decl = cons_con.getTesterDecl(); + FuncDecl[] cons_accessors = cons_con.getAccessorDecls(); + car_decl = cons_accessors[0]; + cdr_decl = cons_accessors[1]; + + nil = ctx.mkConst(nil_decl); + l1 = ctx.mkApp(cons_decl, nil, nil); + l2 = ctx.mkApp(cons_decl, l1, nil); + + /* nil != cons(nil, nil) */ + prove(ctx, ctx.mkNot(ctx.mkEq(nil, l1)), false); + + /* cons(x,u) = cons(x, v) => u = v */ + u = ctx.mkConst("u", cell); + v = ctx.mkConst("v", cell); + x = ctx.mkConst("x", cell); + y = ctx.mkConst("y", cell); + l1 = ctx.mkApp(cons_decl, x, u); + l2 = ctx.mkApp(cons_decl, y, v); + prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(u, v)), false); + prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false); + + /* is_nil(u) or is_cons(u) */ + prove(ctx, + ctx.mkOr((BoolExpr) ctx.mkApp(is_nil_decl, u), + (BoolExpr) ctx.mkApp(is_cons_decl, u)), false); + + /* occurs check u != cons(x,u) */ + prove(ctx, ctx.mkNot(ctx.mkEq(u, l1)), false); + + /* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */ + fml1 = ctx.mkEq( + u, + ctx.mkApp(cons_decl, ctx.mkApp(car_decl, u), + ctx.mkApp(cdr_decl, u))); + fml = ctx.mkImplies((BoolExpr) ctx.mkApp(is_cons_decl, u), fml1); + System.out.println("Formula " + fml); + prove(ctx, fml, false); + + disprove(ctx, fml1, false); + } + + // / Create a forest of trees. + + // / <remarks> + // / forest ::= nil | cons(tree, forest) + // / tree ::= nil | cons(forest, forest) + // / </remarks> + public void forestExample(Context ctx) throws TestFailedException + { + System.out.println("ForestExample"); + Log.append("ForestExample"); + + Sort tree, forest; + @SuppressWarnings("unused") + FuncDecl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl; + @SuppressWarnings("unused") + FuncDecl nil2_decl, is_nil2_decl, cons2_decl, is_cons2_decl, car2_decl, cdr2_decl; + @SuppressWarnings("unused") + Expr nil1, nil2, t1, t2, t3, t4, f1, f2, f3, l1, l2, x, y, u, v; + + // + // Declare the names of the accessors for cons. + // Then declare the sorts of the accessors. + // For this example, all sorts refer to the new types 'forest' and + // 'tree' + // being declared, so we pass in null for both sorts1 and sorts2. + // On the other hand, the sort_refs arrays contain the indices of the + // two new sorts being declared. The first element in sort1_refs + // points to 'tree', which has index 1, the second element in sort1_refs + // array + // points to 'forest', which has index 0. + // + Symbol[] head_tail1 = new Symbol[] { ctx.mkSymbol("head"), + ctx.mkSymbol("tail") }; + Sort[] sorts1 = new Sort[] { null, null }; + int[] sort1_refs = new int[] { 1, 0 }; // the first item points to a + // tree, the second to a forest + + Symbol[] head_tail2 = new Symbol[] { ctx.mkSymbol("car"), + ctx.mkSymbol("cdr") }; + Sort[] sorts2 = new Sort[] { null, null }; + int[] sort2_refs = new int[] { 0, 0 }; // both items point to the forest + // datatype. + Constructor nil1_con, cons1_con, nil2_con, cons2_con; + Constructor[] constructors1 = new Constructor[2], constructors2 = new Constructor[2]; + Symbol[] sort_names = { ctx.mkSymbol("forest"), ctx.mkSymbol("tree") }; + + /* build a forest */ + nil1_con = ctx.mkConstructor(ctx.mkSymbol("nil"), + ctx.mkSymbol("is_nil"), null, null, null); + cons1_con = ctx.mkConstructor(ctx.mkSymbol("cons1"), + ctx.mkSymbol("is_cons1"), head_tail1, sorts1, sort1_refs); + constructors1[0] = nil1_con; + constructors1[1] = cons1_con; + + /* build a tree */ + nil2_con = ctx.mkConstructor(ctx.mkSymbol("nil2"), + ctx.mkSymbol("is_nil2"), null, null, null); + cons2_con = ctx.mkConstructor(ctx.mkSymbol("cons2"), + ctx.mkSymbol("is_cons2"), head_tail2, sorts2, sort2_refs); + constructors2[0] = nil2_con; + constructors2[1] = cons2_con; + + Constructor[][] clists = new Constructor[][] { constructors1, + constructors2 }; + + Sort[] sorts = ctx.mkDatatypeSorts(sort_names, clists); + forest = sorts[0]; + tree = sorts[1]; + + // + // Now that the datatype has been created. + // Query the constructors for the constructor + // functions, testers, and field accessors. + // + nil1_decl = nil1_con.ConstructorDecl(); + is_nil1_decl = nil1_con.getTesterDecl(); + cons1_decl = cons1_con.ConstructorDecl(); + is_cons1_decl = cons1_con.getTesterDecl(); + FuncDecl[] cons1_accessors = cons1_con.getAccessorDecls(); + car1_decl = cons1_accessors[0]; + cdr1_decl = cons1_accessors[1]; + + nil2_decl = nil2_con.ConstructorDecl(); + is_nil2_decl = nil2_con.getTesterDecl(); + cons2_decl = cons2_con.ConstructorDecl(); + is_cons2_decl = cons2_con.getTesterDecl(); + FuncDecl[] cons2_accessors = cons2_con.getAccessorDecls(); + car2_decl = cons2_accessors[0]; + cdr2_decl = cons2_accessors[1]; + + nil1 = ctx.mkConst(nil1_decl); + nil2 = ctx.mkConst(nil2_decl); + f1 = ctx.mkApp(cons1_decl, nil2, nil1); + t1 = ctx.mkApp(cons2_decl, nil1, nil1); + t2 = ctx.mkApp(cons2_decl, f1, nil1); + t3 = ctx.mkApp(cons2_decl, f1, f1); + t4 = ctx.mkApp(cons2_decl, nil1, f1); + f2 = ctx.mkApp(cons1_decl, t1, nil1); + f3 = ctx.mkApp(cons1_decl, t1, f1); + + /* nil != cons(nil,nil) */ + prove(ctx, ctx.mkNot(ctx.mkEq(nil1, f1)), false); + prove(ctx, ctx.mkNot(ctx.mkEq(nil2, t1)), false); + + /* cons(x,u) = cons(x, v) => u = v */ + u = ctx.mkConst("u", forest); + v = ctx.mkConst("v", forest); + x = ctx.mkConst("x", tree); + y = ctx.mkConst("y", tree); + l1 = ctx.mkApp(cons1_decl, x, u); + l2 = ctx.mkApp(cons1_decl, y, v); + prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(u, v)), false); + prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false); + + /* is_nil(u) or is_cons(u) */ + prove(ctx, + ctx.mkOr((BoolExpr) ctx.mkApp(is_nil1_decl, u), + (BoolExpr) ctx.mkApp(is_cons1_decl, u)), false); + + /* occurs check u != cons(x,u) */ + prove(ctx, ctx.mkNot(ctx.mkEq(u, l1)), false); + } + + // / Demonstrate how to use #Eval. + + public void evalExample1(Context ctx) + { + System.out.println("EvalExample1"); + Log.append("EvalExample1"); + + IntExpr x = ctx.mkIntConst("x"); + IntExpr y = ctx.mkIntConst("y"); + IntExpr two = ctx.mkInt(2); + + Solver solver = ctx.mkSolver(); + + /* assert x < y */ + solver.add(ctx.mkLt(x, y)); + + /* assert x > 2 */ + solver.add(ctx.mkGt(x, two)); + + /* find model for the constraints above */ + Model model = null; + if (Status.SATISFIABLE == solver.check()) + { + model = solver.getModel(); + System.out.println(model); + System.out.println("\nevaluating x+y"); + Expr v = model.evaluate(ctx.mkAdd(x, y), false); + if (v != null) + { + System.out.println("result = " + (v)); + } else + { + System.out.println("Failed to evaluate: x+y"); + } + } else + { + System.out.println("BUG, the constraints are satisfiable."); + } + } + + // / Demonstrate how to use #Eval on tuples. + + public void evalExample2(Context ctx) + { + System.out.println("EvalExample2"); + Log.append("EvalExample2"); + + Sort int_type = ctx.getIntSort(); + TupleSort tuple = ctx.mkTupleSort(ctx.mkSymbol("mk_tuple"), // name of + // tuple + // constructor + new Symbol[] { ctx.mkSymbol("first"), ctx.mkSymbol("second") }, // names + // of + // projection + // operators + new Sort[] { int_type, int_type } // types of projection + // operators + ); + FuncDecl first = tuple.getFieldDecls()[0]; // declarations are for + // projections + FuncDecl second = tuple.getFieldDecls()[1]; + Expr tup1 = ctx.mkConst("t1", tuple); + Expr tup2 = ctx.mkConst("t2", tuple); + + Solver solver = ctx.mkSolver(); + + /* assert tup1 != tup2 */ + solver.add(ctx.mkNot(ctx.mkEq(tup1, tup2))); + /* assert first tup1 = first tup2 */ + solver.add(ctx.mkEq(ctx.mkApp(first, tup1), ctx.mkApp(first, tup2))); + + /* find model for the constraints above */ + Model model = null; + if (Status.SATISFIABLE == solver.check()) + { + model = solver.getModel(); + System.out.println(model); + System.out.println("evaluating tup1 " + + (model.evaluate(tup1, false))); + System.out.println("evaluating tup2 " + + (model.evaluate(tup2, false))); + System.out.println("evaluating second(tup2) " + + (model.evaluate(ctx.mkApp(second, tup2), false))); + } else + { + System.out.println("BUG, the constraints are satisfiable."); + } + } + + // / Demonstrate how to use <code>Push</code>and <code>Pop</code>to + // / control the size of models. + + // / <remarks>Note: this test is specialized to 32-bit bitvectors.</remarks> + public void checkSmall(Context ctx, Solver solver, BitVecExpr... to_minimize) + { + int num_Exprs = to_minimize.length; + int[] upper = new int[num_Exprs]; + int[] lower = new int[num_Exprs]; + for (int i = 0; i < upper.length; ++i) + { + upper[i] = Integer.MAX_VALUE; + lower[i] = 0; + } + boolean some_work = true; + int last_index = -1; + int last_upper = 0; + while (some_work) + { + solver.push(); + + boolean check_is_sat = true; + while (check_is_sat && some_work) + { + // Assert all feasible bounds. + for (int i = 0; i < num_Exprs; ++i) + { + solver.add(ctx.mkBVULE(to_minimize[i], + ctx.mkBV(upper[i], 32))); + } + + check_is_sat = Status.SATISFIABLE == solver.check(); + if (!check_is_sat) + { + if (last_index != -1) + { + lower[last_index] = last_upper + 1; + } + break; + } + System.out.println(solver.getModel()); + + // narrow the bounds based on the current model. + for (int i = 0; i < num_Exprs; ++i) + { + Expr v = solver.getModel().evaluate(to_minimize[i], false); + int ui = ((BitVecNum) v).getInt(); + if (ui < upper[i]) + { + upper[i] = (int) ui; + } + System.out.println(i + " " + lower[i] + " " + upper[i]); + } + + // find a new bound to add + some_work = false; + last_index = 0; + for (int i = 0; i < num_Exprs; ++i) + { + if (lower[i] < upper[i]) + { + last_upper = (upper[i] + lower[i]) / 2; + last_index = i; + solver.add(ctx.mkBVULE(to_minimize[i], + ctx.mkBV(last_upper, 32))); + some_work = true; + break; + } + } + } + solver.pop(); + } + } + + // / Reduced-size model generation example. + + public void findSmallModelExample(Context ctx) + { + System.out.println("FindSmallModelExample"); + Log.append("FindSmallModelExample"); + + BitVecExpr x = ctx.mkBVConst("x", 32); + BitVecExpr y = ctx.mkBVConst("y", 32); + BitVecExpr z = ctx.mkBVConst("z", 32); + + Solver solver = ctx.mkSolver(); + + solver.add(ctx.mkBVULE(x, ctx.mkBVAdd(y, z))); + checkSmall(ctx, solver, x, y, z); + } + + // / Simplifier example. + + public void simplifierExample(Context ctx) + { + System.out.println("SimplifierExample"); + Log.append("SimplifierExample"); + + IntExpr x = ctx.mkIntConst("x"); + IntExpr y = ctx.mkIntConst("y"); + IntExpr z = ctx.mkIntConst("z"); + @SuppressWarnings("unused") + IntExpr u = ctx.mkIntConst("u"); + + Expr t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z))); + Expr t2 = t1.simplify(); + System.out.println((t1) + " -> " + (t2)); + } + + // / Extract unsatisfiable core example + + public void unsatCoreAndProofExample(Context ctx) + { + System.out.println("UnsatCoreAndProofExample"); + Log.append("UnsatCoreAndProofExample"); + + Solver solver = ctx.mkSolver(); + + BoolExpr pa = ctx.mkBoolConst("PredA"); + BoolExpr pb = ctx.mkBoolConst("PredB"); + BoolExpr pc = ctx.mkBoolConst("PredC"); + BoolExpr pd = ctx.mkBoolConst("PredD"); + BoolExpr p1 = ctx.mkBoolConst("P1"); + BoolExpr p2 = ctx.mkBoolConst("P2"); + BoolExpr p3 = ctx.mkBoolConst("P3"); + BoolExpr p4 = ctx.mkBoolConst("P4"); + BoolExpr[] assumptions = new BoolExpr[] { ctx.mkNot(p1), ctx.mkNot(p2), + ctx.mkNot(p3), ctx.mkNot(p4) }; + BoolExpr f1 = ctx.mkAnd(pa, pb, pc); + BoolExpr f2 = ctx.mkAnd(pa, ctx.mkNot(pb), pc); + BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc)); + BoolExpr f4 = pd; + + solver.add(ctx.mkOr(f1, p1)); + solver.add(ctx.mkOr(f2, p2)); + solver.add(ctx.mkOr(f3, p3)); + solver.add(ctx.mkOr(f4, p4)); + Status result = solver.check(assumptions); + + if (result == Status.UNSATISFIABLE) + { + System.out.println("unsat"); + System.out.println("proof: " + solver.getProof()); + System.out.println("core: "); + for (Expr c : solver.getUnsatCore()) + { + System.out.println(c); + } + } + } + + /// Extract unsatisfiable core example with AssertAndTrack + + public void unsatCoreAndProofExample2(Context ctx) + { + System.out.println("UnsatCoreAndProofExample2"); + Log.append("UnsatCoreAndProofExample2"); + + Solver solver = ctx.mkSolver(); + + BoolExpr pa = ctx.mkBoolConst("PredA"); + BoolExpr pb = ctx.mkBoolConst("PredB"); + BoolExpr pc = ctx.mkBoolConst("PredC"); + BoolExpr pd = ctx.mkBoolConst("PredD"); + + BoolExpr f1 = ctx.mkAnd(new BoolExpr[] { pa, pb, pc }); + BoolExpr f2 = ctx.mkAnd(new BoolExpr[] { pa, ctx.mkNot(pb), pc }); + BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc)); + BoolExpr f4 = pd; + + BoolExpr p1 = ctx.mkBoolConst("P1"); + BoolExpr p2 = ctx.mkBoolConst("P2"); + BoolExpr p3 = ctx.mkBoolConst("P3"); + BoolExpr p4 = ctx.mkBoolConst("P4"); + + solver.assertAndTrack(f1, p1); + solver.assertAndTrack(f2, p2); + solver.assertAndTrack(f3, p3); + solver.assertAndTrack(f4, p4); + Status result = solver.check(); + + if (result == Status.UNSATISFIABLE) + { + System.out.println("unsat"); + System.out.println("core: "); + for (Expr c : solver.getUnsatCore()) + { + System.out.println(c); + } + } + } + + public void finiteDomainExample(Context ctx) + { + System.out.println("FiniteDomainExample"); + Log.append("FiniteDomainExample"); + + FiniteDomainSort s = ctx.mkFiniteDomainSort("S", 10); + FiniteDomainSort t = ctx.mkFiniteDomainSort("T", 10); + FiniteDomainNum s1 = (FiniteDomainNum)ctx.mkNumeral(1, s); + FiniteDomainNum t1 = (FiniteDomainNum)ctx.mkNumeral(1, t); + System.out.println(s); + System.out.println(t); + System.out.println(s1); + System.out.println(t1); + System.out.println(s1.getInt()); + System.out.println(t1.getInt()); + // But you cannot mix numerals of different sorts + // even if the size of their domains are the same: + // System.out.println(ctx.mkEq(s1, t1)); + } + + public void floatingPointExample1(Context ctx) throws TestFailedException + { + System.out.println("FloatingPointExample1"); + Log.append("FloatingPointExample1"); + + FPSort s = ctx.mkFPSort(11, 53); + System.out.println("Sort: " + s); + + FPNum x = (FPNum)ctx.mkNumeral("-1e1", s); /* -1 * 10^1 = -10 */ + FPNum y = (FPNum)ctx.mkNumeral("-10", s); /* -10 */ + FPNum z = (FPNum)ctx.mkNumeral("-1.25p3", s); /* -1.25 * 2^3 = -1.25 * 8 = -10 */ + System.out.println("x=" + x.toString() + + "; y=" + y.toString() + + "; z=" + z.toString()); + + BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z)); + check(ctx, ctx.mkNot(a), Status.UNSATISFIABLE); + + /* nothing is equal to NaN according to floating-point + * equality, so NaN == k should be unsatisfiable. */ + FPExpr k = (FPExpr)ctx.mkConst("x", s); + FPExpr nan = ctx.mkFPNaN(s); + + /* solver that runs the default tactic for QF_FP. */ + Solver slvr = ctx.mkSolver("QF_FP"); + slvr.add(ctx.mkFPEq(nan, k)); + if (slvr.check() != Status.UNSATISFIABLE) + throw new TestFailedException(); + System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr); + + /* NaN is equal to NaN according to normal equality. */ + slvr = ctx.mkSolver("QF_FP"); + slvr.add(ctx.mkEq(nan, nan)); + if (slvr.check() != Status.SATISFIABLE) + throw new TestFailedException(); + System.out.println("OK, sat:" + System.getProperty("line.separator") + slvr); + + /* Let's prove -1e1 * -1.25e3 == +100 */ + x = (FPNum)ctx.mkNumeral("-1e1", s); + y = (FPNum)ctx.mkNumeral("-1.25p3", s); + FPExpr x_plus_y = (FPExpr)ctx.mkConst("x_plus_y", s); + FPNum r = (FPNum)ctx.mkNumeral("100", s); + slvr = ctx.mkSolver("QF_FP"); + + slvr.add(ctx.mkEq(x_plus_y, ctx.mkFPMul(ctx.mkFPRoundNearestTiesToAway(), x, y))); + slvr.add(ctx.mkNot(ctx.mkFPEq(x_plus_y, r))); + if (slvr.check() != Status.UNSATISFIABLE) + throw new TestFailedException(); + System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr); + } + + public void floatingPointExample2(Context ctx) throws TestFailedException + { + System.out.println("FloatingPointExample2"); + Log.append("FloatingPointExample2"); + FPSort double_sort = ctx.mkFPSort(11, 53); + FPRMSort rm_sort = ctx.mkFPRoundingModeSort(); + + FPRMExpr rm = (FPRMExpr)ctx.mkConst(ctx.mkSymbol("rm"), rm_sort); + BitVecExpr x = (BitVecExpr)ctx.mkConst(ctx.mkSymbol("x"), ctx.mkBitVecSort(64)); + FPExpr y = (FPExpr)ctx.mkConst(ctx.mkSymbol("y"), double_sort); + FPExpr fp_val = ctx.mkFP(42, double_sort); + + BoolExpr c1 = ctx.mkEq(y, fp_val); + BoolExpr c2 = ctx.mkEq(x, ctx.mkFPToBV(rm, y, 64, false)); + BoolExpr c3 = ctx.mkEq(x, ctx.mkBV(42, 64)); + BoolExpr c4 = ctx.mkEq(ctx.mkNumeral(42, ctx.getRealSort()), ctx.mkFPToReal(fp_val)); + BoolExpr c5 = ctx.mkAnd(c1, c2, c3, c4); + System.out.println("c5 = " + c5); + + /* Generic solver */ + Solver s = ctx.mkSolver(); + s.add(c5); + + if (s.check() != Status.SATISFIABLE) + throw new TestFailedException(); + + System.out.println("OK, model: " + s.getModel().toString()); + } + + public void optimizeExample(Context ctx) + { + System.out.println("Opt"); + + Optimize opt = ctx.mkOptimize(); + + // Set constraints. + IntExpr xExp = ctx.mkIntConst("x"); + IntExpr yExp = ctx.mkIntConst("y"); + + opt.Add(ctx.mkEq(ctx.mkAdd(xExp, yExp), ctx.mkInt(10)), + ctx.mkGe(xExp, ctx.mkInt(0)), + ctx.mkGe(yExp, ctx.mkInt(0))); + + // Set objectives. + Optimize.Handle mx = opt.MkMaximize(xExp); + Optimize.Handle my = opt.MkMaximize(yExp); + + System.out.println(opt.Check()); + System.out.println(mx); + System.out.println(my); + } + + public void translationExample() { + Context ctx1 = new Context(); + Context ctx2 = new Context(); + + Sort s1 = ctx1.getIntSort(); + Sort s2 = ctx2.getIntSort(); + Sort s3 = (Sort) s1.translate(ctx2); + + System.out.println(s1 == s2); + System.out.println(s1.equals(s2)); + System.out.println(s2.equals(s3)); + System.out.println(s1.equals(s3)); + + Expr e1 = ctx1.mkIntConst("e1"); + Expr e2 = ctx2.mkIntConst("e1"); + Expr e3 = e1.translate(ctx2); + + System.out.println(e1 == e2); + System.out.println(e1.equals(e2)); + System.out.println(e2.equals(e3)); + System.out.println(e1.equals(e3)); + } + + public static void main(String[] args) + { + JavaExample p = new JavaExample(); + try + { + com.microsoft.z3.Global.ToggleWarningMessages(true); + Log.open("test.log"); + + System.out.print("Z3 Major Version: "); + System.out.println(Version.getMajor()); + System.out.print("Z3 Full Version: "); + System.out.println(Version.getString()); + System.out.print("Z3 Full Version String: "); + System.out.println(Version.getFullVersion()); + + p.simpleExample(); + + { // These examples need model generation turned on. + HashMap<String, String> cfg = new HashMap<String, String>(); + cfg.put("model", "true"); + Context ctx = new Context(cfg); + + p.optimizeExample(ctx); + p.basicTests(ctx); + p.castingTest(ctx); + p.sudokuExample(ctx); + p.quantifierExample1(ctx); + p.quantifierExample2(ctx); + p.logicExample(ctx); + p.parOrExample(ctx); + p.findModelExample1(ctx); + p.findModelExample2(ctx); + p.pushPopExample1(ctx); + p.arrayExample1(ctx); + p.arrayExample3(ctx); + p.bitvectorExample1(ctx); + p.bitvectorExample2(ctx); + p.parserExample1(ctx); + p.parserExample2(ctx); + p.parserExample4(ctx); + p.parserExample5(ctx); + p.iteExample(ctx); + p.evalExample1(ctx); + p.evalExample2(ctx); + p.findSmallModelExample(ctx); + p.simplifierExample(ctx); + p.finiteDomainExample(ctx); + p.floatingPointExample1(ctx); + p.floatingPointExample2(ctx); + } + + { // These examples need proof generation turned on. + HashMap<String, String> cfg = new HashMap<String, String>(); + cfg.put("proof", "true"); + Context ctx = new Context(cfg); + p.proveExample1(ctx); + p.proveExample2(ctx); + p.arrayExample2(ctx); + p.tupleExample(ctx); + p.parserExample3(ctx); + p.enumExample(ctx); + p.listExample(ctx); + p.treeExample(ctx); + p.forestExample(ctx); + p.unsatCoreAndProofExample(ctx); + p.unsatCoreAndProofExample2(ctx); + } + + { // These examples need proof generation turned on and auto-config + // set to false. + HashMap<String, String> cfg = new HashMap<String, String>(); + cfg.put("proof", "true"); + cfg.put("auto-config", "false"); + Context ctx = new Context(cfg); + p.quantifierExample3(ctx); + p.quantifierExample4(ctx); + } + + p.translationExample(); + + Log.close(); + if (Log.isOpen()) + System.out.println("Log is still open!"); + } catch (Z3Exception ex) + { + System.out.println("Z3 Managed Exception: " + ex.getMessage()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); + } catch (TestFailedException ex) + { + System.out.println("TEST CASE FAILED: " + ex.getMessage()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); + } catch (Exception ex) + { + System.out.println("Unknown Exception: " + ex.getMessage()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); + } + } +}
\ No newline at end of file |