mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix java

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-02 14:00:37 -07:00
parent 14d780fb2b
commit bb041495e3
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
examples/java/JavaExample.java
View file

@ -167,12 +167,12 @@ class JavaExample
"function must be binary, and argument types must be equal to return type"); "function must be binary, and argument types must be equal to return type");
} }
String bench = "(benchmark comm :formula (forall (x " + t.getName() String bench = "(assert (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))))";
return ctx.parseSMTLIB2String(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 })[0];
} }
// / "Hello world" example: create a Z3 logical context, and delete it. // / "Hello world" example: create a Z3 logical context, and delete it.
@ -1041,7 +1041,7 @@ class JavaExample
HashMap<String, String> cfg = new HashMap<String, String>(); HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true"); cfg.put("model", "true");
Context ctx = new Context(cfg); Context ctx = new Context(cfg);
Expr a = ctx.parseSMTLIB2File(filename, null, null, null, null); Expr a = ctx.MkAnd(ctx.parseSMTLIB2File(filename, null, null, null, null));
long t_diff = ((new Date()).getTime() - before.getTime()) / 1000; long t_diff = ((new Date()).getTime() - before.getTime()) / 1000;
@ -1445,7 +1445,7 @@ class JavaExample
BoolExpr f = ctx.parseSMTLIB2String( BoolExpr f = ctx.parseSMTLIB2String(
"(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))", "(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))",
null, null, null, null); null, null, null, null)[0];
System.out.println("formula " + f); System.out.println("formula " + f);
@SuppressWarnings("unused") @SuppressWarnings("unused")
@ -1465,7 +1465,7 @@ class JavaExample
FuncDecl[] decls = new FuncDecl[] { a, b }; FuncDecl[] decls = new FuncDecl[] { a, b };
BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null, BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null,
declNames, decls); declNames, decls)[0];
System.out.println("formula: " + f); System.out.println("formula: " + f);
check(ctx, f, Status.SATISFIABLE); check(ctx, f, Status.SATISFIABLE);
} }
@ -1486,7 +1486,7 @@ class JavaExample
BoolExpr thm = ctx.parseSMTLIB2String( BoolExpr thm = ctx.parseSMTLIB2String(
"(assert (forall ((x Int) (y Int)) (=> (= 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 })[0];
System.out.println("formula: " + thm); System.out.println("formula: " + thm);
prove(ctx, thm, false, ca); prove(ctx, thm, false, ca);
} }
@ -1508,7 +1508,7 @@ class JavaExample
* parenthesis * parenthesis
*/ */
"(declare-const x Int (declare-const y Int)) (assert (> x y))", "(declare-const x Int (declare-const y Int)) (assert (> x y))",
null, null, null, null); null, null, null, null)[0];
} catch (Z3Exception e) } catch (Z3Exception e)
{ {
System.out.println("Z3 error: " + e); System.out.println("Z3 error: " + e);