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

diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index fa309933673bbcedb482fe503786a5a18daf9e20..b69ee5d17f1826f8cf17221d0deb6af14fa5df41 100644 (file)
--- 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 f20f5f13c92b9bf13c3d9f0a41dc6aff270a03d0..4533e35e1ddd5c94144b1c7cc8c1b2bad957a6a4 100644 (file)
--- 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 eb3e1642ef97f26d707baa7adc0c8dc90bbb477e..f6e719735f857b1dce05e5fc76822f0a45997dd5 100644 (file)
--- 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 0b0984bf3752ef6f365239569594122e0b867506..b619b053eee7afea57f89cf115b9afb8f830a473 100644 (file)
--- 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 283e24a5f9a9084d532f5e9af0d2f3e0191fd535..b529f6316f1a9650ad5c28968576dec687be69a4 100644 (file)
--- 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 f03dc7f858805cff6824d7639ac85e143efa415e..582c2ab2119f9696c674faa271306b006b0b967d 100644 (file)
--- 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 2e72edf2478ec8246c9ac481f743a8fa21b2fc51..de71eb769ec4ffea86d13296569ab47b1c3aa563 100644 (file)
--- 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 1c1c439df2a23038d57d8250e0e920e8b9c9ec6c..87f9d8a5b7f6175093f6d0abfa45697ed4c29531 100644 (file)
--- 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 e9d071918a3ce0d3a08ba5fb15ec3df203299100..3f5e5424e8ac443afcc2bfe457533e8a3bc5d8f7 100644 (file)
--- 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 6b9944cdd0a6e8e5545dd502af1dab6b1ade177d..f3da7a0a75025b6cf252cf7ec56a2462a2c764fb 100644 (file)
--- 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