diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 75393378b..2085de296 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -248,10 +248,13 @@ namespace test_mapi return res; } - static void Prove(Context ctx, BoolExpr f, params BoolExpr[] assumptions) + static void Prove(Context ctx, BoolExpr f, bool useMBQI = false, params BoolExpr[] assumptions) { Console.WriteLine("Proving: " + f); Solver s = ctx.MkSolver(); + Params p = ctx.MkParams(); + p.Add("mbqi", useMBQI); + s.Parameters = p; foreach (BoolExpr a in assumptions) s.Assert(a); s.Assert(ctx.MkNot(f)); @@ -270,10 +273,13 @@ namespace test_mapi } } - static void Disprove(Context ctx, BoolExpr f, params BoolExpr[] assumptions) + static void Disprove(Context ctx, BoolExpr f, bool useMBQI = false, params BoolExpr[] assumptions) { Console.WriteLine("Disproving: " + f); Solver s = ctx.MkSolver(); + Params p = ctx.MkParams(); + p.Add("mbqi", useMBQI); + s.Parameters = p; foreach (BoolExpr a in assumptions) s.Assert(a); s.Assert(ctx.MkNot(f)); @@ -298,7 +304,7 @@ namespace test_mapi ArithExpr xr = (ArithExpr)ctx.MkConst(ctx.MkSymbol("x"), ctx.MkRealSort()); ArithExpr yr = (ArithExpr)ctx.MkConst(ctx.MkSymbol("y"), ctx.MkRealSort()); - Goal g4 = ctx.MkGoal(true, false, true); + Goal g4 = ctx.MkGoal(true); 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))); @@ -330,7 +336,7 @@ namespace test_mapi { Console.WriteLine("ArrayExample1"); - Goal g = ctx.MkGoal(true, false, false); + Goal g = ctx.MkGoal(true); ArraySort asort = ctx.MkArraySort(ctx.IntSort, ctx.MkBitVecSort(32)); ArrayExpr aex = (ArrayExpr)ctx.MkConst(ctx.MkSymbol("MyArray"), asort); Expr sel = ctx.MkSelect(aex, ctx.MkInt(0)); @@ -640,95 +646,76 @@ namespace test_mapi /// Prove that f(x, y) = f(w, v) implies y = v when /// f is injective in the second argument. /// - public static void QuantifierExample3() + public static void QuantifierExample3(Context ctx) { Console.WriteLine("QuantifierExample3"); - - Dictionary cfg = new Dictionary() { - { "MBQI", "false" }, - { "PROOF_MODE", "2" }, - { "AUTO_CONFIG", "false" } - }; - /* If quantified formulas are asserted in a logical context, then the model produced by Z3 should be viewed as a potential model. */ - using (Context ctx = new Context(cfg)) - { - /* declare function f */ - Sort I = ctx.IntSort; - FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I); + /* declare function f */ + Sort I = ctx.IntSort; + FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I); - /* f is injective in the second argument. */ - BoolExpr inj = InjAxiom(ctx, f, 1); + /* f is injective in the second argument. */ + BoolExpr inj = InjAxiom(ctx, f, 1); - /* create x, y, v, w, fxy, fwv */ - Expr x = ctx.MkIntConst("x"); - Expr y = ctx.MkIntConst("y"); - Expr v = ctx.MkIntConst("v"); - Expr w = ctx.MkIntConst("w"); - Expr fxy = ctx.MkApp(f, x, y); - Expr fwv = ctx.MkApp(f, w, v); + /* create x, y, v, w, fxy, fwv */ + Expr x = ctx.MkIntConst("x"); + Expr y = ctx.MkIntConst("y"); + Expr v = ctx.MkIntConst("v"); + Expr w = ctx.MkIntConst("w"); + Expr fxy = ctx.MkApp(f, x, y); + Expr fwv = ctx.MkApp(f, w, v); - /* f(x, y) = f(w, v) */ - BoolExpr p1 = ctx.MkEq(fxy, fwv); + /* 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, inj, p1); + /* 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, 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 static void QuantifierExample4() + public static void QuantifierExample4(Context ctx) { Console.WriteLine("QuantifierExample4"); - Dictionary cfg = new Dictionary() { - { "MBQI", "false" }, - { "PROOF_MODE", "2" }, - { "AUTO_CONFIG","false" }}; - - /* If quantified formulas are asserted in a logical context, then the model produced by Z3 should be viewed as a potential model. */ - using (Context ctx = new Context(cfg)) - { - /* declare function f */ - Sort I = ctx.IntSort; - FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I); + /* declare function f */ + Sort I = ctx.IntSort; + FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I); - /* f is injective in the second argument. */ - BoolExpr inj = InjAxiomAbs(ctx, f, 1); + /* f is injective in the second argument. */ + BoolExpr inj = InjAxiomAbs(ctx, f, 1); - /* create x, y, v, w, fxy, fwv */ - Expr x = ctx.MkIntConst("x"); - Expr y = ctx.MkIntConst("y"); - Expr v = ctx.MkIntConst("v"); - Expr w = ctx.MkIntConst("w"); - Expr fxy = ctx.MkApp(f, x, y); - Expr fwv = ctx.MkApp(f, w, v); + /* create x, y, v, w, fxy, fwv */ + Expr x = ctx.MkIntConst("x"); + Expr y = ctx.MkIntConst("y"); + Expr v = ctx.MkIntConst("v"); + Expr w = ctx.MkIntConst("w"); + Expr fxy = ctx.MkApp(f, x, y); + Expr fwv = ctx.MkApp(f, w, v); - /* f(x, y) = f(w, v) */ - BoolExpr p1 = ctx.MkEq(fxy, fwv); + /* 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, inj, p1); + /* 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, inj, p1); - } + /* disprove f(x, y) = f(w, v) implies x = w */ + BoolExpr p3 = ctx.MkEq(x, w); + Disprove(ctx, p3, false, inj, p1); } /// @@ -756,7 +743,7 @@ namespace test_mapi BoolExpr trivial_eq = ctx.MkEq(fapp, fapp); BoolExpr nontrivial_eq = ctx.MkEq(fapp, fapp2); - Goal g = ctx.MkGoal(true, false, true); + Goal g = ctx.MkGoal(true); g.Assert(trivial_eq); g.Assert(nontrivial_eq); Console.WriteLine("Goal: " + g); @@ -784,18 +771,18 @@ namespace test_mapi throw new TestFailedException(); - Goal g2 = ctx.MkGoal(true, true, false); + Goal g2 = ctx.MkGoal(true, true); ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g2); if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedSat) throw new TestFailedException(); - g2 = ctx.MkGoal(true, true, false); + g2 = ctx.MkGoal(true, true); g2.Assert(ctx.MkFalse()); ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g2); if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedUnsat) throw new TestFailedException(); - Goal g3 = ctx.MkGoal(true, true, false); + Goal g3 = ctx.MkGoal(true, true); Expr xc = ctx.MkConst(ctx.MkSymbol("x"), ctx.IntSort); Expr yc = ctx.MkConst(ctx.MkSymbol("y"), ctx.IntSort); g3.Assert(ctx.MkEq(xc, ctx.MkNumeral(1, ctx.IntSort))); @@ -1063,7 +1050,7 @@ namespace test_mapi // Or perhaps a tactic for QF_BV - Goal g = ctx.MkGoal(true, false, true); + Goal g = ctx.MkGoal(true); g.Assert(eq); Tactic t = ctx.MkTactic("qfbv"); @@ -1086,7 +1073,7 @@ namespace test_mapi Expr y = ctx.MkConst("y", bvs); BoolExpr q = ctx.MkEq(x, y); - Goal g = ctx.MkGoal(true, false, true); + Goal g = ctx.MkGoal(true); g.Assert(q); Tactic t1 = ctx.MkTactic("qfbv"); @@ -1128,7 +1115,7 @@ namespace test_mapi /// public static void FindModelExample2(Context ctx) { - Console.WriteLine("find_model_example2"); + Console.WriteLine("FindModelExample2"); IntExpr x = ctx.MkIntConst("x"); IntExpr y = ctx.MkIntConst("y"); @@ -1250,13 +1237,13 @@ namespace test_mapi /* prove z < 0 */ BoolExpr f = ctx.MkLt(z, zero); Console.WriteLine("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0"); - Prove(ctx, f, c1, c2, c3); + Prove(ctx, f, false, c1, c2, c3); /* disprove z < -1 */ IntExpr minus_one = ctx.MkInt(-1); f = ctx.MkLt(z, minus_one); Console.WriteLine("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1"); - Disprove(ctx, f, c1, c2, c3); + Disprove(ctx, f, false, c1, c2, c3); } /// @@ -1448,7 +1435,7 @@ namespace test_mapi BoolExpr thm = ctx.SMTLIBFormulas[0]; Console.WriteLine("formula: {0}", thm); - Prove(ctx, thm, ca); + Prove(ctx, thm, false, ca); } /// @@ -1979,45 +1966,40 @@ namespace test_mapi /// /// Extract unsatisfiable core example /// - public static void UnsatCoreAndProofExample() + public static void UnsatCoreAndProofExample(Context ctx) { Console.WriteLine("UnsatCoreAndProofExample"); - Dictionary cfg = new Dictionary() { { "PROOF_MODE", "2" } }; + Solver solver = ctx.MkSolver(); - using (Context ctx = new Context(cfg)) + 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(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; + + solver.Assert(ctx.MkOr(f1, p1)); + solver.Assert(ctx.MkOr(f2, p2)); + solver.Assert(ctx.MkOr(f3, p3)); + solver.Assert(ctx.MkOr(f4, p4)); + Status result = solver.Check(assumptions); + + if (result == Status.UNSATISFIABLE) { - 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(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; - - solver.Assert(ctx.MkOr(f1, p1)); - solver.Assert(ctx.MkOr(f2, p2)); - solver.Assert(ctx.MkOr(f3, p3)); - solver.Assert(ctx.MkOr(f4, p4)); - Status result = solver.Check(assumptions); - - if (result == Status.UNSATISFIABLE) + Console.WriteLine("unsat"); + Console.WriteLine("proof: {0}", solver.Proof); + Console.WriteLine("core: "); + foreach (Expr c in solver.UnsatCore) { - Console.WriteLine("unsat"); - Console.WriteLine("proof: {0}", solver.Proof); - Console.WriteLine("core: "); - foreach (Expr c in solver.UnsatCore) - { - Console.WriteLine("{0}", c); - } + Console.WriteLine("{0}", c); } } } @@ -2054,9 +2036,8 @@ namespace test_mapi SimpleExample(); - using (Context ctx = new Context(new Dictionary() - { { "MODEL", "true"}, - { "PROOF_MODE", "2"} })) + // These examples need model generation turned on. + using (Context ctx = new Context(new Dictionary() { { "model", "true" } })) { BasicTests(ctx); CastingTest(ctx); @@ -2067,25 +2048,16 @@ namespace test_mapi ParOrExample(ctx); FindModelExample1(ctx); FindModelExample2(ctx); - ProveExample1(ctx); - ProveExample2(ctx); PushPopExample1(ctx); ArrayExample1(ctx); - ArrayExample2(ctx); ArrayExample3(ctx); - TupleExample(ctx); BitvectorExample1(ctx); BitvectorExample2(ctx); ParserExample1(ctx); ParserExample2(ctx); - ParserExample3(ctx); ParserExample4(ctx); ParserExample5(ctx); ITEExample(ctx); - EnumExample(ctx); - ListExample(ctx); - TreeExample(ctx); - ForestExample(ctx); EvalExample1(ctx); EvalExample2(ctx); FindSmallModelExample(ctx); @@ -2093,9 +2065,29 @@ namespace test_mapi FiniteDomainExample(ctx); } - QuantifierExample3(); - QuantifierExample4(); - UnsatCoreAndProofExample(); + // These examples need proof generation turned on. + using (Context ctx = new Context(new Dictionary() { { "proof", "true" } })) + { + ProveExample1(ctx); + ProveExample2(ctx); + ArrayExample2(ctx); + TupleExample(ctx); + ParserExample3(ctx); + EnumExample(ctx); + ListExample(ctx); + TreeExample(ctx); + ForestExample(ctx); + UnsatCoreAndProofExample(ctx); + } + + // These examples need proof generation turned on and auto-config set to false. + using (Context ctx = new Context(new Dictionary() + { {"proof", "true" }, + {"auto-config", "false" } })) + { + QuantifierExample3(ctx); + QuantifierExample4(ctx); + } Log.Close(); if (Log.isOpen()) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 0d5f01fc3..b3cb939ac 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -250,24 +250,28 @@ class JavaExample return res; } - void Prove(Context ctx, BoolExpr f) throws Z3Exception, TestFailedException + void Prove(Context ctx, BoolExpr f, boolean useMBQI) throws Z3Exception, + TestFailedException { BoolExpr[] assumptions = new BoolExpr[0]; - Prove(ctx, f, assumptions); + Prove(ctx, f, useMBQI, assumptions); } - void Prove(Context ctx, BoolExpr f, BoolExpr assumption) + void Prove(Context ctx, BoolExpr f, boolean useMBQI, BoolExpr assumption) throws Z3Exception, TestFailedException { BoolExpr[] assumptions = { assumption }; - Prove(ctx, f, assumptions); + Prove(ctx, f, useMBQI, assumptions); } - void Prove(Context ctx, BoolExpr f, BoolExpr[] assumptions) + void Prove(Context ctx, BoolExpr f, boolean useMBQI, BoolExpr[] assumptions) throws Z3Exception, TestFailedException { System.out.println("Proving: " + f); Solver s = ctx.MkSolver(); + Params p = ctx.MkParams(); + p.Add("mbqi", useMBQI); + s.setParameters(p); for (BoolExpr a : assumptions) s.Assert(a); s.Assert(ctx.MkNot(f)); @@ -286,25 +290,28 @@ class JavaExample } } - void Disprove(Context ctx, BoolExpr f) throws Z3Exception, + void Disprove(Context ctx, BoolExpr f, boolean useMBQI) throws Z3Exception, TestFailedException { BoolExpr[] a = {}; - Disprove(ctx, f, a); + Disprove(ctx, f, useMBQI, a); } - void Disprove(Context ctx, BoolExpr f, BoolExpr assumption) + void Disprove(Context ctx, BoolExpr f, boolean useMBQI, BoolExpr assumption) throws Z3Exception, TestFailedException { BoolExpr[] a = { assumption }; - Disprove(ctx, f, a); + Disprove(ctx, f, useMBQI, a); } - void Disprove(Context ctx, BoolExpr f, BoolExpr[] assumptions) - throws Z3Exception, TestFailedException + void Disprove(Context ctx, BoolExpr f, boolean useMBQI, + BoolExpr[] assumptions) throws Z3Exception, TestFailedException { System.out.println("Disproving: " + f); Solver s = ctx.MkSolver(); + Params p = ctx.MkParams(); + p.Add("mbqi", useMBQI); + s.setParameters(p); for (BoolExpr a : assumptions) s.Assert(a); s.Assert(ctx.MkNot(f)); @@ -332,7 +339,7 @@ class JavaExample ctx.MkRealSort()); ArithExpr yr = (ArithExpr) ctx.MkConst(ctx.MkSymbol("y"), ctx.MkRealSort()); - Goal g4 = ctx.MkGoal(true, false, true); + Goal g4 = ctx.MkGoal(true, false, false); g4.Assert(ctx.MkGt(xr, ctx.MkReal(10, 1))); g4.Assert(ctx.MkEq(yr, ctx.MkAdd(new ArithExpr[] { xr, ctx.MkReal(1, 1) }))); @@ -455,7 +462,7 @@ class JavaExample 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); + Prove(ctx, thm, false); } // / Show that distinct(a_0, ... , a_n) is @@ -714,101 +721,83 @@ class JavaExample // / f is injective in the second argument. - public void QuantifierExample3() throws Z3Exception, TestFailedException + public void QuantifierExample3(Context ctx) throws Z3Exception, + TestFailedException { System.out.println("QuantifierExample3"); Log.Append("QuantifierExample3"); - HashMap cfg = new HashMap(); - // We must set a global or provide an argument to Prove - // cfg.put("mbqi", "false"); - cfg.put("proof", "true"); - cfg.put("auto_config", "false"); - /* * If quantified formulas are asserted in a logical context, then the * model produced by Z3 should be viewed as a potential model. */ - { - Context ctx = new Context(cfg); + /* declare function f */ + Sort I = ctx.IntSort(); + FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I); - /* declare function f */ - Sort I = ctx.IntSort(); - FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I); + /* f is injective in the second argument. */ + BoolExpr inj = InjAxiom(ctx, f, 1); - /* f is injective in the second argument. */ - BoolExpr inj = InjAxiom(ctx, f, 1); + /* create x, y, v, w, fxy, fwv */ + Expr x = ctx.MkIntConst("x"); + Expr y = ctx.MkIntConst("y"); + Expr v = ctx.MkIntConst("v"); + Expr w = ctx.MkIntConst("w"); + Expr fxy = ctx.MkApp(f, new Expr[] { x, y }); + Expr fwv = ctx.MkApp(f, new Expr[] { w, v }); - /* create x, y, v, w, fxy, fwv */ - Expr x = ctx.MkIntConst("x"); - Expr y = ctx.MkIntConst("y"); - Expr v = ctx.MkIntConst("v"); - Expr w = ctx.MkIntConst("w"); - Expr fxy = ctx.MkApp(f, new Expr[] { x, y }); - Expr fwv = ctx.MkApp(f, new Expr[] { w, v }); + /* f(x, y) = f(w, v) */ + BoolExpr p1 = ctx.MkEq(fxy, fwv); - /* 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, new BoolExpr[] { inj, p1 }); - /* prove f(x, y) = f(w, v) implies y = v */ - BoolExpr p2 = ctx.MkEq(y, v); - Prove(ctx, p2, new BoolExpr[] { inj, p1 }); - - /* disprove f(x, y) = f(w, v) implies x = w */ - BoolExpr p3 = ctx.MkEq(x, w); - Disprove(ctx, p3, new BoolExpr[] { inj, p1 }); - } + /* disprove f(x, y) = f(w, v) implies x = w */ + BoolExpr p3 = ctx.MkEq(x, w); + Disprove(ctx, p3, false, new BoolExpr[] { inj, p1 }); } // / Prove that f(x, y) = f(w, v) implies y = v when // / f is injective in the second argument. - public void QuantifierExample4() throws Z3Exception, TestFailedException + public void QuantifierExample4(Context ctx) throws Z3Exception, TestFailedException { System.out.println("QuantifierExample4"); Log.Append("QuantifierExample4"); - HashMap cfg = new HashMap(); - // We must set a global or provide an argument to Prove - // cfg.put("mbqi", "false"); - cfg.put("proof", "true"); - cfg.put("auto_config", "false"); - /* * If quantified formulas are asserted in a logical context, then the * model produced by Z3 should be viewed as a potential model. */ - { - Context ctx = new Context(cfg); - /* declare function f */ - Sort I = ctx.IntSort(); - FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I); + /* declare function f */ + Sort I = ctx.IntSort(); + FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I); - /* f is injective in the second argument. */ - BoolExpr inj = InjAxiomAbs(ctx, f, 1); + /* f is injective in the second argument. */ + BoolExpr inj = InjAxiomAbs(ctx, f, 1); - /* create x, y, v, w, fxy, fwv */ - Expr x = ctx.MkIntConst("x"); - Expr y = ctx.MkIntConst("y"); - Expr v = ctx.MkIntConst("v"); - Expr w = ctx.MkIntConst("w"); - Expr fxy = ctx.MkApp(f, new Expr[] { x, y }); - Expr fwv = ctx.MkApp(f, new Expr[] { w, v }); + /* create x, y, v, w, fxy, fwv */ + Expr x = ctx.MkIntConst("x"); + Expr y = ctx.MkIntConst("y"); + Expr v = ctx.MkIntConst("v"); + Expr w = ctx.MkIntConst("w"); + Expr fxy = ctx.MkApp(f, new Expr[] { x, y }); + Expr fwv = ctx.MkApp(f, new Expr[] { w, v }); - /* f(x, y) = f(w, v) */ - BoolExpr p1 = ctx.MkEq(fxy, fwv); + /* 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, new BoolExpr[] { inj, p1 }); + /* prove f(x, y) = f(w, v) implies y = v */ + BoolExpr p2 = ctx.MkEq(y, v); + Prove(ctx, p2, false, new BoolExpr[] { inj, p1 }); - /* disprove f(x, y) = f(w, v) implies x = w */ - BoolExpr p3 = ctx.MkEq(x, w); - Disprove(ctx, p3, new BoolExpr[] { inj, p1 }); - } + /* disprove f(x, y) = f(w, v) implies x = w */ + BoolExpr p3 = ctx.MkEq(x, w); + Disprove(ctx, p3, false, new BoolExpr[] { inj, p1 }); } // / Some basic tests. @@ -835,7 +824,7 @@ class JavaExample BoolExpr trivial_eq = ctx.MkEq(fapp, fapp); BoolExpr nontrivial_eq = ctx.MkEq(fapp, fapp2); - Goal g = ctx.MkGoal(true, false, true); + Goal g = ctx.MkGoal(true, false, false); g.Assert(trivial_eq); g.Assert(nontrivial_eq); System.out.println("Goal: " + g); @@ -921,7 +910,7 @@ class JavaExample IntExpr i = ctx.MkInt("1/2"); throw new TestFailedException(); // unreachable } catch (Z3Exception e) - { + { } } @@ -1144,7 +1133,7 @@ class JavaExample System.out.println("solver result: " + res); // Or perhaps a tactic for QF_BV - Goal g = ctx.MkGoal(true, false, true); + Goal g = ctx.MkGoal(true, false, false); g.Assert(eq); Tactic t = ctx.MkTactic("qfbv"); @@ -1167,7 +1156,7 @@ class JavaExample Expr y = ctx.MkConst("y", bvs); BoolExpr q = ctx.MkEq(x, y); - Goal g = ctx.MkGoal(true, false, true); + Goal g = ctx.MkGoal(true, false, false); g.Assert(q); Tactic t1 = ctx.MkTactic("qfbv"); @@ -1271,7 +1260,7 @@ class JavaExample /* 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)); + Prove(ctx, ctx.MkImplies(eq, f), false); /* create g(g(x)) */ Expr ggx = g.Apply(gx); @@ -1279,7 +1268,7 @@ class JavaExample /* 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)); + Disprove(ctx, ctx.MkImplies(eq, f), false); /* Print the model using the custom model printer */ Model m = Check(ctx, ctx.MkNot(f), Status.SATISFIABLE); @@ -1335,14 +1324,14 @@ class JavaExample 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, new BoolExpr[] { c1, c2, c3 }); + Prove(ctx, f, false, new BoolExpr[] { c1, c2, c3 }); /* disprove z < -1 */ IntExpr minus_one = ctx.MkInt(-1); f = ctx.MkLt(z, minus_one); System.out .println("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1"); - Disprove(ctx, f, new BoolExpr[] { c1, c2, c3 }); + Disprove(ctx, f, false, new BoolExpr[] { c1, c2, c3 }); } // / Show how push & pop can be used to create "backtracking" points. @@ -1442,7 +1431,7 @@ class JavaExample Expr n2 = first.Apply(n1); BoolExpr n3 = ctx.MkEq(x, n2); System.out.println("Tuple example: " + n3); - Prove(ctx, n3); + Prove(ctx, n3, false); } // / Simple bit-vector example. @@ -1468,7 +1457,7 @@ class JavaExample BoolExpr thm = ctx.MkIff(c1, c2); System.out .println("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers"); - Disprove(ctx, thm); + Disprove(ctx, thm, false); } // / Find x and y such that: x ^ y - 103 == x * y @@ -1555,7 +1544,7 @@ class JavaExample BoolExpr thm = ctx.SMTLIBFormulas()[0]; System.out.println("formula: " + thm); - Prove(ctx, thm, ca); + Prove(ctx, thm, false, ca); } // / Display the declarations, assumptions and formulas in a SMT-LIB string. @@ -1647,15 +1636,16 @@ class JavaExample Expr orange = fruit.Consts()[2]; /* Apples are different from oranges */ - Prove(ctx, ctx.MkNot(ctx.MkEq(apple, orange))); + Prove(ctx, ctx.MkNot(ctx.MkEq(apple, orange)), false); /* Apples pass the apple test */ - Prove(ctx, (BoolExpr) ctx.MkApp(fruit.TesterDecls()[0], apple)); + Prove(ctx, (BoolExpr) ctx.MkApp(fruit.TesterDecls()[0], apple), false); /* Oranges fail the apple test */ - Disprove(ctx, (BoolExpr) ctx.MkApp(fruit.TesterDecls()[0], orange)); + Disprove(ctx, (BoolExpr) ctx.MkApp(fruit.TesterDecls()[0], orange), + false); Prove(ctx, (BoolExpr) ctx.MkNot((BoolExpr) ctx.MkApp( - fruit.TesterDecls()[0], orange))); + fruit.TesterDecls()[0], orange)), false); Expr fruity = ctx.MkConst("fruity", fruit); @@ -1663,7 +1653,8 @@ class JavaExample Prove(ctx, ctx.MkOr(new BoolExpr[] { ctx.MkEq(fruity, apple), - ctx.MkEq(fruity, banana), ctx.MkEq(fruity, orange) })); + ctx.MkEq(fruity, banana), ctx.MkEq(fruity, orange) }), + false); } // / Create a list datatype. @@ -1688,25 +1679,25 @@ class JavaExample l2 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { ctx.MkInt(2), nil }); /* nil != cons(1, nil) */ - Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1))); + Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1)), false); /* cons(2,nil) != cons(1, nil) */ - Prove(ctx, ctx.MkNot(ctx.MkEq(l1, l2))); + Prove(ctx, ctx.MkNot(ctx.MkEq(l1, l2)), false); /* cons(x,nil) = cons(y, nil) => x = y */ x = ctx.MkConst("x", int_ty); y = ctx.MkConst("y", int_ty); l1 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { x, nil }); l2 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { y, nil }); - Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y))); + Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)), false); /* cons(x,u) = cons(x, v) => u = v */ u = ctx.MkConst("u", int_list); v = ctx.MkConst("v", int_list); l1 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { x, u }); l2 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { y, v }); - Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v))); - Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y))); + 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, @@ -1714,10 +1705,10 @@ class JavaExample (BoolExpr) ctx.MkApp(int_list.IsNilDecl(), new Expr[] { u }), (BoolExpr) ctx.MkApp(int_list.IsConsDecl(), - new Expr[] { u }) })); + new Expr[] { u }) }), false); /* occurs check u != cons(x,u) */ - Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1))); + Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)), false); /* destructors: is_cons(u) => u = cons(head(u),tail(u)) */ fml1 = ctx.MkEq(u, ctx.MkApp(int_list.ConsDecl(), @@ -1728,9 +1719,9 @@ class JavaExample fml1); System.out.println("Formula " + fml); - Prove(ctx, fml); + Prove(ctx, fml, false); - Disprove(ctx, fml1); + Disprove(ctx, fml1, false); } // / Create a binary tree datatype. @@ -1770,7 +1761,7 @@ class JavaExample l2 = ctx.MkApp(cons_decl, new Expr[] { l1, nil }); /* nil != cons(nil, nil) */ - Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1))); + Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1)), false); /* cons(x,u) = cons(x, v) => u = v */ u = ctx.MkConst("u", cell); @@ -1779,17 +1770,18 @@ class JavaExample y = ctx.MkConst("y", cell); l1 = ctx.MkApp(cons_decl, new Expr[] { x, u }); l2 = ctx.MkApp(cons_decl, new Expr[] { y, v }); - Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v))); - Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y))); + 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(new BoolExpr[] { (BoolExpr) ctx.MkApp(is_nil_decl, new Expr[] { u }), - (BoolExpr) ctx.MkApp(is_cons_decl, new Expr[] { u }) })); + (BoolExpr) ctx.MkApp(is_cons_decl, new Expr[] { u }) }), + false); /* occurs check u != cons(x,u) */ - Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1))); + Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)), false); /* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */ fml1 = ctx.MkEq( @@ -1800,9 +1792,9 @@ class JavaExample ctx.MkApp(cdr_decl, u) })); fml = ctx.MkImplies((BoolExpr) ctx.MkApp(is_cons_decl, u), fml1); System.out.println("Formula " + fml); - Prove(ctx, fml); + Prove(ctx, fml, false); - Disprove(ctx, fml1); + Disprove(ctx, fml1, false); } // / Create a forest of trees. @@ -1904,8 +1896,8 @@ class JavaExample f3 = ctx.MkApp(cons1_decl, new Expr[] { t1, f1 }); /* nil != cons(nil,nil) */ - Prove(ctx, ctx.MkNot(ctx.MkEq(nil1, f1))); - Prove(ctx, ctx.MkNot(ctx.MkEq(nil2, t1))); + Prove(ctx, ctx.MkNot(ctx.MkEq(nil1, f1)), false); + Prove(ctx, ctx.MkNot(ctx.MkEq(nil2, t1)), false); /* cons(x,u) = cons(x, v) => u = v */ u = ctx.MkConst("u", forest); @@ -1914,16 +1906,16 @@ class JavaExample y = ctx.MkConst("y", tree); l1 = ctx.MkApp(cons1_decl, new Expr[] { x, u }); l2 = ctx.MkApp(cons1_decl, new Expr[] { y, v }); - Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v))); - Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y))); + 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(new BoolExpr[] { (BoolExpr) ctx.MkApp(is_nil1_decl, new Expr[] { u }), - (BoolExpr) ctx.MkApp(is_cons1_decl, new Expr[] { u }) })); + (BoolExpr) ctx.MkApp(is_cons1_decl, new Expr[] { u }) }), false); /* occurs check u != cons(x,u) */ - Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1))); + Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)), false); } // / Demonstrate how to use #Eval. @@ -2129,49 +2121,42 @@ class JavaExample // / Extract unsatisfiable core example - public void UnsatCoreAndProofExample() throws Z3Exception + public void UnsatCoreAndProofExample(Context ctx) throws Z3Exception { System.out.println("UnsatCoreAndProofExample"); Log.Append("UnsatCoreAndProofExample"); - HashMap cfg = new HashMap(); - cfg.put("proof", "true"); + 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(new BoolExpr[] { pa, pb, pc }); + BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc }); + BoolExpr f3 = ctx.MkOr(new BoolExpr[] { ctx.MkNot(pa), ctx.MkNot(pc) }); + BoolExpr f4 = pd; + + solver.Assert(ctx.MkOr(new BoolExpr[] { f1, p1 })); + solver.Assert(ctx.MkOr(new BoolExpr[] { f2, p2 })); + solver.Assert(ctx.MkOr(new BoolExpr[] { f3, p3 })); + solver.Assert(ctx.MkOr(new BoolExpr[] { f4, p4 })); + Status result = solver.Check(assumptions); + + if (result == Status.UNSATISFIABLE) { - Context ctx = new Context(cfg); - 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(new BoolExpr[] { pa, pb, pc }); - BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc }); - BoolExpr f3 = ctx.MkOr(new BoolExpr[] { ctx.MkNot(pa), - ctx.MkNot(pc) }); - BoolExpr f4 = pd; - - solver.Assert(ctx.MkOr(new BoolExpr[] { f1, p1 })); - solver.Assert(ctx.MkOr(new BoolExpr[] { f2, p2 })); - solver.Assert(ctx.MkOr(new BoolExpr[] { f3, p3 })); - solver.Assert(ctx.MkOr(new BoolExpr[] { f4, p4 })); - Status result = solver.Check(assumptions); - - if (result == Status.UNSATISFIABLE) + System.out.println("unsat"); + System.out.println("proof: " + solver.Proof()); + System.out.println("core: "); + for (Expr c : solver.UnsatCore()) { - System.out.println("unsat"); - System.out.println("proof: " + solver.Proof()); - System.out.println("core: "); - for (Expr c : solver.UnsatCore()) - { - System.out.println(c); - } + System.out.println(c); } } } @@ -2210,10 +2195,9 @@ class JavaExample p.SimpleExample(); - { + { // These examples need model generation turned on. HashMap cfg = new HashMap(); cfg.put("model", "true"); - cfg.put("proof", "true"); Context ctx = new Context(cfg); p.BasicTests(ctx); p.CastingTest(ctx); @@ -2224,25 +2208,16 @@ class JavaExample p.ParOrExample(ctx); p.FindModelExample1(ctx); p.FindModelExample2(ctx); - p.ProveExample1(ctx); - p.ProveExample2(ctx); p.PushPopExample1(ctx); p.ArrayExample1(ctx); - p.ArrayExample2(ctx); p.ArrayExample3(ctx); - p.TupleExample(ctx); p.BitvectorExample1(ctx); p.BitvectorExample2(ctx); p.ParserExample1(ctx); p.ParserExample2(ctx); - p.ParserExample3(ctx); p.ParserExample4(ctx); p.ParserExample5(ctx); p.ITEExample(ctx); - p.EnumExample(ctx); - p.ListExample(ctx); - p.TreeExample(ctx); - p.ForestExample(ctx); p.EvalExample1(ctx); p.EvalExample2(ctx); p.FindSmallModelExample(ctx); @@ -2250,9 +2225,31 @@ class JavaExample p.FiniteDomainExample(ctx); } - p.QuantifierExample3(); - p.QuantifierExample4(); - p.UnsatCoreAndProofExample(); + { // 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); + p.ParserExample3(ctx); + p.EnumExample(ctx); + p.ListExample(ctx); + p.TreeExample(ctx); + p.ForestExample(ctx); + p.UnsatCoreAndProofExample(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); + } Log.Close(); if (Log.isOpen()) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index ff36b4553..aee60c43f 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3657,6 +3657,7 @@ namespace Microsoft.Z3 Goal_DRQ.Clear(this); Model_DRQ.Clear(this); Params_DRQ.Clear(this); + ParamDescrs_DRQ.Clear(this); Probe_DRQ.Clear(this); Solver_DRQ.Clear(this); Statistics_DRQ.Clear(this); diff --git a/src/api/dotnet/IDecRefQueue.cs b/src/api/dotnet/IDecRefQueue.cs index e6276c4f4..d741a8f05 100644 --- a/src/api/dotnet/IDecRefQueue.cs +++ b/src/api/dotnet/IDecRefQueue.cs @@ -24,7 +24,7 @@ using System.Threading; using System.Diagnostics.Contracts; namespace Microsoft.Z3 -{ +{ [ContractClass(typeof(DecRefQueueContracts))] internal abstract class IDecRefQueue { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 { Contract.Invariant(this.m_queue != null); } - + #endregion readonly internal protected Object m_lock = new Object(); diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index 762b83b28..a1bb868eb 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -252,6 +252,71 @@ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules true + + true + bin\x86\Debug\ + DEBUG;TRACE + true + full + x86 + ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + + + bin\x86\Release\ + true + ..\external\Microsoft.Z3.xml + true + pdbonly + x86 + ..\external\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + + + bin\x86\external\ + true + ..\external\Microsoft.Z3.xml + true + pdbonly + x86 + bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + + + bin\x86\Release_delaysign\ + DELAYSIGN + true + ..\Release_delaysign\Microsoft.Z3.xml + true + pdbonly + x86 + ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 3bc8b4574..c954c50e5 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -44,8 +44,8 @@ public class Params extends Z3Object **/ public void Add(String name, boolean value) throws Z3Exception { - Native.paramsSetBool(Context().nCtx(), NativeObject(), Context() - .MkSymbol(name).NativeObject(), (value) ? true : false); + Native.paramsSetBool(Context().nCtx(), NativeObject(), + Context().MkSymbol(name).NativeObject(), value); } /**