diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
commit | 3cbb76ef86a769cfe3dac5976a14e1bc43c42ca6 (patch) | |
tree | e08efdc63abd663de4f5750db9326b69c79829e5 /src/util | |
parent | 3a7aafccadbfa1543c435b7dfe4f53116224a11f (diff) |
Interruption, time-out, and deterministic time-out ("resource-out") features.
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/options.cpp | 53 | ||||
-rw-r--r-- | src/util/options.h | 10 | ||||
-rw-r--r-- | src/util/result.cpp | 11 | ||||
-rw-r--r-- | src/util/result.h | 2 |
4 files changed, 74 insertions, 2 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index 9c438a5cd..a01237fd0 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -138,7 +138,11 @@ static const string optionsDescription = "\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\ - --incremental | -i enable incremental solving\n"; + --incremental | -i enable incremental solving\n\ + --time-limit=MS enable time limiting (give milliseconds)\n\ + --time-limit-per=MS enable time limiting per query (give milliseconds)\n\ + --limit=N enable resource limiting\n\ + --limit-per=N enable resource limiting per query\n"; #warning "Change CL options as --disable-variable-removal cannot do anything currently." @@ -296,7 +300,11 @@ enum OptionValue { ARITHMETIC_PROPAGATION, ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH, - DISABLE_SYMMETRY_BREAKER + DISABLE_SYMMETRY_BREAKER, + TIME_LIMIT, + TIME_LIMIT_PER, + LIMIT, + LIMIT_PER };/* enum OptionValue */ /** @@ -371,6 +379,10 @@ static struct option cmdlineOptions[] = { { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, + { "time-limit" , required_argument, NULL, TIME_LIMIT }, + { "time-limit-per", required_argument, NULL, TIME_LIMIT_PER }, + { "limit" , required_argument, NULL, LIMIT }, + { "limit-per" , required_argument, NULL, LIMIT_PER }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -677,6 +689,43 @@ throw(OptionException) { ufSymmetryBreaker = false; break; + case TIME_LIMIT: + { + int i = atoi(optarg); + if(i < 0) { + throw OptionException("--time-limit requires a nonnegative argument."); + } + cumulativeMillisecondLimit = (unsigned long) i; + } + break; + case TIME_LIMIT_PER: + { + int i = atoi(optarg); + if(i < 0) { + throw OptionException("--time-limit-per requires a nonnegative argument."); + } + perCallMillisecondLimit = (unsigned long) i; + } + break; + case LIMIT: + { + int i = atoi(optarg); + if(i < 0) { + throw OptionException("--limit requires a nonnegative argument."); + } + cumulativeResourceLimit = (unsigned long) i; + } + break; + case LIMIT_PER: + { + int i = atoi(optarg); + if(i < 0) { + throw OptionException("--limit-per requires a nonnegative argument."); + } + perCallResourceLimit = (unsigned long) i; + break; + } + case RANDOM_SEED: satRandomSeed = atof(optarg); break; diff --git a/src/util/options.h b/src/util/options.h index 7fc894d93..f9dc042d1 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -129,6 +129,16 @@ struct CVC4_PUBLIC Options { */ bool interactiveSetByUser; + /** Per-query resource limit. */ + unsigned long perCallResourceLimit; + /** Cumulative resource limit. */ + unsigned long cumulativeResourceLimit; + + /** Per-query time limit in milliseconds. */ + unsigned long perCallMillisecondLimit; + /** Cumulative time limit in milliseconds. */ + unsigned long cumulativeMillisecondLimit; + /** Whether we should "spin" on a SIG_SEGV. */ bool segvNoSpin; diff --git a/src/util/result.cpp b/src/util/result.cpp index 8a2bcf3b2..bdb17f54c 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -55,10 +55,18 @@ Result::Result(const std::string& instr) : d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = TIMEOUT; + } else if(s == "resourceout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = RESOURCEOUT; } else if(s == "memout") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = MEMOUT; + } else if(s == "interrupted") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = INTERRUPTED; } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; @@ -169,8 +177,11 @@ ostream& operator<<(ostream& out, case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break; case Result::INCOMPLETE: out << "INCOMPLETE"; break; case Result::TIMEOUT: out << "TIMEOUT"; break; + case Result::RESOURCEOUT: out << "RESOURCEOUT"; break; case Result::MEMOUT: out << "MEMOUT"; break; + case Result::INTERRUPTED: out << "INTERRUPTED"; break; case Result::NO_STATUS: out << "NO_STATUS"; break; + case Result::UNSUPPORTED: out << "UNSUPPORTED"; break; case Result::OTHER: out << "OTHER"; break; case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; default: Unhandled(e); diff --git a/src/util/result.h b/src/util/result.h index c4733eab9..ac52ee382 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -59,7 +59,9 @@ public: REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT, + RESOURCEOUT, MEMOUT, + INTERRUPTED, NO_STATUS, UNSUPPORTED, OTHER, |