diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-27 11:12:11 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-27 11:12:26 -0500 |
commit | 86b54ede8a2898a6c51fddd4bb32f8b4b87b5da6 (patch) | |
tree | 989d5595bb52ba2e9cff08e9dd27ccf65e3b0997 /examples/api | |
parent | dd7e0c66cab285c154f59ff27132059c34e09e23 (diff) |
Incremental is now on by default when using from API, off for command-line driver except in interactive mode.
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/bitvectors.cpp | 3 | ||||
-rw-r--r-- | examples/api/combination.cpp | 1 | ||||
-rw-r--r-- | examples/api/java/BitVectors.java | 3 | ||||
-rw-r--r-- | examples/api/java/CVC4Streams.java | 1 | ||||
-rw-r--r-- | examples/api/java/Combination.java | 1 | ||||
-rw-r--r-- | examples/api/java/LinearArith.java | 3 | ||||
-rw-r--r-- | examples/api/java/PipedInput.java | 1 | ||||
-rw-r--r-- | examples/api/linear_arith.cpp | 3 |
8 files changed, 4 insertions, 12 deletions
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index fa3099336..b69ee5d17 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -25,8 +25,7 @@ using namespace CVC4; int main() { ExprManager em; SmtEngine smt(&em); - smt.setOption("incremental", true); // Enable incremental solving - smt.setLogic("QF_BV"); // Set the logic + smt.setLogic("QF_BV"); // Set the logic // The following example has been adapted from the book A Hacker's Delight by // Henry S. Warren. diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index f20f5f13c..4533e35e1 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -45,7 +45,6 @@ int main() { ExprManager em; SmtEngine smt(&em); smt.setOption("produce-models", true); // Produce Models - smt.setOption("incremental", true); // Enable Multiple Queries smt.setOption("output-language", "cvc4"); // Set the output-language to CVC's smt.setOption("default-dag-thresh", 0); //Disable dagifying the output smt.setLogic(string("QF_UFLIRA")); diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index eb3e1642e..f6e719735 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -23,8 +23,7 @@ public class BitVectors { ExprManager em = new ExprManager(); SmtEngine smt = new SmtEngine(em); - smt.setOption("incremental", new SExpr(true)); // Enable incremental solving - smt.setLogic("QF_BV"); // Set the logic + smt.setLogic("QF_BV"); // Set the logic // The following example has been adapted from the book A Hacker's Delight by // Henry S. Warren. diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java index 0b0984bf3..b619b053e 100644 --- a/examples/api/java/CVC4Streams.java +++ b/examples/api/java/CVC4Streams.java @@ -22,7 +22,6 @@ public class CVC4Streams { System.loadLibrary("cvc4jni"); ExprManager exprMgr = new ExprManager(); SmtEngine smt = new SmtEngine(exprMgr); - smt.setOption("incremental", new SExpr(true)); smt.setOption("output-language", new SExpr("smt2")); PipedOutputStream solverPipe = new PipedOutputStream(); diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 283e24a5f..b529f6316 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -41,7 +41,6 @@ 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("cvc4")); // output-language smt.setOption("default-dag-thresh", new SExpr(0)); //Disable dagifying the output smt.setLogic("QF_UFLIRA"); diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index f03dc7f85..582c2ab21 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -24,8 +24,7 @@ public class LinearArith { ExprManager em = new ExprManager(); SmtEngine smt = new SmtEngine(em); - smt.setOption("incremental", new SExpr(true)); // Enable incremental solving - smt.setLogic("QF_LIRA"); // Set the logic + smt.setLogic("QF_LIRA"); // Set the logic // Prove that if given x (Integer) and y (Real) then // the maximum value of y - x is 2/3 diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java index 2e72edf24..de71eb769 100644 --- a/examples/api/java/PipedInput.java +++ b/examples/api/java/PipedInput.java @@ -26,7 +26,6 @@ public class PipedInput { // Boilerplate setup for CVC4 ExprManager exprMgr = new ExprManager(); SmtEngine smt = new SmtEngine(exprMgr); - smt.setOption("incremental", new SExpr(true)); smt.setOption("output-language", new SExpr("smt2")); // Set up a pair of connected Java streams diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index 1c1c439df..87f9d8a5b 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -26,8 +26,7 @@ using namespace CVC4; int main() { ExprManager em; SmtEngine smt(&em); - smt.setOption("incremental", true); // Enable incremental solving - smt.setLogic("QF_LIRA"); // Set the logic + smt.setLogic("QF_LIRA"); // Set the logic // Prove that if given x (Integer) and y (Real) then // the maximum value of y - x is 2/3 |