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, 96 insertions, 0 deletions

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
new file mode 100644
index 000000000..cb2216d6d
--- /dev/null
+++ b/src/decision/justification_heuristic.h
@@ -0,0 +1,96 @@
+/*********************                                                        */
+/*! \file justification_heuristic.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Justification heuristic for decision making
+ **
+ ** A ATGP-inspired justification-based decision heuristic. See
+ ** [insert reference] for more details. This code is, or not, based
+ ** on the CVC3 implementation of the same heuristic.
+ **
+ ** It needs access to the simplified but non-clausal formula.
+ **/
+
+#ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
+#define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
+
+#include "decision_engine.h"
+#include "decision_strategy.h"
+
+#include "prop/sat_solver_types.h"
+#include "expr/node.h"
+
+using namespace CVC4::prop;
+
+namespace CVC4 {
+
+namespace decision {
+
+class JustificationHeuristic : public DecisionStrategy {
+  set<SatVariable> d_justified;
+  unsigned  d_prvsIndex;
+public:
+  JustificationHeuristic(CVC4::DecisionEngine* de) : 
+    DecisionStrategy(de) {
+    Trace("decision") << "Justification heuristic enabled" << std::endl;
+  }
+  prop::SatLiteral getNext() {
+    Trace("decision") << "JustificationHeuristic::getNext()" << std::endl;
+
+    const vector<Node>& assertions = d_decisionEngine->getAssertions();
+
+    for(unsigned i = d_prvsIndex; i < assertions.size(); ++i) {
+      SatLiteral litDecision;
+
+      /* Make sure there is a literal corresponding to the node  */
+      if( not d_decisionEngine->hasSatLiteral(assertions[i]) ) {
+        //    Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
+        continue;
+        //    Assert(not lit.isNull());
+      }
+      
+      SatLiteral lit = d_decisionEngine->getSatLiteral(assertions[i]);
+      SatValue desiredVal = d_decisionEngine->getSatValue(lit);
+      if(desiredVal == SAT_VALUE_UNKNOWN) desiredVal = SAT_VALUE_TRUE;
+      bool ret = findSplitterRec(lit, desiredVal, &litDecision);
+      if(ret == true) {
+        d_prvsIndex = i;
+        return litDecision;
+      }
+    }
+
+    return prop::undefSatLiteral;
+  } 
+  bool needSimplifiedPreITEAssertions() { return true; }
+  void notifyAssertionsAvailable() {
+    Trace("decision") << "JustificationHeuristic::notifyAssertionsAvailable()" 
+                      << "  size = " << d_decisionEngine->getAssertions().size()
+                      << std::endl;
+    /* clear the justifcation labels -- reconsider if/when to do
+       this */
+    d_justified.clear();
+    d_prvsIndex = 0;
+  }
+private:
+  /* Do all the hardwork. */ 
+  bool findSplitterRec(SatLiteral lit, SatValue value, SatLiteral* litDecision);
+
+  /* Helper functions */
+  void setJustified(SatVariable v);
+  bool checkJustified(SatVariable v);
+};/* class JustificationHeuristic */
+
+}/* namespace decision */
+
+}/* namespace CVC4 */
+
+#endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */