diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main/command_executor.cpp | 31 | ||||
| -rw-r--r-- | src/smt/options | 3 |
2 files changed, 28 insertions, 6 deletions
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 |