diff options
| -rwxr-xr-x | contrib/run-script-cascj7-fnt | 8 | ||||
| -rwxr-xr-x | contrib/run-script-cascj7-fof | 4 | ||||
| -rw-r--r-- | src/main/command_executor.cpp | 31 | ||||
| -rw-r--r-- | src/smt/options | 3 |
4 files changed, 34 insertions, 12 deletions
diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt index 9e754ffc7..ce54fe5ae 100755 --- 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 2e4f4d0b9..783eca17e 100755 --- 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 4644c91a7..94f9a6100 100644 --- 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 7b749fc6c..9c7eea12f 100644 --- 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 |