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

1 files changed, 4 insertions, 4 deletions

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);