mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into contrib

Browse source 
Conflicts:
	README
	src/api/ml/build-lib.sh
	src/api/ml/z3.ml
	src/api/ml/z3.mli
	src/api/ml/z3_stubs.c
This commit is contained in:
Christoph M. Wintersteiger 2015-04-28 15:19:08 +01:00
commit 1d49f61b9a
395 changed files with 46184 additions and 69505 deletions
Download patch file Download diff file Expand all files Collapse all files

16
examples/c++/example.cpp
View file

@ -1,9 +1,11 @@
#include<vector>
#include"z3++.h"
using namespace z3;
/**
Demonstration of how Z3 can be used to prove validity of
De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
@ -21,6 +23,7 @@ void demorgan() {
// adding the negation of the conjecture as a constraint.
s.add(!conjecture);
std::cout << s << "\n";
std::cout << s.to_smt2() << "\n";
switch (s.check()) {
case unsat: std::cout << "de-Morgan is valid\n"; break;
case sat: std::cout << "de-Morgan is not valid\n"; break;
@ -974,7 +977,17 @@ void substitute_example() {
std::cout << new_f << std::endl;
}
void extract_example() {
std::cout << "extract example\n";
context c;
expr x(c);
x = c.constant("x", c.bv_sort(32));
expr y = x.extract(21, 10);
std::cout << y << " " << y.hi() << " " << y.lo() << "\n";
}
int main() {
try {
demorgan(); std::cout << "\n";
find_model_example1(); std::cout << "\n";
@ -1012,6 +1025,7 @@ int main() {
expr_vector_example(); std::cout << "\n";
exists_expr_vector_example(); std::cout << "\n";
substitute_example(); std::cout << "\n";
extract_example(); std::cout << "\n";
std::cout << "done\n";
}
catch (exception & ex) {

92
examples/c/test_capi.c
View file

@ -2595,6 +2595,97 @@ void substitute_vars_example() {
Z3_del_context(ctx);
}
/**
\brief Demonstrates some basic features of the FloatingPoint theory.
*/
void fpa_example() {
Z3_config cfg;
Z3_context ctx;
Z3_sort double_sort, rm_sort;
Z3_symbol s_rm, s_x, s_y, s_x_plus_y;
Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5, c6;
Z3_ast args[2], args2[2], and_args[3], args3[3];
printf("\nFPA-example\n");
LOG_MSG("FPA-example");
cfg = Z3_mk_config();
ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
double_sort = Z3_mk_fpa_sort(ctx, 11, 53);
rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx);
// Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).
s_rm = Z3_mk_string_symbol(ctx, "rm");
rm = Z3_mk_const(ctx, s_rm, rm_sort);
s_x = Z3_mk_string_symbol(ctx, "x");
s_y = Z3_mk_string_symbol(ctx, "y");
x = Z3_mk_const(ctx, s_x, double_sort);
y = Z3_mk_const(ctx, s_y, double_sort);
n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y");
x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort);
c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y));
args[0] = c1;
args[1] = Z3_mk_eq(ctx, x_plus_y, n);
c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
args2[0] = c2;
args2[1] = Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx)));
c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
and_args[0] = Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y));
and_args[1] = Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y));
and_args[2] = Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y));
args3[0] = c3;
args3[1] = Z3_mk_and(ctx, 3, and_args);
c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
Z3_push(ctx);
Z3_assert_cnstr(ctx, c4);
check(ctx, Z3_L_TRUE);
Z3_pop(ctx, 1);
// Show that the following are equal:
// (fp #b0 #b10000000001 #xc000000000000)
// ((_ to_fp 11 53) #x401c000000000000))
// ((_ to_fp 11 53) RTZ 1.75 2)))
// ((_ to_fp 11 53) RTZ 7.0)))
Z3_push(ctx);
c1 = Z3_mk_fpa_fp(ctx,
Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)),
Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)));
c2 = Z3_mk_fpa_to_fp_bv(ctx,
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
Z3_mk_fpa_sort(ctx, 11, 53));
c3 = Z3_mk_fpa_to_fp_int_real(ctx,
Z3_mk_fpa_rtz(ctx),
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)),
Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)),
Z3_mk_fpa_sort(ctx, 11, 53));
c4 = Z3_mk_fpa_to_fp_real(ctx,
Z3_mk_fpa_rtz(ctx),
Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
Z3_mk_fpa_sort(ctx, 11, 53));
args3[0] = Z3_mk_eq(ctx, c1, c2);
args3[1] = Z3_mk_eq(ctx, c1, c3);
args3[2] = Z3_mk_eq(ctx, c1, c4);
c5 = Z3_mk_and(ctx, 3, args3);
printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
Z3_assert_cnstr(ctx, c5);
check(ctx, Z3_L_TRUE);
Z3_pop(ctx, 1);
Z3_del_context(ctx);
}
/*@}*/
/*@}*/
@ -2640,5 +2731,6 @@ int main() {
smt2parser_example();
substitute_example();
substitute_vars_example();
fpa_example();
return 0;
}

126
examples/dotnet/Program.cs
View file

@ -1041,7 +1041,7 @@ namespace test_mapi
{
Console.WriteLine("LogicTest");
Context.ToggleWarningMessages(true);
Microsoft.Z3.Global.ToggleWarningMessages(true);
BitVecSort bvs = ctx.MkBitVecSort(32);
Expr x = ctx.MkConst("x", bvs);
@ -2010,6 +2010,47 @@ namespace test_mapi
}
}
/// <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");
@ -2028,11 +2069,89 @@ namespace test_mapi
// 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());
}
static void Main(string[] args)
{
try
{
Context.ToggleWarningMessages(true);
Microsoft.Z3.Global.ToggleWarningMessages(true);
Log.Open("test.log");
Console.Write("Z3 Major Version: ");
@ -2069,6 +2188,8 @@ namespace test_mapi
FindSmallModelExample(ctx);
SimplifierExample(ctx);
FiniteDomainExample(ctx);
FloatingPointExample1(ctx);
FloatingPointExample2(ctx);
}
// These examples need proof generation turned on.
@ -2084,6 +2205,7 @@ namespace test_mapi
TreeExample(ctx);
ForestExample(ctx);
UnsatCoreAndProofExample(ctx);
UnsatCoreAndProofExample2(ctx);
}
// These examples need proof generation turned on and auto-config set to false.

251
examples/java/JavaExample.java
View file

@ -41,7 +41,7 @@ class JavaExample
// / </code>
// / Where, <code>finv</code>is a fresh function declaration.
public BoolExpr injAxiom(Context ctx, FuncDecl f, int i) throws Z3Exception
public BoolExpr injAxiom(Context ctx, FuncDecl f, int i)
{
Sort[] domain = f.getDomain();
int sz = f.getDomainSize();
@ -102,7 +102,6 @@ class JavaExample
// / Where, <code>finv</code>is a fresh function declaration.
public BoolExpr injAxiomAbs(Context ctx, FuncDecl f, int i)
throws Z3Exception
{
Sort[] domain = f.getDomain();
int sz = f.getDomainSize();
@ -179,7 +178,7 @@ class JavaExample
// / "Hello world" example: create a Z3 logical context, and delete it.
public void simpleExample() throws Z3Exception
public void simpleExample()
{
System.out.println("SimpleExample");
Log.append("SimpleExample");
@ -193,8 +192,7 @@ class JavaExample
}
}
Model check(Context ctx, BoolExpr f, Status sat) throws Z3Exception,
TestFailedException
Model check(Context ctx, BoolExpr f, Status sat) throws TestFailedException
{
Solver s = ctx.mkSolver();
s.add(f);
@ -207,7 +205,7 @@ class JavaExample
}
void solveTactical(Context ctx, Tactic t, Goal g, Status sat)
throws Z3Exception, TestFailedException
throws TestFailedException
{
Solver s = ctx.mkSolver(t);
System.out.println("\nTactical solver: " + s);
@ -220,7 +218,7 @@ class JavaExample
throw new TestFailedException();
}
ApplyResult applyTactic(Context ctx, Tactic t, Goal g) throws Z3Exception
ApplyResult applyTactic(Context ctx, Tactic t, Goal g)
{
System.out.println("\nGoal: " + g);
@ -250,15 +248,14 @@ class JavaExample
return res;
}
void prove(Context ctx, BoolExpr f, boolean useMBQI) throws Z3Exception,
TestFailedException
void prove(Context ctx, BoolExpr f, boolean useMBQI) throws TestFailedException
{
BoolExpr[] assumptions = new BoolExpr[0];
prove(ctx, f, useMBQI, assumptions);
}
void prove(Context ctx, BoolExpr f, boolean useMBQI,
BoolExpr... assumptions) throws Z3Exception, TestFailedException
BoolExpr... assumptions) throws TestFailedException
{
System.out.println("Proving: " + f);
Solver s = ctx.mkSolver();
@ -283,15 +280,15 @@ class JavaExample
}
}
void disprove(Context ctx, BoolExpr f, boolean useMBQI) throws Z3Exception,
TestFailedException
void disprove(Context ctx, BoolExpr f, boolean useMBQI)
throws TestFailedException
{
BoolExpr[] a = {};
disprove(ctx, f, useMBQI, a);
}
void disprove(Context ctx, BoolExpr f, boolean useMBQI,
BoolExpr... assumptions) throws Z3Exception, TestFailedException
BoolExpr... assumptions) throws TestFailedException
{
System.out.println("Disproving: " + f);
Solver s = ctx.mkSolver();
@ -316,8 +313,7 @@ class JavaExample
}
}
void modelConverterTest(Context ctx) throws Z3Exception,
TestFailedException
void modelConverterTest(Context ctx) throws TestFailedException
{
System.out.println("ModelConverterTest");
@ -357,7 +353,7 @@ class JavaExample
// / A simple array example.
void arrayExample1(Context ctx) throws Z3Exception, TestFailedException
void arrayExample1(Context ctx) throws TestFailedException
{
System.out.println("ArrayExample1");
Log.append("ArrayExample1");
@ -407,8 +403,7 @@ class JavaExample
// / <remarks>This example demonstrates how to use the array
// theory.</remarks>
public void arrayExample2(Context ctx) throws Z3Exception,
TestFailedException
public void arrayExample2(Context ctx) throws TestFailedException
{
System.out.println("ArrayExample2");
Log.append("ArrayExample2");
@ -457,8 +452,7 @@ class JavaExample
// / <remarks>This example also shows how to use the <code>distinct</code>
// construct.</remarks>
public void arrayExample3(Context ctx) throws Z3Exception,
TestFailedException
public void arrayExample3(Context ctx) throws TestFailedException
{
System.out.println("ArrayExample3");
Log.append("ArrayExample2");
@ -497,7 +491,7 @@ class JavaExample
// / Sudoku solving example.
void sudokuExample(Context ctx) throws Z3Exception, TestFailedException
void sudokuExample(Context ctx) throws TestFailedException
{
System.out.println("SudokuExample");
Log.append("SudokuExample");
@ -600,7 +594,7 @@ class JavaExample
// / A basic example of how to use quantifiers.
void quantifierExample1(Context ctx) throws Z3Exception
void quantifierExample1(Context ctx)
{
System.out.println("QuantifierExample");
Log.append("QuantifierExample");
@ -638,7 +632,7 @@ class JavaExample
System.out.println("Quantifier Y: " + y.toString());
}
void quantifierExample2(Context ctx) throws Z3Exception
void quantifierExample2(Context ctx)
{
System.out.println("QuantifierExample2");
@ -694,8 +688,7 @@ class JavaExample
// / <code>f</code> is injective in the second argument. <seealso
// cref="inj_axiom"/>
public void quantifierExample3(Context ctx) throws Z3Exception,
TestFailedException
public void quantifierExample3(Context ctx) throws TestFailedException
{
System.out.println("QuantifierExample3");
Log.append("QuantifierExample3");
@ -736,8 +729,7 @@ class JavaExample
// / <code>f</code> is injective in the second argument. <seealso
// cref="inj_axiom"/>
public void quantifierExample4(Context ctx) throws Z3Exception,
TestFailedException
public void quantifierExample4(Context ctx) throws TestFailedException
{
System.out.println("QuantifierExample4");
Log.append("QuantifierExample4");
@ -776,7 +768,7 @@ class JavaExample
// / Some basic tests.
void basicTests(Context ctx) throws Z3Exception, TestFailedException
void basicTests(Context ctx) throws TestFailedException
{
System.out.println("BasicTests");
@ -890,7 +882,7 @@ class JavaExample
// / Some basic expression casting tests.
void castingTest(Context ctx) throws Z3Exception, TestFailedException
void castingTest(Context ctx) throws TestFailedException
{
System.out.println("CastingTest");
@ -1038,7 +1030,7 @@ class JavaExample
// / Shows how to read an SMT1 file.
void smt1FileTest(String filename) throws Z3Exception
void smt1FileTest(String filename)
{
System.out.print("SMT File test ");
@ -1054,7 +1046,7 @@ class JavaExample
// / Shows how to read an SMT2 file.
void smt2FileTest(String filename) throws Z3Exception
void smt2FileTest(String filename)
{
Date before = new Date();
@ -1095,13 +1087,13 @@ class JavaExample
// / Shows how to use Solver(logic)
// / <param name="ctx"></param>
void logicExample(Context ctx) throws Z3Exception, TestFailedException
// / @param ctx
void logicExample(Context ctx) throws TestFailedException
{
System.out.println("LogicTest");
Log.append("LogicTest");
Context.ToggleWarningMessages(true);
com.microsoft.z3.Global.ToggleWarningMessages(true);
BitVecSort bvs = ctx.mkBitVecSort(32);
Expr x = ctx.mkConst("x", bvs);
@ -1128,7 +1120,7 @@ class JavaExample
// / Demonstrates how to use the ParOr tactic.
void parOrExample(Context ctx) throws Z3Exception, TestFailedException
void parOrExample(Context ctx) throws TestFailedException
{
System.out.println("ParOrExample");
Log.append("ParOrExample");
@ -1151,7 +1143,7 @@ class JavaExample
throw new TestFailedException();
}
void bigIntCheck(Context ctx, RatNum r) throws Z3Exception
void bigIntCheck(Context ctx, RatNum r)
{
System.out.println("Num: " + r.getBigIntNumerator());
System.out.println("Den: " + r.getBigIntDenominator());
@ -1159,8 +1151,7 @@ class JavaExample
// / Find a model for <code>x xor y</code>.
public void findModelExample1(Context ctx) throws Z3Exception,
TestFailedException
public void findModelExample1(Context ctx) throws TestFailedException
{
System.out.println("FindModelExample1");
Log.append("FindModelExample1");
@ -1177,8 +1168,7 @@ class JavaExample
// / Find a model for <tt>x < y + 1, x > 2</tt>.
// / Then, assert <tt>not(x = y)</tt>, and find another model.
public void findModelExample2(Context ctx) throws Z3Exception,
TestFailedException
public void findModelExample2(Context ctx) throws TestFailedException
{
System.out.println("FindModelExample2");
Log.append("FindModelExample2");
@ -1217,8 +1207,7 @@ class JavaExample
// / <remarks>This function demonstrates how to create uninterpreted
// / types and functions.</remarks>
public void proveExample1(Context ctx) throws Z3Exception,
TestFailedException
public void proveExample1(Context ctx) throws TestFailedException
{
System.out.println("ProveExample1");
Log.append("ProveExample1");
@ -1264,8 +1253,7 @@ class JavaExample
// / <remarks>This example demonstrates how to combine uninterpreted
// functions
// / and arithmetic.</remarks>
public void proveExample2(Context ctx) throws Z3Exception,
TestFailedException
public void proveExample2(Context ctx) throws TestFailedException
{
System.out.println("ProveExample2");
Log.append("ProveExample2");
@ -1319,8 +1307,7 @@ class JavaExample
// / <remarks>This example also demonstrates how big numbers can be
// / created in ctx.</remarks>
public void pushPopExample1(Context ctx) throws Z3Exception,
TestFailedException
public void pushPopExample1(Context ctx) throws TestFailedException
{
System.out.println("PushPopExample1");
Log.append("PushPopExample1");
@ -1386,8 +1373,7 @@ class JavaExample
// / <remarks>Check that the projection of a tuple
// / returns the corresponding element.</remarks>
public void tupleExample(Context ctx) throws Z3Exception,
TestFailedException
public void tupleExample(Context ctx) throws TestFailedException
{
System.out.println("TupleExample");
Log.append("TupleExample");
@ -1422,8 +1408,7 @@ class JavaExample
// / This example disproves that x - 10 &lt;= 0 IFF x &lt;= 10 for (32-bit)
// machine integers
// / </remarks>
public void bitvectorExample1(Context ctx) throws Z3Exception,
TestFailedException
public void bitvectorExample1(Context ctx) throws TestFailedException
{
System.out.println("BitvectorExample1");
Log.append("BitvectorExample1");
@ -1444,8 +1429,7 @@ class JavaExample
// / Find x and y such that: x ^ y - 103 == x * y
public void bitvectorExample2(Context ctx) throws Z3Exception,
TestFailedException
public void bitvectorExample2(Context ctx) throws TestFailedException
{
System.out.println("BitvectorExample2");
Log.append("BitvectorExample2");
@ -1470,8 +1454,7 @@ class JavaExample
// / Demonstrates how to use the SMTLIB parser.
public void parserExample1(Context ctx) throws Z3Exception,
TestFailedException
public void parserExample1(Context ctx) throws TestFailedException
{
System.out.println("ParserExample1");
Log.append("ParserExample1");
@ -1489,8 +1472,7 @@ class JavaExample
// / Demonstrates how to initialize the parser symbol table.
public void parserExample2(Context ctx) throws Z3Exception,
TestFailedException
public void parserExample2(Context ctx) throws TestFailedException
{
System.out.println("ParserExample2");
Log.append("ParserExample2");
@ -1532,7 +1514,7 @@ class JavaExample
// / Display the declarations, assumptions and formulas in a SMT-LIB string.
public void parserExample4(Context ctx) throws Z3Exception
public void parserExample4(Context ctx)
{
System.out.println("ParserExample4");
Log.append("ParserExample4");
@ -1579,7 +1561,7 @@ class JavaExample
// / Create an ite-Expr (if-then-else Exprs).
public void iteExample(Context ctx) throws Z3Exception
public void iteExample(Context ctx)
{
System.out.println("ITEExample");
Log.append("ITEExample");
@ -1594,8 +1576,7 @@ class JavaExample
// / Create an enumeration data type.
public void enumExample(Context ctx) throws Z3Exception,
TestFailedException
public void enumExample(Context ctx) throws TestFailedException
{
System.out.println("EnumExample");
Log.append("EnumExample");
@ -1642,8 +1623,7 @@ class JavaExample
// / Create a list datatype.
public void listExample(Context ctx) throws Z3Exception,
TestFailedException
public void listExample(Context ctx) throws TestFailedException
{
System.out.println("ListExample");
Log.append("ListExample");
@ -1706,8 +1686,7 @@ class JavaExample
// / Create a binary tree datatype.
public void treeExample(Context ctx) throws Z3Exception,
TestFailedException
public void treeExample(Context ctx) throws TestFailedException
{
System.out.println("TreeExample");
Log.append("TreeExample");
@ -1779,8 +1758,7 @@ class JavaExample
// / forest ::= nil | cons(tree, forest)
// / tree ::= nil | cons(forest, forest)
// / </remarks>
public void forestExample(Context ctx) throws Z3Exception,
TestFailedException
public void forestExample(Context ctx) throws TestFailedException
{
System.out.println("ForestExample");
Log.append("ForestExample");
@ -1899,7 +1877,7 @@ class JavaExample
// / Demonstrate how to use #Eval.
public void evalExample1(Context ctx) throws Z3Exception
public void evalExample1(Context ctx)
{
System.out.println("EvalExample1");
Log.append("EvalExample1");
@ -1939,7 +1917,7 @@ class JavaExample
// / Demonstrate how to use #Eval on tuples.
public void evalExample2(Context ctx) throws Z3Exception
public void evalExample2(Context ctx)
{
System.out.println("EvalExample2");
Log.append("EvalExample2");
@ -1990,8 +1968,7 @@ class JavaExample
// / control the size of models.
// / <remarks>Note: this test is specialized to 32-bit bitvectors.</remarks>
public void checkSmall(Context ctx, Solver solver,
BitVecExpr... to_minimize) throws Z3Exception
public void checkSmall(Context ctx, Solver solver, BitVecExpr... to_minimize)
{
int num_Exprs = to_minimize.length;
int[] upper = new int[num_Exprs];
@ -2063,7 +2040,7 @@ class JavaExample
// / Reduced-size model generation example.
public void findSmallModelExample(Context ctx) throws Z3Exception
public void findSmallModelExample(Context ctx)
{
System.out.println("FindSmallModelExample");
Log.append("FindSmallModelExample");
@ -2080,7 +2057,7 @@ class JavaExample
// / Simplifier example.
public void simplifierExample(Context ctx) throws Z3Exception
public void simplifierExample(Context ctx)
{
System.out.println("SimplifierExample");
Log.append("SimplifierExample");
@ -2098,7 +2075,7 @@ class JavaExample
// / Extract unsatisfiable core example
public void unsatCoreAndProofExample(Context ctx) throws Z3Exception
public void unsatCoreAndProofExample(Context ctx)
{
System.out.println("UnsatCoreAndProofExample");
Log.append("UnsatCoreAndProofExample");
@ -2137,8 +2114,49 @@ class JavaExample
}
}
}
/// Extract unsatisfiable core example with AssertAndTrack
public void unsatCoreAndProofExample2(Context ctx)
{
System.out.println("UnsatCoreAndProofExample2");
Log.append("UnsatCoreAndProofExample2");
public void finiteDomainExample(Context ctx) throws Z3Exception
Solver solver = ctx.mkSolver();
BoolExpr pa = ctx.mkBoolConst("PredA");
BoolExpr pb = ctx.mkBoolConst("PredB");
BoolExpr pc = ctx.mkBoolConst("PredC");
BoolExpr pd = ctx.mkBoolConst("PredD");
BoolExpr f1 = ctx.mkAnd(new BoolExpr[] { pa, pb, pc });
BoolExpr f2 = ctx.mkAnd(new BoolExpr[] { pa, ctx.mkNot(pb), pc });
BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc));
BoolExpr f4 = pd;
BoolExpr p1 = ctx.mkBoolConst("P1");
BoolExpr p2 = ctx.mkBoolConst("P2");
BoolExpr p3 = ctx.mkBoolConst("P3");
BoolExpr p4 = ctx.mkBoolConst("P4");
solver.assertAndTrack(f1, p1);
solver.assertAndTrack(f2, p2);
solver.assertAndTrack(f3, p3);
solver.assertAndTrack(f4, p4);
Status result = solver.check();
if (result == Status.UNSATISFIABLE)
{
System.out.println("unsat");
System.out.println("core: ");
for (Expr c : solver.getUnsatCore())
{
System.out.println(c);
}
}
}
public void finiteDomainExample(Context ctx)
{
System.out.println("FiniteDomainExample");
Log.append("FiniteDomainExample");
@ -2157,12 +2175,92 @@ class JavaExample
// System.out.println(ctx.mkEq(s1, t1));
}
public void floatingPointExample1(Context ctx) throws TestFailedException
{
System.out.println("FloatingPointExample1");
Log.append("FloatingPointExample1");
FPSort s = ctx.mkFPSort(11, 53);
System.out.println("Sort: " + s);
FPNum x = (FPNum)ctx.mkNumeral("-1e1", s); /* -1 * 10^1 = -10 */
FPNum y = (FPNum)ctx.mkNumeral("-10", s); /* -10 */
FPNum z = (FPNum)ctx.mkNumeral("-1.25p3", s); /* -1.25 * 2^3 = -1.25 * 8 = -10 */
System.out.println("x=" + x.toString() +
"; y=" + y.toString() +
"; z=" + z.toString());
BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z));
check(ctx, ctx.mkNot(a), Status.UNSATISFIABLE);
/* nothing is equal to NaN according to floating-point
* equality, so NaN == k should be unsatisfiable. */
FPExpr k = (FPExpr)ctx.mkConst("x", s);
FPExpr nan = ctx.mkFPNaN(s);
/* solver that runs the default tactic for QF_FP. */
Solver slvr = ctx.mkSolver("QF_FP");
slvr.add(ctx.mkFPEq(nan, k));
if (slvr.check() != Status.UNSATISFIABLE)
throw new TestFailedException();
System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr);
/* NaN is equal to NaN according to normal equality. */
slvr = ctx.mkSolver("QF_FP");
slvr.add(ctx.mkEq(nan, nan));
if (slvr.check() != Status.SATISFIABLE)
throw new TestFailedException();
System.out.println("OK, sat:" + System.getProperty("line.separator") + slvr);
/* Let's prove -1e1 * -1.25e3 == +100 */
x = (FPNum)ctx.mkNumeral("-1e1", s);
y = (FPNum)ctx.mkNumeral("-1.25p3", s);
FPExpr x_plus_y = (FPExpr)ctx.mkConst("x_plus_y", s);
FPNum r = (FPNum)ctx.mkNumeral("100", s);
slvr = ctx.mkSolver("QF_FP");
slvr.add(ctx.mkEq(x_plus_y, ctx.mkFPMul(ctx.mkFPRoundNearestTiesToAway(), x, y)));
slvr.add(ctx.mkNot(ctx.mkFPEq(x_plus_y, r)));
if (slvr.check() != Status.UNSATISFIABLE)
throw new TestFailedException();
System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr);
}
public void floatingPointExample2(Context ctx) throws TestFailedException
{
System.out.println("FloatingPointExample2");
Log.append("FloatingPointExample2");
FPSort double_sort = ctx.mkFPSort(11, 53);
FPRMSort rm_sort = ctx.mkFPRoundingModeSort();
FPRMExpr rm = (FPRMExpr)ctx.mkConst(ctx.mkSymbol("rm"), rm_sort);
BitVecExpr x = (BitVecExpr)ctx.mkConst(ctx.mkSymbol("x"), ctx.mkBitVecSort(64));
FPExpr y = (FPExpr)ctx.mkConst(ctx.mkSymbol("y"), double_sort);
FPExpr fp_val = ctx.mkFP(42, double_sort);
BoolExpr c1 = ctx.mkEq(y, fp_val);
BoolExpr c2 = ctx.mkEq(x, ctx.mkFPToBV(rm, y, 64, false));
BoolExpr c3 = ctx.mkEq(x, ctx.mkBV(42, 64));
BoolExpr c4 = ctx.mkEq(ctx.mkNumeral(42, ctx.getRealSort()), ctx.mkFPToReal(fp_val));
BoolExpr c5 = ctx.mkAnd(c1, c2, c3, c4);
System.out.println("c5 = " + c5);
/* Generic solver */
Solver s = ctx.mkSolver();
s.add(c5);
if (s.check() != Status.SATISFIABLE)
throw new TestFailedException();
System.out.println("OK, model: " + s.getModel().toString());
}
public static void main(String[] args)
{
JavaExample p = new JavaExample();
try
{
Context.ToggleWarningMessages(true);
com.microsoft.z3.Global.ToggleWarningMessages(true);
Log.open("test.log");
System.out.print("Z3 Major Version: ");
@ -2200,6 +2298,8 @@ class JavaExample
p.findSmallModelExample(ctx);
p.simplifierExample(ctx);
p.finiteDomainExample(ctx);
p.floatingPointExample1(ctx);
p.floatingPointExample2(ctx);
}
{ // These examples need proof generation turned on.
@ -2216,6 +2316,7 @@ class JavaExample
p.treeExample(ctx);
p.forestExample(ctx);
p.unsatCoreAndProofExample(ctx);
p.unsatCoreAndProofExample2(ctx);
}
{ // These examples need proof generation turned on and auto-config

22
examples/ml/README Normal file
View file

@ -0,0 +1,22 @@
Small example using the Z3 ML bindings.
To build the example execute
make examples
in the build directory.
It will create ml_example in the build directory,
which can be run in the build directory via
LD_LIBRARY_PATH=. ./ml_example
or
LD_LIBRARY_PATH=. ./ml_example.byte
for the byte-code version.
If Z3 was installed into the ocamlfind package repository (see src/api/ml/README),
then we can compile this example as follows:
ocamlfind ocamlc -o ml_example.byte -package Z3 -linkpkg ml_example.ml
ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml
Note that the resulting binaries depend on the shared z3 library, which needs to be
in the PATH (Windows), LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX). If Z3 was
installed into ocamlfind, the path that should be added is
`ocamlfind printconf destdir`/Z3

350
examples/ml/ml_example.ml Normal file
View file

@ -0,0 +1,350 @@
(*
Copyright (C) 2012 Microsoft Corporation
Author: CM Wintersteiger (cwinter) 2012-12-17
*)
open Z3
open Z3.Symbol
open Z3.Sort
open Z3.Expr
open Z3.Boolean
open Z3.FuncDecl
open Z3.Goal
open Z3.Tactic
open Z3.Tactic.ApplyResult
open Z3.Probe
open Z3.Solver
open Z3.Arithmetic
open Z3.Arithmetic.Integer
open Z3.Arithmetic.Real
open Z3.BitVector
exception TestFailedException of string
(**
Model Converter test
*)
let model_converter_test ( ctx : context ) =
Printf.printf "ModelConverterTest\n";
let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in
let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in
let g4 = (mk_goal ctx true false false ) in
(Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ;
(Goal.add g4 [ (mk_eq ctx
yr
(Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1) ])) ]) ;
(Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ;
(
let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let ar = (Tactic.apply (and_then ctx (mk_tactic ctx ("simplify")) (mk_tactic ctx "solve-eqs") []) g4 None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
;
let solver = (mk_solver ctx None) in
let f e = (Solver.add solver [ e ]) in
ignore (List.map f (get_formulas (get_subgoal ar 0))) ;
let q = (check solver []) in
if q != SATISFIABLE then
raise (TestFailedException "")
else
let m = (get_model solver) in
match m with
| None -> raise (TestFailedException "")
| Some (m) ->
Printf.printf "Solver says: %s\n" (string_of_status q) ;
Printf.printf "Model: \n%s\n" (Model.to_string m) ;
Printf.printf "Converted Model: \n%s\n" (Model.to_string (convert_model ar 0 m))
)
(**
Some basic tests.
*)
let basic_tests ( ctx : context ) =
Printf.printf "BasicTests\n" ;
let fname = (mk_string ctx "f") in
let x = (mk_string ctx "x") in
let y = (mk_string ctx "y") in
let bs = (Boolean.mk_sort ctx) in
let domain = [ bs; bs ] in
let f = (FuncDecl.mk_func_decl ctx fname domain bs) in
let fapp = (mk_app ctx f
[ (Expr.mk_const ctx x bs); (Expr.mk_const ctx y bs) ]) in
let fargs2 = [ (mk_fresh_const ctx "cp" bs) ] in
let domain2 = [ bs ] in
let fapp2 = (mk_app ctx (mk_fresh_func_decl ctx "fp" domain2 bs) fargs2) in
let trivial_eq = (mk_eq ctx fapp fapp) in
let nontrivial_eq = (mk_eq ctx fapp fapp2) in
let g = (mk_goal ctx true false false) in
(Goal.add g [ trivial_eq ]) ;
(Goal.add g [ nontrivial_eq ]) ;
Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ;
(
let solver = (mk_solver ctx None) in
(List.iter (fun a -> (Solver.add solver [ a ])) (get_formulas g)) ;
if (check solver []) != SATISFIABLE then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let ar = (Tactic.apply (mk_tactic ctx "simplify") g None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_sat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(Goal.add g [ (mk_eq ctx
(mk_numeral_int ctx 1 (BitVector.mk_sort ctx 32))
(mk_numeral_int ctx 2 (BitVector.mk_sort ctx 32))) ] )
;
(
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let g2 = (mk_goal ctx true true false) in
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_sat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let g2 = (mk_goal ctx true true false) in
(Goal.add g2 [ (Boolean.mk_false ctx) ]) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let g3 = (mk_goal ctx true true false) in
let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Integer.mk_sort ctx)) in
let yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Integer.mk_sort ctx)) in
(Goal.add g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (Integer.mk_sort ctx))) ]) ;
(Goal.add g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (Integer.mk_sort ctx))) ]) ;
let constr = (mk_eq ctx xc yc) in
(Goal.add g3 [ constr ] ) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
) ;
model_converter_test ctx ;
(* Real num/den test. *)
let rn = Real.mk_numeral_nd ctx 42 43 in
let inum = (get_numerator rn) in
let iden = get_denominator rn in
Printf.printf "Numerator: %s Denominator: %s\n" (Real.numeral_to_string inum) (Real.numeral_to_string iden) ;
if ((Real.numeral_to_string inum) <> "42" || (Real.numeral_to_string iden) <> "43") then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
;
if ((to_decimal_string rn 3) <> "0.976?") then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
;
if (to_decimal_string (Real.mk_numeral_s ctx "-1231231232/234234333") 5 <> "-5.25640?") then
raise (TestFailedException "")
else if (to_decimal_string (Real.mk_numeral_s ctx "-123123234234234234231232/234234333") 5 <> "-525641278361333.28170?") then
raise (TestFailedException "")
else if (to_decimal_string (Real.mk_numeral_s ctx "-234234333") 5 <> "-234234333") then
raise (TestFailedException "")
else if (to_decimal_string (Real.mk_numeral_s ctx "234234333/2") 5 <> "117117166.5") then
raise (TestFailedException "")
;
(* Error handling test. *)
try (
let i = Integer.mk_numeral_s ctx "1/2" in
raise (TestFailedException (numeral_to_string i)) (* unreachable *)
)
with Z3native.Exception(_) -> (
Printf.printf "Exception caught, OK.\n"
)
(**
A basic example of how to use quantifiers.
**)
let quantifier_example1 ( ctx : context ) =
Printf.printf "QuantifierExample\n" ;
let is = (Integer.mk_sort ctx) in
let types = [ is; is; is ] in
let names = [ (Symbol.mk_string ctx "x_0");
(Symbol.mk_string ctx "x_1");
(Symbol.mk_string ctx "x_2") ] in
let vars = [ (Quantifier.mk_bound ctx 2 (List.nth types 0));
(Quantifier.mk_bound ctx 2 (List.nth types 1));
(Quantifier.mk_bound ctx 2 (List.nth types 2)) ] in
let xs = [ (Integer.mk_const ctx (List.nth names 0));
(Integer.mk_const ctx (List.nth names 1));
(Integer.mk_const ctx (List.nth names 2)) ] in
let body_vars = (Boolean.mk_and ctx
[ (mk_eq ctx
(Arithmetic.mk_add ctx [ (List.nth vars 0) ; (Integer.mk_numeral_i ctx 1)])
(Integer.mk_numeral_i ctx 2)) ;
(mk_eq ctx
(Arithmetic.mk_add ctx [ (List.nth vars 1); (Integer.mk_numeral_i ctx 2)])
(Arithmetic.mk_add ctx [ (List.nth vars 2); (Integer.mk_numeral_i ctx 3)])) ]) in
let body_const = (Boolean.mk_and ctx
[ (mk_eq ctx
(Arithmetic.mk_add ctx [ (List.nth xs 0); (Integer.mk_numeral_i ctx 1)])
(Integer.mk_numeral_i ctx 2)) ;
(mk_eq ctx
(Arithmetic.mk_add ctx [ (List.nth xs 1); (Integer.mk_numeral_i ctx 2)])
(Arithmetic.mk_add ctx [ (List.nth xs 2); (Integer.mk_numeral_i ctx 3)])) ]) in
let x = (Quantifier.mk_forall ctx types names body_vars (Some 1) [] [] (Some (Symbol.mk_string ctx "Q1")) (Some (Symbol.mk_string ctx "skid1"))) in
Printf.printf "Quantifier X: %s\n" (Quantifier.to_string x) ;
let y = (Quantifier.mk_forall_const ctx xs body_const (Some 1) [] [] (Some (Symbol.mk_string ctx "Q2")) (Some (Symbol.mk_string ctx "skid2"))) in
Printf.printf "Quantifier Y: %s\n" (Quantifier.to_string y) ;
if (is_true (Quantifier.expr_of_quantifier x)) then
raise (TestFailedException "") (* unreachable *)
else if (is_false (Quantifier.expr_of_quantifier x)) then
raise (TestFailedException "") (* unreachable *)
else if (is_const (Quantifier.expr_of_quantifier x)) then
raise (TestFailedException "") (* unreachable *)
open Z3.FloatingPoint
(**
A basic example of floating point arithmetic
**)
let fpa_example ( ctx : context ) =
Printf.printf "FPAExample\n" ;
(* let str = ref "" in *)
(* (read_line ()) ; *)
let double_sort = (FloatingPoint.mk_sort_double ctx) in
let rm_sort = (FloatingPoint.RoundingMode.mk_sort ctx) in
(** Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode). *)
let s_rm = (mk_string ctx "rm") in
let rm = (mk_const ctx s_rm rm_sort) in
let s_x = (mk_string ctx "x") in
let s_y = (mk_string ctx "y") in
let x = (mk_const ctx s_x double_sort) in
let y = (mk_const ctx s_y double_sort)in
let n = (FloatingPoint.mk_numeral_f ctx 42.0 double_sort) in
let s_x_plus_y = (mk_string ctx "x_plus_y") in
let x_plus_y = (mk_const ctx s_x_plus_y double_sort) in
let c1 = (mk_eq ctx x_plus_y (mk_add ctx rm x y)) in
let args = [ c1 ; (mk_eq ctx x_plus_y n) ] in
let c2 = (Boolean.mk_and ctx args) in
let args2 = [ c2 ; (Boolean.mk_not ctx (Boolean.mk_eq ctx rm (RoundingMode.mk_rtz ctx))) ] in
let c3 = (Boolean.mk_and ctx args2) in
let and_args = [ (Boolean.mk_not ctx (mk_is_zero ctx y)) ;
(Boolean.mk_not ctx (mk_is_nan ctx y)) ;
(Boolean.mk_not ctx (mk_is_infinite ctx y)) ] in
let args3 = [ c3 ; (Boolean.mk_and ctx and_args) ] in
let c4 = (Boolean.mk_and ctx args3) in
(Printf.printf "c4: %s\n" (Expr.to_string c4)) ;
(
let solver = (mk_solver ctx None) in
(Solver.add solver [ c4 ]) ;
if (check solver []) != SATISFIABLE then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(* Show that the following are equal: *)
(* (fp #b0 #b10000000001 #xc000000000000) *)
(* ((_ to_fp 11 53) #x401c000000000000)) *)
(* ((_ to_fp 11 53) RTZ 1.75 2))) *)
(* ((_ to_fp 11 53) RTZ 7.0))) *)
let c1 = (mk_fp ctx
(mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1))
(mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52))
(mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))) in
let c2 = (mk_to_fp_bv ctx
(mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64))
(mk_sort ctx 11 53)) in
let c3 = (mk_to_fp_int_real ctx
(RoundingMode.mk_rtz ctx)
(mk_numeral_string ctx "2" (Integer.mk_sort ctx))
(mk_numeral_string ctx "1.75" (Real.mk_sort ctx))
(FloatingPoint.mk_sort ctx 11 53)) in
let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx)
(mk_numeral_string ctx "7.0" (Real.mk_sort ctx))
(FloatingPoint.mk_sort ctx 11 53)) in
let args3 = [ (mk_eq ctx c1 c2) ;
(mk_eq ctx c1 c3) ;
(mk_eq ctx c1 c4) ] in
let c5 = (Boolean.mk_and ctx args3) in
(Printf.printf "c5: %s\n" (Expr.to_string c5)) ;
(
let solver = (mk_solver ctx None) in
(Solver.add solver [ c5 ]) ;
if (check solver []) != SATISFIABLE then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
)
let _ =
try (
if not (Log.open_ "z3.log") then
raise (TestFailedException "Log couldn't be opened.")
else
(
Printf.printf "Running Z3 version %s\n" Version.to_string ;
let cfg = [("model", "true"); ("proof", "false")] in
let ctx = (mk_context cfg) in
let is = (Symbol.mk_int ctx 42) in
let ss = (Symbol.mk_string ctx "mySymbol") in
let bs = (Boolean.mk_sort ctx) in
let ints = (Integer.mk_sort ctx) in
let rs = (Real.mk_sort ctx) in
Printf.printf "int symbol: %s\n" (Symbol.to_string is);
Printf.printf "string symbol: %s\n" (Symbol.to_string ss);
Printf.printf "bool sort: %s\n" (Sort.to_string bs);
Printf.printf "int sort: %s\n" (Sort.to_string ints);
Printf.printf "real sort: %s\n" (Sort.to_string rs);
basic_tests ctx ;
quantifier_example1 ctx ;
fpa_example ctx ;
Printf.printf "Disposing...\n";
Gc.full_major ()
);
Printf.printf "Exiting.\n" ;
exit 0
) with Z3native.Exception(msg) -> (
Printf.printf "Z3 EXCEPTION: %s\n" msg ;
exit 1
)
;;

15
examples/python/complex/complex.py
View file

@ -46,6 +46,15 @@ class ComplexExpr:
other = _to_complex(other)
return ComplexExpr(other.r*self.r - other.i*self.i, other.i*self.r + other.r*self.i)
def __pow__(self, k):
if k == 0:
return ComplexExpr(1, 0)
if k == 1:
return self
if k < 0:
return (self ** (-k)).inv()
return reduce(lambda x, y: x * y, [self for _ in xrange(k)], ComplexExpr(1, 0))
def inv(self):
den = self.r*self.r + self.i*self.i
return ComplexExpr(self.r/den, -self.i/den)
@ -65,9 +74,6 @@ class ComplexExpr:
def __neq__(self, other):
return Not(self.__eq__(other))
def __pow__(self, k):
def simplify(self):
return ComplexExpr(simplify(self.r), simplify(self.i))
@ -107,4 +113,5 @@ print(s.model())
s.add(x.i != 1)
print(s.check())
# print(s.model())
print (3 + I)^2/(5 - I)
print ((3 + I) ** 2)/(5 - I)
print ((3 + I) ** -3)/(5 - I)