diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-28 02:28:39 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-28 02:28:39 -0500 |
commit | b8bd234936a499d72cb5a9444f8cfd82d980fe8f (patch) | |
tree | bd2971ad0f7a5239c89f05abba52ebe3b8da2245 /src/main | |
parent | 3b49d2e6938fbee46737bbd71419febca2ec318d (diff) |
Add option to avoid dumping partial models/proofs.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.cpp | 31 |
1 files changed, 25 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; |