diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-12-01 01:43:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-12-01 01:43:08 +0000 |
commit | 8953b603bd6960eb59ccb41a63d4742096da1c4a (patch) | |
tree | 197300f8a004a5ae01cdefb152690c30248d83c7 /examples/api/java/Combination.java | |
parent | e39b94aa9425123420635c298fa6bb8a2ee4f048 (diff) |
updated examples
Diffstat (limited to 'examples/api/java/Combination.java')
-rw-r--r-- | examples/api/java/Combination.java | 25 |
1 files changed, 15 insertions, 10 deletions
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 3f5826f12..d45a8ad16 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -13,22 +13,23 @@ ** ** A simple demonstration of how to use uninterpreted functions, combining this ** with arithmetic, and extracting a model at the end of a satisfiable query. + ** The model is displayed using getValue(). **/ import edu.nyu.acsys.CVC4.*; public class Combination { - private static void preFixPrintGetValue(SmtEngine smt, Expr e, int level) { + private static void prefixPrintGetValue(SmtEngine smt, Expr e, int level) { for(int i = 0; i < level; ++i) { System.out.print('-'); } System.out.println("smt.getValue(" + e + ") -> " + smt.getValue(e)); if(e.hasOperator()) { - preFixPrintGetValue(smt, e.getOperator(), level + 1); + prefixPrintGetValue(smt, e.getOperator(), level + 1); } for(int i = 0; i < e.getNumChildren(); ++i) { Expr curr = e.getChild(i); - preFixPrintGetValue(smt, curr, level + 1); + prefixPrintGetValue(smt, curr, level + 1); } } @@ -41,8 +42,9 @@ public class Combination { smt.setOption("tlimit", new SExpr(100)); smt.setOption("produce-models", new SExpr(true)); // Produce Models smt.setOption("incremental", new SExpr(true)); // Enable Multiple Queries - smt.setOption("output-language", new SExpr("smtlib")); // output-language + smt.setOption("output-language", new SExpr("cvc4")); // output-language smt.setOption("default-dag-thresh", new SExpr(0)); //Disable dagifying the output + smt.setLogic("QF_UFLIRA"); // Sorts SortType u = em.mkSort("u"); @@ -70,6 +72,7 @@ public class Combination { Expr p_0 = em.mkExpr(Kind.APPLY_UF, p, zero); Expr p_f_y = em.mkExpr(Kind.APPLY_UF, p, f_y); + // Construct the assumptions Expr assumptions = em.mkExpr(Kind.AND, em.mkExpr(Kind.LEQ, zero, f_x), // 0 <= f(x) @@ -81,15 +84,17 @@ public class Combination { System.out.println("Given the following assumptions:"); System.out.println(assumptions); - System.out.println("Prove x /= y is valid. " - + "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) + "."); + System.out.println("Prove x /= y is valid. " + + "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) + + "."); System.out.println("Now we call checksat on a trivial query to show that"); - System.out.println("the assumptions are satisfiable: " - + smt.checkSat(em.mkConst(true)) + "."); + System.out.println("the assumptions are satisfiable: " + + smt.checkSat(em.mkConst(true)) + "."); - System.out.println("Finally, after a SAT call, we use smt.getValue(...) to generate a model."); - preFixPrintGetValue(smt, assumptions, 0); + System.out.println("Finally, after a SAT call, we recursively call smt.getValue(...) on" + + "all of the assumptions to see what the satisfying model looks like."); + prefixPrintGetValue(smt, assumptions, 0); } } |