From 8862cb4833a684124baf75897e26598f26883fa1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 9 Apr 2015 14:46:59 +0100 Subject: [PATCH] Java example: Removed throws declarations for Z3Exception. --- examples/java/JavaExample.java | 127 ++++++++++++++------------------- 1 file changed, 52 insertions(+), 75 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 5c49b56ae..4a579f9da 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -41,7 +41,7 @@ class JavaExample // / // / Where, finvis 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, finvis 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 // / This example demonstrates how to use the array // theory. - 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 // / This example also shows how to use the distinct // construct. - 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 // / f is injective in the second argument. - 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 // / f is injective in the second argument. - 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(); @@ -1096,7 +1088,7 @@ class JavaExample // / Shows how to use Solver(logic) // / @param ctx - void logicExample(Context ctx) throws Z3Exception, TestFailedException + void logicExample(Context ctx) throws TestFailedException { System.out.println("LogicTest"); Log.append("LogicTest"); @@ -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 x xor y. - 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 x < y + 1, x > 2. // / Then, assert not(x = y), 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 // / This function demonstrates how to create uninterpreted // / types and functions. - 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 // / This example demonstrates how to combine uninterpreted // functions // / and arithmetic. - 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 // / This example also demonstrates how big numbers can be // / created in ctx. - 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 // / Check that the projection of a tuple // / returns the corresponding element. - 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 <= 0 IFF x <= 10 for (32-bit) // machine integers // / - 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) // / - 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. // / Note: this test is specialized to 32-bit bitvectors. - 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"); @@ -2140,7 +2117,7 @@ class JavaExample /// Extract unsatisfiable core example with AssertAndTrack - public void unsatCoreAndProofExample2(Context ctx) throws Z3Exception + public void unsatCoreAndProofExample2(Context ctx) { System.out.println("UnsatCoreAndProofExample2"); Log.append("UnsatCoreAndProofExample2"); @@ -2179,7 +2156,7 @@ class JavaExample } } - public void finiteDomainExample(Context ctx) throws Z3Exception + public void finiteDomainExample(Context ctx) { System.out.println("FiniteDomainExample"); Log.append("FiniteDomainExample"); @@ -2198,7 +2175,7 @@ class JavaExample // System.out.println(ctx.mkEq(s1, t1)); } - public void floatingPointExample1(Context ctx) throws Z3Exception, TestFailedException + public void floatingPointExample1(Context ctx) throws TestFailedException { System.out.println("FloatingPointExample1"); Log.append("FloatingPointExample1"); @@ -2249,7 +2226,7 @@ class JavaExample System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr); } - public void floatingPointExample2(Context ctx) throws Z3Exception, TestFailedException + public void floatingPointExample2(Context ctx) throws TestFailedException { System.out.println("FloatingPointExample2"); Log.append("FloatingPointExample2");