From 86b54ede8a2898a6c51fddd4bb32f8b4b87b5da6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 27 Nov 2013 11:12:11 -0500 Subject: [PATCH] Incremental is now on by default when using from API, off for command-line driver except in interactive mode. --- examples/api/bitvectors.cpp | 3 +-- examples/api/combination.cpp | 1 - examples/api/java/BitVectors.java | 3 +-- examples/api/java/CVC4Streams.java | 1 - examples/api/java/Combination.java | 1 - examples/api/java/LinearArith.java | 3 +-- examples/api/java/PipedInput.java | 1 - examples/api/linear_arith.cpp | 3 +-- src/main/driver_unified.cpp | 10 +++++++++- src/smt/options | 3 +-- 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 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 -- 2.30.2