diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-17 17:20:37 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-17 17:20:37 +0000 |
commit | 7742c4211f765c2ba2637a211265c20789b861ee (patch) | |
tree | 05622a9df5dc2c900608b8e2ac5611d70e3208c6 /src/theory/arith | |
parent | ccd77233892ace44fd4852999e66534d1c2283ea (diff) |
A dummy decision engine. Expected performance impact: none.
Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.
Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_priority_queue.h | 2 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/simplex.h | 8 |
3 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index 8c7069975..9dd8e588a 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -119,7 +119,7 @@ private: /** * Priority Queue of the basic variables that may be inconsistent. * Variables are ordered according to which violates its bound the most. - * This is a hueristic and makes no guarentees to terminate! + * This is a heuristic and makes no guarentees to terminate! * This heuristic comes from Alberto Griggio's thesis. */ DifferenceArray d_diffQueue; diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 5837d4793..9f48dad77 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -254,9 +254,9 @@ bool SimplexDecisionProcedure::findModel(){ foundConflict = findConflictOnTheQueue(BeforeDiffSearch); } if(!foundConflict){ - uint32_t numHueristicPivots = d_numVariables + 1; - uint32_t pivotsRemaining = numHueristicPivots; - uint32_t pivotsPerCheck = (numHueristicPivots/NUM_CHECKS) + (NUM_CHECKS-1); + uint32_t numHeuristicPivots = d_numVariables + 1; + uint32_t pivotsRemaining = numHeuristicPivots; + uint32_t pivotsPerCheck = (numHeuristicPivots/NUM_CHECKS) + (NUM_CHECKS-1); while(!d_queue.empty() && !foundConflict && pivotsRemaining > 0){ diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 4e5ba3d9e..7ad7734c7 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -27,13 +27,13 @@ ** we do not maintain that the queue of variables needs to be only basic variables or only variables that satisfy their bounds. ** ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a hueristic pivoting rule. (See PreferenceFunction Documentation for the available options.) + ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction Documentation for the available options.) ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that Leonardo invented this first.) ** After this, Bland's pivot rule is invoked. ** ** During this proccess, we periodically inspect the queue of variables to ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the current queue hueristics, and + ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the current queue heuristics, and ** 3) detect multiple conflicts. ** ** Conflicts are greedily slackened to use the weakest bounds that still produce the conflict. @@ -152,7 +152,7 @@ private: * minRowCount is a PreferenceFunction for selecting the variable with the smaller * row count in the tableau. * - * This is a hueristic rule and should not be used + * This is a heuristic rule and should not be used * during the VarOrder stage of findModel. */ static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); @@ -163,7 +163,7 @@ private: * If both have bounds or both do not have bounds, * the rule falls back to minRowCount(...). * - * This is a hueristic rule and should not be used + * This is a heuristic rule and should not be used * during the VarOrder stage of findModel. */ static ArithVar minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); |