mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Java+.Net Examples: refactoring

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-12-04 19:32:20 +00:00
parent f7528456da
commit 4d1d784a1c
2 changed files with 274 additions and 285 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

238
examples/dotnet/Program.cs
View file

@ -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 <tt>f(x, y) = f(w, v) implies y = v</tt> when
/// <code>f</code> is injective in the second argument. <seealso cref="inj_axiom"/>
/// </summary>
public static void QuantifierExample3()
public static void QuantifierExample3(Context ctx)
{
Console.WriteLine("QuantifierExample3");
Dictionary<string, string> cfg = new Dictionary<string, string>() {
{ "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);
}
/// <summary>
/// Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when
/// <code>f</code> is injective in the second argument. <seealso cref="inj_axiom"/>
/// </summary>
public static void QuantifierExample4()
public static void QuantifierExample4(Context ctx)
{
Console.WriteLine("QuantifierExample4");
Dictionary<string, string> cfg = new Dictionary<string, string>() {
{ "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);
}
/// <summary>
@ -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
/// </summary>
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);
}
/// <summary>
@ -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);
}
/// <summary>
@ -1979,45 +1966,40 @@ namespace test_mapi
/// <summary>
/// Extract unsatisfiable core example
/// </summary>
public static void UnsatCoreAndProofExample()
public static void UnsatCoreAndProofExample(Context ctx)
{
Console.WriteLine("UnsatCoreAndProofExample");
Dictionary<string, string> cfg = new Dictionary<string, string>() { { "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<string, string>()
{ { "MODEL", "true"},
{ "PROOF_MODE", "2"} }))
// These examples need model generation turned on.
using (Context ctx = new Context(new Dictionary<string, string>() { { "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<string, string>() { { "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<string, string>()
{ {"proof", "true" },
{"auto-config", "false" } }))
{
QuantifierExample3(ctx);
QuantifierExample4(ctx);
}
Log.Close();
if (Log.isOpen())

321
examples/java/JavaExample.java
View file

@ -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 <code>distinct(a_0, ... , a_n)</code> is
@ -714,101 +721,83 @@ class JavaExample
// / <code>f</code> is injective in the second argument. <seealso
// cref="inj_axiom"/>
public void QuantifierExample3() throws Z3Exception, TestFailedException
public void QuantifierExample3(Context ctx) throws Z3Exception,
TestFailedException
{
System.out.println("QuantifierExample3");
Log.Append("QuantifierExample3");
HashMap<String, String> cfg = new HashMap<String, String>();
// 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 <tt>f(x, y) = f(w, v) implies y = v</tt> when
// / <code>f</code> is injective in the second argument. <seealso
// cref="inj_axiom"/>
public void QuantifierExample4() throws Z3Exception, TestFailedException
public void QuantifierExample4(Context ctx) throws Z3Exception, TestFailedException
{
System.out.println("QuantifierExample4");
Log.Append("QuantifierExample4");
HashMap<String, String> cfg = new HashMap<String, String>();
// 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<String, String> cfg = new HashMap<String, String>();
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<String, String> cfg = new HashMap<String, String>();
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<String, String> cfg = new HashMap<String, String>();
cfg.put("proof", "true");
Context ctx = new Context(cfg);
p.ProveExample1(ctx);
p.ProveExample2(ctx);
p.ArrayExample2(ctx);
p.TupleExample(ctx);
p.ParserExample3(ctx);
p.EnumExample(ctx);
p.ListExample(ctx);
p.TreeExample(ctx);
p.ForestExample(ctx);
p.UnsatCoreAndProofExample(ctx);
}
{ // These examples need proof generation turned on and auto-config
// set to false.
HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("proof", "true");
cfg.put("auto-config", "false");
Context ctx = new Context(cfg);
p.QuantifierExample3(ctx);
p.QuantifierExample4(ctx);
}
Log.Close();
if (Log.isOpen())