From 5fe58c2f2db10b864b21f53df1b9bbbda0d1d6a0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 26 Feb 2013 19:13:48 +0000 Subject: [PATCH] Java API: renamed assert_(...) to add(...) .NET API: added alias Add(...) for Assert(...) Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 80 +++++++++++++++++----------------- src/api/dotnet/Fixedpoint.cs | 8 ++++ src/api/dotnet/Goal.cs | 8 ++++ src/api/dotnet/Solver.cs | 8 ++++ src/api/java/Fixedpoint.java | 2 +- src/api/java/Goal.java | 2 +- src/api/java/Solver.java | 2 +- 7 files changed, 67 insertions(+), 43 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index c2743ece8..48395d8c2 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -197,7 +197,7 @@ class JavaExample TestFailedException { Solver s = ctx.mkSolver(); - s.assert_(f); + s.add(f); if (s.check() != sat) throw new TestFailedException(); if (sat == Status.SATISFIABLE) @@ -213,7 +213,7 @@ class JavaExample System.out.println("\nTactical solver: " + s); for (BoolExpr a : g.getFormulas()) - s.assert_(a); + s.add(a); System.out.println("Solver: " + s); if (s.check() != sat) @@ -266,8 +266,8 @@ class JavaExample p.add("mbqi", useMBQI); s.setParameters(p); for (BoolExpr a : assumptions) - s.assert_(a); - s.assert_(ctx.mkNot(f)); + s.add(a); + s.add(ctx.mkNot(f)); Status q = s.check(); switch (q) @@ -299,8 +299,8 @@ class JavaExample p.add("mbqi", useMBQI); s.setParameters(p); for (BoolExpr a : assumptions) - s.assert_(a); - s.assert_(ctx.mkNot(f)); + s.add(a); + s.add(ctx.mkNot(f)); Status q = s.check(); switch (q) @@ -326,9 +326,9 @@ class JavaExample ArithExpr yr = (ArithExpr) ctx.mkConst(ctx.mkSymbol("y"), ctx.mkRealSort()); Goal g4 = ctx.mkGoal(true, false, false); - g4.assert_(ctx.mkGt(xr, ctx.mkReal(10, 1))); - g4.assert_(ctx.mkEq(yr, ctx.mkAdd(xr, ctx.mkReal(1, 1)))); - g4.assert_(ctx.mkGt(yr, ctx.mkReal(1, 1))); + 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 @@ -345,7 +345,7 @@ class JavaExample Solver s = ctx.mkSolver(); for (BoolExpr e : ar.getSubgoals()[0].getFormulas()) - s.assert_(e); + s.add(e); Status q = s.check(); System.out.println("Solver says: " + q); System.out.println("Model: \n" + s.getModel()); @@ -367,7 +367,7 @@ class JavaExample ctx.mkBitVecSort(32)); ArrayExpr aex = (ArrayExpr) ctx.mkConst(ctx.mkSymbol("MyArray"), asort); Expr sel = ctx.mkSelect(aex, ctx.mkInt(0)); - g.assert_(ctx.mkEq(sel, ctx.mkBV(42, 32))); + g.add(ctx.mkEq(sel, ctx.mkBV(42, 32))); Symbol xs = ctx.mkSymbol("x"); IntExpr xc = (IntExpr) ctx.mkConst(xs, ctx.getIntSort()); @@ -377,11 +377,11 @@ class JavaExample Expr[] fargs = { ctx.mkConst(xs, ctx.getIntSort()) }; IntExpr fapp = (IntExpr) ctx.mkApp(fd, fargs); - g.assert_(ctx.mkEq(ctx.mkAdd(xc, fapp), ctx.mkInt(123))); + g.add(ctx.mkEq(ctx.mkAdd(xc, fapp), ctx.mkInt(123))); Solver s = ctx.mkSolver(); for (BoolExpr a : g.getFormulas()) - s.assert_(a); + s.add(a); System.out.println("Solver: " + s); Status q = s.check(); @@ -574,8 +574,8 @@ class JavaExample ctx.mkEq(X[i][j], ctx.mkInt(instance[i][j])))); Solver s = ctx.mkSolver(); - s.assert_(sudoku_c); - s.assert_(instance_c); + s.add(sudoku_c); + s.add(instance_c); if (s.check() == Status.SATISFIABLE) { @@ -798,14 +798,14 @@ class JavaExample BoolExpr nontrivial_eq = ctx.mkEq(fapp, fapp2); Goal g = ctx.mkGoal(true, false, false); - g.assert_(trivial_eq); - g.assert_(nontrivial_eq); + g.add(trivial_eq); + g.add(nontrivial_eq); System.out.println("Goal: " + g); Solver solver = ctx.mkSolver(); for (BoolExpr a : g.getFormulas()) - solver.assert_(a); + solver.add(a); if (solver.check() != Status.SATISFIABLE) throw new TestFailedException(); @@ -820,7 +820,7 @@ class JavaExample if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat()) throw new TestFailedException(); - g.assert_(ctx.mkEq(ctx.mkNumeral(1, ctx.mkBitVecSort(32)), + 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()) @@ -832,7 +832,7 @@ class JavaExample throw new TestFailedException(); g2 = ctx.mkGoal(true, true, false); - g2.assert_(ctx.mkFalse()); + g2.add(ctx.mkFalse()); ar = applyTactic(ctx, ctx.mkTactic("smt"), g2); if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat()) throw new TestFailedException(); @@ -840,10 +840,10 @@ class JavaExample 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.assert_(ctx.mkEq(xc, ctx.mkNumeral(1, ctx.getIntSort()))); - g3.assert_(ctx.mkEq(yc, ctx.mkNumeral(2, 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.assert_(constr); + g3.add(constr); ar = applyTactic(ctx, ctx.mkTactic("smt"), g3); if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat()) throw new TestFailedException(); @@ -1110,13 +1110,13 @@ class JavaExample // Use a solver for QF_BV Solver s = ctx.mkSolver("QF_BV"); - s.assert_(eq); + s.add(eq); Status res = s.check(); System.out.println("solver result: " + res); // Or perhaps a tactic for QF_BV Goal g = ctx.mkGoal(true, false, false); - g.assert_(eq); + g.add(eq); Tactic t = ctx.mkTactic("qfbv"); ApplyResult ar = t.apply(g); @@ -1139,7 +1139,7 @@ class JavaExample BoolExpr q = ctx.mkEq(x, y); Goal g = ctx.mkGoal(true, false, false); - g.assert_(q); + g.add(q); Tactic t1 = ctx.mkTactic("qfbv"); Tactic t2 = ctx.mkTactic("qfbv"); @@ -1341,7 +1341,7 @@ class JavaExample /* assert x >= "big number" */ BoolExpr c1 = ctx.mkGe(x, big_number); System.out.println("assert: x >= 'big number'"); - solver.assert_(c1); + solver.add(c1); /* create a backtracking point */ System.out.println("push"); @@ -1350,7 +1350,7 @@ class JavaExample /* assert x <= 3 */ BoolExpr c2 = ctx.mkLe(x, three); System.out.println("assert: x <= 3"); - solver.assert_(c2); + solver.add(c2); /* context is inconsistent at this point */ if (solver.check() != Status.UNSATISFIABLE) @@ -1375,7 +1375,7 @@ class JavaExample /* assert y > x */ BoolExpr c3 = ctx.mkGt(y, x); System.out.println("assert: y > x"); - solver.assert_(c3); + solver.add(c3); /* the context is still consistent. */ if (solver.check() != Status.SATISFIABLE) @@ -1911,10 +1911,10 @@ class JavaExample Solver solver = ctx.mkSolver(); /* assert x < y */ - solver.assert_(ctx.mkLt(x, y)); + solver.add(ctx.mkLt(x, y)); /* assert x > 2 */ - solver.assert_(ctx.mkGt(x, two)); + solver.add(ctx.mkGt(x, two)); /* find model for the constraints above */ Model model = null; @@ -1964,9 +1964,9 @@ class JavaExample Solver solver = ctx.mkSolver(); /* assert tup1 != tup2 */ - solver.assert_(ctx.mkNot(ctx.mkEq(tup1, tup2))); + solver.add(ctx.mkNot(ctx.mkEq(tup1, tup2))); /* assert first tup1 = first tup2 */ - solver.assert_(ctx.mkEq(ctx.mkApp(first, tup1), ctx.mkApp(first, tup2))); + solver.add(ctx.mkEq(ctx.mkApp(first, tup1), ctx.mkApp(first, tup2))); /* find model for the constraints above */ Model model = null; @@ -2014,7 +2014,7 @@ class JavaExample // Assert all feasible bounds. for (int i = 0; i < num_Exprs; ++i) { - solver.assert_(ctx.mkBVULE(to_minimize[i], + solver.add(ctx.mkBVULE(to_minimize[i], ctx.mkBV(upper[i], 32))); } @@ -2050,7 +2050,7 @@ class JavaExample { last_upper = (upper[i] + lower[i]) / 2; last_index = i; - solver.assert_(ctx.mkBVULE(to_minimize[i], + solver.add(ctx.mkBVULE(to_minimize[i], ctx.mkBV(last_upper, 32))); some_work = true; break; @@ -2074,7 +2074,7 @@ class JavaExample Solver solver = ctx.mkSolver(); - solver.assert_(ctx.mkBVULE(x, ctx.mkBVAdd(y, z))); + solver.add(ctx.mkBVULE(x, ctx.mkBVAdd(y, z))); checkSmall(ctx, solver, x, y, z); } @@ -2120,10 +2120,10 @@ class JavaExample BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc)); BoolExpr f4 = pd; - solver.assert_(ctx.mkOr(f1, p1)); - solver.assert_(ctx.mkOr(f2, p2)); - solver.assert_(ctx.mkOr(f3, p3)); - solver.assert_(ctx.mkOr(f4, p4)); + 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) diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 8d13fcb43..8c6e6c4c6 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -78,6 +78,14 @@ namespace Microsoft.Z3 } } + /// + /// Alias for Assert. + /// + public void Add(params BoolExpr[] constraints) + { + Assert(constraints); + } + /// /// Register predicate as recursive relation. /// diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index e648ac80c..b108683c9 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -90,6 +90,14 @@ namespace Microsoft.Z3 } } + /// + /// Alias for Assert. + /// + public void Add(params BoolExpr[] constraints) + { + Assert(constraints); + } + /// /// Indicates whether the goal contains `false'. /// diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 8c07ef31e..274f8dc4a 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -117,6 +117,14 @@ namespace Microsoft.Z3 } } + /// + /// Alias for Assert. + /// + public void Add(params BoolExpr[] constraints) + { + Assert(constraints); + } + /// /// Assert multiple constraints into the solver, and track them (in the unsat) core /// using the Boolean constants in ps. diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 6a8cafae2..4710368aa 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -51,7 +51,7 @@ public class Fixedpoint extends Z3Object * * @throws Z3Exception **/ - public void assert_(BoolExpr ... constraints) throws Z3Exception + public void add(BoolExpr ... constraints) throws Z3Exception { getContext().checkContextMatch(constraints); for (BoolExpr a : constraints) diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 520a7af15..c486a57b3 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -65,7 +65,7 @@ public class Goal extends Z3Object * * @throws Z3Exception **/ - public void assert_(BoolExpr ... constraints) throws Z3Exception + public void add(BoolExpr ... constraints) throws Z3Exception { getContext().checkContextMatch(constraints); for (BoolExpr c : constraints) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index c60d3f88c..3827de07a 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -94,7 +94,7 @@ public class Solver extends Z3Object * * @throws Z3Exception **/ - public void assert_(BoolExpr... constraints) throws Z3Exception + public void add(BoolExpr... constraints) throws Z3Exception { getContext().checkContextMatch(constraints); for (BoolExpr a : constraints)