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

7 files changed, 761 insertions, 0 deletions

diff --git a/src/decision/Makefile b/src/decision/Makefile
new file mode 100644
index 000000000..27978f85f
--- /dev/null
+++ b/src/decision/Makefile
@@ -0,0 +1,4 @@
+topdir = ../..
+srcdir = src/decision
+
+include $(topdir)/Makefile.subdir
diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am
new file mode 100644
index 000000000..c399cbf71
--- /dev/null
+++ b/src/decision/Makefile.am
@@ -0,0 +1,13 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libdecision.la
+
+libdecision_la_SOURCES = \
+	decision_engine.h \
+	decision_engine.cpp \
+	decision_strategy.h \
+	justification_heuristic.h \
+	justification_heuristic.cpp
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
new file mode 100644
index 000000000..936ac8e73
--- /dev/null
+++ b/src/decision/decision_engine.cpp
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file decision_engine.cpp
+ ** \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 Decision engine
+ **
+ ** Decision engine
+ **/
+
+#include "decision/decision_engine.h"
+#include "decision/justification_heuristic.h"
+
+#include "expr/node.h"
+#include "util/options.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+DecisionEngine::DecisionEngine() : d_needSimplifiedPreITEAssertions() {
+  const Options* options = Options::current();
+  Trace("decision") << "Creating decision engine" << std::endl;
+  if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
+  if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
+    DecisionStrategy* ds = new decision::JustificationHeuristic(this);
+    enableStrategy(ds);
+  }
+}
+
+void DecisionEngine::enableStrategy(DecisionStrategy* ds)
+{
+  d_enabledStrategies.push_back(ds);
+  if( ds->needSimplifiedPreITEAssertions() )
+    d_needSimplifiedPreITEAssertions.push_back(ds);
+}
+
+void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions)
+{
+  d_assertions.reserve(assertions.size());
+  for(unsigned i = 0; i < assertions.size(); ++i)
+    d_assertions.push_back(assertions[i]);
+  for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i)
+    d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
+}
+
+}/* CVC4 namespace */
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
new file mode 100644
index 000000000..d4037acff
--- /dev/null
+++ b/src/decision/decision_engine.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file decision_engine.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 Decision engine
+ **
+ ** Decision engine
+ **/
+
+#ifndef __CVC4__DECISION__DECISION_ENGINE_H
+#define __CVC4__DECISION__DECISION_ENGINE_H
+
+#include <vector>
+
+#include "decision/decision_strategy.h"
+
+#include "expr/node.h"
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/sat_solver_types.h"
+#include "util/output.h"
+
+using namespace std;
+using namespace CVC4::prop;
+using namespace CVC4::decision;
+
+namespace CVC4 {
+
+class DecisionEngine {
+
+  vector <DecisionStrategy* > d_enabledStrategies;
+  vector <DecisionStrategy* > d_needSimplifiedPreITEAssertions;
+
+  vector <Node> d_assertions;
+
+  // PropEngine* d_propEngine;
+  CnfStream* d_cnfStream;
+  DPLLSatSolverInterface* d_satSolver;
+public:
+  // Necessary functions
+
+  /** Constructor, enables decision stragies based on options */
+  DecisionEngine();
+
+  /** Destructor, currently does nothing */
+  ~DecisionEngine() {
+    Trace("decision") << "Destroying decision engine" << std::endl;
+  }
+  
+  // void setPropEngine(PropEngine* pe) {
+  //   // setPropEngine should not be called more than once
+  //   Assert(d_propEngine == NULL);
+  //   Assert(pe != NULL);
+  //   d_propEngine = pe;
+  // }
+
+  void setSatSolver(DPLLSatSolverInterface* ss) {
+    // setPropEngine should not be called more than once
+    Assert(d_satSolver == NULL);
+    Assert(ss != NULL);
+    d_satSolver = ss;
+  }
+
+  void setCnfStream(CnfStream* cs) {
+    // setPropEngine should not be called more than once
+    Assert(d_cnfStream == NULL);
+    Assert(cs != NULL);
+    d_cnfStream = cs;
+  }
+
+
+  // Interface for External World to use our services
+
+  /** Gets the next decision based on strategies that are enabled */
+  SatLiteral getNext() {
+    SatLiteral ret = undefSatLiteral;
+    for(unsigned i = 0; i < d_enabledStrategies.size() 
+          and ret == undefSatLiteral; ++i) {
+      ret = d_enabledStrategies[i]->getNext();
+    }
+    return ret;
+  }
+
+  /**
+   * This is called by SmtEngine, at shutdown time, just before
+   * destruction.  It is important because there are destruction
+   * ordering issues between some parts of the system.  For now,
+   * there's nothing to do here in the DecisionEngine.
+   */
+  void shutdown() {
+    Trace("decision") << "Shutting down decision engine" << std::endl;
+  }
+
+
+  // External World helping us help the Strategies
+
+  /** If one of the enabled strategies needs them  */
+  bool needSimplifiedPreITEAssertions() {
+    return d_needSimplifiedPreITEAssertions.size() > 0;
+  }
+  void informSimplifiedPreITEAssertions(const vector<Node> &assertions);
+
+
+  // Interface for Strategies to use stuff stored in Decision Engine
+  // (which was possibly requested by them on initialization)
+
+  /**
+   * Get the assertions. Strategies are notified when these are available. 
+   */
+  const vector<Node>& getAssertions() {
+    return d_assertions;
+  }
+
+
+  // Interface for Strategies to get information about External World
+
+  bool hasSatLiteral(Node n) {
+    return d_cnfStream->hasLiteral(n);
+  }
+  SatLiteral getSatLiteral(Node n) {
+    return d_cnfStream->getLiteral(n);
+  }
+  SatValue getSatValue(SatLiteral l) {
+    return d_satSolver->value(l);
+  }
+  Node getNode(SatLiteral l) {
+    return d_cnfStream->getNode(l);
+  }
+
+private:
+  /**
+   * Enable a particular decision strategy, also updating
+   * corresponding vector<DecisionStrategy*>-s is the engine
+   */
+  void enableStrategy(DecisionStrategy* ds);
+
+};/* DecisionEngine class */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DECISION__DECISION_ENGINE_H */
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
new file mode 100644
index 000000000..abcbbaace
--- /dev/null
+++ b/src/decision/decision_strategy.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file decision_strategy.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 Decision stategy
+ **
+ ** Decision strategy
+ **/
+
+#ifndef __CVC4__DECISION__DECISION_STRATEGY_H
+#define __CVC4__DECISION__DECISION_STRATEGY_H
+
+#include "prop/sat_solver_types.h"
+
+namespace CVC4 {
+
+class DecisionEngine;
+
+namespace decision {
+
+class DecisionStrategy {
+protected:
+   DecisionEngine* d_decisionEngine;
+public:
+  DecisionStrategy(DecisionEngine* de) :
+    d_decisionEngine(de) {
+  }
+
+  virtual ~DecisionStrategy() { }
+
+  virtual prop::SatLiteral getNext() = 0;
+  
+  virtual bool needSimplifiedPreITEAssertions() { return false; }
+  
+  virtual void notifyAssertionsAvailable() { return; }
+};
+
+}/* decision namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DECISION__DECISION_STRATEGY_H */
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
new file mode 100644
index 000000000..4b017ef45
--- /dev/null
+++ b/src/decision/justification_heuristic.cpp
@@ -0,0 +1,393 @@
+/*********************                                                        */
+/*! \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 -- note below.
+ **
+ ** It needs access to the simplified but non-clausal formula.
+ **/
+/*****************************************************************************/
+/*!
+ *\file search_sat.cpp
+ *\brief Implementation of Search engine with generic external sat solver
+ *
+ * Author: Clark Barrett
+ *
+ * Created: Wed Dec  7 21:00:24 2005
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ */
+/*****************************************************************************/
+
+#include "justification_heuristic.h"
+
+
+/***
+
+Summary of the algorithm:
+
+
+
+***/
+
+/*
+
+CVC3 code <---->  this code
+ 
+ value            desiredVal
+ getValue(lit)    litVal
+
+***/
+
+void JustificationHeuristic::setJustified(SatVariable v)
+{
+  d_justified.insert(v);
+}
+
+bool JustificationHeuristic::checkJustified(SatVariable v)
+{
+  return d_justified.find(v) != d_justified.end();
+}
+
+SatValue invertValue(SatValue v)
+{
+  if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN;
+  else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE;
+  else return SAT_VALUE_TRUE;
+}
+
+bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal, SatLiteral* litDecision)
+//bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision)
+{
+  // if(not ) {
+  //   //    Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
+  //   return false;
+  //   //    Assert(not lit.isNull());
+  // }
+
+  /** 
+   * TODO -- Base case. Way CVC3 seems to handle is that it has
+   * literals correpsonding to true and false. We'll have to take care
+   * somewhere else.
+   */
+
+  // Var v = lit.getVar();
+  SatVariable v = lit.getSatVariable();
+  SatValue litVal =  d_decisionEngine->getSatValue(lit);
+
+  // if (lit.isFalse() || lit.isTrue()) return false;
+  if (v == 0) return false;
+
+
+  /* You'd better know what you want */
+  // DebugAssert(value != Var::UNKNOWN, "expected known value");
+  Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
+
+  /* Good luck, hope you can get what you want */
+  // DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN,
+  //             "invariant violated");
+  Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, 
+         "invariant voilated");
+
+
+  if (checkJustified(v)) return false;
+
+  if (lit.isNegated()) {
+    desiredVal = invertValue(desiredVal);
+  }
+
+  Node node = d_decisionEngine->getNode(lit);
+  Trace("decision") << "lit = " << lit << std::endl;
+  Trace("decision") << node.getKind() << std::endl;
+  Trace("decision") << node << std::endl;
+
+  /*
+  if (d_cnfManager->numFanins(v) == 0) {
+    if (getValue(v) != Var::UNKNOWN) {
+      setJustified(v);
+      return false;
+    }
+    else {
+      *litDecision = Lit(v, value == Var::TRUE_VAL);
+      return true;
+    }
+  }
+  */
+  if(node.getNumChildren() == 0) {
+    if(litVal != SAT_VALUE_UNKNOWN) {
+      setJustified(v);
+      return false;
+    } else {
+      *litDecision = SatLiteral(v, desiredVal == SAT_VALUE_TRUE );
+      return true;
+    }
+  }
+
+
+  /*
+  else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) {
+    // This node represents a predicate with embedded ITE's
+    // We handle this case specially in order to catch the
+    // corner case when a variable is in its own fanin.
+    n = d_cnfManager->numFanins(v);
+    for (i=0; i < n; ++i) {
+      litTmp = d_cnfManager->getFanin(v, i);
+      varTmp = litTmp.getVar();
+      DebugAssert(!litTmp.isInverted(),"Expected positive fanin");
+      if (checkJustified(varTmp)) continue;
+      DebugAssert(d_cnfManager->concreteVar(varTmp).getKind() == ITE,
+                  "Expected ITE");
+      DebugAssert(getValue(varTmp) == Var::TRUE_VAL,"Expected TRUE");
+      Lit cIf = d_cnfManager->getFanin(varTmp,0);
+      Lit cThen = d_cnfManager->getFanin(varTmp,1);
+      Lit cElse = d_cnfManager->getFanin(varTmp,2);
+      if (getValue(cIf) == Var::UNKNOWN) {
+        if (getValue(cElse) == Var::TRUE_VAL ||
+            getValue(cThen) == Var::FALSE_VAL) {
+          ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision);
+        }
+        else {
+          ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision);
+        }
+        if (!ret) {
+          cout << d_cnfManager->concreteVar(cIf.getVar()) << endl;
+          DebugAssert(false,"No controlling input found (1)");
+        }	  
+        return true;
+      }
+      else if (getValue(cIf) == Var::TRUE_VAL) {
+        if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) {
+            return true;
+        }
+        if (cThen.getVar() != v &&
+            (getValue(cThen) == Var::UNKNOWN ||
+             getValue(cThen) == Var::TRUE_VAL) &&
+            findSplitterRec(cThen, Var::TRUE_VAL, litDecision)) {
+          return true;
+        }
+      }
+      else {
+        if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) {
+          return true;
+        }
+        if (cElse.getVar() != v &&
+            (getValue(cElse) == Var::UNKNOWN ||
+             getValue(cElse) == Var::TRUE_VAL) &&
+            findSplitterRec(cElse, Var::TRUE_VAL, litDecision)) {
+          return true;
+        }
+      }
+      setJustified(varTmp);
+    }
+    if (getValue(v) != Var::UNKNOWN) {
+      setJustified(v);
+      return false;
+    }
+    else {
+      *litDecision = Lit(v, value == Var::TRUE_VAL);
+      return true;
+    }
+  }
+
+  int kind = d_cnfManager->concreteVar(v).getKind();
+  Var::Val valHard = Var::FALSE_VAL;
+  switch (kind) {
+    case AND:
+      valHard = Var::TRUE_VAL;
+    case OR:
+      if (value == valHard) {
+        n = d_cnfManager->numFanins(v);
+        for (i=0; i < n; ++i) {
+          litTmp = d_cnfManager->getFanin(v, i);
+          if (findSplitterRec(litTmp, valHard, litDecision)) {
+            return true;
+          }
+        }
+        DebugAssert(getValue(v) == valHard, "Output should be justified");
+        setJustified(v);
+        return false;
+      }
+      else {
+        Var::Val valEasy = Var::invertValue(valHard);
+        n = d_cnfManager->numFanins(v);
+        for (i=0; i < n; ++i) {
+          litTmp = d_cnfManager->getFanin(v, i);
+          if (getValue(litTmp) != valHard) {
+            if (findSplitterRec(litTmp, valEasy, litDecision)) {
+              return true;
+            }
+            DebugAssert(getValue(v) == valEasy, "Output should be justified");
+            setJustified(v);
+            return false;
+          }
+        }
+        DebugAssert(false, "No controlling input found (2)");
+      }
+      break;
+    case IMPLIES:
+      DebugAssert(d_cnfManager->numFanins(v) == 2, "Expected 2 fanins");
+      if (value == Var::FALSE_VAL) {
+        litTmp = d_cnfManager->getFanin(v, 0);
+        if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
+          return true;
+        }
+        litTmp = d_cnfManager->getFanin(v, 1);
+        if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
+          return true;
+        }
+        DebugAssert(getValue(v) == Var::FALSE_VAL, "Output should be justified");
+        setJustified(v);
+        return false;
+      }
+      else {
+        litTmp = d_cnfManager->getFanin(v, 0);
+        if (getValue(litTmp) != Var::TRUE_VAL) {
+          if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
+            return true;
+          }
+          DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
+          setJustified(v);
+          return false;
+        }
+        litTmp = d_cnfManager->getFanin(v, 1);
+        if (getValue(litTmp) != Var::FALSE_VAL) {
+          if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
+            return true;
+          }
+          DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
+          setJustified(v);
+          return false;
+        }
+        DebugAssert(false, "No controlling input found (3)");
+      }
+      break;
+    case IFF: {
+      litTmp = d_cnfManager->getFanin(v, 0);
+      Var::Val val = getValue(litTmp);
+      if (val != Var::UNKNOWN) {
+        if (findSplitterRec(litTmp, val, litDecision)) {
+          return true;
+        }
+        if (value == Var::FALSE_VAL) val = Var::invertValue(val);
+        litTmp = d_cnfManager->getFanin(v, 1);
+
+        if (findSplitterRec(litTmp, val, litDecision)) {
+          return true;
+        }
+        DebugAssert(getValue(v) == value, "Output should be justified");
+        setJustified(v);
+        return false;
+      }
+      else {
+        val = getValue(d_cnfManager->getFanin(v, 1));
+        if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
+        if (value == Var::FALSE_VAL) val = Var::invertValue(val);
+        if (findSplitterRec(litTmp, val, litDecision)) {
+          return true;
+        }
+        DebugAssert(false, "Unable to find controlling input (4)");
+      }
+      break;
+    }
+    case XOR: {
+      litTmp = d_cnfManager->getFanin(v, 0);
+      Var::Val val = getValue(litTmp);
+      if (val != Var::UNKNOWN) {
+        if (findSplitterRec(litTmp, val, litDecision)) {
+          return true;
+        }
+        if (value == Var::TRUE_VAL) val = Var::invertValue(val);
+        litTmp = d_cnfManager->getFanin(v, 1);
+        if (findSplitterRec(litTmp, val, litDecision)) {
+          return true;
+        }
+        DebugAssert(getValue(v) == value, "Output should be justified");
+        setJustified(v);
+        return false;
+      }
+      else {
+        val = getValue(d_cnfManager->getFanin(v, 1));
+        if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
+        if (value == Var::TRUE_VAL) val = Var::invertValue(val);
+        if (findSplitterRec(litTmp, val, litDecision)) {
+          return true;
+        }
+        DebugAssert(false, "Unable to find controlling input (5)");
+      }
+      break;
+    }
+    case ITE: {
+      Lit cIf = d_cnfManager->getFanin(v, 0);
+      Lit cThen = d_cnfManager->getFanin(v, 1);
+      Lit cElse = d_cnfManager->getFanin(v, 2);
+      if (getValue(cIf) == Var::UNKNOWN) {
+        if (getValue(cElse) == value ||
+            getValue(cThen) == Var::invertValue(value)) {
+          ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision);
+        }
+        else {
+          ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision);
+        }
+        if (!ret) {
+          cout << d_cnfManager->concreteVar(cIf.getVar()) << endl;
+          DebugAssert(false,"No controlling input found (6)");
+        }	  
+        return true;
+      }
+      else if (getValue(cIf) == Var::TRUE_VAL) {
+        if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) {
+            return true;
+        }
+        if (cThen.isVar() && cThen.getVar() != v &&
+            (getValue(cThen) == Var::UNKNOWN ||
+             getValue(cThen) == value) &&
+            findSplitterRec(cThen, value, litDecision)) {
+          return true;
+        }
+      }
+      else {
+        if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) {
+          return true;
+        }
+        if (cElse.isVar() && cElse.getVar() != v &&
+            (getValue(cElse) == Var::UNKNOWN ||
+             getValue(cElse) == value) &&
+            findSplitterRec(cElse, value, litDecision)) {
+          return true;
+        }
+      }
+      DebugAssert(getValue(v) == value, "Output should be justified");
+      setJustified(v);
+      return false;
+    }
+    default:
+      DebugAssert(false, "Unexpected Boolean operator");
+      break;
+  }
+  FatalAssert(false, "Should be unreachable");
+  ------------------------------------------------  */
+  return false;
+
+  Unreachable();
+
+}/* findRecSplit method */
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 */