mirror of
https://github.com/Z3Prover/z3
synced 2025-04-04 16:44:07 +00:00
2225 lines
81 KiB
C#
2225 lines
81 KiB
C#
/*++
|
|
Copyright (c) 2012 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
Program.cs
|
|
|
|
Abstract:
|
|
|
|
Z3 Managed API: Example program
|
|
|
|
Author:
|
|
|
|
Christoph Wintersteiger (cwinter) 2012-03-16
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
|
|
using System;
|
|
using System.Collections;
|
|
using System.Collections.Generic;
|
|
|
|
using Microsoft.Z3;
|
|
|
|
namespace test_mapi
|
|
{
|
|
class Program
|
|
{
|
|
class TestFailedException : Exception
|
|
{
|
|
public TestFailedException() : base("Check FAILED") { }
|
|
};
|
|
|
|
/// <summary>
|
|
/// Create axiom: function f is injective in the i-th argument.
|
|
/// </summary>
|
|
/// <remarks>
|
|
/// The following axiom is produced:
|
|
/// <c>
|
|
/// forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i
|
|
/// </c>
|
|
/// Where, <code>finv</code>is a fresh function declaration.
|
|
/// </summary>
|
|
public static BoolExpr InjAxiom(Context ctx, FuncDecl f, int i)
|
|
{
|
|
Sort[] domain = f.Domain;
|
|
uint sz = f.DomainSize;
|
|
|
|
if (i >= sz)
|
|
{
|
|
Console.WriteLine("failed to create inj axiom");
|
|
return null;
|
|
}
|
|
|
|
/* declare the i-th inverse of f: finv */
|
|
Sort finv_domain = f.Range;
|
|
Sort finv_range = domain[i];
|
|
FuncDecl finv = ctx.MkFuncDecl("f_fresh", finv_domain, finv_range);
|
|
|
|
/* allocate temporary arrays */
|
|
Expr[] xs = new Expr[sz];
|
|
Symbol[] names = new Symbol[sz];
|
|
Sort[] types = new Sort[sz];
|
|
|
|
/* fill types, names and xs */
|
|
|
|
for (uint j = 0; j < sz; j++)
|
|
{
|
|
types[j] = domain[j];
|
|
names[j] = ctx.MkSymbol(String.Format("x_{0}", j));
|
|
xs[j] = ctx.MkBound(j, types[j]);
|
|
}
|
|
Expr x_i = xs[i];
|
|
|
|
/* create f(x_0, ..., x_i, ..., x_{n-1}) */
|
|
Expr fxs = f[xs];
|
|
|
|
/* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
|
|
Expr finv_fxs = finv[fxs];
|
|
|
|
/* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
|
|
Expr 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(new Expr[] { fxs });
|
|
|
|
/* create & assert quantifier */
|
|
BoolExpr q = ctx.MkForall(
|
|
types, /* types of quantified variables */
|
|
names, /* names of quantified variables */
|
|
eq,
|
|
1,
|
|
new Pattern[] { p } /* patterns */);
|
|
|
|
return q;
|
|
}
|
|
|
|
/// <summary>
|
|
/// Create axiom: function f is injective in the i-th argument.
|
|
/// </summary>
|
|
/// <remarks>
|
|
/// The following axiom is produced:
|
|
/// <c>
|
|
/// forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i
|
|
/// </c>
|
|
/// Where, <code>finv</code>is a fresh function declaration.
|
|
/// </summary>
|
|
public static BoolExpr InjAxiomAbs(Context ctx, FuncDecl f, int i)
|
|
{
|
|
Sort[] domain = f.Domain;
|
|
uint sz = f.DomainSize;
|
|
|
|
if (i >= sz)
|
|
{
|
|
Console.WriteLine("failed to create inj axiom");
|
|
return null;
|
|
}
|
|
|
|
/* declare the i-th inverse of f: finv */
|
|
Sort finv_domain = f.Range;
|
|
Sort finv_range = domain[i];
|
|
FuncDecl finv = ctx.MkFuncDecl("f_fresh", finv_domain, finv_range);
|
|
|
|
/* allocate temporary arrays */
|
|
Expr[] xs = new Expr[sz];
|
|
|
|
/* fill types, names and xs */
|
|
for (uint j = 0; j < sz; j++)
|
|
{
|
|
xs[j] = ctx.MkConst(String.Format("x_{0}", j), domain[j]);
|
|
}
|
|
Expr x_i = xs[i];
|
|
|
|
/* create f(x_0, ..., x_i, ..., x_{n-1}) */
|
|
Expr fxs = f[xs];
|
|
|
|
/* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
|
|
Expr finv_fxs = finv[fxs];
|
|
|
|
/* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
|
|
Expr 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(new Expr[] { fxs });
|
|
|
|
/* create & assert quantifier */
|
|
BoolExpr q = ctx.MkForall(
|
|
xs, /* types of quantified variables */
|
|
eq, /* names of quantified variables */
|
|
1,
|
|
new Pattern[] { p } /* patterns */);
|
|
|
|
return q;
|
|
}
|
|
|
|
/// <summary>
|
|
/// Assert the axiom: function f is commutative.
|
|
/// </summary>
|
|
/// <remarks>
|
|
/// This example uses the SMT-LIB parser to simplify the axiom construction.
|
|
/// </remarks>
|
|
private static BoolExpr CommAxiom(Context ctx, FuncDecl f)
|
|
{
|
|
Sort t = f.Range;
|
|
Sort[] dom = f.Domain;
|
|
|
|
if (dom.Length != 2 ||
|
|
!t.Equals(dom[0]) ||
|
|
!t.Equals(dom[1]))
|
|
{
|
|
Console.WriteLine("{0} {1} {2} {3}", 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 {0}) (y {1})) (= ({2} x y) ({3} y x))))",
|
|
t.Name, t.Name, f.Name, f.Name);
|
|
return ctx.ParseSMTLIB2String(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f })[0];
|
|
}
|
|
|
|
/// <summary>
|
|
/// "Hello world" example: create a Z3 logical context, and delete it.
|
|
/// </summary>
|
|
public static void SimpleExample()
|
|
{
|
|
Console.WriteLine("SimpleExample");
|
|
|
|
using (Context ctx = new Context())
|
|
{
|
|
/* do something with the context */
|
|
|
|
/* be kind to dispose manually and not wait for the GC. */
|
|
ctx.Dispose();
|
|
}
|
|
}
|
|
|
|
static Model Check(Context ctx, BoolExpr f, Status sat)
|
|
{
|
|
Solver s = ctx.MkSolver();
|
|
s.Assert(f);
|
|
if (s.Check() != sat)
|
|
throw new TestFailedException();
|
|
if (sat == Status.SATISFIABLE)
|
|
return s.Model;
|
|
else
|
|
return null;
|
|
}
|
|
|
|
static void SolveTactical(Context ctx, Tactic t, Goal g, Status sat)
|
|
{
|
|
Solver s = ctx.MkSolver(t);
|
|
Console.WriteLine("\nTactical solver: " + s);
|
|
|
|
foreach (BoolExpr a in g.Formulas)
|
|
s.Assert(a);
|
|
Console.WriteLine("Solver: " + s);
|
|
|
|
if (s.Check() != sat)
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
static ApplyResult ApplyTactic(Context ctx, Tactic t, Goal g)
|
|
{
|
|
Console.WriteLine("\nGoal: " + g);
|
|
|
|
ApplyResult res = t.Apply(g);
|
|
Console.WriteLine("Application result: " + res);
|
|
|
|
Status q = Status.UNKNOWN;
|
|
foreach (Goal sg in res.Subgoals)
|
|
if (sg.IsDecidedSat) q = Status.SATISFIABLE;
|
|
else if (sg.IsDecidedUnsat) q = Status.UNSATISFIABLE;
|
|
|
|
switch (q)
|
|
{
|
|
case Status.UNKNOWN:
|
|
Console.WriteLine("Tactic result: Undecided");
|
|
break;
|
|
case Status.SATISFIABLE:
|
|
Console.WriteLine("Tactic result: SAT");
|
|
break;
|
|
case Status.UNSATISFIABLE:
|
|
Console.WriteLine("Tactic result: UNSAT");
|
|
break;
|
|
}
|
|
|
|
return res;
|
|
}
|
|
|
|
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));
|
|
Status q = s.Check();
|
|
|
|
switch (q)
|
|
{
|
|
case Status.UNKNOWN:
|
|
Console.WriteLine("Unknown because: " + s.ReasonUnknown);
|
|
break;
|
|
case Status.SATISFIABLE:
|
|
throw new TestFailedException();
|
|
case Status.UNSATISFIABLE:
|
|
Console.WriteLine("OK, proof: " + s.Proof);
|
|
break;
|
|
}
|
|
}
|
|
|
|
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));
|
|
Status q = s.Check();
|
|
|
|
switch (q)
|
|
{
|
|
case Status.UNKNOWN:
|
|
Console.WriteLine("Unknown because: " + s.ReasonUnknown);
|
|
break;
|
|
case Status.SATISFIABLE:
|
|
Console.WriteLine("OK, model: " + s.Model);
|
|
break;
|
|
case Status.UNSATISFIABLE:
|
|
throw new TestFailedException();
|
|
}
|
|
}
|
|
|
|
static void ModelConverterTest(Context ctx)
|
|
{
|
|
Console.WriteLine("ModelConverterTest");
|
|
|
|
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);
|
|
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)));
|
|
|
|
ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g4);
|
|
if (ar.NumSubgoals == 1 && (ar.Subgoals[0].IsDecidedSat || ar.Subgoals[0].IsDecidedUnsat))
|
|
throw new TestFailedException();
|
|
|
|
ar = ApplyTactic(ctx, ctx.AndThen(ctx.MkTactic("simplify"), ctx.MkTactic("solve-eqs")), g4);
|
|
if (ar.NumSubgoals == 1 && (ar.Subgoals[0].IsDecidedSat || ar.Subgoals[0].IsDecidedUnsat))
|
|
throw new TestFailedException();
|
|
|
|
Solver s = ctx.MkSolver();
|
|
foreach (BoolExpr e in ar.Subgoals[0].Formulas)
|
|
s.Assert(e);
|
|
Status q = s.Check();
|
|
Console.WriteLine("Solver says: " + q);
|
|
Console.WriteLine("Model: \n" + s.Model);
|
|
if (q != Status.SATISFIABLE)
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
/// <summary>
|
|
/// A simple array example.
|
|
/// </summary>
|
|
/// <param name="ctx"></param>
|
|
static void ArrayExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("ArrayExample1");
|
|
|
|
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));
|
|
g.Assert(ctx.MkEq(sel, ctx.MkBV(42, 32)));
|
|
Symbol xs = ctx.MkSymbol("x");
|
|
IntExpr xc = (IntExpr)ctx.MkConst(xs, ctx.IntSort);
|
|
|
|
Symbol fname = ctx.MkSymbol("f");
|
|
Sort[] domain = { ctx.IntSort };
|
|
FuncDecl fd = ctx.MkFuncDecl(fname, domain, ctx.IntSort);
|
|
Expr[] fargs = { ctx.MkConst(xs, ctx.IntSort) };
|
|
IntExpr fapp = (IntExpr)ctx.MkApp(fd, fargs);
|
|
|
|
g.Assert(ctx.MkEq(ctx.MkAdd(xc, fapp), ctx.MkInt(123)));
|
|
|
|
Solver s = ctx.MkSolver();
|
|
foreach (BoolExpr a in g.Formulas)
|
|
s.Assert(a);
|
|
Console.WriteLine("Solver: " + s);
|
|
|
|
Status q = s.Check();
|
|
Console.WriteLine("Status: " + q);
|
|
|
|
if (q != Status.SATISFIABLE)
|
|
throw new TestFailedException();
|
|
|
|
Console.WriteLine("Model = " + s.Model);
|
|
|
|
Console.WriteLine("Interpretation of MyArray:\n" + s.Model.ConstInterp(aex.FuncDecl));
|
|
Console.WriteLine("Interpretation of x:\n" + s.Model.ConstInterp(xc));
|
|
Console.WriteLine("Interpretation of f:\n" + s.Model.FuncInterp(fd));
|
|
Console.WriteLine("Interpretation of MyArray as Term:\n" + s.Model.ConstInterp(aex.FuncDecl));
|
|
}
|
|
|
|
/// <summary>
|
|
/// Prove <tt>store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))</tt>.
|
|
/// </summary>
|
|
/// <remarks>This example demonstrates how to use the array theory.</remarks>
|
|
public static void ArrayExample2(Context ctx)
|
|
{
|
|
Console.WriteLine("ArrayExample2");
|
|
|
|
Sort int_type = ctx.IntSort;
|
|
Sort array_type = ctx.MkArraySort(int_type, int_type);
|
|
|
|
ArrayExpr a1 = (ArrayExpr)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);
|
|
|
|
Expr st1 = ctx.MkStore(a1, i1, v1);
|
|
Expr 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(new BoolExpr[] { 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);
|
|
Console.WriteLine("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))");
|
|
Console.WriteLine("{0}", (thm));
|
|
Prove(ctx, thm);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Show that <code>distinct(a_0, ... , a_n)</code> is
|
|
/// unsatisfiable when <code>a_i</code>'s are arrays from boolean to
|
|
/// boolean and n > 4.
|
|
/// </summary>
|
|
/// <remarks>This example also shows how to use the <code>distinct</code> construct.</remarks>
|
|
public static void ArrayExample3(Context ctx)
|
|
{
|
|
Console.WriteLine("ArrayExample3");
|
|
|
|
for (int n = 2; n <= 5; n++)
|
|
{
|
|
Console.WriteLine("n = {0}", n);
|
|
|
|
Sort bool_type = ctx.MkBoolSort();
|
|
Sort array_type = ctx.MkArraySort(bool_type, bool_type);
|
|
Expr[] a = new Expr[n];
|
|
|
|
/* create arrays */
|
|
for (int i = 0; i < n; i++)
|
|
{
|
|
a[i] = ctx.MkConst(String.Format("array_{0}", i), array_type);
|
|
}
|
|
|
|
/* assert distinct(a[0], ..., a[n]) */
|
|
BoolExpr d = ctx.MkDistinct(a);
|
|
Console.WriteLine("{0}", (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++)
|
|
{
|
|
Console.WriteLine("{0} = {1}",
|
|
a[i],
|
|
model.Evaluate(a[i]));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// Sudoku solving example.
|
|
/// </summary>
|
|
static void SudokuExample(Context ctx)
|
|
{
|
|
Console.WriteLine("SudokuExample");
|
|
|
|
// 9x9 matrix of integer variables
|
|
IntExpr[][] X = new IntExpr[9][];
|
|
for (uint i = 0; i < 9; i++)
|
|
{
|
|
X[i] = new IntExpr[9];
|
|
for (uint j = 0; j < 9; j++)
|
|
X[i][j] = (IntExpr)ctx.MkConst(ctx.MkSymbol("x_" + (i + 1) + "_" + (j + 1)), ctx.IntSort);
|
|
}
|
|
|
|
// each cell contains a value in {1, ..., 9}
|
|
Expr[][] cells_c = new Expr[9][];
|
|
for (uint i = 0; i < 9; i++)
|
|
{
|
|
cells_c[i] = new BoolExpr[9];
|
|
for (uint j = 0; j < 9; j++)
|
|
cells_c[i][j] = ctx.MkAnd(ctx.MkLe(ctx.MkInt(1), X[i][j]),
|
|
ctx.MkLe(X[i][j], ctx.MkInt(9)));
|
|
}
|
|
|
|
// each row contains a digit at most once
|
|
BoolExpr[] rows_c = new BoolExpr[9];
|
|
for (uint i = 0; i < 9; i++)
|
|
rows_c[i] = ctx.MkDistinct(X[i]);
|
|
|
|
// each column contains a digit at most once
|
|
BoolExpr[] cols_c = new BoolExpr[9];
|
|
for (uint j = 0; j < 9; j++)
|
|
{
|
|
IntExpr[] column = new IntExpr[9];
|
|
for (uint i = 0; i < 9; i++)
|
|
column[i] = X[i][j];
|
|
|
|
cols_c[j] = ctx.MkDistinct(column);
|
|
}
|
|
|
|
// each 3x3 square contains a digit at most once
|
|
BoolExpr[][] sq_c = new BoolExpr[3][];
|
|
for (uint i0 = 0; i0 < 3; i0++)
|
|
{
|
|
sq_c[i0] = new BoolExpr[3];
|
|
for (uint j0 = 0; j0 < 3; j0++)
|
|
{
|
|
IntExpr[] square = new IntExpr[9];
|
|
for (uint i = 0; i < 3; i++)
|
|
for (uint j = 0; j < 3; j++)
|
|
square[3 * i + j] = X[3 * i0 + i][3 * j0 + j];
|
|
sq_c[i0][j0] = ctx.MkDistinct(square);
|
|
}
|
|
}
|
|
|
|
BoolExpr sudoku_c = ctx.MkTrue();
|
|
foreach (BoolExpr[] t in cells_c)
|
|
sudoku_c = ctx.MkAnd(ctx.MkAnd(t), sudoku_c);
|
|
sudoku_c = ctx.MkAnd(ctx.MkAnd(rows_c), sudoku_c);
|
|
sudoku_c = ctx.MkAnd(ctx.MkAnd(cols_c), sudoku_c);
|
|
foreach (BoolExpr[] t in sq_c)
|
|
sudoku_c = ctx.MkAnd(ctx.MkAnd(t), sudoku_c);
|
|
|
|
// 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}};
|
|
|
|
BoolExpr instance_c = ctx.MkTrue();
|
|
for (uint i = 0; i < 9; i++)
|
|
for (uint j = 0; j < 9; j++)
|
|
instance_c = ctx.MkAnd(instance_c,
|
|
(BoolExpr)
|
|
ctx.MkITE(ctx.MkEq(ctx.MkInt(instance[i, j]), ctx.MkInt(0)),
|
|
ctx.MkTrue(),
|
|
ctx.MkEq(X[i][j], ctx.MkInt(instance[i, j]))));
|
|
|
|
Solver s = ctx.MkSolver();
|
|
s.Assert(sudoku_c);
|
|
s.Assert(instance_c);
|
|
|
|
if (s.Check() == Status.SATISFIABLE)
|
|
{
|
|
Model m = s.Model;
|
|
Expr[,] R = new Expr[9, 9];
|
|
for (uint i = 0; i < 9; i++)
|
|
for (uint j = 0; j < 9; j++)
|
|
R[i, j] = m.Evaluate(X[i][j]);
|
|
Console.WriteLine("Sudoku solution:");
|
|
for (uint i = 0; i < 9; i++)
|
|
{
|
|
for (uint j = 0; j < 9; j++)
|
|
Console.Write(" " + R[i, j]);
|
|
Console.WriteLine();
|
|
}
|
|
}
|
|
else
|
|
{
|
|
Console.WriteLine("Failed to solve sudoku");
|
|
throw new TestFailedException();
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// A basic example of how to use quantifiers.
|
|
/// </summary>
|
|
static void QuantifierExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("QuantifierExample");
|
|
|
|
Sort[] types = new Sort[3];
|
|
IntExpr[] xs = new IntExpr[3];
|
|
Symbol[] names = new Symbol[3];
|
|
IntExpr[] vars = new IntExpr[3];
|
|
|
|
for (uint j = 0; j < 3; j++)
|
|
{
|
|
types[j] = ctx.IntSort;
|
|
names[j] = ctx.MkSymbol(String.Format("x_{0}", j));
|
|
xs[j] = (IntExpr)ctx.MkConst(names[j], types[j]);
|
|
vars[j] = (IntExpr)ctx.MkBound(2 - j, types[j]); // <-- vars reversed!
|
|
}
|
|
|
|
Expr body_vars = ctx.MkAnd(ctx.MkEq(ctx.MkAdd(vars[0], ctx.MkInt(1)), ctx.MkInt(2)),
|
|
ctx.MkEq(ctx.MkAdd(vars[1], ctx.MkInt(2)),
|
|
ctx.MkAdd(vars[2], ctx.MkInt(3))));
|
|
|
|
Expr body_const = ctx.MkAnd(ctx.MkEq(ctx.MkAdd(xs[0], ctx.MkInt(1)), ctx.MkInt(2)),
|
|
ctx.MkEq(ctx.MkAdd(xs[1], ctx.MkInt(2)),
|
|
ctx.MkAdd(xs[2], ctx.MkInt(3))));
|
|
|
|
Expr x = ctx.MkForall(types, names, body_vars, 1, null, null, ctx.MkSymbol("Q1"), ctx.MkSymbol("skid1"));
|
|
Console.WriteLine("Quantifier X: " + x.ToString());
|
|
|
|
Expr y = ctx.MkForall(xs, body_const, 1, null, null, ctx.MkSymbol("Q2"), ctx.MkSymbol("skid2"));
|
|
Console.WriteLine("Quantifier Y: " + y.ToString());
|
|
}
|
|
|
|
static void QuantifierExample2(Context ctx)
|
|
{
|
|
|
|
Console.WriteLine("QuantifierExample2");
|
|
|
|
Expr q1, q2;
|
|
FuncDecl f = ctx.MkFuncDecl("f", ctx.IntSort, ctx.IntSort);
|
|
FuncDecl g = ctx.MkFuncDecl("g", ctx.IntSort, ctx.IntSort);
|
|
|
|
// Quantifier with Exprs as the bound variables.
|
|
{
|
|
Expr x = ctx.MkConst("x", ctx.IntSort);
|
|
Expr y = ctx.MkConst("y", ctx.IntSort);
|
|
Expr f_x = ctx.MkApp(f, x);
|
|
Expr f_y = ctx.MkApp(f, y);
|
|
Expr g_y = ctx.MkApp(g, y);
|
|
Expr[] no_pats = new Expr[] { f_y };
|
|
Expr[] bound = new Expr[2] { x, y };
|
|
Expr 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"));
|
|
|
|
Console.WriteLine("{0}", q1);
|
|
}
|
|
|
|
// Quantifier with de-Bruijn indices.
|
|
{
|
|
Expr x = ctx.MkBound(1, ctx.IntSort);
|
|
Expr y = ctx.MkBound(0, ctx.IntSort);
|
|
Expr f_x = ctx.MkApp(f, x);
|
|
Expr f_y = ctx.MkApp(f, y);
|
|
Expr g_y = ctx.MkApp(g, y);
|
|
Expr[] no_pats = new Expr[] { f_y };
|
|
Symbol[] names = new Symbol[] { ctx.MkSymbol("x"), ctx.MkSymbol("y") };
|
|
Sort[] sorts = new Sort[] { ctx.IntSort, ctx.IntSort };
|
|
Expr 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")
|
|
);
|
|
Console.WriteLine("{0}", q2);
|
|
}
|
|
|
|
Console.WriteLine("{0}", (q1.Equals(q2)));
|
|
}
|
|
|
|
/// <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 QuantifierExample3(Context ctx)
|
|
{
|
|
Console.WriteLine("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 */
|
|
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);
|
|
|
|
/* 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);
|
|
|
|
/* 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);
|
|
}
|
|
|
|
/// <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(Context ctx)
|
|
{
|
|
Console.WriteLine("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 */
|
|
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);
|
|
|
|
/* 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);
|
|
|
|
/* 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);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Some basic tests.
|
|
/// </summary>
|
|
static void BasicTests(Context ctx)
|
|
{
|
|
Console.WriteLine("BasicTests");
|
|
|
|
Symbol fname = ctx.MkSymbol("f");
|
|
Symbol x = ctx.MkSymbol("x");
|
|
Symbol y = ctx.MkSymbol("y");
|
|
|
|
Sort 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);
|
|
g.Assert(trivial_eq);
|
|
g.Assert(nontrivial_eq);
|
|
Console.WriteLine("Goal: " + g);
|
|
|
|
Solver solver = ctx.MkSolver();
|
|
|
|
foreach (BoolExpr a in g.Formulas)
|
|
solver.Assert(a);
|
|
|
|
if (solver.Check() != Status.SATISFIABLE)
|
|
throw new TestFailedException();
|
|
|
|
ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g);
|
|
if (ar.NumSubgoals == 1 && (ar.Subgoals[0].IsDecidedSat || ar.Subgoals[0].IsDecidedUnsat))
|
|
throw new TestFailedException();
|
|
|
|
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g);
|
|
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedSat)
|
|
throw new TestFailedException();
|
|
|
|
g.Assert(ctx.MkEq(ctx.MkNumeral(1, ctx.MkBitVecSort(32)),
|
|
ctx.MkNumeral(2, ctx.MkBitVecSort(32))));
|
|
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g);
|
|
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedUnsat)
|
|
throw new TestFailedException();
|
|
|
|
|
|
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);
|
|
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);
|
|
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)));
|
|
g3.Assert(ctx.MkEq(yc, ctx.MkNumeral(2, ctx.IntSort)));
|
|
BoolExpr constr = ctx.MkEq(xc, yc);
|
|
g3.Assert(constr);
|
|
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g3);
|
|
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedUnsat)
|
|
throw new TestFailedException();
|
|
|
|
ModelConverterTest(ctx);
|
|
|
|
// Real num/den test.
|
|
RatNum rn = ctx.MkReal(42, 43);
|
|
Expr inum = rn.Numerator;
|
|
Expr iden = rn.Denominator;
|
|
Console.WriteLine("Numerator: " + inum + " Denominator: " + iden);
|
|
if (inum.ToString() != "42" || iden.ToString() != "43")
|
|
throw new TestFailedException();
|
|
|
|
if (rn.ToDecimalString(3) != "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"));
|
|
|
|
|
|
#if !FRAMEWORK_LT_4
|
|
string bn = "1234567890987654321";
|
|
|
|
if (ctx.MkInt(bn).BigInteger.ToString() != bn)
|
|
throw new TestFailedException();
|
|
|
|
if (ctx.MkBV(bn, 128).BigInteger.ToString() != bn)
|
|
throw new TestFailedException();
|
|
|
|
if (ctx.MkBV(bn, 32).BigInteger.ToString() == bn)
|
|
throw new TestFailedException();
|
|
#endif
|
|
|
|
// Error handling test.
|
|
try
|
|
{
|
|
IntExpr i = ctx.MkInt("1/2");
|
|
throw new TestFailedException(); // unreachable
|
|
}
|
|
catch (Z3Exception)
|
|
{
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// Some basic expression casting tests.
|
|
/// </summary>
|
|
static void CastingTest(Context ctx)
|
|
{
|
|
Console.WriteLine("CastingTest");
|
|
|
|
Sort[] domain = { ctx.BoolSort, ctx.BoolSort };
|
|
FuncDecl f = ctx.MkFuncDecl("f", domain, ctx.BoolSort);
|
|
|
|
AST upcast = ctx.MkFuncDecl(ctx.MkSymbol("q"), domain, ctx.BoolSort);
|
|
|
|
try
|
|
{
|
|
FuncDecl downcast = (FuncDecl)f; // OK
|
|
}
|
|
catch (InvalidCastException)
|
|
{
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
try
|
|
{
|
|
Expr uc = (Expr)upcast;
|
|
throw new TestFailedException(); // should not be reachable!
|
|
}
|
|
catch (InvalidCastException)
|
|
{
|
|
}
|
|
|
|
Symbol s = ctx.MkSymbol(42);
|
|
IntSymbol si = s as IntSymbol;
|
|
if (si == null) throw new TestFailedException();
|
|
try
|
|
{
|
|
IntSymbol si2 = (IntSymbol)s;
|
|
}
|
|
catch (InvalidCastException)
|
|
{
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
s = ctx.MkSymbol("abc");
|
|
StringSymbol ss = s as StringSymbol;
|
|
if (ss == null) throw new TestFailedException();
|
|
try
|
|
{
|
|
StringSymbol ss2 = (StringSymbol)s;
|
|
}
|
|
catch (InvalidCastException)
|
|
{
|
|
throw new TestFailedException();
|
|
}
|
|
try
|
|
{
|
|
IntSymbol si2 = (IntSymbol)s;
|
|
throw new TestFailedException(); // unreachable
|
|
}
|
|
catch
|
|
{
|
|
}
|
|
|
|
Sort srt = ctx.MkBitVecSort(32);
|
|
BitVecSort bvs = null;
|
|
try
|
|
{
|
|
bvs = (BitVecSort)srt;
|
|
}
|
|
catch (InvalidCastException)
|
|
{
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
if (bvs.Size != 32)
|
|
throw new TestFailedException();
|
|
|
|
Expr q = ctx.MkAdd(ctx.MkInt(1), ctx.MkInt(2));
|
|
Expr q2 = q.Args[1];
|
|
Sort qs = q2.Sort;
|
|
if (qs as IntSort == null)
|
|
throw new TestFailedException();
|
|
try
|
|
{
|
|
IntSort isrt = (IntSort)qs;
|
|
}
|
|
catch (InvalidCastException)
|
|
{
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
AST a = ctx.MkInt(42);
|
|
Expr ae = a as Expr;
|
|
if (ae == null) throw new TestFailedException();
|
|
ArithExpr aae = a as ArithExpr;
|
|
if (aae == null) throw new TestFailedException();
|
|
IntExpr aie = a as IntExpr;
|
|
if (aie == null) throw new TestFailedException();
|
|
IntNum ain = a as IntNum;
|
|
if (ain == null) throw new TestFailedException();
|
|
|
|
|
|
Expr[][] earr = new Expr[2][];
|
|
earr[0] = new Expr[2];
|
|
earr[1] = new Expr[2];
|
|
earr[0][0] = ctx.MkTrue();
|
|
earr[0][1] = ctx.MkTrue();
|
|
earr[1][0] = ctx.MkFalse();
|
|
earr[1][1] = ctx.MkFalse();
|
|
foreach (Expr[] ea in earr)
|
|
foreach (Expr e in ea)
|
|
{
|
|
try
|
|
{
|
|
Expr ns = ctx.MkNot((BoolExpr)e);
|
|
BoolExpr ens = (BoolExpr)ns;
|
|
}
|
|
catch (InvalidCastException)
|
|
{
|
|
throw new TestFailedException();
|
|
}
|
|
}
|
|
}
|
|
|
|
|
|
/// <summary>
|
|
/// Shows how to read an SMT2 file.
|
|
/// </summary>
|
|
static void SMT2FileTest(string filename)
|
|
{
|
|
System.DateTime before = System.DateTime.Now;
|
|
|
|
Console.WriteLine("SMT2 File test ");
|
|
System.GC.Collect();
|
|
|
|
using (Context ctx = new Context(new Dictionary<string, string>() { { "MODEL", "true" } }))
|
|
{
|
|
BoolExpr[] fmls = ctx.ParseSMTLIB2File(filename);
|
|
BoolExpr a = ctx.MkAnd(fmls);
|
|
|
|
Console.WriteLine("SMT2 file read time: " + (System.DateTime.Now - before).TotalSeconds + " sec");
|
|
|
|
// Iterate over the formula.
|
|
|
|
Queue q = new Queue();
|
|
q.Enqueue(a);
|
|
uint cnt = 0;
|
|
while (q.Count > 0)
|
|
{
|
|
AST cur = (AST)q.Dequeue();
|
|
cnt++;
|
|
|
|
// This here ...
|
|
if (cur is Expr)
|
|
if (!(cur.IsVar))
|
|
foreach (Expr c in ((Expr)cur).Args)
|
|
q.Enqueue(c);
|
|
|
|
// Takes the same time as this:
|
|
//switch ((cur).ASTKind)
|
|
//{
|
|
// case Z3_ast_kind.Z3_APP_AST:
|
|
// foreach (Expr e in ((Expr)cur).Args)
|
|
// q.Enqueue(e);
|
|
// break;
|
|
// case Z3_ast_kind.Z3_QUANTIFIER_AST:
|
|
// q.Enqueue(((Quantifier)cur).Args[0]);
|
|
// break;
|
|
// case Z3_ast_kind.Z3_VAR_AST: break;
|
|
// case Z3_ast_kind.Z3_NUMERAL_AST: break;
|
|
// case Z3_ast_kind.Z3_FUNC_DECL_AST: break;
|
|
// case Z3_ast_kind.Z3_SORT_AST: break;
|
|
//}
|
|
}
|
|
Console.WriteLine(cnt + " ASTs");
|
|
}
|
|
|
|
Console.WriteLine("SMT2 file test took " + (System.DateTime.Now - before).TotalSeconds + " sec");
|
|
}
|
|
|
|
/// <summary>
|
|
/// Shows how to use Solver(logic)
|
|
/// </summary>
|
|
/// <param name="ctx"></param>
|
|
static void LogicExample(Context ctx)
|
|
{
|
|
Console.WriteLine("LogicTest");
|
|
|
|
Microsoft.Z3.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.Assert(eq);
|
|
Status res = s.Check();
|
|
Console.WriteLine("solver result: " + res);
|
|
|
|
|
|
// Or perhaps a tactic for QF_BV
|
|
Goal g = ctx.MkGoal(true);
|
|
g.Assert(eq);
|
|
|
|
Tactic t = ctx.MkTactic("qfbv");
|
|
ApplyResult ar = t.Apply(g);
|
|
Console.WriteLine("tactic result: " + ar);
|
|
|
|
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedSat)
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
/// <summary>
|
|
/// Demonstrates how to use the ParOr tactic.
|
|
/// </summary>
|
|
static void ParOrExample(Context ctx)
|
|
{
|
|
Console.WriteLine("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);
|
|
g.Assert(q);
|
|
|
|
Tactic t1 = ctx.MkTactic("qfbv");
|
|
Tactic t2 = ctx.MkTactic("qfbv");
|
|
Tactic p = ctx.ParOr(t1, t2);
|
|
|
|
ApplyResult ar = p.Apply(g);
|
|
|
|
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedSat)
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
static void BigIntCheck(Context ctx, RatNum r)
|
|
{
|
|
#if !FRAMEWORK_LT_4
|
|
Console.WriteLine("Num: " + r.BigIntNumerator);
|
|
Console.WriteLine("Den: " + r.BigIntDenominator);
|
|
#endif
|
|
}
|
|
|
|
/// <summary>
|
|
/// Find a model for <code>x xor y</code>.
|
|
/// </summary>
|
|
public static void FindModelExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("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);
|
|
Console.WriteLine("x = {0}, y = {1}",
|
|
model.Evaluate(x),
|
|
model.Evaluate(y));
|
|
}
|
|
|
|
/// <summary>
|
|
/// Find a model for <tt>x < y + 1, x > 2</tt>.
|
|
/// Then, assert <tt>not(x = y)</tt>, and find another model.
|
|
/// </summary>
|
|
public static void FindModelExample2(Context ctx)
|
|
{
|
|
Console.WriteLine("FindModelExample2");
|
|
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
IntExpr y = ctx.MkIntConst("y");
|
|
IntExpr one = ctx.MkInt(1);
|
|
IntExpr 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);
|
|
|
|
Console.WriteLine("model for: x < y + 1, x > 2");
|
|
Model model = Check(ctx, q, Status.SATISFIABLE);
|
|
Console.WriteLine("x = {0}, y = {1}",
|
|
(model.Evaluate(x)),
|
|
(model.Evaluate(y)));
|
|
|
|
/* assert not(x = y) */
|
|
BoolExpr x_eq_y = ctx.MkEq(x, y);
|
|
BoolExpr c3 = ctx.MkNot(x_eq_y);
|
|
|
|
q = ctx.MkAnd(q, c3);
|
|
|
|
Console.WriteLine("model for: x < y + 1, x > 2, not(x = y)");
|
|
model = Check(ctx, q, Status.SATISFIABLE);
|
|
Console.WriteLine("x = {0}, y = {1}",
|
|
(model.Evaluate(x)),
|
|
(model.Evaluate(y)));
|
|
}
|
|
|
|
/// <summary>
|
|
/// Prove <tt>x = y implies g(x) = g(y)</tt>, and
|
|
/// disprove <tt>x = y implies g(g(x)) = g(y)</tt>.
|
|
/// </summary>
|
|
/// <remarks>This function demonstrates how to create uninterpreted
|
|
/// types and functions.</remarks>
|
|
public static void ProveExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("ProveExample1");
|
|
|
|
/* create uninterpreted type. */
|
|
Sort 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[x];
|
|
Expr gy = g[y];
|
|
|
|
/* assert x = y */
|
|
BoolExpr eq = ctx.MkEq(x, y);
|
|
|
|
/* prove g(x) = g(y) */
|
|
BoolExpr f = ctx.MkEq(gx, gy);
|
|
Console.WriteLine("prove: x = y implies g(x) = g(y)");
|
|
Prove(ctx, ctx.MkImplies(eq, f));
|
|
|
|
/* create g(g(x)) */
|
|
Expr ggx = g[gx];
|
|
|
|
/* disprove g(g(x)) = g(y) */
|
|
f = ctx.MkEq(ggx, gy);
|
|
Console.WriteLine("disprove: x = y implies g(g(x)) = g(y)");
|
|
Disprove(ctx, ctx.MkImplies(eq, f));
|
|
|
|
|
|
/* Print the model using the custom model printer */
|
|
Model m = Check(ctx, ctx.MkNot(f), Status.SATISFIABLE);
|
|
Console.WriteLine(m);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Prove <tt>not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 </tt>.
|
|
/// Then, show that <tt>z < -1</tt> is not implied.
|
|
/// </summary>
|
|
/// <remarks>This example demonstrates how to combine uninterpreted functions
|
|
/// and arithmetic.</remarks>
|
|
public static void ProveExample2(Context ctx)
|
|
{
|
|
Console.WriteLine("ProveExample2");
|
|
|
|
/* declare function g */
|
|
Sort I = ctx.IntSort;
|
|
|
|
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 */
|
|
IntExpr zero = ctx.MkInt(0);
|
|
|
|
/* assert not(g(g(x) - g(y)) = g(z)) */
|
|
ArithExpr gx_gy = ctx.MkSub((IntExpr)gx, (IntExpr)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);
|
|
Console.WriteLine("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 */
|
|
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, false, c1, c2, c3);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Show how push & pop can be used to create "backtracking" points.
|
|
/// </summary>
|
|
/// <remarks>This example also demonstrates how big numbers can be
|
|
/// created in ctx.</remarks>
|
|
public static void PushPopExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("PushPopExample1");
|
|
|
|
/* create a big number */
|
|
IntSort int_type = ctx.IntSort;
|
|
IntExpr 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);
|
|
Console.WriteLine("assert: x >= 'big number'");
|
|
solver.Assert(c1);
|
|
|
|
/* create a backtracking point */
|
|
Console.WriteLine("push");
|
|
solver.Push();
|
|
|
|
/* assert x <= 3 */
|
|
BoolExpr c2 = ctx.MkLe(x, three);
|
|
Console.WriteLine("assert: x <= 3");
|
|
solver.Assert(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. */
|
|
Console.WriteLine("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);
|
|
Console.WriteLine("assert: y > x");
|
|
solver.Assert(c3);
|
|
|
|
/* the context is still consistent. */
|
|
if (solver.Check() != Status.SATISFIABLE)
|
|
throw new TestFailedException();
|
|
}
|
|
|
|
/// <summary>
|
|
/// Tuples.
|
|
/// </summary>
|
|
/// <remarks>Check that the projection of a tuple
|
|
/// returns the corresponding element.</remarks>
|
|
public static void TupleExample(Context ctx)
|
|
{
|
|
Console.WriteLine("TupleExample");
|
|
|
|
Sort int_type = ctx.IntSort;
|
|
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 = tuple.FieldDecls[0]; // declarations are for projections
|
|
// FuncDecl second = tuple.FieldDecls[1];
|
|
Expr x = ctx.MkConst("x", int_type);
|
|
Expr y = ctx.MkConst("y", int_type);
|
|
Expr n1 = tuple.MkDecl[x, y];
|
|
Expr n2 = first[n1];
|
|
BoolExpr n3 = ctx.MkEq(x, n2);
|
|
Console.WriteLine("Tuple example: {0}", n3);
|
|
Prove(ctx, n3);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Simple bit-vector example.
|
|
/// </summary>
|
|
/// <remarks>
|
|
/// This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers
|
|
/// </remarks>
|
|
public static void BitvectorExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("BitvectorExample1");
|
|
|
|
Sort 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);
|
|
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);
|
|
Console.WriteLine("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers");
|
|
Disprove(ctx, thm);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Find x and y such that: x ^ y - 103 == x * y
|
|
/// </summary>
|
|
public static void BitvectorExample2(Context ctx)
|
|
{
|
|
Console.WriteLine("BitvectorExample2");
|
|
|
|
/* construct x ^ y - 103 == x * y */
|
|
Sort 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);
|
|
BitVecExpr c103 = (BitVecNum)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);
|
|
|
|
Console.WriteLine("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);
|
|
Console.WriteLine(m);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Demonstrates how to use the SMTLIB parser.
|
|
/// </summary>
|
|
public static void ParserExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("ParserExample1");
|
|
|
|
var fmls = ctx.ParseSMTLIB2String("(declare-const x Int) (declare-const y Int) (assert (> x y)) (assert (> x 0))");
|
|
var fml = ctx.MkAnd(fmls);
|
|
|
|
Console.WriteLine("formula {0}", fml);
|
|
|
|
Model m = Check(ctx, fml, Status.SATISFIABLE);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Demonstrates how to initialize the parser symbol table.
|
|
/// </summary>
|
|
public static void ParserExample2(Context ctx)
|
|
{
|
|
Console.WriteLine("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];
|
|
Console.WriteLine("formula: {0}", f);
|
|
Check(ctx, f, Status.SATISFIABLE);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Demonstrates how to initialize the parser symbol table.
|
|
/// </summary>
|
|
public static void ParserExample3(Context ctx)
|
|
{
|
|
Console.WriteLine("ParserExample3");
|
|
|
|
/* declare function g */
|
|
Sort I = ctx.MkIntSort();
|
|
FuncDecl g = ctx.MkFuncDecl("g", new Sort[] { I, I }, I);
|
|
|
|
BoolExpr ca = CommAxiom(ctx, g);
|
|
|
|
BoolExpr thm = ctx.ParseSMTLIB2String("(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];
|
|
|
|
Console.WriteLine("formula: {0}", thm);
|
|
Prove(ctx, thm, false, ca);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Demonstrates how to handle parser errors using Z3 error handling support.
|
|
/// </summary>
|
|
/// <remarks></remarks>
|
|
public static void ParserExample5(Context ctx)
|
|
{
|
|
Console.WriteLine("ParserExample5");
|
|
|
|
try
|
|
{
|
|
ctx.ParseSMTLIB2String(
|
|
/* the following string has a parsing error: missing parenthesis */
|
|
"(declare-const x Int (declare-const y Int)) (assert (> x y))");
|
|
}
|
|
catch (Z3Exception e)
|
|
{
|
|
Console.WriteLine("Z3 error: {0}", e);
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// Create an ite-Expr (if-then-else Exprs).
|
|
/// </summary>
|
|
public static void ITEExample(Context ctx)
|
|
{
|
|
Console.WriteLine("ITEExample");
|
|
|
|
BoolExpr f = ctx.MkFalse();
|
|
Expr one = ctx.MkInt(1);
|
|
Expr zero = ctx.MkInt(0);
|
|
Expr ite = ctx.MkITE(f, one, zero);
|
|
|
|
Console.WriteLine("Expr: {0}", ite);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Create an enumeration data type.
|
|
/// </summary>
|
|
public static void EnumExample(Context ctx)
|
|
{
|
|
Console.WriteLine("EnumExample");
|
|
|
|
Symbol name = ctx.MkSymbol("fruit");
|
|
|
|
EnumSort fruit = ctx.MkEnumSort(ctx.MkSymbol("fruit"), new Symbol[] { ctx.MkSymbol("apple"), ctx.MkSymbol("banana"), ctx.MkSymbol("orange") });
|
|
|
|
Console.WriteLine("{0}", (fruit.Consts[0]));
|
|
Console.WriteLine("{0}", (fruit.Consts[1]));
|
|
Console.WriteLine("{0}", (fruit.Consts[2]));
|
|
|
|
Console.WriteLine("{0}", (fruit.TesterDecls[0]));
|
|
Console.WriteLine("{0}", (fruit.TesterDecls[1]));
|
|
Console.WriteLine("{0}", (fruit.TesterDecls[2]));
|
|
|
|
Expr apple = fruit.Consts[0];
|
|
Expr banana = fruit.Consts[1];
|
|
Expr orange = fruit.Consts[2];
|
|
|
|
/* Apples are different from oranges */
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(apple, orange)));
|
|
|
|
/* Apples pass the apple test */
|
|
Prove(ctx, (BoolExpr)ctx.MkApp(fruit.TesterDecls[0], apple));
|
|
|
|
/* Oranges fail the apple test */
|
|
Disprove(ctx, (BoolExpr)ctx.MkApp(fruit.TesterDecls[0], orange));
|
|
Prove(ctx, (BoolExpr)ctx.MkNot((BoolExpr)ctx.MkApp(fruit.TesterDecls[0], orange)));
|
|
|
|
Expr fruity = ctx.MkConst("fruity", fruit);
|
|
|
|
/* If something is fruity, then it is an apple, banana, or orange */
|
|
|
|
Prove(ctx, ctx.MkOr(new BoolExpr[] { ctx.MkEq(fruity, apple), ctx.MkEq(fruity, banana), ctx.MkEq(fruity, orange) }));
|
|
}
|
|
|
|
/// <summary>
|
|
/// Create a list datatype.
|
|
/// </summary>
|
|
public static void ListExample(Context ctx)
|
|
{
|
|
Console.WriteLine("ListExample");
|
|
|
|
Sort int_ty;
|
|
ListSort int_list;
|
|
Expr nil, l1, l2, x, y, u, v;
|
|
BoolExpr fml, fml1;
|
|
|
|
int_ty = ctx.MkIntSort();
|
|
|
|
int_list = ctx.MkListSort(ctx.MkSymbol("int_list"), int_ty);
|
|
|
|
nil = ctx.MkConst(int_list.NilDecl);
|
|
l1 = ctx.MkApp(int_list.ConsDecl, ctx.MkInt(1), nil);
|
|
l2 = ctx.MkApp(int_list.ConsDecl, ctx.MkInt(2), nil);
|
|
|
|
/* nil != cons(1, nil) */
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1)));
|
|
|
|
/* cons(2,nil) != cons(1, nil) */
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(l1, l2)));
|
|
|
|
/* 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, x, nil);
|
|
l2 = ctx.MkApp(int_list.ConsDecl, y, nil);
|
|
Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)));
|
|
|
|
/* 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, x, u);
|
|
l2 = ctx.MkApp(int_list.ConsDecl, 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)));
|
|
|
|
/* is_nil(u) or is_cons(u) */
|
|
Prove(ctx, ctx.MkOr((BoolExpr)ctx.MkApp(int_list.IsNilDecl, u),
|
|
(BoolExpr)ctx.MkApp(int_list.IsConsDecl, u)));
|
|
|
|
/* occurs check u != cons(x,u) */
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)));
|
|
|
|
/* destructors: is_cons(u) => u = cons(head(u),tail(u)) */
|
|
fml1 = ctx.MkEq(u, ctx.MkApp(int_list.ConsDecl, ctx.MkApp(int_list.HeadDecl, u),
|
|
ctx.MkApp(int_list.TailDecl, u)));
|
|
fml = ctx.MkImplies((BoolExpr)ctx.MkApp(int_list.IsConsDecl, u), fml1);
|
|
Console.WriteLine("Formula {0}", fml);
|
|
|
|
Prove(ctx, fml);
|
|
|
|
Disprove(ctx, fml1);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Create a binary tree datatype.
|
|
/// </summary>
|
|
public static void TreeExample(Context ctx)
|
|
{
|
|
Console.WriteLine("TreeExample");
|
|
|
|
Sort cell;
|
|
FuncDecl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl;
|
|
Expr nil, l1, l2, x, y, u, v;
|
|
BoolExpr fml, fml1;
|
|
string[] head_tail = new string[] { "car", "cdr" };
|
|
Sort[] sorts = new Sort[] { null, null };
|
|
uint[] sort_refs = new uint[] { 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 };
|
|
|
|
cell = ctx.MkDatatypeSort("cell", constructors);
|
|
|
|
nil_decl = nil_con.ConstructorDecl;
|
|
is_nil_decl = nil_con.TesterDecl;
|
|
cons_decl = cons_con.ConstructorDecl;
|
|
is_cons_decl = cons_con.TesterDecl;
|
|
FuncDecl[] cons_accessors = cons_con.AccessorDecls;
|
|
car_decl = cons_accessors[0];
|
|
cdr_decl = cons_accessors[1];
|
|
|
|
nil = ctx.MkConst(nil_decl);
|
|
l1 = ctx.MkApp(cons_decl, nil, nil);
|
|
l2 = ctx.MkApp(cons_decl, l1, nil);
|
|
|
|
/* nil != cons(nil, nil) */
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1)));
|
|
|
|
/* cons(x,u) = cons(x, v) => u = v */
|
|
u = ctx.MkConst("u", cell);
|
|
v = ctx.MkConst("v", cell);
|
|
x = ctx.MkConst("x", cell);
|
|
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)));
|
|
Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)));
|
|
|
|
/* is_nil(u) or is_cons(u) */
|
|
Prove(ctx, ctx.MkOr((BoolExpr)ctx.MkApp(is_nil_decl, u), (BoolExpr)ctx.MkApp(is_cons_decl, u)));
|
|
|
|
/* occurs check u != cons(x,u) */
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)));
|
|
|
|
/* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
|
|
fml1 = ctx.MkEq(u, ctx.MkApp(cons_decl, ctx.MkApp(car_decl, u), ctx.MkApp(cdr_decl, u)));
|
|
fml = ctx.MkImplies((BoolExpr)ctx.MkApp(is_cons_decl, u), fml1);
|
|
Console.WriteLine("Formula {0}", fml);
|
|
Prove(ctx, fml);
|
|
|
|
Disprove(ctx, fml1);
|
|
}
|
|
|
|
/// <summary>
|
|
/// Create a forest of trees.
|
|
/// </summary>
|
|
/// <remarks>
|
|
/// forest ::= nil | cons(tree, forest)
|
|
/// tree ::= nil | cons(forest, forest)
|
|
/// </remarks>
|
|
public static void ForestExample(Context ctx)
|
|
{
|
|
Console.WriteLine("ForestExample");
|
|
|
|
Sort tree, forest;
|
|
FuncDecl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl;
|
|
FuncDecl nil2_decl, is_nil2_decl, cons2_decl, is_cons2_decl, car2_decl, cdr2_decl;
|
|
Expr nil1, nil2, t1, t2, t3, t4, f1, f2, f3, l1, l2, x, y, u, v;
|
|
|
|
//
|
|
// 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 };
|
|
uint[] sort1_refs = new uint[] { 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 };
|
|
uint[] sort2_refs = new uint[] { 0, 0 }; // both items point to the forest datatype.
|
|
Constructor nil1_con, cons1_con, nil2_con, cons2_con;
|
|
Constructor[] constructors1 = new Constructor[2], constructors2 = new Constructor[2];
|
|
Symbol[] sort_names = { ctx.MkSymbol("forest"), ctx.MkSymbol("tree") };
|
|
|
|
/* build a forest */
|
|
nil1_con = ctx.MkConstructor(ctx.MkSymbol("nil"), ctx.MkSymbol("is_nil"), 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 = sorts[0];
|
|
tree = 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.TesterDecl;
|
|
cons1_decl = cons1_con.ConstructorDecl;
|
|
is_cons1_decl = cons1_con.TesterDecl;
|
|
FuncDecl[] cons1_accessors = cons1_con.AccessorDecls;
|
|
car1_decl = cons1_accessors[0];
|
|
cdr1_decl = cons1_accessors[1];
|
|
|
|
nil2_decl = nil2_con.ConstructorDecl;
|
|
is_nil2_decl = nil2_con.TesterDecl;
|
|
cons2_decl = cons2_con.ConstructorDecl;
|
|
is_cons2_decl = cons2_con.TesterDecl;
|
|
FuncDecl[] cons2_accessors = cons2_con.AccessorDecls;
|
|
car2_decl = cons2_accessors[0];
|
|
cdr2_decl = cons2_accessors[1];
|
|
|
|
|
|
nil1 = ctx.MkConst(nil1_decl);
|
|
nil2 = ctx.MkConst(nil2_decl);
|
|
f1 = ctx.MkApp(cons1_decl, nil2, nil1);
|
|
t1 = ctx.MkApp(cons2_decl, nil1, nil1);
|
|
t2 = ctx.MkApp(cons2_decl, f1, nil1);
|
|
t3 = ctx.MkApp(cons2_decl, f1, f1);
|
|
t4 = ctx.MkApp(cons2_decl, nil1, f1);
|
|
f2 = ctx.MkApp(cons1_decl, t1, nil1);
|
|
f3 = ctx.MkApp(cons1_decl, t1, f1);
|
|
|
|
|
|
/* nil != cons(nil,nil) */
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(nil1, f1)));
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(nil2, t1)));
|
|
|
|
|
|
/* cons(x,u) = cons(x, v) => u = v */
|
|
u = ctx.MkConst("u", forest);
|
|
v = ctx.MkConst("v", forest);
|
|
x = ctx.MkConst("x", tree);
|
|
y = ctx.MkConst("y", tree);
|
|
l1 = ctx.MkApp(cons1_decl, x, u);
|
|
l2 = ctx.MkApp(cons1_decl, 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)));
|
|
|
|
/* is_nil(u) or is_cons(u) */
|
|
Prove(ctx, ctx.MkOr((BoolExpr)ctx.MkApp(is_nil1_decl, u),
|
|
(BoolExpr)ctx.MkApp(is_cons1_decl, u)));
|
|
|
|
/* occurs check u != cons(x,u) */
|
|
Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)));
|
|
}
|
|
|
|
/// <summary>
|
|
/// Demonstrate how to use #Eval.
|
|
/// </summary>
|
|
public static void EvalExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("EvalExample1");
|
|
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
IntExpr y = ctx.MkIntConst("y");
|
|
IntExpr two = ctx.MkInt(2);
|
|
|
|
Solver solver = ctx.MkSolver();
|
|
|
|
/* assert x < y */
|
|
solver.Assert(ctx.MkLt(x, y));
|
|
|
|
/* assert x > 2 */
|
|
solver.Assert(ctx.MkGt(x, two));
|
|
|
|
/* find model for the constraints above */
|
|
Model model = null;
|
|
if (Status.SATISFIABLE == solver.Check())
|
|
{
|
|
model = solver.Model;
|
|
Console.WriteLine("{0}", model);
|
|
Console.WriteLine("\nevaluating x+y");
|
|
Expr v = model.Evaluate(ctx.MkAdd(x, y));
|
|
if (v != null)
|
|
{
|
|
Console.WriteLine("result = {0}", (v));
|
|
}
|
|
else
|
|
{
|
|
Console.WriteLine("Failed to evaluate: x+y");
|
|
}
|
|
}
|
|
else
|
|
{
|
|
Console.WriteLine("BUG, the constraints are satisfiable.");
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// Demonstrate how to use #Eval on tuples.
|
|
/// </summary>
|
|
public static void EvalExample2(Context ctx)
|
|
{
|
|
Console.WriteLine("EvalExample2");
|
|
|
|
Sort int_type = ctx.IntSort;
|
|
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 = tuple.FieldDecls[0]; // declarations are for projections
|
|
FuncDecl second = tuple.FieldDecls[1];
|
|
Expr tup1 = ctx.MkConst("t1", tuple);
|
|
Expr tup2 = ctx.MkConst("t2", tuple);
|
|
|
|
Solver solver = ctx.MkSolver();
|
|
|
|
/* assert tup1 != tup2 */
|
|
solver.Assert(ctx.MkNot(ctx.MkEq(tup1, tup2)));
|
|
/* assert first tup1 = first tup2 */
|
|
solver.Assert(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.Model;
|
|
Console.WriteLine("{0}", model);
|
|
Console.WriteLine("evaluating tup1 {0}", (model.Evaluate(tup1)));
|
|
Console.WriteLine("evaluating tup2 {0}", (model.Evaluate(tup2)));
|
|
Console.WriteLine("evaluating second(tup2) {0}",
|
|
(model.Evaluate(ctx.MkApp(second, tup2))));
|
|
}
|
|
else
|
|
{
|
|
Console.WriteLine("BUG, the constraints are satisfiable.");
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// Demonstrate how to use <code>Push</code>and <code>Pop</code>to
|
|
/// control the size of models.
|
|
/// </summary>
|
|
/// <remarks>Note: this test is specialized to 32-bit bitvectors.</remarks>
|
|
public static void CheckSmall(Context ctx, Solver solver, BitVecExpr[] to_minimize)
|
|
{
|
|
Sort bv32 = ctx.MkBitVecSort(32);
|
|
|
|
int num_Exprs = to_minimize.Length;
|
|
UInt32[] upper = new UInt32[num_Exprs];
|
|
UInt32[] lower = new UInt32[num_Exprs];
|
|
BitVecExpr[] values = new BitVecExpr[num_Exprs];
|
|
for (int i = 0; i < upper.Length; ++i)
|
|
{
|
|
upper[i] = UInt32.MaxValue;
|
|
lower[i] = 0;
|
|
}
|
|
bool some_work = true;
|
|
int last_index = -1;
|
|
UInt32 last_upper = 0;
|
|
while (some_work)
|
|
{
|
|
solver.Push();
|
|
|
|
bool check_is_sat = true;
|
|
while (check_is_sat && some_work)
|
|
{
|
|
// Assert all feasible bounds.
|
|
for (int i = 0; i < num_Exprs; ++i)
|
|
{
|
|
solver.Assert(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;
|
|
}
|
|
Console.WriteLine("{0}", solver.Model);
|
|
|
|
// narrow the bounds based on the current model.
|
|
for (int i = 0; i < num_Exprs; ++i)
|
|
{
|
|
Expr v = solver.Model.Evaluate(to_minimize[i]);
|
|
UInt64 ui = ((BitVecNum)v).UInt64;
|
|
if (ui < upper[i])
|
|
{
|
|
upper[i] = (UInt32)ui;
|
|
}
|
|
Console.WriteLine("{0} {1} {2}", 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.Assert(ctx.MkBVULE(to_minimize[i], ctx.MkBV(last_upper, 32)));
|
|
some_work = true;
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
solver.Pop();
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// Reduced-size model generation example.
|
|
/// </summary>
|
|
public static void FindSmallModelExample(Context ctx)
|
|
{
|
|
Console.WriteLine("FindSmallModelExample");
|
|
|
|
BitVecExpr x = ctx.MkBVConst("x", 32);
|
|
BitVecExpr y = ctx.MkBVConst("y", 32);
|
|
BitVecExpr z = ctx.MkBVConst("z", 32);
|
|
|
|
Solver solver = ctx.MkSolver();
|
|
|
|
solver.Assert(ctx.MkBVULE(x, ctx.MkBVAdd(y, z)));
|
|
CheckSmall(ctx, solver, new BitVecExpr[] { x, y, z });
|
|
}
|
|
|
|
/// <summary>
|
|
/// Simplifier example.
|
|
/// </summary>
|
|
public static void SimplifierExample(Context ctx)
|
|
{
|
|
Console.WriteLine("SimplifierExample");
|
|
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
IntExpr y = ctx.MkIntConst("y");
|
|
IntExpr z = ctx.MkIntConst("z");
|
|
IntExpr u = ctx.MkIntConst("u");
|
|
|
|
Expr t1 = ctx.MkAdd(x, ctx.MkSub(y, ctx.MkAdd(x, z)));
|
|
Expr t2 = t1.Simplify();
|
|
Console.WriteLine("{0} -> {1}", (t1), (t2));
|
|
}
|
|
|
|
/// <summary>
|
|
/// Extract unsatisfiable core example
|
|
/// </summary>
|
|
public static void UnsatCoreAndProofExample(Context ctx)
|
|
{
|
|
Console.WriteLine("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");
|
|
Expr[] assumptions = new Expr[] { 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("{0}", c);
|
|
}
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// Extract unsatisfiable core example with AssertAndTrack
|
|
/// </summary>
|
|
public static void UnsatCoreAndProofExample2(Context ctx)
|
|
{
|
|
Console.WriteLine("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)
|
|
{
|
|
Console.WriteLine("unsat");
|
|
Console.WriteLine("core: ");
|
|
foreach (Expr c in solver.UnsatCore)
|
|
{
|
|
Console.WriteLine("{0}", c);
|
|
}
|
|
}
|
|
}
|
|
|
|
public static void FiniteDomainExample(Context ctx)
|
|
{
|
|
Console.WriteLine("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);
|
|
Console.WriteLine("{0} of size {1}", s, s.Size);
|
|
Console.WriteLine("{0} of size {1}", t, t.Size);
|
|
Console.WriteLine("{0}", s1);
|
|
Console.WriteLine("{0}", t1);
|
|
Console.WriteLine("{0}", s1.Int);
|
|
Console.WriteLine("{0}", t1.Int);
|
|
// But you cannot mix numerals of different sorts
|
|
// even if the size of their domains are the same:
|
|
// Console.WriteLine("{0}", ctx.MkEq(s1, t1));
|
|
}
|
|
|
|
public static void FloatingPointExample1(Context ctx)
|
|
{
|
|
Console.WriteLine("FloatingPointExample1");
|
|
|
|
FPSort s = ctx.MkFPSort(11, 53);
|
|
Console.WriteLine("Sort: {0}", 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 */
|
|
Console.WriteLine("x={0}; y={1}; z={2}", 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();
|
|
Console.WriteLine("OK, unsat:" + Environment.NewLine + 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();
|
|
Console.WriteLine("OK, sat:" + Environment.NewLine + 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();
|
|
Console.WriteLine("OK, unsat:" + Environment.NewLine + slvr);
|
|
}
|
|
|
|
public static void FloatingPointExample2(Context ctx)
|
|
{
|
|
Console.WriteLine("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.RealSort), ctx.MkFPToReal(fp_val));
|
|
BoolExpr c5 = ctx.MkAnd(c1, c2, c3, c4);
|
|
Console.WriteLine("c5 = " + c5);
|
|
|
|
/* Generic solver */
|
|
Solver s = ctx.MkSolver();
|
|
s.Assert(c5);
|
|
|
|
Console.WriteLine(s);
|
|
|
|
if (s.Check() != Status.SATISFIABLE)
|
|
throw new TestFailedException();
|
|
|
|
Console.WriteLine("OK, model: {0}", s.Model.ToString());
|
|
}
|
|
|
|
|
|
public static void TranslationExample()
|
|
{
|
|
Context ctx1 = new Context();
|
|
Context ctx2 = new Context();
|
|
|
|
Sort s1 = ctx1.IntSort;
|
|
Sort s2 = ctx2.IntSort;
|
|
Sort s3 = s1.Translate(ctx2);
|
|
|
|
Console.WriteLine(s1 == s2);
|
|
Console.WriteLine(s1.Equals(s2));
|
|
Console.WriteLine(s2.Equals(s3));
|
|
Console.WriteLine(s1.Equals(s3));
|
|
|
|
Expr e1 = ctx1.MkIntConst("e1");
|
|
Expr e2 = ctx2.MkIntConst("e1");
|
|
Expr e3 = e1.Translate(ctx2);
|
|
|
|
Console.WriteLine(e1 == e2);
|
|
Console.WriteLine(e1.Equals(e2));
|
|
Console.WriteLine(e2.Equals(e3));
|
|
Console.WriteLine(e1.Equals(e3));
|
|
}
|
|
|
|
|
|
static void Main(string[] args)
|
|
{
|
|
try
|
|
{
|
|
Microsoft.Z3.Global.ToggleWarningMessages(true);
|
|
Log.Open("test.log");
|
|
|
|
Console.Write("Z3 Major Version: ");
|
|
Console.WriteLine(Microsoft.Z3.Version.Major.ToString());
|
|
Console.Write("Z3 Full Version: ");
|
|
Console.WriteLine(Microsoft.Z3.Version.ToString());
|
|
Console.Write("Z3 Full Version String: ");
|
|
Console.WriteLine(Microsoft.Z3.Version.FullVersion);
|
|
|
|
|
|
SimpleExample();
|
|
|
|
// These examples need model generation turned on.
|
|
using (Context ctx = new Context(new Dictionary<string, string>() { { "model", "true" } }))
|
|
{
|
|
BasicTests(ctx);
|
|
CastingTest(ctx);
|
|
SudokuExample(ctx);
|
|
QuantifierExample1(ctx);
|
|
QuantifierExample2(ctx);
|
|
LogicExample(ctx);
|
|
ParOrExample(ctx);
|
|
FindModelExample1(ctx);
|
|
FindModelExample2(ctx);
|
|
PushPopExample1(ctx);
|
|
ArrayExample1(ctx);
|
|
ArrayExample3(ctx);
|
|
BitvectorExample1(ctx);
|
|
BitvectorExample2(ctx);
|
|
ParserExample1(ctx);
|
|
ParserExample2(ctx);
|
|
ParserExample5(ctx);
|
|
ITEExample(ctx);
|
|
EvalExample1(ctx);
|
|
EvalExample2(ctx);
|
|
FindSmallModelExample(ctx);
|
|
SimplifierExample(ctx);
|
|
FiniteDomainExample(ctx);
|
|
FloatingPointExample1(ctx);
|
|
FloatingPointExample2(ctx);
|
|
}
|
|
|
|
// 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);
|
|
UnsatCoreAndProofExample2(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);
|
|
}
|
|
|
|
TranslationExample();
|
|
|
|
Log.Close();
|
|
if (Log.isOpen())
|
|
Console.WriteLine("Log is still open!");
|
|
}
|
|
catch (Z3Exception ex)
|
|
{
|
|
Console.WriteLine("Z3 Managed Exception: " + ex.Message);
|
|
Console.WriteLine("Stack trace: " + ex.StackTrace);
|
|
}
|
|
catch (TestFailedException ex)
|
|
{
|
|
Console.WriteLine("TEST CASE FAILED: " + ex.Message);
|
|
}
|
|
}
|
|
}
|
|
}
|