From 3bca1fbcd82d0dd8afec741d8759a72f8490f1e2 Mon Sep 17 00:00:00 2001 From: Addison Crump Date: Mon, 30 Nov 2020 12:04:54 -0600 Subject: [PATCH] Java type generics (#4832) * Generify, needs some testing and review * Remove unnecessary change * Whoops, ? capture that type * Misread the docs, whoops * More permissible arithmetic operations * Implement believed Optimize generics * Missed a few generics * More permissible expr for arrays in parameters * More permissible expr for bitvecs in parameters * More permissible expr for bools in parameters * More permissible expr for fps in parameters * More permissible expr for fprms in parameters * More permissible expr for ints in parameters * More permissible expr for reals in parameters * Undo breaking name conflict due to type erasure; see notes * Whoops, fix typing of ReExpr * Sort corrections for Re, Seq * More permissible expr for regular expressions in parameters * Fix name conflict between sequences and regular expressions; see notes * Minor typo, big implications! * Make Constructor consistent, associate captured types with other unknown capture types for datatype consistency * More expressive; outputs of multiple datatype definitions are only known to be sort, not capture, and Constructor.of should make a capture * Be less dumb and just type it a little differently * Update examples, make sure to type Expr and FuncDecl sort returns * General fixups * Downgrade java version, make it only for the generic support, remove var and Expr[]::new construction * Turns out Java 8 hadn't figured out how to do stream generics yet. Didn't even show up in my IDE, weird --- examples/java/JavaExample.java | 6 +- examples/java/JavaGenericExample.java | 2135 ++++++++++++++++++ src/api/java/AST.java | 2 +- src/api/java/ASTVector.java | 22 +- src/api/java/ArithExpr.java | 2 +- src/api/java/ArrayExpr.java | 2 +- src/api/java/ArraySort.java | 15 +- src/api/java/BitVecExpr.java | 2 +- src/api/java/BoolExpr.java | 2 +- src/api/java/Constructor.java | 20 +- src/api/java/ConstructorDecRefQueue.java | 2 +- src/api/java/ConstructorList.java | 4 +- src/api/java/ConstructorListDecRefQueue.java | 2 +- src/api/java/Context.java | 630 +++--- src/api/java/DatatypeExpr.java | 2 +- src/api/java/DatatypeSort.java | 28 +- src/api/java/EnumSort.java | 36 +- src/api/java/Expr.java | 69 +- src/api/java/FPExpr.java | 2 +- src/api/java/FPRMExpr.java | 2 +- src/api/java/FiniteDomainExpr.java | 2 +- src/api/java/FiniteDomainNum.java | 2 +- src/api/java/FiniteDomainSort.java | 2 +- src/api/java/Fixedpoint.java | 32 +- src/api/java/FuncDecl.java | 34 +- src/api/java/FuncInterp.java | 29 +- src/api/java/FuncInterpDecRefQueue.java | 2 +- src/api/java/FuncInterpEntryDecRefQueue.java | 2 +- src/api/java/Goal.java | 5 +- src/api/java/IntExpr.java | 2 +- src/api/java/Lambda.java | 24 +- src/api/java/ListSort.java | 28 +- src/api/java/Model.java | 45 +- src/api/java/Optimize.java | 51 +- src/api/java/Pattern.java | 4 +- src/api/java/Quantifier.java | 10 +- src/api/java/ReExpr.java | 2 +- src/api/java/ReSort.java | 2 +- src/api/java/RealExpr.java | 2 +- src/api/java/SeqExpr.java | 2 +- src/api/java/SeqSort.java | 2 +- src/api/java/SetSort.java | 4 +- src/api/java/Solver.java | 21 +- src/api/java/Sort.java | 8 +- src/api/java/TupleSort.java | 10 +- 45 files changed, 2724 insertions(+), 588 deletions(-) create mode 100644 examples/java/JavaGenericExample.java diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 936184e3c2c..bd705456f37 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -599,7 +599,7 @@ void quantifierExample1(Context ctx) System.out.println("QuantifierExample"); Log.append("QuantifierExample"); - Sort[] types = new Sort[3]; + IntSort[] types = new IntSort[3]; IntExpr[] xs = new IntExpr[3]; Symbol[] names = new Symbol[3]; IntExpr[] vars = new IntExpr[3]; @@ -1398,7 +1398,7 @@ public void bitvectorExample1(Context ctx) throws TestFailedException System.out.println("BitvectorExample1"); Log.append("BitvectorExample1"); - Sort bv_type = ctx.mkBitVecSort(32); + BitVecSort 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); @@ -1420,7 +1420,7 @@ public void bitvectorExample2(Context ctx) throws TestFailedException Log.append("BitvectorExample2"); /* construct x ^ y - 103 == x * y */ - Sort bv_type = ctx.mkBitVecSort(32); + BitVecSort 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); diff --git a/examples/java/JavaGenericExample.java b/examples/java/JavaGenericExample.java new file mode 100644 index 00000000000..8dd31fed028 --- /dev/null +++ b/examples/java/JavaGenericExample.java @@ -0,0 +1,2135 @@ +/*++ + Copyright (c) 2012 Microsoft Corporation + +Module Name: + + Program.java + +Abstract: + + Z3 Java API: Example program + +Author: + + Christoph Wintersteiger (cwinter) 2012-11-27 + +Notes: + +--*/ + +import com.microsoft.z3.*; + +import java.util.*; +import java.util.stream.Collectors; +import java.util.stream.IntStream; +import java.util.stream.Stream; + +import static java.util.stream.Stream.concat; + +class JavaGenericExample +{ + @SuppressWarnings("serial") + static class TestFailedException extends Exception + { + public TestFailedException() + { + super("Check FAILED"); + } + } + + // / Create axiom: function f is injective in the i-th argument. + + // / + // / The following axiom is produced: + // / + // / forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i + // / + // / Where, finvis 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 */ + /* fill types, names and xs */ + Sort[] types = domain.clone(); + List> 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 x_i = xs.get(i); + + /* create f(x_0, ..., x_i, ..., x_{n-1}) */ + Expr fxs = f.apply(xs.toArray(new Expr[0])); + + /* 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 */ + 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. + + // / + // / The following axiom is produced: + // / + // / forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i + // / + // / Where, finvis 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 */ + R finv_domain = f.getRange(); + Sort finv_range = domain[i]; + FuncDecl finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range); + + /* allocate temporary arrays */ + List> 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 x_i = xs.get(i); + + /* create f(x_0, ..., x_i, ..., x_{n-1}) */ + Expr fxs = f.apply(xs.toArray(new Expr[0])); + + /* 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 */ + 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. + + // / + // / This example uses the SMT-LIB parser to simplify the axiom + // construction. + // / + private BoolExpr commAxiom(Context ctx, FuncDecl 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 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 f, boolean useMBQI) throws TestFailedException + { + BoolExpr[] assumptions = new BoolExpr[0]; + prove(ctx, f, useMBQI, assumptions); + } + + @SafeVarargs + final void prove(Context ctx, Expr f, boolean useMBQI, + Expr... 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 f, boolean useMBQI) + throws TestFailedException + { + BoolExpr[] a = {}; + disprove(ctx, f, useMBQI, a); + } + + @SafeVarargs + final void disprove(Context ctx, Expr f, boolean useMBQI, + Expr... 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 xr = ctx.mkConst(ctx.mkSymbol("x"), ctx.mkRealSort()); + Expr 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 asort = ctx.mkArraySort(ctx.getIntSort(), + ctx.mkBitVecSort(32)); + Expr> aex = 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()) }; + Expr 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 store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 + // = i3 or select(a1, i3) = select(a2, i3)). + + // / This example demonstrates how to use the array + // theory. + public void arrayExample2(Context ctx) throws TestFailedException + { + System.out.println("ArrayExample2"); + Log.append("ArrayExample2"); + + IntSort int_type = ctx.getIntSort(); + ArraySort array_type = ctx.mkArraySort(int_type, int_type); + + Expr> a1 = 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); + + ArrayExpr st1 = ctx.mkStore(a1, i1, v1); + ArrayExpr 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 distinct(a_0, ... , a_n) is + // / unsatisfiable when a_i's are arrays from boolean to + // / boolean and n > 4. + + // / This example also shows how to use the distinct + // construct. + @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 array_type = ctx.mkArraySort(bool_type, bool_type); + List>> 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>> 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> 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 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 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> sq_c = new ArrayList<>(); + for (int i0 = 0; i0 < 3; i0++) { + List collect = new ArrayList<>(); + for (int j0 = 0; j0 < 3; j0++) { + List> list = new ArrayList<>(); + for (int i = 0; i < 3; i++) { + for (int j = 0; j < 3; j++) { + Expr 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 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>> 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> xs = IntStream.range(0, 3).mapToObj(j -> ctx.mkConst(names[j], types[j])).collect(Collectors.toList()); + List> 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 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 }; + 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 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() }; + 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 f(x, y) = f(w, v) implies y = v when + // / f is injective in the second argument. + + 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 */ + IntSort 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 */ + IntExpr x = ctx.mkIntConst("x"); + IntExpr y = ctx.mkIntConst("y"); + IntExpr v = ctx.mkIntConst("v"); + IntExpr 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 f(x, y) = f(w, v) implies y = v when + // / f is injective in the second argument. + + 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 */ + IntSort 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 */ + IntExpr x = ctx.mkIntConst("x"); + IntExpr y = ctx.mkIntConst("y"); + IntExpr v = ctx.mkIntConst("v"); + IntExpr 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"); + + BoolSort 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.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 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); + 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) + { + } + } + + // / 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 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.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 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.printf("Num: %s%n", r.getBigIntNumerator()); + System.out.printf("Den: %s%n", r.getBigIntDenominator()); + } + + // / Find a model for x xor y. + + 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 x < y + 1, x > 2. + // / Then, assert not(x = y), 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 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 x = y implies g(x) = g(y), and + // / disprove x = y implies g(g(x)) = g(y). + + // / This function demonstrates how to create uninterpreted + // / types and functions. + 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 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 not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 + // . + // / Then, show that z < -1 is not implied. + + // / This example demonstrates how to combine uninterpreted + // functions + // / and arithmetic. + public void proveExample2(Context ctx) throws TestFailedException + { + System.out.println("ProveExample2"); + Log.append("ProveExample2"); + + /* declare function g */ + IntSort 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 */ + IntNum zero = ctx.mkInt(0); + + /* assert not(g(g(x) - g(y)) = g(z)) */ + ArithExpr gx_gy = ctx.mkSub(gx, 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 */ + IntNum 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. + + // / This example also demonstrates how big numbers can be + // / created in ctx. + public void pushPopExample1(Context ctx) throws TestFailedException + { + System.out.println("PushPopExample1"); + Log.append("PushPopExample1"); + + /* create a big number */ + IntSort int_type = ctx.getIntSort(); + IntNum 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. + + // / Check that the projection of a tuple + // / returns the corresponding element. + public void tupleExample(Context ctx) throws TestFailedException + { + System.out.println("TupleExample"); + Log.append("TupleExample"); + + IntSort 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 + ); + // have to cast here because it is not possible to type a member of an array of mixed generics + @SuppressWarnings("unchecked") + FuncDecl first = (FuncDecl) 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.printf("Tuple example: %s%n", n3); + prove(ctx, n3, false); + } + + // / Simple bit-vector example. + + // / + // / This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) + // machine integers + // / + public void bitvectorExample1(Context ctx) throws TestFailedException + { + System.out.println("BitvectorExample1"); + Log.append("BitvectorExample1"); + + BitVecSort bv_type = ctx.mkBitVecSort(32); + Expr x = ctx.mkConst("x", bv_type); + Expr zero = 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 */ + BitVecSort 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); + Expr c103 = 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"); + + BoolExpr f = ctx.parseSMTLIB2String( + "(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))", + null, null, null, null)[0]; + System.out.printf("formula %s%n", f); + + @SuppressWarnings("unused") + Model m = check(ctx, f, 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 }; + + BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null, declNames, decls)[0]; + System.out.printf("formula: %s%n", 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 */ + IntSort I = ctx.mkIntSort(); + FuncDecl g = ctx.mkFuncDecl("g", new Sort[] { I, I }, I); + + BoolExpr ca = commAxiom(ctx, g); + + BoolExpr thm = ctx.parseSMTLIB2String( + "(declare-fun (Int Int) Int) (assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))", + null, null, new Symbol[] { ctx.mkSymbol("gg") }, + new FuncDecl[] { g })[0]; + System.out.printf("formula: %s%n", thm); + prove(ctx, thm, false, ca); + } + + + // / Demonstrates how to handle parser errors using Z3 error handling + // support. + + // / + public void parserExample5(Context ctx) + { + System.out.println("ParserExample5"); + + try + { + ctx.parseSMTLIB2String( + /* + * the following string has a parsing error: missing + * parenthesis + */ + "(declare-const x Int (declare-const y Int)) (assert (> x y))", + null, null, null, null); + } catch (Z3Exception e) + { + System.out.printf("Z3 error: %s%n", 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(); + IntNum one = ctx.mkInt(1); + IntNum zero = ctx.mkInt(0); + Expr ite = ctx.mkITE(f, one, zero); + + System.out.printf("Expr: %s%n", ite); + } + + // / Create an enumeration data type. + + public void enumExampleTyped(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")); + + // helper function for consistent typing: https://docs.oracle.com/javase/tutorial/java/generics/capture.html + 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, ctx.mkApp(fruit.getTesterDecls()[0], apple), + false); + + /* Oranges fail the apple test */ + disprove(ctx, ctx.mkApp(fruit.getTesterDecls()[0], orange), false); + prove(ctx, ctx.mkNot(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); + } + + // while you can do this untyped, it's safer to have a helper function -- this will prevent you from + // mixing up your enum types + public void enumExampleUntyped(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, ctx.mkApp(fruit.getTesterDecls()[0], apple), + false); + + /* Oranges fail the apple test */ + disprove(ctx, ctx.mkApp(fruit.getTesterDecls()[0], orange), false); + prove(ctx, ctx.mkNot(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. + + @SuppressWarnings("unchecked") + public void listExample(Context ctx) throws TestFailedException + { + System.out.println("ListExample"); + Log.append("ListExample"); + + IntSort int_ty = ctx.mkIntSort(); + + ListSort int_list = ctx.mkListSort(ctx.mkSymbol("int_list"), int_ty); + + Expr> nil = ctx.mkConst(int_list.getNilDecl()); + Expr> l1 = ctx.mkApp(int_list.getConsDecl(), ctx.mkInt(1), nil); + Expr> 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 */ + Expr x = ctx.mkConst("x", int_ty); + Expr 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 */ + Expr> u = ctx.mkConst("u", int_list); + Expr> 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(ctx.mkApp(int_list.getIsNilDecl(), u), 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)) */ + BoolExpr fml1 = ctx.mkEq(u, ctx.mkApp(int_list.getConsDecl(), + ctx.mkApp(int_list.getHeadDecl(), u), + ctx.mkApp(int_list.getTailDecl(), u))); + BoolExpr fml = ctx.mkImplies(ctx.mkApp(int_list.getIsConsDecl(), u), fml1); + System.out.printf("Formula %s%n", fml); + + prove(ctx, fml, false); + + disprove(ctx, fml1, false); + } + + // / Create a binary tree datatype. + + @SuppressWarnings("unchecked") + public void treeExample(Context ctx) throws TestFailedException + { + System.out.println("TreeExample"); + Log.append("TreeExample"); + + 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 }; + + DatatypeSort cell = ctx.mkDatatypeSort("cell", constructors); + + FuncDecl> nil_decl = nil_con.ConstructorDecl(); + FuncDecl is_nil_decl = nil_con.getTesterDecl(); + FuncDecl> cons_decl = cons_con.ConstructorDecl(); + FuncDecl is_cons_decl = cons_con.getTesterDecl(); + FuncDecl[] cons_accessors = cons_con.getAccessorDecls(); + FuncDecl car_decl = cons_accessors[0]; + FuncDecl cdr_decl = cons_accessors[1]; + + Expr> nil = ctx.mkConst(nil_decl); + Expr> l1 = ctx.mkApp(cons_decl, nil, nil); + Expr> 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 */ + Expr> u = ctx.mkConst("u", cell); + Expr> v = ctx.mkConst("v", cell); + Expr> x = ctx.mkConst("x", cell); + Expr> 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(ctx.mkApp(is_nil_decl, u), 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)) */ + BoolExpr fml1 = ctx.mkEq(u, ctx.mkApp(cons_decl, ctx.mkApp(car_decl, u), ctx.mkApp(cdr_decl, u))); + BoolExpr fml = ctx.mkImplies(ctx.mkApp(is_cons_decl, u), fml1); + System.out.printf("Formula %s%n", fml); + prove(ctx, fml, false); + + disprove(ctx, fml1, false); + } + + // / Create a forest of trees. + + // / + // / forest ::= nil | cons(tree, forest) + // / tree ::= nil | cons(forest, forest) + // / + @SuppressWarnings({"unchecked", "unused", "UnusedAssignment"}) + public void forestExample(Context ctx) throws TestFailedException + { + System.out.println("ForestExample"); + Log.append("ForestExample"); + + DatatypeSort forest; + DatatypeSort tree; + FuncDecl> nil1_decl, cons1_decl, cdr1_decl, car2_decl, cdr2_decl; + FuncDecl> car1_decl, nil2_decl, cons2_decl; + FuncDecl is_nil1_decl, is_nil2_decl, is_cons1_decl, is_cons2_decl; + + // + // 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; + Constructor nil2_con, cons2_con; + Constructor[] constructors1 = new Constructor[2]; + Constructor[] constructors2 = new Constructor[2]; + Symbol[] sort_names = { ctx.mkSymbol("forest"), ctx.mkSymbol("tree") }; + + /* build a forest */ + nil1_con = ctx.mkConstructor(ctx.mkSymbol("nil1"), + ctx.mkSymbol("is_nil1"), 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 = (DatatypeSort) sorts[0]; + tree = (DatatypeSort) 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 = (FuncDecl>) cons1_accessors[0]; + cdr1_decl = (FuncDecl>) 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 = (FuncDecl>) cons2_accessors[0]; + cdr2_decl = (FuncDecl>) cons2_accessors[1]; + + Expr> nil1 = ctx.mkConst(nil1_decl); + Expr> nil2 = ctx.mkConst(nil2_decl); + Expr> f1 = ctx.mkApp(cons1_decl, nil2, nil1); + Expr> t1 = ctx.mkApp(cons2_decl, nil1, nil1); + Expr> t2 = ctx.mkApp(cons2_decl, f1, nil1); + Expr> t3 = ctx.mkApp(cons2_decl, f1, f1); + Expr> t4 = ctx.mkApp(cons2_decl, nil1, f1); + Expr> f2 = ctx.mkApp(cons1_decl, t1, nil1); + Expr> 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 */ + Expr> u = ctx.mkConst("u", forest); + Expr> v = ctx.mkConst("v", forest); + Expr> x = ctx.mkConst("x", tree); + Expr> y = ctx.mkConst("y", tree); + Expr> l1 = ctx.mkApp(cons1_decl, x, u); + Expr> 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(ctx.mkApp(is_nil1_decl, u), 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"); + IntNum 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.printf("result = %s%n", 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. + + @SuppressWarnings("unchecked") + public void evalExample2(Context ctx) + { + System.out.println("EvalExample2"); + Log.append("EvalExample2"); + + IntSort 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 = (FuncDecl) tuple.getFieldDecls()[0]; // declarations are for + // projections + FuncDecl second = (FuncDecl) 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.printf("evaluating tup1 %s%n", model.evaluate(tup1, false)); + System.out.printf("evaluating tup2 %s%n", model.evaluate(tup2, false)); + System.out.printf("evaluating second(tup2) %s%n", model.evaluate(ctx.mkApp(second, tup2), false)); + } else + { + System.out.println("BUG, the constraints are satisfiable."); + } + } + + // / Demonstrate how to use Pushand Popto + // / control the size of models. + + // / Note: this test is specialized to 32-bit bitvectors. + 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 (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); + // we still have to cast because we want to use a method in BitVecNum + // however, we cannot cast to a type which doesn't match the generic, e.g. IntNum + int ui = ((BitVecNum) v).getInt(); + if (ui < upper[i]) + { + upper[i] = ui; + } + System.out.printf("%d %d %d%n", 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. + + @SuppressWarnings("unchecked") + 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"); + + ArithExpr t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z))); + Expr t2 = t1.simplify(); + System.out.printf("%s -> %s%n", 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.printf("proof: %s%n", 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.printf("Sort: %s%n", 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.printf("x=%s; y=%s; z=%s%n", x.toString(), y.toString(), 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.printf("OK, unsat:%n%s%n", 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.printf("OK, sat:%n%s%n", 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.printf("OK, unsat:%n%s%n", 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.printf("c5 = %s%n", c5); + + /* Generic solver */ + Solver s = ctx.mkSolver(); + s.add(c5); + + if (s.check() != Status.SATISFIABLE) + throw new TestFailedException(); + + System.out.printf("OK, model: %s%n", s.getModel()); + } + + @SuppressWarnings("unchecked") + 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 = 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)); + + IntExpr e1 = ctx1.mkIntConst("e1"); + IntExpr 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) + { + JavaGenericExample p = new JavaGenericExample(); + try + { + 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 cfg = new HashMap<>(); + cfg.put("model", "true"); + Context ctx = new Context(cfg); + + p.optimizeExample(ctx); + p.basicTests(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.parserExample5(ctx); + p.iteExample(ctx); + p.evalExample1(ctx); + p.evalExample2(ctx); + p.findSmallModelExample(ctx); + p.simplifierExample(ctx); + p.finiteDomainExample(ctx); + p.floatingPointExample1(ctx); + // core dumps: p.floatingPointExample2(ctx); + } + + { // These examples need proof generation turned on. + HashMap cfg = new HashMap<>(); + cfg.put("proof", "true"); + Context ctx = new Context(cfg); + p.proveExample1(ctx); + p.proveExample2(ctx); + p.arrayExample2(ctx); + p.tupleExample(ctx); + // throws p.parserExample3(ctx); + p.enumExampleTyped(ctx); + p.enumExampleUntyped(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 cfg = new HashMap<>(); + 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.printf("Z3 Managed Exception: %s%n", ex.getMessage()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); + } catch (TestFailedException ex) + { + System.out.printf("TEST CASE FAILED: %s%n", ex.getMessage()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); + } catch (Exception ex) + { + System.out.printf("Unknown Exception: %s%n", ex.getMessage()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); + } + } +} diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 350830443f3..c28c0cfcba7 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -204,7 +204,7 @@ static AST create(Context ctx, long obj) switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj))) { case Z3_FUNC_DECL_AST: - return new FuncDecl(ctx, obj); + return new FuncDecl<>(ctx, obj); case Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj); case Z3_SORT_AST: diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 4ee53103503..a6b436a99f4 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -126,9 +126,9 @@ public AST[] ToArray() /** * Translates the AST vector into an Expr[] * */ - public Expr[] ToExprArray() { + public Expr[] ToExprArray() { int n = size(); - Expr[] res = new Expr[n]; + Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) res[i] = Expr.create(getContext(), get(i).getNativeObject()); return res; @@ -161,36 +161,36 @@ public BitVecExpr[] ToBitVecExprArray() /** * Translates the AST vector into an ArithExpr[] * */ - public ArithExpr[] ToArithExprExprArray() + public ArithExpr[] ToArithExprExprArray() { int n = size(); - ArithExpr[] res = new ArithExpr[n]; + ArithExpr[] res = new ArithExpr[n]; for (int i = 0; i < n; i++) - res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject()); + res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject()); return res; } /** * Translates the AST vector into an ArrayExpr[] * */ - public ArrayExpr[] ToArrayExprArray() + public ArrayExpr[] ToArrayExprArray() { int n = size(); - ArrayExpr[] res = new ArrayExpr[n]; + ArrayExpr[] res = new ArrayExpr[n]; for (int i = 0; i < n; i++) - res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject()); + res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject()); return res; } /** * Translates the AST vector into an DatatypeExpr[] * */ - public DatatypeExpr[] ToDatatypeExprArray() + public DatatypeExpr[] ToDatatypeExprArray() { int n = size(); - DatatypeExpr[] res = new DatatypeExpr[n]; + DatatypeExpr[] res = new DatatypeExpr[n]; for (int i = 0; i < n; i++) - res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject()); + res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject()); return res; } diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java index d92d8523bb3..f26eb8b6b61 100644 --- a/src/api/java/ArithExpr.java +++ b/src/api/java/ArithExpr.java @@ -20,7 +20,7 @@ /** * Arithmetic expressions (int/real) **/ -public class ArithExpr extends Expr +public class ArithExpr extends Expr { /** * Constructor for ArithExpr diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java index b8318b648a7..fe6c511811c 100644 --- a/src/api/java/ArrayExpr.java +++ b/src/api/java/ArrayExpr.java @@ -21,7 +21,7 @@ /** * Array expressions **/ -public class ArrayExpr extends Expr +public class ArrayExpr extends Expr> { /** * Constructor for ArrayExpr diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java index db4d992ed0b..30f4178fac5 100644 --- a/src/api/java/ArraySort.java +++ b/src/api/java/ArraySort.java @@ -20,7 +20,8 @@ /** * Array sorts. **/ -public class ArraySort extends Sort +@SuppressWarnings("unchecked") +public class ArraySort extends Sort { /** * The domain of the array sort. @@ -28,9 +29,9 @@ public class ArraySort extends Sort * @throws Z3Exception on error * @return a sort **/ - public Sort getDomain() + public D getDomain() { - return Sort.create(getContext(), + return (D) Sort.create(getContext(), Native.getArraySortDomain(getContext().nCtx(), getNativeObject())); } @@ -40,9 +41,9 @@ public Sort getDomain() * @throws Z3Exception on error * @return a sort **/ - public Sort getRange() + public R getRange() { - return Sort.create(getContext(), + return (R) Sort.create(getContext(), Native.getArraySortRange(getContext().nCtx(), getNativeObject())); } @@ -51,13 +52,13 @@ public Sort getRange() super(ctx, obj); } - ArraySort(Context ctx, Sort domain, Sort range) + ArraySort(Context ctx, D domain, R range) { super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(), range.getNativeObject())); } - ArraySort(Context ctx, Sort[] domains, Sort range) + ArraySort(Context ctx, Sort[] domains, R range) { super(ctx, Native.mkArraySortN(ctx.nCtx(), domains.length, AST.arrayToNative(domains), range.getNativeObject())); diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java index 175da9d6692..b4d62b2d618 100644 --- a/src/api/java/BitVecExpr.java +++ b/src/api/java/BitVecExpr.java @@ -20,7 +20,7 @@ /** * Bit-vector expressions **/ -public class BitVecExpr extends Expr +public class BitVecExpr extends Expr { /** diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java index dc75b2e7c36..7907ca28693 100644 --- a/src/api/java/BoolExpr.java +++ b/src/api/java/BoolExpr.java @@ -20,7 +20,7 @@ /** * Boolean expressions **/ -public class BoolExpr extends Expr { +public class BoolExpr extends Expr { /** * Constructor for BoolExpr diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 87ab86c3fdc..59565f56509 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -20,7 +20,7 @@ /** * Constructors are used for datatype sorts. **/ -public class Constructor extends Z3Object { +public class Constructor extends Z3Object { private final int n; Constructor(Context ctx, int n, long nativeObj) { @@ -44,13 +44,13 @@ public int getNumFields() * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl ConstructorDecl() + public FuncDecl> ConstructorDecl() { Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); long[] accessors = new long[n]; Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); - return new FuncDecl(getContext(), constructor.value); + return new FuncDecl<>(getContext(), constructor.value); } /** @@ -58,13 +58,13 @@ public FuncDecl ConstructorDecl() * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl getTesterDecl() + public FuncDecl getTesterDecl() { Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); long[] accessors = new long[n]; Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); - return new FuncDecl(getContext(), tester.value); + return new FuncDecl<>(getContext(), tester.value); } /** @@ -72,15 +72,15 @@ public FuncDecl getTesterDecl() * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl[] getAccessorDecls() + public FuncDecl[] getAccessorDecls() { Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); long[] accessors = new long[n]; Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); - FuncDecl[] t = new FuncDecl[n]; + FuncDecl[] t = new FuncDecl[n]; for (int i = 0; i < n; i++) - t[i] = new FuncDecl(getContext(), accessors[i]); + t[i] = new FuncDecl<>(getContext(), accessors[i]); return t; } @@ -94,7 +94,7 @@ void addToReferenceQueue() { getContext().getConstructorDRQ().storeReference(getContext(), this); } - static Constructor of(Context ctx, Symbol name, Symbol recognizer, + static Constructor of(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) { int n = AST.arrayLength(fieldNames); @@ -111,7 +111,7 @@ static Constructor of(Context ctx, Symbol name, Symbol recognizer, long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(), recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames), Sort.arrayToNative(sorts), sortRefs); - return new Constructor(ctx, n, nativeObj); + return new Constructor<>(ctx, n, nativeObj); } } diff --git a/src/api/java/ConstructorDecRefQueue.java b/src/api/java/ConstructorDecRefQueue.java index 5003dde5f2c..a76b26bb73c 100644 --- a/src/api/java/ConstructorDecRefQueue.java +++ b/src/api/java/ConstructorDecRefQueue.java @@ -1,6 +1,6 @@ package com.microsoft.z3; -public class ConstructorDecRefQueue extends IDecRefQueue { +public class ConstructorDecRefQueue extends IDecRefQueue> { public ConstructorDecRefQueue() { super(); } diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index c79e08d9e32..d015c51c0ad 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -20,7 +20,7 @@ /** * Lists of constructors **/ -public class ConstructorList extends Z3Object { +public class ConstructorList extends Z3Object { ConstructorList(Context ctx, long obj) { @@ -37,7 +37,7 @@ void addToReferenceQueue() { getContext().getConstructorListDRQ().storeReference(getContext(), this); } - ConstructorList(Context ctx, Constructor[] constructors) + ConstructorList(Context ctx, Constructor[] constructors) { super(ctx, Native.mkConstructorList(ctx.nCtx(), constructors.length, diff --git a/src/api/java/ConstructorListDecRefQueue.java b/src/api/java/ConstructorListDecRefQueue.java index 1a24607313c..2f5dfcb3526 100644 --- a/src/api/java/ConstructorListDecRefQueue.java +++ b/src/api/java/ConstructorListDecRefQueue.java @@ -1,6 +1,6 @@ package com.microsoft.z3; -public class ConstructorListDecRefQueue extends IDecRefQueue { +public class ConstructorListDecRefQueue extends IDecRefQueue> { public ConstructorListDecRefQueue() { super(); } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 06e4a0f60e1..dc3b2a0c393 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -32,6 +32,7 @@ * related to terms and formulas that are created relative * to them. **/ +@SuppressWarnings("unchecked") public class Context implements AutoCloseable { private long m_ctx; static final Object creation_lock = new Object(); @@ -119,7 +120,7 @@ Symbol[] mkSymbols(String[] names) private BoolSort m_boolSort = null; private IntSort m_intSort = null; private RealSort m_realSort = null; - private SeqSort m_stringSort = null; + private SeqSort m_stringSort = null; /** * Retrieves the Boolean sort of the context. @@ -165,7 +166,7 @@ public BoolSort mkBoolSort() /** * Retrieves the Integer sort of the context. **/ - public SeqSort getStringSort() + public SeqSort getStringSort() { if (m_stringSort == null) { m_stringSort = mkStringSort(); @@ -217,46 +218,46 @@ public BitVecSort mkBitVecSort(int size) /** * Create a new array sort. **/ - public ArraySort mkArraySort(Sort domain, Sort range) + public ArraySort mkArraySort(D domain, R range) { checkContextMatch(domain); checkContextMatch(range); - return new ArraySort(this, domain, range); + return new ArraySort<>(this, domain, range); } /** * Create a new array sort. **/ - public ArraySort mkArraySort(Sort[] domains, Sort range) + public ArraySort mkArraySort(Sort[] domains, R range) { checkContextMatch(domains); checkContextMatch(range); - return new ArraySort(this, domains, range); + return new ArraySort<>(this, domains, range); } /** * Create a new string sort **/ - public SeqSort mkStringSort() + public SeqSort mkStringSort() { - return new SeqSort(this, Native.mkStringSort(nCtx())); + return new SeqSort<>(this, Native.mkStringSort(nCtx())); } /** * Create a new sequence sort **/ - public SeqSort mkSeqSort(Sort s) + public SeqSort mkSeqSort(R s) { - return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject())); + return new SeqSort<>(this, Native.mkSeqSort(nCtx(), s.getNativeObject())); } /** * Create a new regular expression sort **/ - public ReSort mkReSort(Sort s) + public ReSort mkReSort(R s) { - return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject())); + return new ReSort<>(this, Native.mkReSort(nCtx(), s.getNativeObject())); } @@ -276,59 +277,59 @@ public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, /** * Create a new enumeration sort. **/ - public EnumSort mkEnumSort(Symbol name, Symbol... enumNames) + public EnumSort mkEnumSort(Symbol name, Symbol... enumNames) { checkContextMatch(name); checkContextMatch(enumNames); - return new EnumSort(this, name, enumNames); + return new EnumSort<>(this, name, enumNames); } /** * Create a new enumeration sort. **/ - public EnumSort mkEnumSort(String name, String... enumNames) + public EnumSort mkEnumSort(String name, String... enumNames) { - return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames)); + return new EnumSort<>(this, mkSymbol(name), mkSymbols(enumNames)); } /** * Create a new list sort. **/ - public ListSort mkListSort(Symbol name, Sort elemSort) + public ListSort mkListSort(Symbol name, R elemSort) { checkContextMatch(name); checkContextMatch(elemSort); - return new ListSort(this, name, elemSort); + return new ListSort<>(this, name, elemSort); } /** * Create a new list sort. **/ - public ListSort mkListSort(String name, Sort elemSort) + public ListSort mkListSort(String name, R elemSort) { checkContextMatch(elemSort); - return new ListSort(this, mkSymbol(name), elemSort); + return new ListSort<>(this, mkSymbol(name), elemSort); } /** * Create a new finite domain sort. **/ - public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size) + public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size) { checkContextMatch(name); - return new FiniteDomainSort(this, name, size); + return new FiniteDomainSort<>(this, name, size); } /** * Create a new finite domain sort. **/ - public FiniteDomainSort mkFiniteDomainSort(String name, long size) + public FiniteDomainSort mkFiniteDomainSort(String name, long size) { - return new FiniteDomainSort(this, mkSymbol(name), size); + return new FiniteDomainSort<>(this, mkSymbol(name), size); } /** @@ -342,43 +343,40 @@ public FiniteDomainSort mkFiniteDomainSort(String name, long size) * an index referring to one of the recursive datatypes that is * declared. **/ - public Constructor mkConstructor(Symbol name, Symbol recognizer, + public Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) { - return of(this, name, recognizer, fieldNames, sorts, - sortRefs); + return of(this, name, recognizer, fieldNames, sorts, sortRefs); } /** * Create a datatype constructor. **/ - public Constructor mkConstructor(String name, String recognizer, + public Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) { - return of(this, mkSymbol(name), mkSymbol(recognizer), - mkSymbols(fieldNames), sorts, sortRefs); + return of(this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs); } /** * Create a new datatype sort. **/ - public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors) - + public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors) { checkContextMatch(name); checkContextMatch(constructors); - return new DatatypeSort(this, name, constructors); + return new DatatypeSort<>(this, name, constructors); } /** * Create a new datatype sort. **/ - public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors) + public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors) { checkContextMatch(constructors); - return new DatatypeSort(this, mkSymbol(name), constructors); + return new DatatypeSort<>(this, mkSymbol(name), constructors); } /** @@ -386,34 +384,33 @@ public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors) * @param names names of datatype sorts * @param c list of constructors, one list per sort. **/ - public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c) - + public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c) { checkContextMatch(names); int n = names.length; - ConstructorList[] cla = new ConstructorList[n]; + ConstructorList[] cla = new ConstructorList[n]; long[] n_constr = new long[n]; for (int i = 0; i < n; i++) { - Constructor[] constructor = c[i]; + Constructor[] constructor = c[i]; checkContextMatch(constructor); - cla[i] = new ConstructorList(this, constructor); + cla[i] = new ConstructorList<>(this, constructor); n_constr[i] = cla[i].getNativeObject(); } long[] n_res = new long[n]; Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res, n_constr); - DatatypeSort[] res = new DatatypeSort[n]; + DatatypeSort[] res = new DatatypeSort[n]; for (int i = 0; i < n; i++) - res[i] = new DatatypeSort(this, n_res[i]); + res[i] = new DatatypeSort<>(this, n_res[i]); return res; } /** * Create mutually recursive data-types. **/ - public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c) + public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c) { return mkDatatypeSorts(mkSymbols(names), c); @@ -425,10 +422,10 @@ public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c) * that is passed in as argument is updated with value v, * the remaining fields of t are unchanged. **/ - public Expr mkUpdateField(FuncDecl field, Expr t, Expr v) + public Expr mkUpdateField(FuncDecl field, Expr t, Expr v) throws Z3Exception { - return Expr.create (this, + return (Expr) Expr.create(this, Native.datatypeUpdateField (nCtx(), field.getNativeObject(), t.getNativeObject(), v.getNativeObject())); @@ -438,59 +435,59 @@ public Expr mkUpdateField(FuncDecl field, Expr t, Expr v) /** * Creates a new function declaration. **/ - public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range) + public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, R range) { checkContextMatch(name); checkContextMatch(domain); checkContextMatch(range); - return new FuncDecl(this, name, domain, range); + return new FuncDecl<>(this, name, domain, range); } /** * Creates a new function declaration. **/ - public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range) + public FuncDecl mkFuncDecl(Symbol name, Sort domain, R range) { checkContextMatch(name); checkContextMatch(domain); checkContextMatch(range); Sort[] q = new Sort[] { domain }; - return new FuncDecl(this, name, q, range); + return new FuncDecl<>(this, name, q, range); } /** * Creates a new function declaration. **/ - public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range) + public FuncDecl mkFuncDecl(String name, Sort[] domain, R range) { checkContextMatch(domain); checkContextMatch(range); - return new FuncDecl(this, mkSymbol(name), domain, range); + return new FuncDecl<>(this, mkSymbol(name), domain, range); } /** * Creates a new function declaration. **/ - public FuncDecl mkFuncDecl(String name, Sort domain, Sort range) + public FuncDecl mkFuncDecl(String name, Sort domain, R range) { checkContextMatch(domain); checkContextMatch(range); Sort[] q = new Sort[] { domain }; - return new FuncDecl(this, mkSymbol(name), q, range); + return new FuncDecl<>(this, mkSymbol(name), q, range); } /** * Creates a new recursive function declaration. **/ - public FuncDecl mkRecFuncDecl(Symbol name, Sort[] domain, Sort range) + public FuncDecl mkRecFuncDecl(Symbol name, Sort[] domain, R range) { checkContextMatch(name); checkContextMatch(domain); checkContextMatch(range); - return new FuncDecl(this, name, domain, range, true); + return new FuncDecl<>(this, name, domain, range, true); } @@ -500,14 +497,14 @@ public FuncDecl mkRecFuncDecl(Symbol name, Sort[] domain, Sort range) * MkRecFuncDecl. The body may contain recursive uses of the function or * other mutually recursive functions. */ - public void AddRecDef(FuncDecl f, Expr[] args, Expr body) + public void AddRecDef(FuncDecl f, Expr[] args, Expr body) { checkContextMatch(f); checkContextMatch(args); checkContextMatch(body); long[] argsNative = AST.arrayToNative(args); Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject()); - } + } /** * Creates a fresh function declaration with a name prefixed with @@ -515,31 +512,31 @@ public void AddRecDef(FuncDecl f, Expr[] args, Expr body) * @see #mkFuncDecl(String,Sort,Sort) * @see #mkFuncDecl(String,Sort[],Sort) **/ - public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range) + public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, R range) { checkContextMatch(domain); checkContextMatch(range); - return new FuncDecl(this, prefix, domain, range); + return new FuncDecl<>(this, prefix, domain, range); } /** * Creates a new constant function declaration. **/ - public FuncDecl mkConstDecl(Symbol name, Sort range) + public FuncDecl mkConstDecl(Symbol name, R range) { checkContextMatch(name); checkContextMatch(range); - return new FuncDecl(this, name, null, range); + return new FuncDecl<>(this, name, null, range); } /** * Creates a new constant function declaration. **/ - public FuncDecl mkConstDecl(String name, Sort range) + public FuncDecl mkConstDecl(String name, R range) { checkContextMatch(range); - return new FuncDecl(this, mkSymbol(name), null, range); + return new FuncDecl<>(this, mkSymbol(name), null, range); } /** @@ -548,11 +545,11 @@ public FuncDecl mkConstDecl(String name, Sort range) * @see #mkFuncDecl(String,Sort,Sort) * @see #mkFuncDecl(String,Sort[],Sort) **/ - public FuncDecl mkFreshConstDecl(String prefix, Sort range) + public FuncDecl mkFreshConstDecl(String prefix, R range) { checkContextMatch(range); - return new FuncDecl(this, prefix, null, range); + return new FuncDecl<>(this, prefix, null, range); } /** @@ -560,16 +557,16 @@ public FuncDecl mkFreshConstDecl(String prefix, Sort range) * @param index The de-Bruijn index of the variable * @param ty The sort of the variable **/ - public Expr mkBound(int index, Sort ty) + public Expr mkBound(int index, R ty) { - return Expr.create(this, + return (Expr) Expr.create(this, Native.mkBound(nCtx(), index, ty.getNativeObject())); } /** * Create a quantifier pattern. **/ - public Pattern mkPattern(Expr... terms) + public Pattern mkPattern(Expr... terms) { if (terms.length == 0) throw new Z3Exception("Cannot create a pattern from zero terms"); @@ -583,12 +580,12 @@ public Pattern mkPattern(Expr... terms) * Creates a new Constant of sort {@code range} and named * {@code name}. **/ - public Expr mkConst(Symbol name, Sort range) + public Expr mkConst(Symbol name, R range) { checkContextMatch(name); checkContextMatch(range); - return Expr.create( + return (Expr) Expr.create( this, Native.mkConst(nCtx(), name.getNativeObject(), range.getNativeObject())); @@ -598,7 +595,7 @@ public Expr mkConst(Symbol name, Sort range) * Creates a new Constant of sort {@code range} and named * {@code name}. **/ - public Expr mkConst(String name, Sort range) + public Expr mkConst(String name, R range) { return mkConst(mkSymbol(name), range); } @@ -607,10 +604,10 @@ public Expr mkConst(String name, Sort range) * Creates a fresh Constant of sort {@code range} and a name * prefixed with {@code prefix}. **/ - public Expr mkFreshConst(String prefix, Sort range) + public Expr mkFreshConst(String prefix, R range) { checkContextMatch(range); - return Expr.create(this, + return (Expr) Expr.create(this, Native.mkFreshConst(nCtx(), prefix, range.getNativeObject())); } @@ -618,9 +615,9 @@ public Expr mkFreshConst(String prefix, Sort range) * Creates a fresh constant from the FuncDecl {@code f}. * @param f A decl of a 0-arity function **/ - public Expr mkConst(FuncDecl f) + public Expr mkConst(FuncDecl f) { - return mkApp(f, (Expr[]) null); + return mkApp(f, (Expr[]) null); } /** @@ -690,7 +687,7 @@ public BitVecExpr mkBVConst(String name, int size) /** * Create a new function application. **/ - public Expr mkApp(FuncDecl f, Expr... args) + public Expr mkApp(FuncDecl f, Expr... args) { checkContextMatch(f); checkContextMatch(args); @@ -724,7 +721,7 @@ public BoolExpr mkBool(boolean value) /** * Creates the equality {@code x = y} **/ - public BoolExpr mkEq(Expr x, Expr y) + public BoolExpr mkEq(Expr x, Expr y) { checkContextMatch(x); checkContextMatch(y); @@ -735,7 +732,7 @@ public BoolExpr mkEq(Expr x, Expr y) /** * Creates a {@code distinct} term. **/ - public BoolExpr mkDistinct(Expr... args) + public BoolExpr mkDistinct(Expr... args) { checkContextMatch(args); return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length, @@ -745,7 +742,7 @@ public BoolExpr mkDistinct(Expr... args) /** * Create an expression representing {@code not(a)}. **/ - public BoolExpr mkNot(BoolExpr a) + public BoolExpr mkNot(Expr a) { checkContextMatch(a); return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject())); @@ -758,19 +755,19 @@ public BoolExpr mkNot(BoolExpr a) * @param t2 An expression * @param t3 An expression with the same sort as {@code t2} **/ - public Expr mkITE(BoolExpr t1, Expr t2, Expr t3) + public Expr mkITE(Expr t1, Expr t2, Expr t3) { checkContextMatch(t1); checkContextMatch(t2); checkContextMatch(t3); - return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(), + return (Expr) Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject())); } /** * Create an expression representing {@code t1 iff t2}. **/ - public BoolExpr mkIff(BoolExpr t1, BoolExpr t2) + public BoolExpr mkIff(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -781,7 +778,7 @@ public BoolExpr mkIff(BoolExpr t1, BoolExpr t2) /** * Create an expression representing {@code t1 -> t2}. **/ - public BoolExpr mkImplies(BoolExpr t1, BoolExpr t2) + public BoolExpr mkImplies(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -792,7 +789,7 @@ public BoolExpr mkImplies(BoolExpr t1, BoolExpr t2) /** * Create an expression representing {@code t1 xor t2}. **/ - public BoolExpr mkXor(BoolExpr t1, BoolExpr t2) + public BoolExpr mkXor(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -803,7 +800,7 @@ public BoolExpr mkXor(BoolExpr t1, BoolExpr t2) /** * Create an expression representing {@code t[0] and t[1] and ...}. **/ - public BoolExpr mkAnd(BoolExpr... t) + public BoolExpr mkAnd(Expr... t) { checkContextMatch(t); return new BoolExpr(this, Native.mkAnd(nCtx(), t.length, @@ -813,7 +810,7 @@ public BoolExpr mkAnd(BoolExpr... t) /** * Create an expression representing {@code t[0] or t[1] or ...}. **/ - public BoolExpr mkOr(BoolExpr... t) + public BoolExpr mkOr(Expr... t) { checkContextMatch(t); return new BoolExpr(this, Native.mkOr(nCtx(), t.length, @@ -823,51 +820,51 @@ public BoolExpr mkOr(BoolExpr... t) /** * Create an expression representing {@code t[0] + t[1] + ...}. **/ - public ArithExpr mkAdd(ArithExpr... t) + public ArithExpr mkAdd(Expr... t) { checkContextMatch(t); - return (ArithExpr) Expr.create(this, + return (ArithExpr) Expr.create(this, Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t))); } /** * Create an expression representing {@code t[0] * t[1] * ...}. **/ - public ArithExpr mkMul(ArithExpr... t) + public ArithExpr mkMul(Expr... t) { checkContextMatch(t); - return (ArithExpr) Expr.create(this, + return (ArithExpr) Expr.create(this, Native.mkMul(nCtx(), t.length, AST.arrayToNative(t))); } /** * Create an expression representing {@code t[0] - t[1] - ...}. **/ - public ArithExpr mkSub(ArithExpr... t) + public ArithExpr mkSub(Expr... t) { checkContextMatch(t); - return (ArithExpr) Expr.create(this, + return (ArithExpr) Expr.create(this, Native.mkSub(nCtx(), t.length, AST.arrayToNative(t))); } /** * Create an expression representing {@code -t}. **/ - public ArithExpr mkUnaryMinus(ArithExpr t) + public ArithExpr mkUnaryMinus(Expr t) { checkContextMatch(t); - return (ArithExpr) Expr.create(this, + return (ArithExpr) Expr.create(this, Native.mkUnaryMinus(nCtx(), t.getNativeObject())); } /** * Create an expression representing {@code t1 / t2}. **/ - public ArithExpr mkDiv(ArithExpr t1, ArithExpr t2) + public ArithExpr mkDiv(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); - return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(), + return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -876,7 +873,7 @@ public ArithExpr mkDiv(ArithExpr t1, ArithExpr t2) * Remarks: The * arguments must have int type. **/ - public IntExpr mkMod(IntExpr t1, IntExpr t2) + public IntExpr mkMod(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -889,7 +886,7 @@ public IntExpr mkMod(IntExpr t1, IntExpr t2) * Remarks: The * arguments must have int type. **/ - public IntExpr mkRem(IntExpr t1, IntExpr t2) + public IntExpr mkRem(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -900,11 +897,11 @@ public IntExpr mkRem(IntExpr t1, IntExpr t2) /** * Create an expression representing {@code t1 ^ t2}. **/ - public ArithExpr mkPower(ArithExpr t1, ArithExpr t2) + public ArithExpr mkPower(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); - return (ArithExpr) Expr.create( + return (ArithExpr) Expr.create( this, Native.mkPower(nCtx(), t1.getNativeObject(), t2.getNativeObject())); @@ -913,7 +910,7 @@ public ArithExpr mkPower(ArithExpr t1, ArithExpr t2) /** * Create an expression representing {@code t1 < t2} **/ - public BoolExpr mkLt(ArithExpr t1, ArithExpr t2) + public BoolExpr mkLt(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -924,7 +921,7 @@ public BoolExpr mkLt(ArithExpr t1, ArithExpr t2) /** * Create an expression representing {@code t1 <= t2} **/ - public BoolExpr mkLe(ArithExpr t1, ArithExpr t2) + public BoolExpr mkLe(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -935,7 +932,7 @@ public BoolExpr mkLe(ArithExpr t1, ArithExpr t2) /** * Create an expression representing {@code t1 > t2} **/ - public BoolExpr mkGt(ArithExpr t1, ArithExpr t2) + public BoolExpr mkGt(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -946,7 +943,7 @@ public BoolExpr mkGt(ArithExpr t1, ArithExpr t2) /** * Create an expression representing {@code t1 >= t2} **/ - public BoolExpr mkGe(ArithExpr t1, ArithExpr t2) + public BoolExpr mkGe(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -964,7 +961,7 @@ public BoolExpr mkGe(ArithExpr t1, ArithExpr t2) * {@code MakeInt2Real(k) <= t1 < MkInt2Real(k)+1}. The argument * must be of integer sort. **/ - public RealExpr mkInt2Real(IntExpr t) + public RealExpr mkInt2Real(Expr t) { checkContextMatch(t); return new RealExpr(this, @@ -977,7 +974,7 @@ public RealExpr mkInt2Real(IntExpr t) * follows the SMT-LIB standard for the function to_int. The argument must * be of real sort. **/ - public IntExpr mkReal2Int(RealExpr t) + public IntExpr mkReal2Int(Expr t) { checkContextMatch(t); return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject())); @@ -986,7 +983,7 @@ public IntExpr mkReal2Int(RealExpr t) /** * Creates an expression that checks whether a real number is an integer. **/ - public BoolExpr mkIsInteger(RealExpr t) + public BoolExpr mkIsInteger(Expr t) { checkContextMatch(t); return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject())); @@ -997,7 +994,7 @@ public BoolExpr mkIsInteger(RealExpr t) * Remarks: The argument must have a bit-vector * sort. **/ - public BitVecExpr mkBVNot(BitVecExpr t) + public BitVecExpr mkBVNot(Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject())); @@ -1008,7 +1005,7 @@ public BitVecExpr mkBVNot(BitVecExpr t) * * Remarks: The argument must have a bit-vector sort. **/ - public BitVecExpr mkBVRedAND(BitVecExpr t) + public BitVecExpr mkBVRedAND(Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkBvredand(nCtx(), @@ -1020,7 +1017,7 @@ public BitVecExpr mkBVRedAND(BitVecExpr t) * * Remarks: The argument must have a bit-vector sort. **/ - public BitVecExpr mkBVRedOR(BitVecExpr t) + public BitVecExpr mkBVRedOR(Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkBvredor(nCtx(), @@ -1032,7 +1029,7 @@ public BitVecExpr mkBVRedOR(BitVecExpr t) * Remarks: The arguments must have a bit-vector * sort. **/ - public BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVAND(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1045,7 +1042,7 @@ public BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have a bit-vector * sort. **/ - public BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVOR(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1058,7 +1055,7 @@ public BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have a bit-vector * sort. **/ - public BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVXOR(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1071,7 +1068,7 @@ public BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have a bit-vector * sort. **/ - public BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVNAND(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1084,7 +1081,7 @@ public BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have a bit-vector * sort. **/ - public BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVNOR(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1097,7 +1094,7 @@ public BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have a bit-vector * sort. **/ - public BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVXNOR(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1110,7 +1107,7 @@ public BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have a * bit-vector sort. **/ - public BitVecExpr mkBVNeg(BitVecExpr t) + public BitVecExpr mkBVNeg(Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject())); @@ -1121,7 +1118,7 @@ public BitVecExpr mkBVNeg(BitVecExpr t) * Remarks: The arguments must have the same * bit-vector sort. **/ - public BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVAdd(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1134,7 +1131,7 @@ public BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have the same * bit-vector sort. **/ - public BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVSub(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1147,7 +1144,7 @@ public BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have the * same bit-vector sort. **/ - public BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVMul(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1162,7 +1159,7 @@ public BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2) * zero, then the result is undefined. The arguments must have the same * bit-vector sort. **/ - public BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVUDiv(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1183,7 +1180,7 @@ public BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2) * If {@code t2} is zero, then the result is undefined. The arguments * must have the same bit-vector sort. **/ - public BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVSDiv(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1198,7 +1195,7 @@ public BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2) * unsigned division. If {@code t2} is zero, then the result is * undefined. The arguments must have the same bit-vector sort. **/ - public BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVURem(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1216,7 +1213,7 @@ public BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2) * If {@code t2} is zero, then the result is undefined. The arguments * must have the same bit-vector sort. **/ - public BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVSRem(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1230,7 +1227,7 @@ public BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2) * {@code t2} is zero, then the result is undefined. The arguments must * have the same bit-vector sort. **/ - public BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVSMod(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1243,7 +1240,7 @@ public BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have the same bit-vector * sort. **/ - public BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVULT(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1256,7 +1253,7 @@ public BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have the * same bit-vector sort. **/ - public BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVSLT(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1269,7 +1266,7 @@ public BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have the * same bit-vector sort. **/ - public BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVULE(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1282,7 +1279,7 @@ public BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments * must have the same bit-vector sort. **/ - public BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVSLE(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1295,7 +1292,7 @@ public BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have the * same bit-vector sort. **/ - public BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVUGE(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1308,7 +1305,7 @@ public BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments * must have the same bit-vector sort. **/ - public BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVSGE(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1321,7 +1318,7 @@ public BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have the same * bit-vector sort. **/ - public BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVUGT(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1334,7 +1331,7 @@ public BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2) * Remarks: The arguments must have * the same bit-vector sort. **/ - public BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVSGT(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1352,7 +1349,7 @@ public BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2) * ({@code t2}). * **/ - public BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkConcat(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1368,7 +1365,7 @@ public BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2) * {@code n = high - low + 1}. The argument {@code t} must * have a bit-vector sort. **/ - public BitVecExpr mkExtract(int high, int low, BitVecExpr t) + public BitVecExpr mkExtract(int high, int low, Expr t) { checkContextMatch(t); @@ -1383,7 +1380,7 @@ public BitVecExpr mkExtract(int high, int low, BitVecExpr t) * the size of the given bit-vector. The argument {@code t} must * have a bit-vector sort. **/ - public BitVecExpr mkSignExt(int i, BitVecExpr t) + public BitVecExpr mkSignExt(int i, Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkSignExt(nCtx(), i, @@ -1397,7 +1394,7 @@ public BitVecExpr mkSignExt(int i, BitVecExpr t) * where \c m is the size of the given bit-vector. The argument {@code t} * must have a bit-vector sort. **/ - public BitVecExpr mkZeroExt(int i, BitVecExpr t) + public BitVecExpr mkZeroExt(int i, Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i, @@ -1409,7 +1406,7 @@ public BitVecExpr mkZeroExt(int i, BitVecExpr t) * Remarks: The argument {@code t} must * have a bit-vector sort. **/ - public BitVecExpr mkRepeat(int i, BitVecExpr t) + public BitVecExpr mkRepeat(int i, Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkRepeat(nCtx(), i, @@ -1427,7 +1424,7 @@ public BitVecExpr mkRepeat(int i, BitVecExpr t) * * The arguments must have a bit-vector sort. **/ - public BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVSHL(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1446,7 +1443,7 @@ public BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2) * * The arguments must have a bit-vector sort. **/ - public BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVLSHR(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1466,7 +1463,7 @@ public BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2) * * The arguments must have a bit-vector sort. **/ - public BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVASHR(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -1479,7 +1476,7 @@ public BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2) * Remarks: Rotate bits of \c t to the left \c i times. The * argument {@code t} must have a bit-vector sort. **/ - public BitVecExpr mkBVRotateLeft(int i, BitVecExpr t) + public BitVecExpr mkBVRotateLeft(int i, Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i, @@ -1491,7 +1488,7 @@ public BitVecExpr mkBVRotateLeft(int i, BitVecExpr t) * Remarks: Rotate bits of \c t to the right \c i times. The * argument {@code t} must have a bit-vector sort. **/ - public BitVecExpr mkBVRotateRight(int i, BitVecExpr t) + public BitVecExpr mkBVRotateRight(int i, Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i, @@ -1504,7 +1501,7 @@ public BitVecExpr mkBVRotateRight(int i, BitVecExpr t) * {@code t2} times. The arguments must have the same bit-vector * sort. **/ - public BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVRotateLeft(Expr t1, Expr t2) { checkContextMatch(t1); @@ -1519,7 +1516,7 @@ public BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2) * right{@code t2} times. The arguments must have the same * bit-vector sort. **/ - public BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2) + public BitVecExpr mkBVRotateRight(Expr t1, Expr t2) { checkContextMatch(t1); @@ -1537,7 +1534,7 @@ public BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2) * * The argument must be of integer sort. **/ - public BitVecExpr mkInt2BV(int n, IntExpr t) + public BitVecExpr mkInt2BV(int n, Expr t) { checkContextMatch(t); return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n, @@ -1558,7 +1555,7 @@ public BitVecExpr mkInt2BV(int n, IntExpr t) * * The argument must be of bit-vector sort. **/ - public IntExpr mkBV2Int(BitVecExpr t, boolean signed) + public IntExpr mkBV2Int(Expr t, boolean signed) { checkContextMatch(t); return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(), @@ -1570,7 +1567,7 @@ public IntExpr mkBV2Int(BitVecExpr t, boolean signed) * overflow. * Remarks: The arguments must be of bit-vector sort. **/ - public BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, + public BoolExpr mkBVAddNoOverflow(Expr t1, Expr t2, boolean isSigned) { checkContextMatch(t1); @@ -1584,7 +1581,7 @@ public BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, * underflow. * Remarks: The arguments must be of bit-vector sort. **/ - public BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVAddNoUnderflow(Expr t1, Expr t2) { checkContextMatch(t1); @@ -1598,7 +1595,7 @@ public BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2) * overflow. * Remarks: The arguments must be of bit-vector sort. **/ - public BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVSubNoOverflow(Expr t1, Expr t2) { checkContextMatch(t1); @@ -1612,7 +1609,7 @@ public BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2) * underflow. * Remarks: The arguments must be of bit-vector sort. **/ - public BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, + public BoolExpr mkBVSubNoUnderflow(Expr t1, Expr t2, boolean isSigned) { checkContextMatch(t1); @@ -1626,7 +1623,7 @@ public BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, * overflow. * Remarks: The arguments must be of bit-vector sort. **/ - public BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVSDivNoOverflow(Expr t1, Expr t2) { checkContextMatch(t1); @@ -1640,7 +1637,7 @@ public BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2) * overflow. * Remarks: The arguments must be of bit-vector sort. **/ - public BoolExpr mkBVNegNoOverflow(BitVecExpr t) + public BoolExpr mkBVNegNoOverflow(Expr t) { checkContextMatch(t); return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(), @@ -1652,7 +1649,7 @@ public BoolExpr mkBVNegNoOverflow(BitVecExpr t) * overflow. * Remarks: The arguments must be of bit-vector sort. **/ - public BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, + public BoolExpr mkBVMulNoOverflow(Expr t1, Expr t2, boolean isSigned) { checkContextMatch(t1); @@ -1666,7 +1663,7 @@ public BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, * underflow. * Remarks: The arguments must be of bit-vector sort. **/ - public BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2) + public BoolExpr mkBVMulNoUnderflow(Expr t1, Expr t2) { checkContextMatch(t1); @@ -1678,19 +1675,19 @@ public BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2) /** * Create an array constant. **/ - public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range) + public ArrayExpr mkArrayConst(Symbol name, D domain, R range) { - return (ArrayExpr) mkConst(name, mkArraySort(domain, range)); + return (ArrayExpr) mkConst(name, mkArraySort(domain, range)); } /** * Create an array constant. **/ - public ArrayExpr mkArrayConst(String name, Sort domain, Sort range) + public ArrayExpr mkArrayConst(String name, D domain, R range) { - return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range)); + return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range)); } /** @@ -1706,11 +1703,11 @@ public ArrayExpr mkArrayConst(String name, Sort domain, Sort range) * @see #mkStore **/ - public Expr mkSelect(ArrayExpr a, Expr i) + public Expr mkSelect(Expr> a, Expr i) { checkContextMatch(a); checkContextMatch(i); - return Expr.create( + return (Expr) Expr.create( this, Native.mkSelect(nCtx(), a.getNativeObject(), i.getNativeObject())); @@ -1727,13 +1724,12 @@ public Expr mkSelect(ArrayExpr a, Expr i) * * @see #mkArraySort * @see #mkStore - **/ - public Expr mkSelect(ArrayExpr a, Expr[] args) + public Expr mkSelect(Expr> a, Expr[] args) { checkContextMatch(a); checkContextMatch(args); - return Expr.create( + return (Expr) Expr.create( this, Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args))); } @@ -1754,12 +1750,12 @@ public Expr mkSelect(ArrayExpr a, Expr[] args) * @see #mkSelect **/ - public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v) + public ArrayExpr mkStore(Expr> a, Expr i, Expr v) { checkContextMatch(a); checkContextMatch(i); checkContextMatch(v); - return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(), + return new ArrayExpr<>(this, Native.mkStore(nCtx(), a.getNativeObject(), i.getNativeObject(), v.getNativeObject())); } @@ -1779,12 +1775,12 @@ public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v) * @see #mkSelect **/ - public ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v) + public ArrayExpr mkStore(Expr> a, Expr[] args, Expr v) { checkContextMatch(a); checkContextMatch(args); checkContextMatch(v); - return new ArrayExpr(this, Native.mkStoreN(nCtx(), a.getNativeObject(), + return new ArrayExpr<>(this, Native.mkStoreN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args), v.getNativeObject())); } @@ -1797,11 +1793,11 @@ public ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v) * @see #mkSelect * **/ - public ArrayExpr mkConstArray(Sort domain, Expr v) + public ArrayExpr mkConstArray(D domain, Expr v) { checkContextMatch(domain); checkContextMatch(v); - return new ArrayExpr(this, Native.mkConstArray(nCtx(), + return new ArrayExpr<>(this, Native.mkConstArray(nCtx(), domain.getNativeObject(), v.getNativeObject())); } @@ -1818,11 +1814,11 @@ public ArrayExpr mkConstArray(Sort domain, Expr v) * @see #mkStore **/ - public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args) + public ArrayExpr mkMap(FuncDecl f, Expr>... args) { checkContextMatch(f); checkContextMatch(args); - return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(), + return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(), f.getNativeObject(), AST.arrayLength(args), AST.arrayToNative(args))); } @@ -1833,61 +1829,61 @@ public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args) * value, for arrays that can be represented as finite maps with a default * range value. **/ - public Expr mkTermArray(ArrayExpr array) + public Expr mkTermArray(Expr> array) { checkContextMatch(array); - return Expr.create(this, + return (Expr) Expr.create(this, Native.mkArrayDefault(nCtx(), array.getNativeObject())); } /** * Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt. **/ - public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2) + public Expr mkArrayExt(Expr> arg1, Expr> arg2) { checkContextMatch(arg1); checkContextMatch(arg2); - return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); + return (Expr) Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); } /** * Create a set type. **/ - public SetSort mkSetSort(Sort ty) + public SetSort mkSetSort(D ty) { checkContextMatch(ty); - return new SetSort(this, ty); + return new SetSort<>(this, ty); } /** * Create an empty set. **/ - public ArrayExpr mkEmptySet(Sort domain) + public ArrayExpr mkEmptySet(D domain) { checkContextMatch(domain); - return (ArrayExpr)Expr.create(this, + return (ArrayExpr) Expr.create(this, Native.mkEmptySet(nCtx(), domain.getNativeObject())); } /** * Create the full set. **/ - public ArrayExpr mkFullSet(Sort domain) + public ArrayExpr mkFullSet(D domain) { checkContextMatch(domain); - return (ArrayExpr)Expr.create(this, + return (ArrayExpr) Expr.create(this, Native.mkFullSet(nCtx(), domain.getNativeObject())); } /** * Add an element to the set. **/ - public ArrayExpr mkSetAdd(ArrayExpr set, Expr element) + public ArrayExpr mkSetAdd(Expr> set, Expr element) { checkContextMatch(set); checkContextMatch(element); - return (ArrayExpr)Expr.create(this, + return (ArrayExpr) Expr.create(this, Native.mkSetAdd(nCtx(), set.getNativeObject(), element.getNativeObject())); } @@ -1895,11 +1891,11 @@ public ArrayExpr mkSetAdd(ArrayExpr set, Expr element) /** * Remove an element from a set. **/ - public ArrayExpr mkSetDel(ArrayExpr set, Expr element) + public ArrayExpr mkSetDel(Expr> set, Expr element) { checkContextMatch(set); checkContextMatch(element); - return (ArrayExpr)Expr.create(this, + return (ArrayExpr)Expr.create(this, Native.mkSetDel(nCtx(), set.getNativeObject(), element.getNativeObject())); } @@ -1907,10 +1903,10 @@ public ArrayExpr mkSetDel(ArrayExpr set, Expr element) /** * Take the union of a list of sets. **/ - public ArrayExpr mkSetUnion(ArrayExpr... args) + public ArrayExpr mkSetUnion(Expr>... args) { checkContextMatch(args); - return (ArrayExpr)Expr.create(this, + return (ArrayExpr)Expr.create(this, Native.mkSetUnion(nCtx(), args.length, AST.arrayToNative(args))); } @@ -1918,10 +1914,10 @@ public ArrayExpr mkSetUnion(ArrayExpr... args) /** * Take the intersection of a list of sets. **/ - public ArrayExpr mkSetIntersection(ArrayExpr... args) + public ArrayExpr mkSetIntersection(Expr>... args) { checkContextMatch(args); - return (ArrayExpr)Expr.create(this, + return (ArrayExpr) Expr.create(this, Native.mkSetIntersect(nCtx(), args.length, AST.arrayToNative(args))); } @@ -1929,11 +1925,11 @@ public ArrayExpr mkSetIntersection(ArrayExpr... args) /** * Take the difference between two sets. **/ - public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2) + public ArrayExpr mkSetDifference(Expr> arg1, Expr> arg2) { checkContextMatch(arg1); checkContextMatch(arg2); - return (ArrayExpr)Expr.create(this, + return (ArrayExpr) Expr.create(this, Native.mkSetDifference(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); } @@ -1941,17 +1937,17 @@ public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2) /** * Take the complement of a set. **/ - public ArrayExpr mkSetComplement(ArrayExpr arg) + public ArrayExpr mkSetComplement(Expr> arg) { checkContextMatch(arg); - return (ArrayExpr)Expr.create(this, + return (ArrayExpr)Expr.create(this, Native.mkSetComplement(nCtx(), arg.getNativeObject())); } /** * Check for set membership. **/ - public BoolExpr mkSetMembership(Expr elem, ArrayExpr set) + public BoolExpr mkSetMembership(Expr elem, Expr> set) { checkContextMatch(elem); checkContextMatch(set); @@ -1963,7 +1959,7 @@ public BoolExpr mkSetMembership(Expr elem, ArrayExpr set) /** * Check for subsetness of sets. **/ - public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2) + public BoolExpr mkSetSubset(Expr> arg1, Expr> arg2) { checkContextMatch(arg1); checkContextMatch(arg2); @@ -1980,41 +1976,41 @@ public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2) /** * Create the empty sequence. */ - public SeqExpr mkEmptySeq(Sort s) + public SeqExpr mkEmptySeq(R s) { checkContextMatch(s); - return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject())); } /** * Create the singleton sequence. */ - public SeqExpr mkUnit(Expr elem) + public SeqExpr mkUnit(Expr elem) { checkContextMatch(elem); - return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject())); } /** * Create a string constant. */ - public SeqExpr mkString(String s) + public SeqExpr mkString(String s) { - return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s)); + return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s)); } /** * Convert an integer expression to a string. */ - public SeqExpr intToString(Expr e) + public SeqExpr intToString(Expr e) { - return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject())); } /** * Convert an integer expression to a string. */ - public IntExpr stringToInt(Expr e) + public IntExpr stringToInt(Expr> e) { return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject())); } @@ -2022,17 +2018,17 @@ public IntExpr stringToInt(Expr e) /** * Concatenate sequences. */ - public SeqExpr mkConcat(SeqExpr... t) + public SeqExpr mkConcat(SeqSort... t) { checkContextMatch(t); - return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t))); + return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t))); } /** * Retrieve the length of a given sequence. */ - public IntExpr mkLength(SeqExpr s) + public IntExpr mkLength(Expr> s) { checkContextMatch(s); return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject())); @@ -2041,7 +2037,7 @@ public IntExpr mkLength(SeqExpr s) /** * Check for sequence prefix. */ - public BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2) + public BoolExpr mkPrefixOf(Expr> s1, Expr> s2) { checkContextMatch(s1, s2); return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject())); @@ -2050,7 +2046,7 @@ public BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2) /** * Check for sequence suffix. */ - public BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2) + public BoolExpr mkSuffixOf(Expr> s1, Expr> s2) { checkContextMatch(s1, s2); return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject())); @@ -2059,7 +2055,7 @@ public BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2) /** * Check for sequence containment of s2 in s1. */ - public BoolExpr mkContains(SeqExpr s1, SeqExpr s2) + public BoolExpr mkContains(Expr> s1, Expr> s2) { checkContextMatch(s1, s2); return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject())); @@ -2068,35 +2064,35 @@ public BoolExpr mkContains(SeqExpr s1, SeqExpr s2) /** * Retrieve sequence of length one at index. */ - public SeqExpr mkAt(SeqExpr s, IntExpr index) + public SeqExpr mkAt(Expr> s, Expr index) { checkContextMatch(s, index); - return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject())); } /** * Retrieve element at index. */ - public Expr MkNth(SeqExpr s, Expr index) + public Expr MkNth(Expr> s, Expr index) { checkContextMatch(s, index); - return Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); + return (Expr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); } /** * Extract subsequence. */ - public SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length) + public SeqExpr mkExtract(Expr> s, Expr offset, Expr length) { checkContextMatch(s, offset, length); - return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject())); } /** * Extract index of sub-string starting at offset. */ - public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset) + public IntExpr mkIndexOf(Expr> s, Expr> substr, Expr offset) { checkContextMatch(s, substr, offset); return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject())); @@ -2105,26 +2101,26 @@ public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset) /** * Replace the first occurrence of src by dst in s. */ - public SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst) + public SeqExpr mkReplace(Expr> s, Expr> src, Expr> dst) { checkContextMatch(s, src, dst); - return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject())); } /** * Convert a regular expression that accepts sequence s. */ - public ReExpr mkToRe(SeqExpr s) + public ReExpr mkToRe(Expr> s) { checkContextMatch(s); - return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject())); } /** * Check for regular expression membership. */ - public BoolExpr mkInRe(SeqExpr s, ReExpr re) + public BoolExpr mkInRe(Expr> s, Expr> re) { checkContextMatch(s, re); return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject())); @@ -2133,114 +2129,113 @@ public BoolExpr mkInRe(SeqExpr s, ReExpr re) /** * Take the Kleene star of a regular expression. */ - public ReExpr mkStar(ReExpr re) + public ReExpr mkStar(Expr> re) { checkContextMatch(re); - return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject())); } /** * Take the lower and upper-bounded Kleene star of a regular expression. */ - public ReExpr mkLoop(ReExpr re, int lo, int hi) + public ReExpr mkLoop(Expr> re, int lo, int hi) { - return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi)); + return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi)); } /** * Take the lower-bounded Kleene star of a regular expression. */ - public ReExpr mkLoop(ReExpr re, int lo) + public ReExpr mkLoop(Expr> re, int lo) { - return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0)); + return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0)); } /** * Take the Kleene plus of a regular expression. */ - public ReExpr mkPlus(ReExpr re) + public ReExpr mkPlus(Expr> re) { checkContextMatch(re); - return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject())); } /** * Create the optional regular expression. */ - public ReExpr mkOption(ReExpr re) + public ReExpr mkOption(Expr> re) { checkContextMatch(re); - return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject())); } - /** * Create the complement regular expression. */ - public ReExpr mkComplement(ReExpr re) + public ReExpr mkComplement(Expr> re) { checkContextMatch(re); - return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject())); } /** * Create the concatenation of regular languages. */ - public ReExpr mkConcat(ReExpr... t) + public ReExpr mkConcat(ReExpr... t) { checkContextMatch(t); - return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t))); + return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t))); } /** * Create the union of regular languages. */ - public ReExpr mkUnion(ReExpr... t) + public ReExpr mkUnion(Expr>... t) { checkContextMatch(t); - return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t))); + return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t))); } /** * Create the intersection of regular languages. */ - public ReExpr mkIntersect(ReExpr... t) + public ReExpr mkIntersect(Expr>... t) { checkContextMatch(t); - return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t))); + return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t))); } /** * Create the empty regular expression. */ - public ReExpr mkEmptyRe(Sort s) + public ReExpr mkEmptyRe(R s) { - return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); } /** * Create the full regular expression. */ - public ReExpr mkFullRe(Sort s) + public ReExpr mkFullRe(R s) { - return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); } /** * Create a range expression. */ - public ReExpr mkRange(SeqExpr lo, SeqExpr hi) + public ReExpr mkRange(Expr> lo, Expr> hi) { checkContextMatch(lo, hi); - return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject())); } /** * Create an at-most-k constraint. */ - public BoolExpr mkAtMost(BoolExpr[] args, int k) + public BoolExpr mkAtMost(Expr[] args, int k) { checkContextMatch(args); return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k)); @@ -2249,7 +2244,7 @@ public BoolExpr mkAtMost(BoolExpr[] args, int k) /** * Create an at-least-k constraint. */ - public BoolExpr mkAtLeast(BoolExpr[] args, int k) + public BoolExpr mkAtLeast(Expr[] args, int k) { checkContextMatch(args); return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k)); @@ -2258,7 +2253,7 @@ public BoolExpr mkAtLeast(BoolExpr[] args, int k) /** * Create a pseudo-Boolean less-or-equal constraint. */ - public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k) + public BoolExpr mkPBLe(int[] coeffs, Expr[] args, int k) { checkContextMatch(args); return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k)); @@ -2267,7 +2262,7 @@ public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k) /** * Create a pseudo-Boolean greater-or-equal constraint. */ - public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k) + public BoolExpr mkPBGe(int[] coeffs, Expr[] args, int k) { checkContextMatch(args); return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k)); @@ -2276,13 +2271,12 @@ public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k) /** * Create a pseudo-Boolean equal constraint. */ - public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k) + public BoolExpr mkPBEq(int[] coeffs, Expr[] args, int k) { checkContextMatch(args); return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k)); } - /** * Create a Term of a given sort. * @param v A string representing the term value in decimal notation. If the given sort is a real, then the @@ -2294,10 +2288,10 @@ public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k) * * @return A Term with value {@code v} and sort {@code ty} **/ - public Expr mkNumeral(String v, Sort ty) + public Expr mkNumeral(String v, R ty) { checkContextMatch(ty); - return Expr.create(this, + return (Expr) Expr.create(this, Native.mkNumeral(nCtx(), v, ty.getNativeObject())); } @@ -2311,10 +2305,10 @@ public Expr mkNumeral(String v, Sort ty) * * @return A Term with value {@code v} and type {@code ty} **/ - public Expr mkNumeral(int v, Sort ty) + public Expr mkNumeral(int v, R ty) { checkContextMatch(ty); - return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject())); + return (Expr) Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject())); } /** @@ -2327,10 +2321,10 @@ public Expr mkNumeral(int v, Sort ty) * * @return A Term with value {@code v} and type {@code ty} **/ - public Expr mkNumeral(long v, Sort ty) + public Expr mkNumeral(long v, R ty) { checkContextMatch(ty); - return Expr.create(this, + return (Expr) Expr.create(this, Native.mkInt64(nCtx(), v, ty.getNativeObject())); } @@ -2483,11 +2477,10 @@ public BitVecNum mkBV(long v, int size) * of {@code names} and {@code sorts} refers to the variable * with index 1, etc. **/ - public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, - int weight, Pattern[] patterns, Expr[] noPatterns, + public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, + int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { - return Quantifier.of(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -2496,8 +2489,8 @@ public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, * Creates a universal quantifier using a list of constants that will form the set of bound variables. * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) **/ - public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, - Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, + public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, + Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2509,8 +2502,8 @@ public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, * Creates an existential quantifier using de-Bruijn indexed variables. * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) **/ - public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, - int weight, Pattern[] patterns, Expr[] noPatterns, + public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, + int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2522,8 +2515,8 @@ public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, * Creates an existential quantifier using a list of constants that will form the set of bound variables. * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) **/ - public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, - Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, + public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, + Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2536,8 +2529,8 @@ public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) **/ public Quantifier mkQuantifier(boolean universal, Sort[] sorts, - Symbol[] names, Expr body, int weight, Pattern[] patterns, - Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + Symbol[] names, Expr body, int weight, Pattern[] patterns, + Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2553,8 +2546,8 @@ public Quantifier mkQuantifier(boolean universal, Sort[] sorts, * Create a Quantifier * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) **/ - public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, - Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, + public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, + Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2583,7 +2576,7 @@ public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, * @param names names of the bound variables. * @param body the body of the quantifier. **/ - public Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body) + public Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body) { return Lambda.of(this, sorts, names, body); } @@ -2594,7 +2587,7 @@ public Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body) * Creates a lambda expression using a list of constants that will * form the set of bound variables. **/ - public Lambda mkLambda(Expr[] boundConstants, Expr body) + public Lambda mkLambda(Expr[] boundConstants, Expr body) { return Lambda.of(this, boundConstants, body); } @@ -2633,8 +2626,8 @@ public void setPrintMode(Z3_ast_print_mode value) * @return A string representation of the benchmark. **/ public String benchmarkToSMTString(String name, String logic, - String status, String attributes, BoolExpr[] assumptions, - BoolExpr formula) + String status, String attributes, Expr[] assumptions, + Expr formula) { return Native.benchmarkToSmtlibString(nCtx(), name, logic, status, @@ -2652,8 +2645,7 @@ public String benchmarkToSMTString(String name, String logic, * last scope level. **/ public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, - Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) - + Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { int csn = Symbol.arrayLength(sortNames); int cs = Sort.arrayLength(sorts); @@ -2674,8 +2666,7 @@ public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, * @see #parseSMTLIB2String **/ public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, - Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) - + Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { int csn = Symbol.arrayLength(sortNames); int cs = Sort.arrayLength(sorts); @@ -2702,7 +2693,6 @@ public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, * enabled. **/ public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs) - { return new Goal(this, models, unsatCores, proofs); } @@ -3505,7 +3495,7 @@ public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s) * @param t floating-point term * @throws Z3Exception **/ - public FPExpr mkFPAbs(FPExpr t) + public FPExpr mkFPAbs(Expr t) { return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject())); } @@ -3515,7 +3505,7 @@ public FPExpr mkFPAbs(FPExpr t) * @param t floating-point term * @throws Z3Exception **/ - public FPExpr mkFPNeg(FPExpr t) + public FPExpr mkFPNeg(Expr t) { return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject())); } @@ -3527,7 +3517,7 @@ public FPExpr mkFPNeg(FPExpr t) * @param t2 floating-point term * @throws Z3Exception **/ - public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) + public FPExpr mkFPAdd(Expr rm, Expr t1, Expr t2) { return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3539,7 +3529,7 @@ public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) * @param t2 floating-point term * @throws Z3Exception **/ - public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) + public FPExpr mkFPSub(Expr rm, Expr t1, Expr t2) { return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3551,7 +3541,7 @@ public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) * @param t2 floating-point term * @throws Z3Exception **/ - public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) + public FPExpr mkFPMul(Expr rm, Expr t1, Expr t2) { return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3563,7 +3553,7 @@ public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) * @param t2 floating-point term * @throws Z3Exception **/ - public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) + public FPExpr mkFPDiv(Expr rm, Expr t1, Expr t2) { return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3578,7 +3568,7 @@ public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) * The result is round((t1 * t2) + t3) * @throws Z3Exception **/ - public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) + public FPExpr mkFPFMA(Expr rm, Expr t1, Expr t2, Expr t3) { return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject())); } @@ -3589,7 +3579,7 @@ public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) * @param t floating-point term * @throws Z3Exception **/ - public FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t) + public FPExpr mkFPSqrt(Expr rm, Expr t) { return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject())); } @@ -3600,7 +3590,7 @@ public FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t) * @param t2 floating-point term * @throws Z3Exception **/ - public FPExpr mkFPRem(FPExpr t1, FPExpr t2) + public FPExpr mkFPRem(Expr t1, Expr t2) { return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3612,7 +3602,7 @@ public FPExpr mkFPRem(FPExpr t1, FPExpr t2) * @param t floating-point term * @throws Z3Exception **/ - public FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t) + public FPExpr mkFPRoundToIntegral(Expr rm, Expr t) { return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject())); } @@ -3623,7 +3613,7 @@ public FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t) * @param t2 floating-point term * @throws Z3Exception **/ - public FPExpr mkFPMin(FPExpr t1, FPExpr t2) + public FPExpr mkFPMin(Expr t1, Expr t2) { return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3634,7 +3624,7 @@ public FPExpr mkFPMin(FPExpr t1, FPExpr t2) * @param t2 floating-point term * @throws Z3Exception **/ - public FPExpr mkFPMax(FPExpr t1, FPExpr t2) + public FPExpr mkFPMax(Expr t1, Expr t2) { return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3645,7 +3635,7 @@ public FPExpr mkFPMax(FPExpr t1, FPExpr t2) * @param t2 floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2) + public BoolExpr mkFPLEq(Expr t1, Expr t2) { return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3656,7 +3646,7 @@ public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2) * @param t2 floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPLt(FPExpr t1, FPExpr t2) + public BoolExpr mkFPLt(Expr t1, Expr t2) { return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3667,7 +3657,7 @@ public BoolExpr mkFPLt(FPExpr t1, FPExpr t2) * @param t2 floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2) + public BoolExpr mkFPGEq(Expr t1, Expr t2) { return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3678,7 +3668,7 @@ public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2) * @param t2 floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPGt(FPExpr t1, FPExpr t2) + public BoolExpr mkFPGt(Expr t1, Expr t2) { return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3691,7 +3681,7 @@ public BoolExpr mkFPGt(FPExpr t1, FPExpr t2) * Note that this is IEEE 754 equality (as opposed to standard =). * @throws Z3Exception **/ - public BoolExpr mkFPEq(FPExpr t1, FPExpr t2) + public BoolExpr mkFPEq(Expr t1, Expr t2) { return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject())); } @@ -3701,7 +3691,7 @@ public BoolExpr mkFPEq(FPExpr t1, FPExpr t2) * @param t floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPIsNormal(FPExpr t) + public BoolExpr mkFPIsNormal(Expr t) { return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject())); } @@ -3711,7 +3701,7 @@ public BoolExpr mkFPIsNormal(FPExpr t) * @param t floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPIsSubnormal(FPExpr t) + public BoolExpr mkFPIsSubnormal(Expr t) { return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject())); } @@ -3721,7 +3711,7 @@ public BoolExpr mkFPIsSubnormal(FPExpr t) * @param t floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPIsZero(FPExpr t) + public BoolExpr mkFPIsZero(Expr t) { return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject())); } @@ -3731,7 +3721,7 @@ public BoolExpr mkFPIsZero(FPExpr t) * @param t floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPIsInfinite(FPExpr t) + public BoolExpr mkFPIsInfinite(Expr t) { return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject())); } @@ -3741,7 +3731,7 @@ public BoolExpr mkFPIsInfinite(FPExpr t) * @param t floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPIsNaN(FPExpr t) + public BoolExpr mkFPIsNaN(Expr t) { return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject())); } @@ -3751,7 +3741,7 @@ public BoolExpr mkFPIsNaN(FPExpr t) * @param t floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPIsNegative(FPExpr t) + public BoolExpr mkFPIsNegative(Expr t) { return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject())); } @@ -3761,7 +3751,7 @@ public BoolExpr mkFPIsNegative(FPExpr t) * @param t floating-point term * @throws Z3Exception **/ - public BoolExpr mkFPIsPositive(FPExpr t) + public BoolExpr mkFPIsPositive(Expr t) { return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject())); } @@ -3779,7 +3769,7 @@ public BoolExpr mkFPIsPositive(FPExpr t) * of the arguments. * @throws Z3Exception **/ - public FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp) + public FPExpr mkFP(Expr sgn, Expr sig, Expr exp) { return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject())); } @@ -3795,7 +3785,7 @@ public FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp) * IEEE 754-2008 interchange format. * @throws Z3Exception **/ - public FPExpr mkFPToFP(BitVecExpr bv, FPSort s) + public FPExpr mkFPToFP(Expr bv, FPSort s) { return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject())); } @@ -3811,7 +3801,7 @@ public FPExpr mkFPToFP(BitVecExpr bv, FPSort s) * to rounding mode rm. * @throws Z3Exception **/ - public FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s) + public FPExpr mkFPToFP(Expr rm, FPExpr t, FPSort s) { return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject())); } @@ -3827,7 +3817,7 @@ public FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s) * to rounding mode rm. * @throws Z3Exception **/ - public FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s) + public FPExpr mkFPToFP(Expr rm, RealExpr t, FPSort s) { return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject())); } @@ -3845,7 +3835,7 @@ public FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s) * result will be rounded according to rounding mode rm. * @throws Z3Exception **/ - public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed) + public FPExpr mkFPToFP(Expr rm, Expr t, FPSort s, boolean signed) { if (signed) return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject())); @@ -3863,7 +3853,7 @@ public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed) * FloatingPoint sort s. If necessary, rounding according to rm is applied. * @throws Z3Exception **/ - public FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t) + public FPExpr mkFPToFP(FPSort s, Expr rm, Expr t) { return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject())); } @@ -3880,7 +3870,7 @@ public FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t) * the result will be rounded according to rounding mode rm. * @throws Z3Exception **/ - public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed) + public BitVecExpr mkFPToBV(Expr rm, Expr t, int sz, boolean signed) { if (signed) return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz)); @@ -3897,7 +3887,7 @@ public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed) * constraints over real terms. * @throws Z3Exception **/ - public RealExpr mkFPToReal(FPExpr t) + public RealExpr mkFPToReal(Expr t) { return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject())); } @@ -3912,7 +3902,7 @@ public RealExpr mkFPToReal(FPExpr t) * that NaN. * @throws Z3Exception **/ - public BitVecExpr mkFPToIEEEBV(FPExpr t) + public BitVecExpr mkFPToIEEEBV(Expr t) { return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject())); } @@ -3930,7 +3920,7 @@ public BitVecExpr mkFPToIEEEBV(FPExpr t) * @throws Z3Exception **/ - public BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) + public BitVecExpr mkFPToFP(Expr rm, Expr exp, Expr sig, FPSort s) { return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject())); } @@ -4053,11 +4043,11 @@ void checkContextMatch(Z3Object[] arr) private ConstructorListDecRefQueue m_ConstructorList_DRQ = new ConstructorListDecRefQueue(); - public IDecRefQueue getConstructorDRQ() { + public IDecRefQueue> getConstructorDRQ() { return m_Constructor_DRQ; } - public IDecRefQueue getConstructorListDRQ() { + public IDecRefQueue> getConstructorListDRQ() { return m_ConstructorList_DRQ; } @@ -4081,12 +4071,12 @@ public IDecRefQueue getApplyResultDRQ() return m_ApplyResult_DRQ; } - public IDecRefQueue getFuncEntryDRQ() + public IDecRefQueue> getFuncEntryDRQ() { return m_FuncEntry_DRQ; } - public IDecRefQueue getFuncInterpDRQ() + public IDecRefQueue> getFuncInterpDRQ() { return m_FuncInterp_DRQ; } diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java index 9abe230f6ae..7db3bf0834b 100644 --- a/src/api/java/DatatypeExpr.java +++ b/src/api/java/DatatypeExpr.java @@ -20,7 +20,7 @@ /** * Datatype expressions **/ -public class DatatypeExpr extends Expr +public class DatatypeExpr extends Expr> { /** * Constructor for DatatypeExpr diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java index 644d434d32c..8d7f53c2460 100644 --- a/src/api/java/DatatypeSort.java +++ b/src/api/java/DatatypeSort.java @@ -20,7 +20,7 @@ /** * Datatype sorts. **/ -public class DatatypeSort extends Sort +public class DatatypeSort extends Sort { /** * The number of constructors of the datatype sort. @@ -39,12 +39,13 @@ public int getNumConstructors() * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl[] getConstructors() + @SuppressWarnings("unchecked") + public FuncDecl>[] getConstructors() { int n = getNumConstructors(); - FuncDecl[] res = new FuncDecl[n]; + FuncDecl>[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) - res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor( + res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor( getContext().nCtx(), getNativeObject(), i)); return res; } @@ -55,12 +56,13 @@ public FuncDecl[] getConstructors() * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl[] getRecognizers() + @SuppressWarnings("unchecked") + public FuncDecl[] getRecognizers() { int n = getNumConstructors(); - FuncDecl[] res = new FuncDecl[n]; + FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) - res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer( + res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer( getContext().nCtx(), getNativeObject(), i)); return res; } @@ -71,20 +73,20 @@ public FuncDecl[] getRecognizers() * @throws Z3Exception * @throws Z3Exception on error **/ - public FuncDecl[][] getAccessors() + public FuncDecl[][] getAccessors() { int n = getNumConstructors(); - FuncDecl[][] res = new FuncDecl[n][]; + FuncDecl[][] res = new FuncDecl[n][]; for (int i = 0; i < n; i++) { - FuncDecl fd = new FuncDecl(getContext(), + FuncDecl fd = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i)); int ds = fd.getDomainSize(); - FuncDecl[] tmp = new FuncDecl[ds]; + FuncDecl[] tmp = new FuncDecl[ds]; for (int j = 0; j < ds; j++) - tmp[j] = new FuncDecl(getContext(), + tmp[j] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext() .nCtx(), getNativeObject(), i, j)); res[i] = tmp; @@ -97,7 +99,7 @@ public FuncDecl[][] getAccessors() super(ctx, obj); } - DatatypeSort(Context ctx, Symbol name, Constructor[] constructors) + DatatypeSort(Context ctx, Symbol name, Constructor[] constructors) { super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(), diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index e0bd0f617be..5cd11ba08bd 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -20,28 +20,29 @@ /** * Enumeration sorts. **/ -public class EnumSort extends Sort +@SuppressWarnings("unchecked") +public class EnumSort extends Sort { /** * The function declarations of the constants in the enumeration. * @throws Z3Exception on error **/ - public FuncDecl[] getConstDecls() + public FuncDecl>[] getConstDecls() { int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject()); - FuncDecl[] t = new FuncDecl[n]; + FuncDecl[] t = new FuncDecl[n]; for (int i = 0; i < n; i++) - t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i)); - return t; + t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i)); + return (FuncDecl>[]) t; } /** * Retrieves the inx'th constant declaration in the enumeration. * @throws Z3Exception on error **/ - public FuncDecl getConstDecl(int inx) + public FuncDecl> getConstDecl(int inx) { - return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx)); + return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx)); } /** @@ -49,13 +50,13 @@ public FuncDecl getConstDecl(int inx) * @throws Z3Exception on error * @return an Expr[] **/ - public Expr[] getConsts() + public Expr>[] getConsts() { - FuncDecl[] cds = getConstDecls(); - Expr[] t = new Expr[cds.length]; + FuncDecl[] cds = getConstDecls(); + Expr[] t = new Expr[cds.length]; for (int i = 0; i < t.length; i++) t[i] = getContext().mkApp(cds[i]); - return t; + return (Expr>[]) t; } /** @@ -63,7 +64,7 @@ public Expr[] getConsts() * @throws Z3Exception on error * @return an Expr **/ - public Expr getConst(int inx) + public Expr> getConst(int inx) { return getContext().mkApp(getConstDecl(inx)); } @@ -72,12 +73,13 @@ public Expr getConst(int inx) * The test predicates for the constants in the enumeration. * @throws Z3Exception on error **/ - public FuncDecl[] getTesterDecls() + @SuppressWarnings("unchecked") + public FuncDecl[] getTesterDecls() { int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject()); - FuncDecl[] t = new FuncDecl[n]; + FuncDecl[] t = new FuncDecl[n]; for (int i = 0; i < n; i++) - t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i)); + t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i)); return t; } @@ -85,9 +87,9 @@ public FuncDecl[] getTesterDecls() * Retrieves the inx'th tester/recognizer declaration in the enumeration. * @throws Z3Exception on error **/ - public FuncDecl getTesterDecl(int inx) + public FuncDecl getTesterDecl(int inx) { - return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx)); + return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx)); } EnumSort(Context ctx, Symbol name, Symbol[] enumNames) diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index d1d554b54f1..f2f64efee2b 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -27,14 +27,15 @@ /** * Expressions are terms. **/ -public class Expr extends AST +@SuppressWarnings("unchecked") +public class Expr extends AST { /** * Returns a simplified version of the expression * @return Expr * @throws Z3Exception on error **/ - public Expr simplify() + public Expr simplify() { return simplify(null); } @@ -48,15 +49,15 @@ public Expr simplify() * @return an Expr * @throws Z3Exception on error **/ - public Expr simplify(Params p) + public Expr simplify(Params p) { if (p == null) { - return Expr.create(getContext(), + return (Expr) Expr.create(getContext(), Native.simplify(getContext().nCtx(), getNativeObject())); } else { - return Expr.create( + return (Expr) Expr.create( getContext(), Native.simplifyEx(getContext().nCtx(), getNativeObject(), p.getNativeObject())); @@ -69,9 +70,9 @@ public Expr simplify(Params p) * @return a FuncDecl * @throws Z3Exception on error **/ - public FuncDecl getFuncDecl() + public FuncDecl getFuncDecl() { - return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(), + return new FuncDecl<>(getContext(), Native.getAppDecl(getContext().nCtx(), getNativeObject())); } @@ -102,10 +103,10 @@ public int getNumArgs() * @throws Z3Exception on error * @return an Expr[] **/ - public Expr[] getArgs() + public Expr[] getArgs() { int n = getNumArgs(); - Expr[] res = new Expr[n]; + Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) { res[i] = Expr.create(getContext(), Native.getAppArg(getContext().nCtx(), getNativeObject(), i)); @@ -120,13 +121,13 @@ public Expr[] getArgs() * @param args arguments * @throws Z3Exception on error **/ - public Expr update(Expr[] args) + public Expr update(Expr[] args) { getContext().checkContextMatch(args); if (isApp() && args.length != getNumArgs()) { throw new Z3Exception("Number of arguments does not match"); } - return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(), + return (Expr) Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(), args.length, Expr.arrayToNative(args))); } @@ -142,14 +143,14 @@ public Expr update(Expr[] args) * @throws Z3Exception on error * @return an Expr **/ - public Expr substitute(Expr[] from, Expr[] to) + public Expr substitute(Expr[] from, Expr[] to) { getContext().checkContextMatch(from); getContext().checkContextMatch(to); if (from.length != to.length) { throw new Z3Exception("Argument sizes do not match"); } - return Expr.create(getContext(), Native.substitute(getContext().nCtx(), + return (Expr) Expr.create(getContext(), Native.substitute(getContext().nCtx(), getNativeObject(), from.length, Expr.arrayToNative(from), Expr.arrayToNative(to))); } @@ -161,7 +162,7 @@ public Expr substitute(Expr[] from, Expr[] to) * @throws Z3Exception on error * @return an Expr **/ - public Expr substitute(Expr from, Expr to) + public Expr substitute(Expr from, Expr to) { return substitute(new Expr[] { from }, new Expr[] { to }); } @@ -176,11 +177,11 @@ public Expr substitute(Expr from, Expr to) * @throws Z3Exception on error * @return an Expr **/ - public Expr substituteVars(Expr[] to) + public Expr substituteVars(Expr[] to) { getContext().checkContextMatch(to); - return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(), + return (Expr) Expr.create(getContext(), Native.substituteVars(getContext().nCtx(), getNativeObject(), to.length, Expr.arrayToNative(to))); } @@ -192,9 +193,9 @@ public Expr substituteVars(Expr[] to) * @return A copy of the term which is associated with {@code ctx} * @throws Z3Exception on error **/ - public Expr translate(Context ctx) + public Expr translate(Context ctx) { - return (Expr) super.translate(ctx); + return (Expr) super.translate(ctx); } /** @@ -232,9 +233,9 @@ public boolean isWellSorted() * @throws Z3Exception on error * @return a sort **/ - public Sort getSort() + public R getSort() { - return Sort.create(getContext(), + return (R) Sort.create(getContext(), Native.getSort(getContext().nCtx(), getNativeObject())); } @@ -1635,7 +1636,7 @@ public boolean isProofLemma() /** * Indicates whether the term is a proof by unit resolution - * Remarks: T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) * [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') + * Remarks: T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... R(n+1): (not l_n) * [unit-resolution T1 ... R(n+1)]: (or l_1' ... l_m') * @throws Z3Exception on error * @return a boolean **/ @@ -1770,8 +1771,8 @@ public boolean isProofIFFOEQ() * The negation normal form steps NNF_POS and NNF_NEG are used in the * following cases: (a) When creating the NNF of a positive force * quantifier. The quantifier is retained (unless the bound variables are - * eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x T) q) - * (forall (x T) q_new)) + * eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x R) q) + * (forall (x R) q_new)) * * (b) When recursively creating NNF over Boolean formulas, where the * top-level connective is changed during NNF conversion. The relevant @@ -2107,15 +2108,15 @@ void checkNativeObject(long obj) { super.checkNativeObject(obj); } - static Expr create(Context ctx, FuncDecl f, Expr ... arguments) - + static Expr create(Context ctx, FuncDecl f, Expr ... arguments) { long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(), AST.arrayLength(arguments), AST.arrayToNative(arguments)); - return create(ctx, obj); + return (Expr) create(ctx, obj); } - static Expr create(Context ctx, long obj) + // TODO generify, but it conflicts with AST.create + static Expr create(Context ctx, long obj) { Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)); if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) @@ -2143,7 +2144,7 @@ static Expr create(Context ctx, long obj) return new FPRMNum(ctx, obj); case Z3_FINITE_DOMAIN_SORT: return new FiniteDomainNum(ctx, obj); - default: ; + default: } } @@ -2158,9 +2159,9 @@ static Expr create(Context ctx, long obj) case Z3_BV_SORT: return new BitVecExpr(ctx, obj); case Z3_ARRAY_SORT: - return new ArrayExpr(ctx, obj); + return new ArrayExpr<>(ctx, obj); case Z3_DATATYPE_SORT: - return new DatatypeExpr(ctx, obj); + return new DatatypeExpr<>(ctx, obj); case Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj); case Z3_ROUNDING_MODE_SORT: @@ -2168,12 +2169,12 @@ static Expr create(Context ctx, long obj) case Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj); case Z3_SEQ_SORT: - return new SeqExpr(ctx, obj); + return new SeqExpr<>(ctx, obj); case Z3_RE_SORT: - return new ReExpr(ctx, obj); - default: ; + return new ReExpr<>(ctx, obj); + default: } - return new Expr(ctx, obj); + return new Expr<>(ctx, obj); } } diff --git a/src/api/java/FPExpr.java b/src/api/java/FPExpr.java index 8218f0f79a7..c348e642045 100644 --- a/src/api/java/FPExpr.java +++ b/src/api/java/FPExpr.java @@ -19,7 +19,7 @@ Christoph Wintersteiger (cwinter) 2013-06-10 /** * FloatingPoint Expressions */ -public class FPExpr extends Expr +public class FPExpr extends Expr { /** * The number of exponent bits. diff --git a/src/api/java/FPRMExpr.java b/src/api/java/FPRMExpr.java index 08db43b8aae..fd88c9a0ea7 100644 --- a/src/api/java/FPRMExpr.java +++ b/src/api/java/FPRMExpr.java @@ -19,7 +19,7 @@ Christoph Wintersteiger (cwinter) 2013-06-10 /** * FloatingPoint RoundingMode Expressions */ -public class FPRMExpr extends Expr +public class FPRMExpr extends Expr { public FPRMExpr(Context ctx, long obj) { diff --git a/src/api/java/FiniteDomainExpr.java b/src/api/java/FiniteDomainExpr.java index f7d9307583b..b3da5cf9dbe 100644 --- a/src/api/java/FiniteDomainExpr.java +++ b/src/api/java/FiniteDomainExpr.java @@ -20,7 +20,7 @@ /** * Finite-domain expressions **/ -public class FiniteDomainExpr extends Expr +public class FiniteDomainExpr extends Expr> { /** * Constructor for FiniteDomainExpr diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java index 68467e408ad..fec44017db8 100644 --- a/src/api/java/FiniteDomainNum.java +++ b/src/api/java/FiniteDomainNum.java @@ -22,7 +22,7 @@ /** * Finite-domain Numerals **/ -public class FiniteDomainNum extends FiniteDomainExpr +public class FiniteDomainNum extends FiniteDomainExpr { FiniteDomainNum(Context ctx, long obj) diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java index dcb52cd2211..ede57ac5493 100644 --- a/src/api/java/FiniteDomainSort.java +++ b/src/api/java/FiniteDomainSort.java @@ -20,7 +20,7 @@ /** * Finite domain sorts. **/ -public class FiniteDomainSort extends Sort +public class FiniteDomainSort extends Sort { /** * The size of the finite domain sort. diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 8560b6292a2..96e1dd0cb21 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -62,10 +62,11 @@ public ParamDescrs getParameterDescriptions() * * @throws Z3Exception **/ - public void add(BoolExpr ... constraints) + @SafeVarargs + public final void add(Expr... constraints) { getContext().checkContextMatch(constraints); - for (BoolExpr a : constraints) + for (Expr a : constraints) { Native.fixedpointAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject()); @@ -77,9 +78,8 @@ public void add(BoolExpr ... constraints) * * @throws Z3Exception **/ - public void registerRelation(FuncDecl f) + public void registerRelation(FuncDecl f) { - getContext().checkContextMatch(f); Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(), f.getNativeObject()); @@ -92,7 +92,7 @@ public void registerRelation(FuncDecl f) * @param name Nullable rule name. * @throws Z3Exception **/ - public void addRule(BoolExpr rule, Symbol name) { + public void addRule(Expr rule, Symbol name) { getContext().checkContextMatch(rule); Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(), rule.getNativeObject(), AST.getNativeObject(name)); @@ -103,7 +103,7 @@ public void addRule(BoolExpr rule, Symbol name) { * * @throws Z3Exception **/ - public void addFact(FuncDecl pred, int ... args) { + public void addFact(FuncDecl pred, int ... args) { getContext().checkContextMatch(pred); Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(), pred.getNativeObject(), args.length, args); @@ -118,7 +118,7 @@ public void addFact(FuncDecl pred, int ... args) { * * @throws Z3Exception **/ - public Status query(BoolExpr query) { + public Status query(Expr query) { getContext().checkContextMatch(query); Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(), getNativeObject(), query.getNativeObject())); @@ -141,7 +141,7 @@ public Status query(BoolExpr query) { * * @throws Z3Exception **/ - public Status query(FuncDecl[] relations) { + public Status query(FuncDecl[] relations) { getContext().checkContextMatch(relations); Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext() .nCtx(), getNativeObject(), AST.arrayLength(relations), AST @@ -164,7 +164,7 @@ public Status query(FuncDecl[] relations) { * @param name Nullable rule name. * @throws Z3Exception **/ - public void updateRule(BoolExpr rule, Symbol name) { + public void updateRule(Expr rule, Symbol name) { getContext().checkContextMatch(rule); Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(), rule.getNativeObject(), AST.getNativeObject(name)); @@ -176,7 +176,7 @@ public void updateRule(BoolExpr rule, Symbol name) { * * @throws Z3Exception **/ - public Expr getAnswer() + public Expr getAnswer() { long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject()); return (ans == 0) ? null : Expr.create(getContext(), ans); @@ -194,7 +194,7 @@ public String getReasonUnknown() /** * Retrieve the number of levels explored for a given predicate. **/ - public int getNumLevels(FuncDecl predicate) + public int getNumLevels(FuncDecl predicate) { return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(), predicate.getNativeObject()); @@ -205,7 +205,7 @@ public int getNumLevels(FuncDecl predicate) * * @throws Z3Exception **/ - public Expr getCoverDelta(int level, FuncDecl predicate) + public Expr getCoverDelta(int level, FuncDecl predicate) { long res = Native.fixedpointGetCoverDelta(getContext().nCtx(), getNativeObject(), level, predicate.getNativeObject()); @@ -216,7 +216,7 @@ public Expr getCoverDelta(int level, FuncDecl predicate) * Add property about the predicate. The property is added * at level. **/ - public void addCover(int level, FuncDecl predicate, Expr property) + public void addCover(int level, FuncDecl predicate, Expr property) { Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level, @@ -237,9 +237,8 @@ public String toString() * Instrument the Datalog engine on which table representation to use for * recursive predicate. **/ - public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) + public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) { - Native.fixedpointSetPredicateRepresentation(getContext().nCtx(), getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds), Symbol.arrayToNative(kinds)); @@ -249,9 +248,8 @@ public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) /** * Convert benchmark given as set of axioms, rules and queries to a string. **/ - public String toString(BoolExpr[] queries) + public String toString(Expr[] queries) { - return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), AST.arrayLength(queries), AST.arrayToNative(queries)); } diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 8a19427bf79..57517219962 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -24,7 +24,7 @@ /** * Function declarations. **/ -public class FuncDecl extends AST +public class FuncDecl extends AST { /** * Object comparison. @@ -34,7 +34,7 @@ public boolean equals(Object o) { if (o == this) return true; if (!(o instanceof FuncDecl)) return false; - FuncDecl other = (FuncDecl) o; + FuncDecl other = (FuncDecl) o; return (getContext().nCtx() == other.getContext().nCtx()) && @@ -66,9 +66,10 @@ public int getId() * @return A copy of the function declaration which is associated with {@code ctx} * @throws Z3Exception on error **/ - public FuncDecl translate(Context ctx) + @SuppressWarnings("unchecked") + public FuncDecl translate(Context ctx) { - return (FuncDecl) super.translate(ctx); + return (FuncDecl) super.translate(ctx); } /** @@ -106,10 +107,10 @@ public Sort[] getDomain() /** * The range of the function declaration **/ - public Sort getRange() + @SuppressWarnings("unchecked") + public R getRange() { - - return Sort.create(getContext(), + return (R) Sort.create(getContext(), Native.getRange(getContext().nCtx(), getNativeObject())); } @@ -178,7 +179,7 @@ public Parameter[] getParameters() getNativeObject(), i))); break; case Z3_PARAMETER_FUNC_DECL: - res[i] = new Parameter(k, new FuncDecl(getContext(), + res[i] = new Parameter(k, new FuncDecl<>(getContext(), Native.getDeclFuncDeclParameter(getContext().nCtx(), getNativeObject(), i))); break; @@ -197,7 +198,7 @@ public Parameter[] getParameters() /** * Function declarations can have Parameters associated with them. **/ - public class Parameter + public static class Parameter { private Z3_parameter_kind kind; private int i; @@ -205,7 +206,7 @@ public class Parameter private Symbol sym; private Sort srt; private AST ast; - private FuncDecl fd; + private FuncDecl fd; private String r; /** @@ -261,7 +262,7 @@ public AST getAST() /** * The FunctionDeclaration value of the parameter. **/ - public FuncDecl getFuncDecl() + public FuncDecl getFuncDecl() { if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); @@ -316,7 +317,7 @@ public Z3_parameter_kind getParameterKind() this.ast = a; } - Parameter(Z3_parameter_kind k, FuncDecl fd) + Parameter(Z3_parameter_kind k, FuncDecl fd) { this.kind = k; this.fd = fd; @@ -335,14 +336,14 @@ public Z3_parameter_kind getParameterKind() } - FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) + FuncDecl(Context ctx, Symbol name, Sort[] domain, R range) { super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(), AST.arrayLength(domain), AST.arrayToNative(domain), range.getNativeObject())); } - FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range, boolean is_rec) + FuncDecl(Context ctx, Symbol name, Sort[] domain, R range, boolean is_rec) { super(ctx, Native.mkRecFuncDecl(ctx.nCtx(), name.getNativeObject(), AST.arrayLength(domain), AST.arrayToNative(domain), @@ -350,8 +351,7 @@ public Z3_parameter_kind getParameterKind() } - FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) - + FuncDecl(Context ctx, String prefix, Sort[] domain, R range) { super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, AST.arrayLength(domain), AST.arrayToNative(domain), @@ -371,7 +371,7 @@ void checkNativeObject(long obj) /** * Create expression that applies function to arguments. **/ - public Expr apply(Expr ... args) + public Expr apply(Expr ... args) { getContext().checkContextMatch(args); return Expr.create(getContext(), this, args); diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index b5873d98e9e..64f96534b05 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -22,13 +22,14 @@ * Each entry in the finite map represents the value of a function given a set * of arguments. **/ -public class FuncInterp extends Z3Object { +@SuppressWarnings("unchecked") +public class FuncInterp extends Z3Object { /** * An Entry object represents an element in the finite map used to encode a * function interpretation. **/ - public static class Entry extends Z3Object { + public static class Entry extends Z3Object { /** * Return the (symbolic) value of this entry. @@ -36,9 +37,9 @@ public static class Entry extends Z3Object { * @throws Z3Exception * @throws Z3Exception on error **/ - public Expr getValue() + public Expr getValue() { - return Expr.create(getContext(), + return (Expr) Expr.create(getContext(), Native.funcEntryGetValue(getContext().nCtx(), getNativeObject())); } @@ -57,10 +58,10 @@ public int getNumArgs() * @throws Z3Exception * @throws Z3Exception on error **/ - public Expr[] getArgs() + public Expr[] getArgs() { int n = getNumArgs(); - Expr[] res = new Expr[n]; + Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) res[i] = Expr.create(getContext(), Native.funcEntryGetArg( getContext().nCtx(), getNativeObject(), i)); @@ -75,7 +76,7 @@ public String toString() { int n = getNumArgs(); String res = "["; - Expr[] args = getArgs(); + Expr[] args = getArgs(); for (int i = 0; i < n; i++) res += args[i] + ", "; return res + getValue() + "]"; @@ -112,12 +113,12 @@ public int getNumEntries() * @throws Z3Exception * @throws Z3Exception on error **/ - public Entry[] getEntries() + public Entry[] getEntries() { int n = getNumEntries(); - Entry[] res = new Entry[n]; + Entry[] res = new Entry[n]; for (int i = 0; i < n; i++) - res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext() + res[i] = new Entry<>(getContext(), Native.funcInterpGetEntry(getContext() .nCtx(), getNativeObject(), i)); return res; } @@ -129,9 +130,9 @@ public Entry[] getEntries() * @throws Z3Exception on error * @return an Expr **/ - public Expr getElse() + public Expr getElse() { - return Expr.create(getContext(), + return (Expr) Expr.create(getContext(), Native.funcInterpGetElse(getContext().nCtx(), getNativeObject())); } @@ -152,12 +153,12 @@ public String toString() { String res = ""; res += "["; - for (Entry e : getEntries()) + for (Entry e : getEntries()) { int n = e.getNumArgs(); if (n > 1) res += "["; - Expr[] args = e.getArgs(); + Expr[] args = e.getArgs(); for (int i = 0; i < n; i++) { if (i != 0) diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java index d8715bd0eb6..06a6f2af851 100644 --- a/src/api/java/FuncInterpDecRefQueue.java +++ b/src/api/java/FuncInterpDecRefQueue.java @@ -17,7 +17,7 @@ package com.microsoft.z3; -class FuncInterpDecRefQueue extends IDecRefQueue +class FuncInterpDecRefQueue extends IDecRefQueue> { public FuncInterpDecRefQueue() { diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java index a4d8a069040..77bb78f5b6c 100644 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ b/src/api/java/FuncInterpEntryDecRefQueue.java @@ -17,7 +17,7 @@ package com.microsoft.z3; -class FuncInterpEntryDecRefQueue extends IDecRefQueue { +class FuncInterpEntryDecRefQueue extends IDecRefQueue> { public FuncInterpEntryDecRefQueue() { super(); diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index f5fa35fdb5a..3326f81fe02 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -76,10 +76,11 @@ public boolean isGarbage() * * @throws Z3Exception **/ - public void add(BoolExpr ... constraints) + @SafeVarargs + public final void add(Expr... constraints) { getContext().checkContextMatch(constraints); - for (BoolExpr c : constraints) + for (Expr c : constraints) { Native.goalAssert(getContext().nCtx(), getNativeObject(), c.getNativeObject()); diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java index 56ba9ccdf52..77e41302034 100644 --- a/src/api/java/IntExpr.java +++ b/src/api/java/IntExpr.java @@ -20,7 +20,7 @@ /** * Int expressions **/ -public class IntExpr extends ArithExpr +public class IntExpr extends ArithExpr { /** * Constructor for IntExpr diff --git a/src/api/java/Lambda.java b/src/api/java/Lambda.java index cf9809a239e..780e543c863 100644 --- a/src/api/java/Lambda.java +++ b/src/api/java/Lambda.java @@ -19,12 +19,11 @@ Christoph Wintersteiger (cwinter) 2012-03-19 package com.microsoft.z3; -import com.microsoft.z3.enumerations.Z3_ast_kind; - /** * Lambda expressions. -*/public class Lambda extends ArrayExpr +*/ +public class Lambda extends ArrayExpr { /** @@ -70,9 +69,10 @@ public Sort[] getBoundVariableSorts() * * @throws Z3Exception **/ - public Expr getBody() + @SuppressWarnings("unchecked") + public Expr getBody() { - return Expr.create(getContext(), Native.getQuantifierBody(getContext() + return (Expr) Expr.create(getContext(), Native.getQuantifierBody(getContext() .nCtx(), getNativeObject())); } @@ -81,17 +81,17 @@ public Expr getBody() * Translates (copies) the quantifier to the Context {@code ctx}. * * @param ctx A context - * + * * @return A copy of the quantifier which is associated with {@code ctx} * @throws Z3Exception on error **/ - public Lambda translate(Context ctx) + public Lambda translate(Context ctx) { - return (Lambda) super.translate(ctx); + return (Lambda) super.translate(ctx); } - public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body) + public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body) { ctx.checkContextMatch(sorts); ctx.checkContextMatch(names); @@ -106,7 +106,7 @@ public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body) Symbol.arrayToNative(names), body.getNativeObject()); - return new Lambda(ctx, nativeObject); + return new Lambda<>(ctx, nativeObject); } /** @@ -115,14 +115,14 @@ public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body) * @param body Body of the lambda expression. */ - public static Lambda of(Context ctx, Expr[] bound, Expr body) { + public static Lambda of(Context ctx, Expr[] bound, Expr body) { ctx.checkContextMatch(body); long nativeObject = Native.mkLambdaConst(ctx.nCtx(), AST.arrayLength(bound), AST.arrayToNative(bound), body.getNativeObject()); - return new Lambda(ctx, nativeObject); + return new Lambda<>(ctx, nativeObject); } diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java index 0ff2c36cf5e..8b7582791b9 100644 --- a/src/api/java/ListSort.java +++ b/src/api/java/ListSort.java @@ -22,22 +22,22 @@ /** * List sorts. **/ -public class ListSort extends Sort +public class ListSort extends Sort { /** * The declaration of the nil function of this list sort. * @throws Z3Exception **/ - public FuncDecl getNilDecl() + public FuncDecl> getNilDecl() { - return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0)); + return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0)); } /** * The empty list. * @throws Z3Exception **/ - public Expr getNil() + public Expr> getNil() { return getContext().mkApp(getNilDecl()); } @@ -46,18 +46,18 @@ public Expr getNil() * The declaration of the isNil function of this list sort. * @throws Z3Exception **/ - public FuncDecl getIsNilDecl() + public FuncDecl getIsNilDecl() { - return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0)); + return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0)); } /** * The declaration of the cons function of this list sort. * @throws Z3Exception **/ - public FuncDecl getConsDecl() + public FuncDecl> getConsDecl() { - return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1)); + return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1)); } /** @@ -65,27 +65,27 @@ public FuncDecl getConsDecl() * @throws Z3Exception * **/ - public FuncDecl getIsConsDecl() + public FuncDecl getIsConsDecl() { - return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1)); + return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1)); } /** * The declaration of the head function of this list sort. * @throws Z3Exception **/ - public FuncDecl getHeadDecl() + public FuncDecl getHeadDecl() { - return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0)); + return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0)); } /** * The declaration of the tail function of this list sort. * @throws Z3Exception **/ - public FuncDecl getTailDecl() + public FuncDecl> getTailDecl() { - return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1)); + return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1)); } ListSort(Context ctx, Symbol name, Sort elemSort) diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 4c9abef7a4b..032745fc5f7 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -22,17 +22,18 @@ /** * A Model contains interpretations (assignments) of constants and functions. **/ +@SuppressWarnings("unchecked") public class Model extends Z3Object { /** * Retrieves the interpretation (the assignment) of {@code a} in * the model. * @param a A Constant - * + * * @return An expression if the constant has an interpretation in the model, * null otherwise. * @throws Z3Exception **/ - public Expr getConstInterp(Expr a) + public Expr getConstInterp(Expr a) { getContext().checkContextMatch(a); return getConstInterp(a.getFuncDecl()); @@ -47,7 +48,7 @@ public Expr getConstInterp(Expr a) * null otherwise. * @throws Z3Exception **/ - public Expr getConstInterp(FuncDecl f) + public Expr getConstInterp(FuncDecl f) { getContext().checkContextMatch(f); if (f.getArity() != 0) @@ -59,7 +60,7 @@ public Expr getConstInterp(FuncDecl f) if (n == 0) return null; else - return Expr.create(getContext(), n); + return (Expr) Expr.create(getContext(), n); } /** @@ -70,7 +71,7 @@ public Expr getConstInterp(FuncDecl f) * the model, null otherwise. * @throws Z3Exception **/ - public FuncInterp getFuncInterp(FuncDecl f) + public FuncInterp getFuncInterp(FuncDecl f) { getContext().checkContextMatch(f); @@ -90,7 +91,7 @@ public FuncInterp getFuncInterp(FuncDecl f) { if (Native.isAsArray(getContext().nCtx(), n)) { long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n); - return getFuncInterp(new FuncDecl(getContext(), fd)); + return getFuncInterp(new FuncDecl<>(getContext(), fd)); } return null; } @@ -106,7 +107,7 @@ public FuncInterp getFuncInterp(FuncDecl f) if (n == 0) return null; else - return new FuncInterp(getContext(), n); + return new FuncInterp<>(getContext(), n); } } @@ -123,12 +124,12 @@ public int getNumConsts() * * @throws Z3Exception **/ - public FuncDecl[] getConstDecls() + public FuncDecl[] getConstDecls() { int n = getNumConsts(); - FuncDecl[] res = new FuncDecl[n]; + FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) - res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext() + res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext() .nCtx(), getNativeObject(), i)); return res; } @@ -146,12 +147,12 @@ public int getNumFuncs() * * @throws Z3Exception **/ - public FuncDecl[] getFuncDecls() + public FuncDecl[] getFuncDecls() { int n = getNumFuncs(); - FuncDecl[] res = new FuncDecl[n]; + FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) - res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext() + res[i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(getContext() .nCtx(), getNativeObject(), i)); return res; } @@ -161,17 +162,17 @@ public FuncDecl[] getFuncDecls() * * @throws Z3Exception **/ - public FuncDecl[] getDecls() + public FuncDecl[] getDecls() { int nFuncs = getNumFuncs(); int nConsts = getNumConsts(); int n = nFuncs + nConsts; - FuncDecl[] res = new FuncDecl[n]; + FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < nConsts; i++) - res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext() + res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext() .nCtx(), getNativeObject(), i)); for (int i = 0; i < nFuncs; i++) - res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl( + res[nConsts + i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl( getContext().nCtx(), getNativeObject(), i)); return res; } @@ -205,14 +206,14 @@ public ModelEvaluationFailedException() * @return The evaluation of {@code t} in the model. * @throws Z3Exception **/ - public Expr eval(Expr t, boolean completion) + public Expr eval(Expr t, boolean completion) { Native.LongPtr v = new Native.LongPtr(); if (!Native.modelEval(getContext().nCtx(), getNativeObject(), t.getNativeObject(), (completion), v)) throw new ModelEvaluationFailedException(); else - return Expr.create(getContext(), v.value); + return (Expr) Expr.create(getContext(), v.value); } /** @@ -220,7 +221,7 @@ public Expr eval(Expr t, boolean completion) * * @throws Z3Exception **/ - public Expr evaluate(Expr t, boolean completion) + public Expr evaluate(Expr t, boolean completion) { return eval(t, completion); } @@ -265,12 +266,12 @@ public Sort[] getSorts() * of {@code s} * @throws Z3Exception **/ - public Expr[] getSortUniverse(Sort s) + public Expr[] getSortUniverse(R s) { ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse( getContext().nCtx(), getNativeObject(), s.getNativeObject())); - return nUniv.ToExprArray(); + return (Expr[]) nUniv.ToExprArray(); } /** diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index ae50d7f33b0..741dd08d99d 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -24,6 +24,7 @@ Nikolaj Bjorner (nbjorner) 2015-07-16 /** * Object for managing optimization context **/ +@SuppressWarnings("unchecked") public class Optimize extends Z3Object { /** @@ -55,10 +56,10 @@ public ParamDescrs getParameterDescriptions() /** * Assert a constraint (or multiple) into the optimize solver. **/ - public void Assert(BoolExpr ... constraints) + public void Assert(Expr ... constraints) { getContext().checkContextMatch(constraints); - for (BoolExpr a : constraints) + for (Expr a : constraints) { Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject()); } @@ -67,7 +68,7 @@ public void Assert(BoolExpr ... constraints) /** * Alias for Assert. **/ - public void Add(BoolExpr ... constraints) + public void Add(Expr ... constraints) { Assert(constraints); } @@ -75,7 +76,7 @@ public void Add(BoolExpr ... constraints) /** * Handle to objectives returned by objective functions. **/ - public static class Handle { + public static class Handle { private final Optimize opt; private final int handle; @@ -89,7 +90,7 @@ public static class Handle { /** * Retrieve a lower bound for the objective handle. **/ - public Expr getLower() + public Expr getLower() { return opt.GetLower(handle); } @@ -97,7 +98,7 @@ public Expr getLower() /** * Retrieve an upper bound for the objective handle. **/ - public Expr getUpper() + public Expr getUpper() { return opt.GetUpper(handle); } @@ -110,7 +111,7 @@ public Expr getUpper() * and otherwise is represented by the expression {@code value + eps * EPSILON}, * where {@code EPSILON} is an arbitrarily small real number. */ - public Expr[] getUpperAsVector() + public Expr[] getUpperAsVector() { return opt.GetUpperAsVector(handle); } @@ -120,7 +121,7 @@ public Expr[] getUpperAsVector() * *

See {@link #getUpperAsVector()} for triple semantics. */ - public Expr[] getLowerAsVector() + public Expr[] getLowerAsVector() { return opt.GetLowerAsVector(handle); } @@ -128,7 +129,7 @@ public Expr[] getLowerAsVector() /** * Retrieve the value of an objective. **/ - public Expr getValue() + public Expr getValue() { return getLower(); } @@ -149,11 +150,11 @@ public String toString() * Return an objective which associates with the group of constraints. * **/ - public Handle AssertSoft(BoolExpr constraint, int weight, String group) + public Handle AssertSoft(Expr constraint, int weight, String group) { getContext().checkContextMatch(constraint); Symbol s = getContext().mkSymbol(group); - return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject())); + return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject())); } /** @@ -161,7 +162,7 @@ public Handle AssertSoft(BoolExpr constraint, int weight, String group) * Produce a model that (when the objectives are bounded and * don't use strict inequalities) meets the objectives. **/ - public Status Check(Expr... assumptions) + public Status Check(Expr... assumptions) { Z3_lbool r; if (assumptions == null) { @@ -243,34 +244,34 @@ public BoolExpr[] getUnsatCore() * Return a handle to the objective. The handle is used as * to retrieve the values of objectives after calling Check. **/ - public Handle MkMaximize(Expr e) + public Handle MkMaximize(Expr e) { - return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); + return new Handle<>(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); } /** * Declare an arithmetical minimization objective. * Similar to MkMaximize. **/ - public Handle MkMinimize(Expr e) + public Handle MkMinimize(Expr e) { - return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); + return new Handle<>(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); } /** * Retrieve a lower bound for the objective handle. **/ - private Expr GetLower(int index) + private Expr GetLower(int index) { - return Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index)); + return (Expr) Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index)); } /** * Retrieve an upper bound for the objective handle. **/ - private Expr GetUpper(int index) + private Expr GetUpper(int index) { - return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index)); + return (Expr) Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index)); } /** @@ -278,7 +279,7 @@ private Expr GetUpper(int index) * *

See {@link Handle#getUpperAsVector}. */ - private Expr[] GetUpperAsVector(int index) { + private Expr[] GetUpperAsVector(int index) { return unpackObjectiveValueVector( Native.optimizeGetUpperAsVector( getContext().nCtx(), getNativeObject(), index @@ -291,7 +292,7 @@ private Expr[] GetUpperAsVector(int index) { * *

See {@link Handle#getLowerAsVector}. */ - private Expr[] GetLowerAsVector(int index) { + private Expr[] GetLowerAsVector(int index) { return unpackObjectiveValueVector( Native.optimizeGetLowerAsVector( getContext().nCtx(), getNativeObject(), index @@ -299,12 +300,12 @@ private Expr[] GetLowerAsVector(int index) { ); } - private Expr[] unpackObjectiveValueVector(long nativeVec) { + private Expr[] unpackObjectiveValueVector(long nativeVec) { ASTVector vec = new ASTVector( getContext(), nativeVec ); return new Expr[] { - (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2) + (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2) }; } @@ -355,7 +356,7 @@ public BoolExpr[] getAssertions() /** * The set of asserted formulas. */ - public Expr[] getObjectives() + public Expr[] getObjectives() { ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject())); return objectives.ToExprArray(); diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java index 852ffcd0f53..ae29d8b7d83 100644 --- a/src/api/java/Pattern.java +++ b/src/api/java/Pattern.java @@ -36,11 +36,11 @@ public int getNumTerms() * * @throws Z3Exception **/ - public Expr[] getTerms() + public Expr[] getTerms() { int n = getNumTerms(); - Expr[] res = new Expr[n]; + Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) res[i] = Expr.create(getContext(), Native.getPattern(getContext().nCtx(), getNativeObject(), i)); diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 6b2f1d4fcc1..89ff61a3dc0 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -139,9 +139,9 @@ public Sort[] getBoundVariableSorts() * * @throws Z3Exception **/ - public Expr getBody() + public BoolExpr getBody() { - return Expr.create(getContext(), Native.getQuantifierBody(getContext() + return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext() .nCtx(), getNativeObject())); } @@ -168,7 +168,7 @@ public Quantifier translate(Context ctx) */ public static Quantifier of( Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, - Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, + Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { ctx.checkContextMatch(patterns); ctx.checkContextMatch(noPatterns); @@ -212,8 +212,8 @@ public static Quantifier of( * @param quantifierID Nullable quantifier identifier. * @param skolemID Nullable skolem identifier. */ - public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body, - int weight, Pattern[] patterns, Expr[] noPatterns, + public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body, + int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { ctx.checkContextMatch(noPatterns); ctx.checkContextMatch(patterns); diff --git a/src/api/java/ReExpr.java b/src/api/java/ReExpr.java index 60dc2bf96f3..fa3d85b542e 100644 --- a/src/api/java/ReExpr.java +++ b/src/api/java/ReExpr.java @@ -20,7 +20,7 @@ /** * Re expressions **/ -public class ReExpr extends Expr +public class ReExpr extends Expr> { /** * Constructor for ReExpr diff --git a/src/api/java/ReSort.java b/src/api/java/ReSort.java index 74e7c5c5fde..250eb42522c 100644 --- a/src/api/java/ReSort.java +++ b/src/api/java/ReSort.java @@ -20,7 +20,7 @@ /** * A Regular expression sort **/ -public class ReSort extends Sort +public class ReSort extends Sort { ReSort(Context ctx, long obj) { diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java index c977e2ac0e0..cae9865a599 100644 --- a/src/api/java/RealExpr.java +++ b/src/api/java/RealExpr.java @@ -20,7 +20,7 @@ /** * Real expressions **/ -public class RealExpr extends ArithExpr +public class RealExpr extends ArithExpr { /** * Constructor for RealExpr diff --git a/src/api/java/SeqExpr.java b/src/api/java/SeqExpr.java index 47976dd5eb1..56980856059 100644 --- a/src/api/java/SeqExpr.java +++ b/src/api/java/SeqExpr.java @@ -20,7 +20,7 @@ /** * Seq expressions **/ -public class SeqExpr extends Expr +public class SeqExpr extends Expr> { /** * Constructor for SeqExpr diff --git a/src/api/java/SeqSort.java b/src/api/java/SeqSort.java index 5c7a549c910..28b865733a9 100644 --- a/src/api/java/SeqSort.java +++ b/src/api/java/SeqSort.java @@ -20,7 +20,7 @@ /** * A Sequence sort **/ -public class SeqSort extends Sort +public class SeqSort extends Sort { SeqSort(Context ctx, long obj) { diff --git a/src/api/java/SetSort.java b/src/api/java/SetSort.java index 2aa821250e0..bb89a735060 100644 --- a/src/api/java/SetSort.java +++ b/src/api/java/SetSort.java @@ -20,14 +20,14 @@ /** * Set sorts. **/ -public class SetSort extends Sort +public class SetSort extends ArraySort { SetSort(Context ctx, long obj) { super(ctx, obj); } - SetSort(Context ctx, Sort ty) + SetSort(Context ctx, D ty) { super(ctx, Native.mkSetSort(ctx.nCtx(), ty.getNativeObject())); } diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 7711adb3633..ce795d75833 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -24,6 +24,7 @@ /** * Solvers. **/ +@SuppressWarnings("unchecked") public class Solver extends Z3Object { /** * A string that describes all available solver parameters. @@ -122,10 +123,10 @@ public void interrupt() * * @throws Z3Exception **/ - public void add(BoolExpr... constraints) + public void add(Expr... constraints) { getContext().checkContextMatch(constraints); - for (BoolExpr a : constraints) + for (Expr a : constraints) { Native.solverAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject()); @@ -147,7 +148,7 @@ public void add(BoolExpr... constraints) * and the Boolean literals * provided using {@link #check()} with assumptions. **/ - public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) + public void assertAndTrack(Expr[] constraints, Expr[] ps) { getContext().checkContextMatch(constraints); getContext().checkContextMatch(ps); @@ -174,7 +175,7 @@ public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) * and the Boolean literals * provided using {@link #check} with assumptions. */ - public void assertAndTrack(BoolExpr constraint, BoolExpr p) + public void assertAndTrack(Expr constraint, Expr p) { getContext().checkContextMatch(constraint); getContext().checkContextMatch(p); @@ -229,7 +230,8 @@ public BoolExpr[] getAssertions() * @see #getUnsatCore * @see #getProof **/ - public Status check(Expr... assumptions) + @SafeVarargs + public final Status check(Expr... assumptions) { Z3_lbool r; if (assumptions == null) { @@ -250,6 +252,7 @@ public Status check(Expr... assumptions) * @see #getUnsatCore * @see #getProof **/ + @SuppressWarnings("rawtypes") public Status check() { return check((Expr[]) null); @@ -266,13 +269,13 @@ public Status check() * is fixed. * */ - public Status getConsequences(BoolExpr[] assumptions, Expr[] variables, List consequences) + public Status getConsequences(Expr[] assumptions, Expr[] variables, List> consequences) { ASTVector result = new ASTVector(getContext()); ASTVector asms = new ASTVector(getContext()); ASTVector vars = new ASTVector(getContext()); - for (BoolExpr asm : assumptions) asms.push(asm); - for (Expr v : variables) vars.push(v); + for (Expr asm : assumptions) asms.push(asm); + for (Expr v : variables) vars.push(v); int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject()); for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject())); return lboolToStatus(Z3_lbool.fromInt(r)); @@ -307,7 +310,7 @@ public Model getModel() * * @throws Z3Exception **/ - public Expr getProof() + public Expr getProof() { long x = Native.solverGetProof(getContext().nCtx(), getNativeObject()); if (x == 0) { diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index a8941705910..f612b9031c9 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -119,13 +119,13 @@ static Sort create(Context ctx, long obj) switch (sk) { case Z3_ARRAY_SORT: - return new ArraySort(ctx, obj); + return new ArraySort<>(ctx, obj); case Z3_BOOL_SORT: return new BoolSort(ctx, obj); case Z3_BV_SORT: return new BitVecSort(ctx, obj); case Z3_DATATYPE_SORT: - return new DatatypeSort(ctx, obj); + return new DatatypeSort<>(ctx, obj); case Z3_INT_SORT: return new IntSort(ctx, obj); case Z3_REAL_SORT: @@ -141,9 +141,9 @@ static Sort create(Context ctx, long obj) case Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj); case Z3_SEQ_SORT: - return new SeqSort(ctx, obj); + return new SeqSort<>(ctx, obj); case Z3_RE_SORT: - return new ReSort(ctx, obj); + return new ReSort<>(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); } diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java index ede20d26055..3b600f0fac1 100644 --- a/src/api/java/TupleSort.java +++ b/src/api/java/TupleSort.java @@ -26,10 +26,10 @@ public class TupleSort extends Sort * The constructor function of the tuple. * @throws Z3Exception **/ - public FuncDecl mkDecl() + public FuncDecl mkDecl() { - return new FuncDecl(getContext(), Native.getTupleSortMkDecl(getContext() + return new FuncDecl<>(getContext(), Native.getTupleSortMkDecl(getContext() .nCtx(), getNativeObject())); } @@ -45,13 +45,13 @@ public int getNumFields() * The field declarations. * @throws Z3Exception **/ - public FuncDecl[] getFieldDecls() + public FuncDecl[] getFieldDecls() { int n = getNumFields(); - FuncDecl[] res = new FuncDecl[n]; + FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) - res[i] = new FuncDecl(getContext(), Native.getTupleSortFieldDecl( + res[i] = new FuncDecl<>(getContext(), Native.getTupleSortFieldDecl( getContext().nCtx(), getNativeObject(), i)); return res; }