From ec834d513b8d390682a08f2ea2d159c3e35a4a2d Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 27 Feb 2011 19:59:52 +0000 Subject: [PATCH] - Adds a path for Theory to be passed a reference to Options. - Adds 3 choices of heuristic variable orders to use in ArithPriorityQueue. - Adds the pivot-rule command line option. --- src/theory/arith/arith_priority_queue.cpp | 50 +++++++++++++++++++++-- src/theory/arith/arith_priority_queue.h | 35 ++++++++++++++-- src/theory/arith/simplex.h | 18 ++++++++ src/theory/arith/theory_arith.h | 3 ++ src/theory/theory.h | 5 +++ src/theory/theory_engine.cpp | 1 + src/theory/theory_engine.h | 4 ++ src/util/options.cpp | 26 +++++++++++- src/util/options.h | 8 +++- 9 files changed, 141 insertions(+), 9 deletions(-) diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 14a228e62..23f547344 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -12,9 +12,19 @@ using namespace CVC4::theory; using namespace CVC4::theory::arith; ArithPriorityQueue::ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau): - d_partialModel(pm), d_tableau(tableau), d_modeInUse(Collection), d_ZERO_DELTA(0,0) + d_pivotRule(MINIMUM), + d_partialModel(pm), + d_tableau(tableau), + d_modeInUse(Collection), + d_ZERO_DELTA(0,0) {} +void ArithPriorityQueue::setPivotRule(PivotRule rule){ + Assert(!inDifferenceMode()); + Debug("arith::setPivotRule") << "setting pivot rule " << rule << endl; + d_pivotRule = rule; +} + ArithVar ArithPriorityQueue::dequeueInconsistentBasicVariable(){ AlwaysAssert(!inCollectionMode()); @@ -23,7 +33,17 @@ ArithVar ArithPriorityQueue::dequeueInconsistentBasicVariable(){ if(inDifferenceMode()){ while(!d_diffQueue.empty()){ ArithVar var = d_diffQueue.front().variable(); - pop_heap(d_diffQueue.begin(), d_diffQueue.end()); + switch(d_pivotRule){ + case MINIMUM: + pop_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule); + break; + case BREAK_TIES: + pop_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules); + break; + case MAXIMUM: + pop_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule); + break; + } d_diffQueue.pop_back(); Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl; if(basicAndInconsistent(var)){ @@ -73,7 +93,17 @@ void ArithPriorityQueue::enqueueIfInconsistent(ArithVar basic){ break; case Difference: d_diffQueue.push_back(computeDiff(basic)); - push_heap(d_diffQueue.begin(), d_diffQueue.end()); + switch(d_pivotRule){ + case MINIMUM: + push_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule); + break; + case BREAK_TIES: + push_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules); + break; + case MAXIMUM: + push_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule); + break; + } break; default: Unreachable(); @@ -95,7 +125,19 @@ void ArithPriorityQueue::transitionToDifferenceMode() { d_diffQueue.push_back(computeDiff(var)); } } - make_heap(d_diffQueue.begin(), d_diffQueue.end()); + + switch(d_pivotRule){ + case MINIMUM: + make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule); + break; + case BREAK_TIES: + make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules); + break; + case MAXIMUM: + make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule); + break; + } + d_candidates.clear(); d_modeInUse = Difference; diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index 2f150b73a..ec0a96aa3 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -41,8 +41,10 @@ namespace arith { * The queue begins in Collection mode. */ class ArithPriorityQueue { -private: +public: + enum PivotRule {MINIMUM, BREAK_TIES, MAXIMUM}; +private: class VarDRatPair { private: ArithVar d_variable; @@ -56,14 +58,38 @@ private: return d_variable; } - bool operator<(const VarDRatPair& other){ - return d_orderBy > other.d_orderBy; + static bool minimumRule(const VarDRatPair& a, const VarDRatPair& b){ + return a.d_orderBy > b.d_orderBy; + } + static bool maximumRule(const VarDRatPair& a, const VarDRatPair& b){ + return a.d_orderBy < b.d_orderBy; + } + + static bool breakTiesRules(const VarDRatPair& a, const VarDRatPair& b){ + const Rational& nonInfA = a.d_orderBy.getNoninfinitesimalPart(); + const Rational& nonInfB = b.d_orderBy.getNoninfinitesimalPart(); + int cmpNonInf = nonInfA.cmp(nonInfB); + if(cmpNonInf == 0){ + const Rational& infA = a.d_orderBy.getInfinitesimalPart(); + const Rational& infB = b.d_orderBy.getInfinitesimalPart(); + int cmpInf = infA.cmp(infB); + if(cmpInf == 0){ + return a.d_variable > b.d_variable; + }else{ + return cmpInf > 0; + } + }else{ + return cmpNonInf > 0; + } + + return a.d_orderBy > b.d_orderBy; } }; typedef std::vector DifferenceArray; typedef std::vector ArithVarArray; + PivotRule d_pivotRule; /** * An unordered array with no heap structure for use during collection mode. @@ -116,6 +142,9 @@ public: ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau); + /** precondition: !inDifferenceMode() */ + void setPivotRule(PivotRule rule); + ArithVar dequeueInconsistentBasicVariable(); void enqueueIfInconsistent(ArithVar basic); diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 3b86935bd..a32a188b4 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -12,6 +12,8 @@ #include "theory/arith/partial_model.h" #include "theory/output_channel.h" +#include "util/options.h" + #include "util/stats.h" #include @@ -150,6 +152,22 @@ private: Node generateConflictBelow(ArithVar conflictVar); public: + void notifyOptions(const Options& opt){ + switch(opt.pivotRule){ + case Options::MINIMUM: + d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); + break; + case Options::BREAK_TIES: + d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES); + break; + case Options::MAXIMUM: + d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM); + break; + default: + Unhandled(opt.pivotRule); + } + } + /** * Checks to make sure the assignment is consistent with the tableau. * This code is for debugging. diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e29054c16..dc841170b 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -162,6 +162,9 @@ public: std::string identify() const { return std::string("TheoryArith"); } + void notifyOptions(const Options& opt) { + d_simplex.notifyOptions(opt); + } private: ArithVar determineLeftVariable(TNode assertion, Kind simpleKind); diff --git a/src/theory/theory.h b/src/theory/theory.h index b4c3a897b..85ea375f7 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -27,6 +27,7 @@ #include "context/context.h" #include "context/cdlist.h" #include "context/cdo.h" +#include "util/options.h" #include #include @@ -95,6 +96,8 @@ protected: d_out(&out) { } + + /** * This is called at shutdown time by the TheoryEngine, just before * destruction. It is important because there are destruction @@ -376,6 +379,8 @@ public: */ virtual std::string identify() const = 0; + virtual void notifyOptions(const Options& opt) {} + // // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS) // diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 97cb8f471..a577e8f9b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -135,6 +135,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) : d_hasShutDown(false), d_incomplete(ctxt, false), d_valuation(this), + d_opts(opts), d_statistics() { Rewriter::init(); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6a343717a..7a82a1b05 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -154,6 +154,8 @@ class TheoryEngine { */ Node removeITEs(TNode t); + const Options& d_opts; + public: /** @@ -174,6 +176,8 @@ public: TheoryClass* theory = new TheoryClass(d_context, d_theoryOut); d_theoryTable[theory->getId()] = theory; d_sharedTermManager->registerTheory(static_cast(theory)); + + theory->notifyOptions(d_opts); } SharedTermManager* getSharedTermManager() { diff --git a/src/util/options.cpp b/src/util/options.cpp index dcf146010..0c3915d1d 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -120,7 +120,8 @@ enum OptionValue { NO_TYPE_CHECKING, LAZY_TYPE_CHECKING, EAGER_TYPE_CHECKING, - INCREMENTAL + INCREMENTAL, + PIVOT_RULE };/* enum OptionValue */ /** @@ -177,6 +178,7 @@ static struct option cmdlineOptions[] = { { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING}, { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING}, { "incremental", no_argument, NULL, INCREMENTAL}, + { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -374,6 +376,28 @@ throw(OptionException) { incrementalSolving = true; break; + case PIVOT_RULE: + if(!strcmp(optarg, "min")) { + pivotRule = MINIMUM; + break; + } else if(!strcmp(optarg, "min-break-ties")) { + pivotRule = BREAK_TIES; + break; + } else if(!strcmp(optarg, "max")) { + pivotRule = MAXIMUM; + break; + } else if(!strcmp(optarg, "help")) { + printf("Pivot rules available:\n"); + printf("min\n"); + printf("min-break-ties\n"); + printf("max\n"); + exit(1); + } else { + throw OptionException(string("unknown option for --pivot-rule: `") + + optarg + "'. Try --pivot-rule help."); + } + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); diff --git a/src/util/options.h b/src/util/options.h index 1eca0d499..2618f8512 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -129,6 +129,10 @@ struct CVC4_PUBLIC Options { /** Whether incemental solving (push/pop) */ bool incrementalSolving; + + typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; + ArithPivotRule pivotRule; + Options() : binary_name(), statistics(false), @@ -151,7 +155,9 @@ struct CVC4_PUBLIC Options { produceAssignments(false), typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT), earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT), - incrementalSolving(false) { + incrementalSolving(false), + pivotRule(MINIMUM) + { } /** -- 2.30.2