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 java

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

65
examples/java/JavaExample.java
View file

@ -170,10 +170,9 @@ class JavaExample
String bench = "(benchmark comm :formula (forall (x " + t.getName() String bench = "(benchmark comm :formula (forall (x " + t.getName()
+ ") (y " + t.getName() + ") (= (" + f.getName() + " x y) (" + ") (y " + t.getName() + ") (= (" + f.getName() + " x y) ("
+ f.getName() + " y x))))"; + f.getName() + " y x))))";
ctx.parseSMTLIBString(bench, new Symbol[] { t.getName() }, return ctx.parseSMTLIB2String(bench, new Symbol[] { t.getName() },
new Sort[] { t }, new Symbol[] { f.getName() }, new Sort[] { t }, new Symbol[] { f.getName() },
new FuncDecl[] { f }); new FuncDecl[] { f });
return ctx.getSMTLIBFormulas()[0];
} }
// / "Hello world" example: create a Z3 logical context, and delete it. // / "Hello world" example: create a Z3 logical context, and delete it.
@ -1028,21 +1027,6 @@ class JavaExample
} }
} }
// / Shows how to read an SMT1 file.
void smt1FileTest(String filename)
{
System.out.print("SMT File test ");
{
HashMap<String, String> cfg = new HashMap<String, String>();
Context ctx = new Context(cfg);
ctx.parseSMTLIBFile(filename, null, null, null, null);
BoolExpr a = ctx.mkAnd(ctx.getSMTLIBFormulas());
System.out.println("read formula: " + a);
}
}
// / Shows how to read an SMT2 file. // / Shows how to read an SMT2 file.
@ -1459,15 +1443,13 @@ class JavaExample
System.out.println("ParserExample1"); System.out.println("ParserExample1");
Log.append("ParserExample1"); Log.append("ParserExample1");
ctx.parseSMTLIBString( BoolExpr f = ctx.parseSMTLIB2String(
"(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))", "(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))",
null, null, null, null); null, null, null, null);
for (BoolExpr f : ctx.getSMTLIBFormulas()) System.out.println("formula " + f);
System.out.println("formula " + f);
@SuppressWarnings("unused") @SuppressWarnings("unused")
Model m = check(ctx, ctx.mkAnd(ctx.getSMTLIBFormulas()), Model m = check(ctx, f, Status.SATISFIABLE);
Status.SATISFIABLE);
} }
// / Demonstrates how to initialize the parser symbol table. // / Demonstrates how to initialize the parser symbol table.
@ -1482,9 +1464,8 @@ class JavaExample
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 };
ctx.parseSMTLIBString("(benchmark tst :formula (> a b))", null, null, BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null,
declNames, decls); declNames, decls);
BoolExpr f = ctx.getSMTLIBFormulas()[0];
System.out.println("formula: " + f); System.out.println("formula: " + f);
check(ctx, f, Status.SATISFIABLE); check(ctx, f, Status.SATISFIABLE);
} }
@ -1502,39 +1483,14 @@ class JavaExample
BoolExpr ca = commAxiom(ctx, g); BoolExpr ca = commAxiom(ctx, g);
ctx.parseSMTLIBString( BoolExpr thm = ctx.parseSMTLIB2String(
"(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (gg x 0) (gg 0 y)))))", "(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
null, null, new Symbol[] { ctx.mkSymbol("gg") }, null, null, new Symbol[] { ctx.mkSymbol("gg") },
new FuncDecl[] { g }); new FuncDecl[] { g });
BoolExpr thm = ctx.getSMTLIBFormulas()[0];
System.out.println("formula: " + thm); System.out.println("formula: " + thm);
prove(ctx, thm, false, ca); prove(ctx, thm, false, ca);
} }
// / Display the declarations, assumptions and formulas in a SMT-LIB string.
public void parserExample4(Context ctx)
{
System.out.println("ParserExample4");
Log.append("ParserExample4");
ctx.parseSMTLIBString(
"(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))",
null, null, null, null);
for (FuncDecl decl : ctx.getSMTLIBDecls())
{
System.out.println("Declaration: " + decl);
}
for (BoolExpr f : ctx.getSMTLIBAssumptions())
{
System.out.println("Assumption: " + f);
}
for (BoolExpr f : ctx.getSMTLIBFormulas())
{
System.out.println("Formula: " + f);
}
}
// / Demonstrates how to handle parser errors using Z3 error handling // / Demonstrates how to handle parser errors using Z3 error handling
// support. // support.
@ -1546,12 +1502,12 @@ class JavaExample
try try
{ {
ctx.parseSMTLIBString( ctx.parseSMTLIB2String(
/* /*
* the following string has a parsing error: missing * the following string has a parsing error: missing
* parenthesis * 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))",
null, null, null, null); null, null, null, null);
} catch (Z3Exception e) } catch (Z3Exception e)
{ {
@ -2341,7 +2297,6 @@ class JavaExample
p.bitvectorExample2(ctx); p.bitvectorExample2(ctx);
p.parserExample1(ctx); p.parserExample1(ctx);
p.parserExample2(ctx); p.parserExample2(ctx);
p.parserExample4(ctx);
p.parserExample5(ctx); p.parserExample5(ctx);
p.iteExample(ctx); p.iteExample(ctx);
p.evalExample1(ctx); p.evalExample1(ctx);