{

@SuppressWarnings("serial")

static 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 <R extends Sort> BoolExpr injAxiom(Context ctx, FuncDecl<R> 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<Sort> finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range);

/* allocate temporary arrays */

/* fill types, names and xs */

Sort[] types = domain.clone();

List<Expr<Sort>> xs = IntStream.range(0, sz).mapToObj(j -> ctx.mkBound(j, types[j])).collect(Collectors.toList());

Symbol[] names = IntStream.range(0, sz).mapToObj(j -> ctx.mkSymbol(String.format("x_%d", j))).toArray(Symbol[]::new);

Expr<Sort> x_i = xs.get(i);

/* create f(x_0, ..., x_i, ..., x_{n-1}) */

Expr<R> fxs = f.apply(xs.toArray(new Expr[0]));

/* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */

Expr<Sort> finv_fxs = finv.apply(fxs);

/* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */

BoolExpr 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 */

return ctx.mkForall(types, /* types of quantified variables */

names, /* names of quantified variables */

eq, 1, new Pattern[] { p } /* patterns */, null, null, null);

}

// / 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 <R extends Sort> BoolExpr injAxiomAbs(Context ctx, FuncDecl<R> 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 */

R finv_domain = f.getRange();

Sort finv_range = domain[i];

FuncDecl<Sort> finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range);

/* allocate temporary arrays */

List<Expr<Sort>> xs = IntStream.range(0, sz).mapToObj(j -> ctx.mkConst(String.format("x_%d", j), domain[j])).collect(Collectors.toList());

/* fill types, names and xs */

Expr<Sort> x_i = xs.get(i);

/* create f(x_0, ..., x_i, ..., x_{n-1}) */

Expr<R> fxs = f.apply(xs.toArray(new Expr[0]));

/* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */

Expr<Sort> finv_fxs = finv.apply(fxs);

/* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */

BoolExpr 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 */

return ctx.mkForall(xs.toArray(new Expr[0]), /* types of quantified variables */

eq, /* names of quantified variables */

1, new Pattern[] { p } /* patterns */, null, null, null);

}

// / Assert the axiom: function f is commutative.

// / <remarks>

// / This example uses the SMT-LIB parser to simplify the axiom

// construction.

// / </remarks>

private <R extends Sort> BoolExpr commAxiom(Context ctx, FuncDecl<R> f) throws Exception

{

R t = f.getRange();

Sort[] dom = f.getDomain();

if (dom.length != 2 || !t.equals(dom[0]) || !t.equals(dom[1]))

{

System.out.printf("%d %s %s %s%n", dom.length, dom[0], dom[1], t);

throw new Exception("function must be binary, and argument types must be equal to return type");

}

String bench = String.format("(assert (forall (x %s) (y %s) (= (%s x y) (%s y x))))", t.getName(), t.getName(), f.getName(), f.getName());

return ctx.parseSMTLIB2String(bench, new Symbol[] { t.getName() },

new Sort[] { t }, new Symbol[] { f.getName() },

new FuncDecl[] { f })[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();

}

}

@SuppressWarnings("unchecked")

Model check(Context ctx, Expr<BoolSort> 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.printf("%nTactical solver: %s%n", s);

s.add(g.getFormulas());

System.out.printf("Solver: %s%n", s);

if (s.check() != sat)

throw new TestFailedException();

}

ApplyResult applyTactic(Context ctx, Tactic t, Goal g)

{

System.out.printf("%nGoal: %s%n", g);

ApplyResult res = t.apply(g);

System.out.printf("Application result: %s%n", 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, Expr<BoolSort> f, boolean useMBQI) throws TestFailedException

{

BoolExpr[] assumptions = new BoolExpr[0];

prove(ctx, f, useMBQI, assumptions);

}

@SafeVarargs

final void prove(Context ctx, Expr<BoolSort> f, boolean useMBQI,

Expr<BoolSort>... assumptions) throws TestFailedException

{

System.out.printf("Proving: %s%n", f);

Solver s = ctx.mkSolver();

Params p = ctx.mkParams();

p.add("mbqi", useMBQI);

s.setParameters(p);

s.add(assumptions);

s.add(ctx.mkNot(f));

Status q = s.check();

switch (q)

{

case UNKNOWN:

System.out.printf("Unknown because: %s%n", s.getReasonUnknown());

break;

case SATISFIABLE:

throw new TestFailedException();

case UNSATISFIABLE:

System.out.printf("OK, proof: %s%n", s.getProof());

break;

}

}

void disprove(Context ctx, Expr<BoolSort> f, boolean useMBQI)

throws TestFailedException

{

BoolExpr[] a = {};

disprove(ctx, f, useMBQI, a);

}

@SafeVarargs

final void disprove(Context ctx, Expr<BoolSort> f, boolean useMBQI,

Expr<BoolSort>... assumptions) throws TestFailedException

{

System.out.printf("Disproving: %s%n", f);

Solver s = ctx.mkSolver();

Params p = ctx.mkParams();

p.add("mbqi", useMBQI);

s.setParameters(p);

s.add(assumptions);

s.add(ctx.mkNot(f));

Status q = s.check();

switch (q)

{

case UNKNOWN:

System.out.printf("Unknown because: %s%n", s.getReasonUnknown());

break;

case SATISFIABLE:

System.out.printf("OK, model: %s%n", s.getModel());

break;

case UNSATISFIABLE:

throw new TestFailedException();

}

}

@SuppressWarnings("unchecked")

void modelConverterTest(Context ctx) throws TestFailedException

{

System.out.println("ModelConverterTest");

Expr<RealSort> xr = ctx.mkConst(ctx.mkSymbol("x"), ctx.mkRealSort());

Expr<RealSort> yr = 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.printf("Solver says: %s%n", q);

System.out.printf("Model: %n%s%n", s.getModel());

if (q != Status.SATISFIABLE)

throw new TestFailedException();

}

// / A simple array example.

@SuppressWarnings("unchecked")

void arrayExample1(Context ctx) throws TestFailedException

{

System.out.println("ArrayExample1");

Log.append("ArrayExample1");

Goal g = ctx.mkGoal(true, false, false);

ArraySort<IntSort, BitVecSort> asort = ctx.mkArraySort(ctx.getIntSort(),

ctx.mkBitVecSort(32));

Expr<ArraySort<IntSort, BitVecSort>> aex = ctx.mkConst(ctx.mkSymbol("MyArray"), asort);

Expr<BitVecSort> 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<IntSort> fd = ctx.mkFuncDecl(fname, domain, ctx.getIntSort());

Expr<?>[] fargs = { ctx.mkConst(xs, ctx.getIntSort()) };

Expr<IntSort> fapp = 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.printf("Solver: %s%n", s);

Status q = s.check();

System.out.printf("Status: %s%n", q);

if (q != Status.SATISFIABLE)

throw new TestFailedException();

System.out.printf("Model = %s%n", s.getModel());

System.out.printf("Interpretation of MyArray:%n%s%n", s.getModel().getFuncInterp(aex.getFuncDecl()));

System.out.printf("Interpretation of x:%n%s%n", s.getModel().getConstInterp(xc));

System.out.printf("Interpretation of f:%n%s%n", s.getModel().getFuncInterp(fd));

System.out.printf("Interpretation of MyArray as Term:%n%s%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");

IntSort int_type = ctx.getIntSort();

ArraySort<IntSort, IntSort> array_type = ctx.mkArraySort(int_type, int_type);

Expr<ArraySort<IntSort, IntSort>> a1 = ctx.mkConst("a1", array_type);

ArrayExpr<IntSort, IntSort> a2 = ctx.mkArrayConst("a2", int_type, int_type);

Expr<IntSort> i1 = ctx.mkConst("i1", int_type);

Expr<IntSort> i2 = ctx.mkConst("i2", int_type);

Expr<IntSort> i3 = ctx.mkConst("i3", int_type);

Expr<IntSort> v1 = ctx.mkConst("v1", int_type);

Expr<IntSort> v2 = ctx.mkConst("v2", int_type);

ArrayExpr<IntSort, IntSort> st1 = ctx.mkStore(a1, i1, v1);

ArrayExpr<IntSort, IntSort> st2 = ctx.mkStore(a2, i2, v2);

Expr<IntSort> sel1 = ctx.mkSelect(a1, i3);

Expr<IntSort> sel2 = ctx.mkSelect(a2, i3);

/* create antecedent */

BoolExpr antecedent = ctx.mkEq(st1, st2);

/*

BoolExpr consequent = ctx.mkOr(ctx.mkEq(i1, i3), ctx.mkEq(i2, i3), ctx.mkEq(sel1, sel2));

/*

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>

@SuppressWarnings("unchecked")

public void arrayExample3(Context ctx) throws TestFailedException

{

System.out.println("ArrayExample3");

Log.append("ArrayExample2");

for (int n = 2; n <= 5; n++)

{

System.out.printf("n = %d%n", n);

BoolSort bool_type = ctx.mkBoolSort();

ArraySort<BoolSort, BoolSort> array_type = ctx.mkArraySort(bool_type, bool_type);

List<Expr<ArraySort<BoolSort, BoolSort>>> a = IntStream.range(0, n).mapToObj(i -> ctx.mkConst(String.format("array_%d", i), array_type)).collect(Collectors.toList());

/* create arrays */

/* assert distinct(a[0], ..., a[n]) */

BoolExpr d = ctx.mkDistinct(a.toArray(new Expr[0]));

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.printf("%s = %s%n", a.get(i), model.evaluate(a.get(i), false));

}

}

}

}

// / Sudoku solving example.

@SuppressWarnings({"unchecked", "CodeBlock2Expr"})

void sudokuExample(Context ctx) throws TestFailedException

{

System.out.println("SudokuExample");

Log.append("SudokuExample");

// 9x9 matrix of integer variables

List<List<Expr<IntSort>>> X = IntStream.range(0, 9).mapToObj(i -> IntStream.range(0, 9).mapToObj(j ->

ctx.mkConst(ctx.mkSymbol(String.format("x_%d_%d", i + 1, j + 1)), ctx.getIntSort()))

.collect(Collectors.toList())).collect(Collectors.toList());

// each cell contains a value in {1, ..., 9}

List<List<BoolExpr>> cells_c = X.stream().map(r -> r.stream().map(c ->

ctx.mkAnd(ctx.mkLe(ctx.mkInt(1), c), ctx.mkLe(c, ctx.mkInt(9))))

.collect(Collectors.toList())).collect(Collectors.toList());

// each row contains a digit at most once

List<BoolExpr> rows_c = new ArrayList<>();

for (int i1 = 0; i1 < 9; i1++) {

BoolExpr boolExpr = ctx.mkDistinct(X.get(i1).toArray(new Expr[0]));

rows_c.add(boolExpr);

}

// each column contains a digit at most once

List<BoolExpr> cols_c = new ArrayList<>();

for (int idx = 0; idx < 9; idx++) {

int j1 = idx;

BoolExpr boolExpr = ctx.mkDistinct(X.stream().map(r -> r.get(j1)).toArray(Expr[]::new));

cols_c.add(boolExpr);

}

// each 3x3 square contains a digit at most once

List<List<BoolExpr>> sq_c = new ArrayList<>();

for (int i0 = 0; i0 < 3; i0++) {

List<BoolExpr> collect = new ArrayList<>();

for (int j0 = 0; j0 < 3; j0++) {

List<Expr<IntSort>> list = new ArrayList<>();

for (int i = 0; i < 3; i++) {

for (int j = 0; j < 3; j++) {

Expr<IntSort> intSortExpr = X.get(3 * i0 + i).get(3 * j0 + j);

list.add(intSortExpr);

}

}

BoolExpr boolExpr = ctx.mkDistinct(list.toArray(new Expr[0]));

collect.add(boolExpr);

}

sq_c.add(collect);

}

Stream<BoolExpr> sudoku_s = cells_c.stream().flatMap(Collection::stream);

sudoku_s = concat(sudoku_s, rows_c.stream());

sudoku_s = concat(sudoku_s, cols_c.stream());

sudoku_s = concat(sudoku_s, sq_c.stream().flatMap(Collection::stream));

BoolExpr sudoku_c = ctx.mkAnd(sudoku_s.toArray(BoolExpr[]::new));

// 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 }

};

// assert the variables we know

BoolExpr instance_c = ctx.mkAnd(IntStream.range(0, 9).boxed().flatMap(i -> IntStream.range(0, 9).filter(j -> instance[i][j] != 0).mapToObj(j -> ctx.mkEq(X.get(i).get(j), ctx.mkInt(instance[i][j])))).toArray(Expr[]::new));

Solver s = ctx.mkSolver();

s.add(sudoku_c);

s.add(instance_c);

if (s.check() == Status.SATISFIABLE)

{

Model m = s.getModel();

List<List<Expr<IntSort>>> R = X.stream().map(r -> r.stream().map(c -> m.eval(c, false)).collect(Collectors.toList())).collect(Collectors.toList());

System.out.println("Sudoku solution:");

R.forEach(r -> System.out.println(r.stream().map(Objects::toString).collect(Collectors.joining(" "))));

} else

{

System.out.println("Failed to solve sudoku");

throw new TestFailedException();

}

}

// / A basic example of how to use quantifiers.

@SuppressWarnings("unchecked")

void quantifierExample1(Context ctx)

{

System.out.println("QuantifierExample");

Log.append("QuantifierExample");

IntSort[] types = new IntSort[3];

Arrays.fill(types, ctx.getIntSort());

Symbol[] names = IntStream.range(0, 3).mapToObj(j -> ctx.mkSymbol(String.format("x_%d", j))).toArray(Symbol[]::new);

List<Expr<IntSort>> xs = IntStream.range(0, 3).mapToObj(j -> ctx.mkConst(names[j], types[j])).collect(Collectors.toList());

List<Expr<IntSort>> vars = IntStream.range(0, 3).mapToObj(j -> ctx.mkBound(2 - j, types[j])).collect(Collectors.toList());

BoolExpr body_vars = ctx.mkAnd(

ctx.mkEq(ctx.mkAdd(vars.get(0), ctx.mkInt(1)), ctx.mkInt(2)),

ctx.mkEq(ctx.mkAdd(vars.get(1), ctx.mkInt(2)),

ctx.mkAdd(vars.get(2), ctx.mkInt(3))));

BoolExpr body_const = ctx.mkAnd(

ctx.mkEq(ctx.mkAdd(xs.get(0), ctx.mkInt(1)), ctx.mkInt(2)),

ctx.mkEq(ctx.mkAdd(xs.get(1), ctx.mkInt(2)),

ctx.mkAdd(xs.get(2), ctx.mkInt(3))));

Quantifier x = ctx.mkForall(types, names, body_vars, 1, null, null,

ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1"));

System.out.printf("Quantifier X: %s%n", x.toString());

Quantifier y = ctx.mkForall(xs.toArray(new Expr[0]), body_const, 1, null, null,

ctx.mkSymbol("Q2"), ctx.mkSymbol("skid2"));

System.out.printf("Quantifier Y: %s%n", y.toString());

}

void quantifierExample2(Context ctx)

{

System.out.println("QuantifierExample2");

Log.append("QuantifierExample2");

Quantifier q1, q2;

FuncDecl<IntSort> f = ctx.mkFuncDecl("f", ctx.getIntSort(), ctx.getIntSort());

FuncDecl<IntSort> g = ctx.mkFuncDecl("g", ctx.getIntSort(), ctx.getIntSort());

// Quantifier with Exprs as the bound variables.

{

Expr<IntSort> x = ctx.mkConst("x", ctx.getIntSort());

Expr<IntSort> y = ctx.mkConst("y", ctx.getIntSort());

Expr<IntSort> f_x = ctx.mkApp(f, x);

Expr<IntSort> f_y = ctx.mkApp(f, y);

Expr<IntSort> 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 };

BoolExpr 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-Bruijn indices.

{

Expr<IntSort> x = ctx.mkBound(1, ctx.getIntSort());

Expr<IntSort> y = ctx.mkBound(0, ctx.getIntSort());

Expr<IntSort> f_x = ctx.mkApp(f, x);

Expr<IntSort> f_y = ctx.mkApp(f, y);

Expr<IntSort> 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() };

BoolExpr 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");

/*

/* declare function f */

IntSort I = ctx.getIntSort();

FuncDecl<IntSort> 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 */

IntExpr x = ctx.mkIntConst("x");

IntExpr y = ctx.mkIntConst("y");

IntExpr v = ctx.mkIntConst("v");

IntExpr w = ctx.mkIntConst("w");

Expr<IntSort> fxy = ctx.mkApp(f, x, y);

Expr<IntSort> 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");

/*

/* declare function f */

IntSort I = ctx.getIntSort();

FuncDecl<IntSort> 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 */

IntExpr x = ctx.mkIntConst("x");

IntExpr y = ctx.mkIntConst("y");

IntExpr v = ctx.mkIntConst("v");

IntExpr w = ctx.mkIntConst("w");

Expr<IntSort> fxy = ctx.mkApp(f, x, y);

Expr<IntSort> 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");

BoolSort bs = ctx.mkBoolSort();

Sort[] domain = { bs, bs };

FuncDecl<BoolSort> f = ctx.mkFuncDecl(fname, domain, bs);

Expr<BoolSort> fapp = ctx.mkApp(f, ctx.mkConst(x, bs), ctx.mkConst(y, bs));

Expr<?>[] fargs2 = { ctx.mkFreshConst("cp", bs) };

Sort[] domain2 = { bs };

Expr<BoolSort> 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.printf("Goal: %s%n", g);

Solver solver = ctx.mkSolver();

solver.add(g.getFormulas());

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<IntSort> xc = ctx.mkConst(ctx.mkSymbol("x"), ctx.getIntSort());

Expr<IntSort> 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);

IntNum inum = rn.getNumerator();

IntNum iden = rn.getDenominator();

System.out.printf("Numerator: %s Denominator: %s%n", inum, iden);

if (!inum.toString().equals("42") || !iden.toString().equals("43"))

throw new TestFailedException();

if (!rn.toDecimalString(3).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 ignored)

{

}

// Coercing type change in Z3

Expr<IntSort> integerDivision = ctx.mkDiv(ctx.mkInt(1), ctx.mkInt(2));

System.out.printf("%s -> %s%n", integerDivision, integerDivision.simplify()); // (div 1 2) -> 0

Expr<RealSort> realDivision = ctx.mkDiv(ctx.mkReal(1), ctx.mkReal(2));

System.out.printf("%s -> %s%n", realDivision, realDivision.simplify()); // (/ 1.0 2.0) -> 1/2

Expr<ArithSort> mixedDivision1 = ctx.mkDiv(ctx.mkReal(1), ctx.mkInt(2));

Expr<ArithSort> tmp = mixedDivision1;

// the return type is a Expr<ArithSort> here but since we know it is a

// real view it as such.

Expr<RealSort> mixedDivision2 = mixedDivision1.distillSort(RealSort.class);

System.out.printf("%s -> %s%n", mixedDivision2, mixedDivision2.simplify()); // (/ 1.0 (to_real 2)) -> 1/2

// empty distillSort

mixedDivision1.distillSort(ArithSort.class);

try {

mixedDivision1.distillSort(IntSort.class);

throw new TestFailedException(); // unreachable

} catch (Z3Exception exception) {

System.out.println(exception); // com.microsoft.z3.Z3Exception: Cannot cast expression of sort

// com.microsoft.z3.RealSort to com.microsoft.z3.IntSort.

}

Expr<BoolSort> eq1 = ctx.mkEq(realDivision, integerDivision);

System.out.printf("%s -> %s%n", eq1, eq1.simplify()); // (= (/ 1.0 2.0) (to_real (div 1 2))) -> false

Expr<BoolSort> eq2 = ctx.mkEq(realDivision, mixedDivision2);

System.out.printf("%s -> %s%n", eq2, eq2.simplify()); // (= (/ 1.0 2.0) (/ 1.0 (to_real 2))) -> true

}

// / Shows how to use Solver(logic)

// / @param ctx

void logicExample(Context ctx) throws TestFailedException

{

System.out.println("LogicTest");

Log.append("LogicTest");

Global.ToggleWarningMessages(true);

BitVecSort bvs = ctx.mkBitVecSort(32);

Expr<BitVecSort> x = ctx.mkConst("x", bvs);

Expr<BitVecSort> 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.printf("solver result: %s%n", 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.printf("tactic result: %s%n", 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<BitVecSort> x = ctx.mkConst("x", bvs);

Expr<BitVecSort> 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.printf("Num: %s%n", r.getBigIntNumerator());

System.out.printf("Den: %s%n", 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.printf("x = %s, y = %s%n", model.evaluate(x, false), 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");

IntNum one = ctx.mkInt(1);

IntNum two = ctx.mkInt(2);

ArithExpr<IntSort> 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.printf("x = %s, y =%s%n", model.evaluate(x, false), 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.printf("x = %s, y = %s%n", model.evaluate(x, false), 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. */

UninterpretedSort U = ctx.mkUninterpretedSort(ctx.mkSymbol("U"));

/* declare function g */

FuncDecl<UninterpretedSort> g = ctx.mkFuncDecl("g", U, U);

/* create x and y */

Expr<UninterpretedSort> x = ctx.mkConst("x", U);

Expr<UninterpretedSort> y = ctx.mkConst("y", U);

/* create g(x), g(y) */

Expr<UninterpretedSort> gx = g.apply(x);

Expr<UninterpretedSort> gy = g.apply(y);