Add option to avoid dumping partial models/proofs.

diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt
index 9e754ffc72991704365bd2fd59a1ba51f35ee247..ce54fe5aec6bd5df7e9edba5be5a1204939b0fcd 100755 (executable)
--- a/contrib/run-script-cascj7-fnt
+++ b/contrib/run-script-cascj7-fnt
@@ -15,7 +15,7 @@ echo "------- cvc4-fnt casc j7 : $bench at $2..."
 function trywith {
   limit=$1; shift;
   echo "--- Run $@ at $limit...";
-  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null |
+  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
   (read w1 w2 w3 result w4 w5;
   case "$result" in
   Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
@@ -25,12 +25,12 @@ function trywith {
 }
 function finishwith {
   echo "--- Run $@...";
-  $cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench
+  $cvc4 --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
 }
 
 trywith 30 --finite-model-find --sort-inference --uf-ss-fair
 trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal --sort-inference --uf-ss-fair
-trywith 10 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair
-trywith 30 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
+trywith 15 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair
+trywith 60 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
 finishwith --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair --mbqi-one-inst-per-round
 # echo "% SZS status" "GaveUp for $filename"

diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof
index 2e4f4d0b925c54e48a8e17e0165b4ada1c461c3c..783eca17e3bdab55aa20b0efff4367fdd986b917 100755 (executable)
--- a/contrib/run-script-cascj7-fof
+++ b/contrib/run-script-cascj7-fof
@@ -15,7 +15,7 @@ echo "------- cvc4-fof casc j7 : $bench at $2..."
 function trywith {
   limit=$1; shift;
   echo "--- Run $@ at $limit...";
-  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench) 2>/dev/null |
+  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
   (read w1 w2 w3 result w4 w5;
   case "$result" in
   Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
@@ -25,7 +25,7 @@ function trywith {
 }
 function finishwith {
   echo "--- Run $@...";
-  $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench
+  $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
 }
 
 trywith 15 --quant-cf --pre-skolem-quant --full-saturate-quant

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 4644c91a7dcbad8bc450085e725d2d5c3f73b914..94f9a61004474d09958973265089d52d387c4202 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -21,9 +21,23 @@
 
 #include "smt/options.h"
 
+#include <sys/resource.h>
+
 namespace CVC4 {
 namespace main {
 
+//function to set no limit on CPU time.
+//this is used for competitions while a solution (proof or model) is being dumped.
+void setNoLimitCPU(){
+  struct rlimit rlc;
+  int st = getrlimit(RLIMIT_CPU, &rlc );
+  if( st==0 ){
+    rlc.rlim_cur = rlc.rlim_max;
+    setrlimit(RLIMIT_CPU, &rlc );
+  }
+}
+
+
 void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
 
 CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
@@ -98,21 +112,26 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 
   // dump the model/proof if option is set
   if(status) {
+    Command * g = NULL;
     if( d_options[options::produceModels] &&
         d_options[options::dumpModels] &&
         ( res.asSatisfiabilityResult() == Result::SAT ||
           (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
-      Command* gm = new GetModelCommand();
-      status = doCommandSingleton(gm);
+      g = new GetModelCommand();
     } else if( d_options[options::proof] &&
                d_options[options::dumpProofs] &&
                res.asSatisfiabilityResult() == Result::UNSAT ) {
-      Command* gp = new GetProofCommand();
-      status = doCommandSingleton(gp);
+      g = new GetProofCommand();
     } else if( d_options[options::dumpInstantiations] &&
                res.asSatisfiabilityResult() == Result::UNSAT ) {
-      Command* gi = new GetInstantiationsCommand();
-      status = doCommandSingleton(gi);
+      g = new GetInstantiationsCommand();
+    }
+    if( g ){
+      //set no time limit during dumping if applicable
+      if( d_options[options::forceNoLimitCpuWhileDump] ){
+        setNoLimitCPU();
+      }
+      status = doCommandSingleton(g);
     }
   }
   return status;

diff --git a/src/smt/options b/src/smt/options
index 7b749fc6cbeeb51ed67da8c32077085bb781a224..9c7eea12fd7eb2906132f86431c6fb418b96602a 100644 (file)
--- a/src/smt/options
+++ b/src/smt/options
@@ -110,4 +110,7 @@ option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_i
 option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
  The output channel to receive notfication events for new lemmas
 
+option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
+ Force no CPU limit when dumping models and proofs
+
 endmodule