Incremental is now on by default when using from API, off for command-line driver except in interactive mode.

10 files changed, 14 insertions, 15 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
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index e9d071918..3f5e5424e 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -194,7 +194,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   pExecutor = new CommandExecutor(*exprMgr, opts);
 # else
   vector<Options> threadOpts = parseThreadSpecificOptions(opts);
-  if(opts[options::incrementalSolving] && !opts[options::incrementalParallel]) {
+  if(opts.wasSetByUser[options::incrementalSolving] &&
+     opts[options::incrementalSolving] &&
+     !opts[options::incrementalParallel]) {
     Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n"
              << "Notice: ...the experimental --incremental-parallel option.\n";
     exprMgr = new ExprManager(opts);
@@ -264,6 +266,12 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
     } else {
+      if(!opts.wasSetByUser(options::incrementalSolving)) {
+        cmd = new SetOptionCommand("incremental", false);
+        pExecutor->doCommand(cmd);
+        delete cmd;
+      }
+
       ParserBuilder parserBuilder(exprMgr, filename, opts);
 
       if( inputFromStdin ) {
diff --git a/src/smt/options b/src/smt/options
index 6b9944cdd..f3da7a0a7 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -63,10 +63,9 @@ option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288
 option sortInference --sort-inference bool :read-write :default false
  calculate sort inference of input problem, convert the input based on monotonic sorts
 
-common-option incrementalSolving incremental -i --incremental bool
+common-option incrementalSolving incremental -i --incremental bool :default true
  enable incremental solving
 
-
 option abstractValues abstract-values --abstract-values bool :default false
  in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
 option modelUninterpDtEnum --model-u-dt-enum bool :default false