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

fix dotnet example

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-29 20:52:19 -08:00
parent 9f567a6215
commit ab58723ffc
1 changed files with 9 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

64
examples/dotnet/Program.cs
View file

@ -173,10 +173,9 @@ namespace test_mapi
throw new Exception("function must be binary, and argument types must be equal to return type"); throw new Exception("function must be binary, and argument types must be equal to return type");
} }
string bench = string.Format("(benchmark comm :formula (forall (x {0}) (y {1}) (= ({2} x y) ({3} y x))))", string bench = string.Format("(assert (forall ((x {0}) (y {1})) (= ({2} x y) ({3} y x))))",
t.Name, t.Name, f.Name, f.Name); t.Name, t.Name, f.Name, f.Name);
ctx.ParseSMTLIBString(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f }); return ctx.ParseSMTLIB2String(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f });
return ctx.SMTLIBFormulas[0];
} }
/// <summary> /// <summary>
@ -965,21 +964,6 @@ namespace test_mapi
} }
} }
/// <summary>
/// Shows how to read an SMT1 file.
/// </summary>
static void SMT1FileTest(string filename)
{
Console.Write("SMT File test ");
using (Context ctx = new Context(new Dictionary<string, string>() { { "MODEL", "true" } }))
{
ctx.ParseSMTLIBFile(filename);
BoolExpr a = ctx.MkAnd(ctx.SMTLIBFormulas);
Console.WriteLine("read formula: " + a);
}
}
/// <summary> /// <summary>
/// Shows how to read an SMT2 file. /// Shows how to read an SMT2 file.
@ -1399,11 +1383,10 @@ namespace test_mapi
{ {
Console.WriteLine("ParserExample1"); Console.WriteLine("ParserExample1");
ctx.ParseSMTLIBString("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); var fml = ctx.ParseSMTLIB2String("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");
foreach (BoolExpr f in ctx.SMTLIBFormulas) Console.WriteLine("formula {0}", fml);
Console.WriteLine("formula {0}", f);
Model m = Check(ctx, ctx.MkAnd(ctx.SMTLIBFormulas), Status.SATISFIABLE); Model m = Check(ctx, fml, Status.SATISFIABLE);
} }
/// <summary> /// <summary>
@ -1412,15 +1395,11 @@ namespace test_mapi
public static void ParserExample2(Context ctx) public static void ParserExample2(Context ctx)
{ {
Console.WriteLine("ParserExample2"); Console.WriteLine("ParserExample2");
Symbol[] declNames = { ctx.MkSymbol("a"), ctx.MkSymbol("b") }; Symbol[] declNames = { ctx.MkSymbol("a"), ctx.MkSymbol("b") };
FuncDecl a = ctx.MkConstDecl(declNames[0], ctx.MkIntSort()); FuncDecl a = ctx.MkConstDecl(declNames[0], ctx.MkIntSort());
FuncDecl b = ctx.MkConstDecl(declNames[1], ctx.MkIntSort()); FuncDecl b = ctx.MkConstDecl(declNames[1], ctx.MkIntSort());
FuncDecl[] decls = new FuncDecl[] { a, b }; FuncDecl[] decls = new FuncDecl[] { a, b };
BoolExpr f = ctx.ParseSMTLIB2String("(assert (> a b))", null, null, declNames, decls);
ctx.ParseSMTLIBString("(benchmark tst :formula (> a b))",
null, null, declNames, decls);
BoolExpr f = ctx.SMTLIBFormulas[0];
Console.WriteLine("formula: {0}", f); Console.WriteLine("formula: {0}", f);
Check(ctx, f, Status.SATISFIABLE); Check(ctx, f, Status.SATISFIABLE);
} }
@ -1438,39 +1417,15 @@ namespace test_mapi
BoolExpr ca = CommAxiom(ctx, g); BoolExpr ca = CommAxiom(ctx, g);
ctx.ParseSMTLIBString("(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (gg x 0) (gg 0 y)))))", BoolExpr thm = ctx.ParseSMTLIB2String("(assert (forall ((x Int) (y Int)) (implies (= x y) (= (gg x 0) (gg 0 y)))))",
null, null, null, null,
new Symbol[] { ctx.MkSymbol("gg") }, new Symbol[] { ctx.MkSymbol("gg") },
new FuncDecl[] { g }); new FuncDecl[] { g });
BoolExpr thm = ctx.SMTLIBFormulas[0];
Console.WriteLine("formula: {0}", thm); Console.WriteLine("formula: {0}", thm);
Prove(ctx, thm, false, ca); Prove(ctx, thm, false, ca);
} }
/// <summary>
/// Display the declarations, assumptions and formulas in a SMT-LIB string.
/// </summary>
public static void ParserExample4(Context ctx)
{
Console.WriteLine("ParserExample4");
ctx.ParseSMTLIBString
("(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))");
foreach (var decl in ctx.SMTLIBDecls)
{
Console.WriteLine("Declaration: {0}", decl);
}
foreach (var f in ctx.SMTLIBAssumptions)
{
Console.WriteLine("Assumption: {0}", f);
}
foreach (var f in ctx.SMTLIBFormulas)
{
Console.WriteLine("Formula: {0}", f);
}
}
/// <summary> /// <summary>
/// Demonstrates how to handle parser errors using Z3 error handling support. /// Demonstrates how to handle parser errors using Z3 error handling support.
/// </summary> /// </summary>
@ -1481,9 +1436,9 @@ namespace test_mapi
try try
{ {
ctx.ParseSMTLIBString( ctx.ParseSMTLIB2String(
/* the following string has a parsing error: missing parenthesis */ /* the following string has a parsing error: missing parenthesis */
"(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))"); "(declare-const x Int (declare-const y Int)) (assert (> x y))");
} }
catch (Z3Exception e) catch (Z3Exception e)
{ {
@ -2213,7 +2168,6 @@ namespace test_mapi
BitvectorExample2(ctx); BitvectorExample2(ctx);
ParserExample1(ctx); ParserExample1(ctx);
ParserExample2(ctx); ParserExample2(ctx);
ParserExample4(ctx);
ParserExample5(ctx); ParserExample5(ctx);
ITEExample(ctx); ITEExample(ctx);
EvalExample1(ctx); EvalExample1(ctx);