rm decision/relevancy

6 files changed, 1 insertions, 892 deletions

diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am
index 6d49c6301..f75a17a69 100644
--- a/src/decision/Makefile.am
+++ b/src/decision/Makefile.am
@@ -12,9 +12,7 @@ libdecision_la_SOURCES = \
 	decision_engine.cpp \
 	decision_strategy.h \
 	justification_heuristic.h \
-	justification_heuristic.cpp \
-	relevancy.h \
-	relevancy.cpp
+	justification_heuristic.cpp
 
 EXTRA_DIST = \
 	options_handlers.h
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index f634a28d9..073a3ff6b 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -16,7 +16,6 @@
 
 #include "decision/decision_engine.h"
 #include "decision/justification_heuristic.h"
-#include "decision/relevancy.h"
 
 #include "expr/node.h"
 #include "decision/options.h"
@@ -62,18 +61,6 @@ void DecisionEngine::init()
     enableStrategy(ds);
     d_needIteSkolemMap.push_back(ds);
   }
-  if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) {
-    if(options::incrementalSolving()) {
-      Warning() << "Relevancy decision heuristic and incremental not supported together"
-                << std::endl;
-      return; // Currently not supported with incremental
-    }
-    RelevancyStrategy* ds = 
-      new decision::Relevancy(this, d_satContext);
-    enableStrategy(ds);
-    d_needIteSkolemMap.push_back(ds);
-    d_relevancyStrategy = ds;
-  }
 }
 
 
@@ -112,13 +99,6 @@ SatValue DecisionEngine::getPolarity(SatVariable var)
   }
 }
 
-
-
-
-
-
-
-
 void DecisionEngine::addAssertions(const vector<Node> &assertions)
 {
   Assert(false);  // doing this so that we revisit what to do
@@ -146,15 +126,4 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions,
       addAssertions(assertions, assertionsEnd, iteSkolemMap);
 }
 
-// void DecisionEngine::addAssertion(Node n)
-// {
-//   d_result = SAT_VALUE_UNKNOWN;
-//   if(needIteSkolemMap()) {
-//     d_assertions.push_back(n);
-//   }
-//   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
-//     d_needIteSkolemMap[i]->notifyAssertionsAvailable();
-// }
-  
-
 }/* CVC4 namespace */
diff --git a/src/decision/options b/src/decision/options
index b86577e7b..5f89e9611 100644
--- a/src/decision/options
+++ b/src/decision/options
@@ -9,14 +9,6 @@ module DECISION "decision/options.h" Decision heuristics
 option decisionMode --decision=MODE decision::DecisionMode :handler CVC4::decision::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "decision/decision_mode.h" :handler-include "decision/options_handlers.h"
  choose decision mode, see --decision=help
 
-option decisionRelevancyLeaves bool
-# permille = part per thousand
-option decisionMaxRelTimeAsPermille --decision-budget=N "unsigned short" :read-write :predicate less_equal(1000L) :predicate CVC4::decision::checkDecisionBudget :predicate-include "decision/options_handlers.h"
- impose a budget for relevancy heuristic which increases linearly with each decision. N between 0 and 1000. (default: 1000, no budget)
-# if false, do justification stuff using relevancy.h
-option decisionComputeRelevancy bool
-# use the must be relevant
-option decisionMustRelevancy bool
 # only use DE to determine when to stop, not to make decisions
 option decisionStopOnly bool
 
diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h
index 05d975ef1..44a623970 100644
--- a/src/decision/options_handlers.h
+++ b/src/decision/options_handlers.h
@@ -37,31 +37,8 @@ justification\n\
 justification-stoponly\n\
 + Use the justification heuristic only to stop early, not for decisions\n\
 ";
-/** Under-development options, commenting out from help for the release */
-/*
-\n\
-relevancy\n\
-+ Under development may-relevancy\n\
-\n\
-relevancy-leaves\n\
-+ May-relevancy, but decide only on leaves\n\
-\n\
-Developer modes:\n\
-\n\
-justification-rel\n\
-+ Use the relevancy code to do the justification stuff\n\
-+ (This should do exact same thing as justification)\n\
-\n\
-justification-must\n\
-+ Start deciding on literals close to root instead of those\n\
-+ near leaves (don't expect it to work well) [Unimplemented]\n\
-";*/
 
 inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  options::decisionRelevancyLeaves.set(false);
-  options::decisionMaxRelTimeAsPermille.set(1000);
-  options::decisionComputeRelevancy.set(true);
-  options::decisionMustRelevancy.set(false);
   options::decisionStopOnly.set(false);
 
   if(optarg == "internal") {
@@ -71,25 +48,6 @@ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg,
   } else if(optarg == "justification-stoponly") {
     options::decisionStopOnly.set(true);
     return DECISION_STRATEGY_JUSTIFICATION;
-  } else if(optarg == "relevancy") {
-    options::decisionRelevancyLeaves.set(false);
-    return DECISION_STRATEGY_RELEVANCY;
-  } else if(optarg == "relevancy-leaves") {
-    options::decisionRelevancyLeaves.set(true);
-    Trace("options") << "version is " << options::version() << std::endl;
-    return DECISION_STRATEGY_RELEVANCY;
-  } else if(optarg == "justification-rel") {
-    // relevancyLeaves : irrelevant
-    // maxRelTimeAsPermille : irrelevant
-    options::decisionComputeRelevancy.set(false);
-    options::decisionMustRelevancy.set(false);
-    return DECISION_STRATEGY_RELEVANCY;
-  } else if(optarg == "justification-must") {
-    // relevancyLeaves : irrelevant
-    // maxRelTimeAsPermille : irrelevant
-    options::decisionComputeRelevancy.set(false);
-    options::decisionMustRelevancy.set(true);
-    return DECISION_STRATEGY_RELEVANCY;
   } else if(optarg == "help") {
     puts(decisionModeHelp.c_str());
     exit(1);
@@ -99,14 +57,6 @@ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg,
   }
 }
 
-inline void checkDecisionBudget(std::string option, unsigned short budget, SmtEngine* smt) throw(OptionException) {
-  if(budget == 0) {
-    Warning() << "Decision budget is 0. Consider using internal decision heuristic and "
-              << std::endl << " removing this option." << std::endl;
-              
-  }
-}
-
 inline DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "off")
     return DECISION_WEIGHT_INTERNAL_OFF;
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp
deleted file mode 100644
index f83e238d4..000000000
--- a/src/decision/relevancy.cpp
+++ /dev/null
@@ -1,379 +0,0 @@
-/*********************                                                        */
-/*! \file relevancy.cpp
- ** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** 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.
- **/
-/*****************************************************************************/
-
-#include "relevancy.h"
-
-#include "expr/node_manager.h"
-#include "expr/kind.h"
-#include "theory/rewriter.h"
-#include "util/ite_removal.h"
-
-// Relevancy stuff
-
-const double Relevancy::secondsPerDecision = 0.001;
-const double Relevancy::secondsPerExpense = 1e-7;
-const double Relevancy::EPS = 1e-9;
-
-
-void Relevancy::setJustified(TNode n)
-{
-  Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl;
-  d_justified.insert(n);
-  if(options::decisionComputeRelevancy()) {
-    d_relevancy[n] = d_maxRelevancy[n];
-    updateRelevancy(n);
-  }
-}
-
-bool Relevancy::checkJustified(TNode n)
-{
-  return d_justified.find(n) != d_justified.end();
-}
-
-SatValue Relevancy::tryGetSatValue(Node n)
-{
-  Debug("decision") << "   "  << n << " has sat value " << " ";
-  if(d_decisionEngine->hasSatLiteral(n) ) {
-    Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl;
-    return d_decisionEngine->getSatValue(n);
-  } else {
-    Debug("decision") << "NO SAT LITERAL" << std::endl;
-    return SAT_VALUE_UNKNOWN;
-  }//end of else
-}
-
-void Relevancy::computeITEs(TNode n, IteList &l)
-{
-  Debug("jh-ite") << " computeITEs( " << n << ", &l)\n";
-  for(unsigned i=0; i<n.getNumChildren(); ++i) {
-    SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
-    if(it2 != d_iteAssertions.end())
-      l.push_back(it2->second);
-    computeITEs(n[i], l);
-  }
-}
-
-const Relevancy::IteList& Relevancy::getITEs(TNode n)
-{
-  IteCache::iterator it = d_iteCache.find(n);
-  if(it != d_iteCache.end()) {
-    return it->second;
-  } else {
-    // Compute the list of ITEs
-    // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
-    d_iteCache[n] = vector<TNode>();
-    computeITEs(n, d_iteCache[n]);
-    return d_iteCache[n];
-  }
-}
-
-bool Relevancy::findSplitterRec(TNode node, 
-                                SatValue desiredVal)
-{
-  Trace("decision") 
-    << "findSplitterRec([" << node.getId() << "]" << node << ", " 
-    << desiredVal << ", .. )" << std::endl; 
-
-  ++d_expense;
-
-  /* Handle NOT as a special case */
-  while (node.getKind() == kind::NOT) {
-    desiredVal = invertValue(desiredVal);
-    node = node[0];
-  }
-
-  /* Avoid infinite loops */
-  if(d_visited.find(node) != d_visited.end()) {
-    Debug("decision") << " node repeated. kind was " << node.getKind() << std::endl;
-    Assert(false);
-    Assert(node.getKind() == kind::ITE);
-    return false;
-  }
-
-  /* Base case */
-  if(checkJustified(node)) {
-    return false;
-  }
-
-  /**
-   * If we have already explored the subtree for some desiredVal, we
-   * skip this and continue exploring the rest
-   */
-  if(d_polarityCache.find(node) == d_polarityCache.end()) {
-    d_polarityCache[node] = desiredVal;
-  } else {
-    Assert(d_multipleBacktrace || options::decisionComputeRelevancy());
-    return true;
-  }
-
-  d_visited.insert(node);
-
-#if defined CVC4_ASSERTIONS || defined CVC4_TRACING
-  // We don't always have a sat literal, so remember that. Will need
-  // it for some assertions we make.
-  bool litPresent = d_decisionEngine->hasSatLiteral(node);
-  if(Trace.isOn("decision")) {
-    if(!litPresent) {
-      Trace("decision") << "no sat literal for this node" << std::endl;
-    }
-  }
-  //Assert(litPresent); -- fails
-#endif
-
-  // Get value of sat literal for the node, if there is one
-  SatValue litVal = tryGetSatValue(node);
-
-  /* You'd better know what you want */
-  Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
-
-  /* Good luck, hope you can get what you want */
-  Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, 
-         "invariant violated");
-
-  /* What type of node is this */
-  Kind k = node.getKind();	
-  theory::TheoryId tId = theory::kindToTheoryId(k);
-
-  /* Some debugging stuff */
-  Trace("jh-findSplitterRec") << "kind = " << k << std::endl;
-  Trace("jh-findSplitterRec") << "theoryId = " << tId << std::endl;
-  Trace("jh-findSplitterRec") << "node = " << node << std::endl;
-  Trace("jh-findSplitterRec") << "litVal = " << litVal << std::endl;
-
-  /**
-   * If not in theory of booleans, and not a "boolean" EQUAL (IFF),
-   * then check if this is something to split-on.
-   */
-  if(tId != theory::THEORY_BOOL
-     //      && !(k == kind::EQUAL && node[0].getType().isBoolean()) 
-     ) {
-
-    // if node has embedded ites -- which currently happens iff it got
-    // replaced during ite removal -- then try to resolve that first
-    const IteList& l = getITEs(node);
-    Debug("jh-ite") << " ite size = " << l.size() << std::endl;
-    for(unsigned i = 0; i < l.size(); ++i) {
-      Assert(l[i].getKind() == kind::ITE, "Expected ITE");
-      Debug("jh-ite") << " i = " << i 
-                      << " l[i] = " << l[i] << std::endl;
-      if(d_visited.find(node) != d_visited.end() ) continue;
-      if(findSplitterRec(l[i], SAT_VALUE_TRUE)) {
-        d_visited.erase(node);
-        return true;
-      }
-    }
-    Debug("jh-ite") << " ite done " << l.size() << std::endl;
-
-    if(litVal != SAT_VALUE_UNKNOWN) {
-      d_visited.erase(node);
-      setJustified(node);
-      return false;
-    } else {
-      /* if(not d_decisionEngine->hasSatLiteral(node))
-         throw GiveUpException(); */
-      Assert(d_decisionEngine->hasSatLiteral(node));
-      SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable();
-      *d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
-      Trace("decision") << "decision " << *d_curDecision << std::endl;
-      Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
-      d_visited.erase(node);
-      return true;
-    }
-  }
-
-  bool ret = false;
-  SatValue flipCaseVal = SAT_VALUE_FALSE;
-  switch (k) {
-
-  case kind::CONST_BOOLEAN:
-    Assert(node.getConst<bool>() == false || desiredVal == SAT_VALUE_TRUE);
-    Assert(node.getConst<bool>() == true  || desiredVal == SAT_VALUE_FALSE);
-    break;
-
-  case kind::AND:
-    if (desiredVal == SAT_VALUE_FALSE) ret = handleOrTrue(node, SAT_VALUE_FALSE);
-    else                               ret = handleOrFalse(node, SAT_VALUE_TRUE);
-    break;
-
-  case kind::OR:
-    if (desiredVal == SAT_VALUE_FALSE) ret = handleOrFalse(node, SAT_VALUE_FALSE);
-    else                               ret = handleOrTrue(node, SAT_VALUE_TRUE);
-    break;
-
-  case kind::IMPLIES:
-    Assert(node.getNumChildren() == 2, "Expected 2 fanins");
-    if (desiredVal == SAT_VALUE_FALSE) {
-      ret = findSplitterRec(node[0], SAT_VALUE_TRUE);
-      if(ret) break;
-      ret = findSplitterRec(node[1], SAT_VALUE_FALSE);
-      break;
-    }
-    else {
-      if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) {
-        ret = findSplitterRec(node[0], SAT_VALUE_FALSE);
-        //if(!ret || !d_multipleBacktrace) 
-          break;
-      }
-      if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) {
-        ret = findSplitterRec(node[1], SAT_VALUE_TRUE);
-        break;
-      }
-      Assert(d_multipleBacktrace, "No controlling input found (3)");
-    }
-    break;
-
-  case kind::XOR:
-    flipCaseVal = SAT_VALUE_TRUE;
-  case kind::IFF: {
-    SatValue val = tryGetSatValue(node[0]);
-    if (val != SAT_VALUE_UNKNOWN) {
-      ret = findSplitterRec(node[0], val);
-      if (ret) break;
-      if (desiredVal == flipCaseVal) val = invertValue(val);
-      ret = findSplitterRec(node[1], val);
-    }
-    else {
-      val = tryGetSatValue(node[1]);
-      if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
-      if (desiredVal == flipCaseVal) val = invertValue(val);
-      ret = findSplitterRec(node[0], val);
-      if(ret) break;
-      Assert(false, "Unable to find controlling input (4)");
-    }
-    break;
-  }
-
-  case kind::ITE:
-    ret = handleITE(node, desiredVal);
-    break;
-
-  default:
-    Assert(false, "Unexpected Boolean operator");
-    break;
-  }//end of switch(k)
-
-  d_visited.erase(node);
-  if(ret == false) {
-    Assert(litPresent == false || litVal ==  desiredVal,
-           "Output should be justified");
-    setJustified(node);
-  }
-  return ret;
-
-  Unreachable();
-}/* findRecSplit method */
-
-bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) {
-  Debug("jh-findSplitterRec") << " handleOrFalse (" << node << ", "
-                              << desiredVal << std::endl;
-
-  Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or 
-          (node.getKind() == kind::OR  and desiredVal == SAT_VALUE_FALSE) );
-
-  int n = node.getNumChildren();
-  bool ret = false;
-  for(int i = 0; i < n; ++i) {
-    if (findSplitterRec(node[i], desiredVal)) {
-      if(!options::decisionComputeRelevancy()) 
-        return true;
-      else
-        ret = true;
-    }
-  }
-  return ret;
-}
-
-bool Relevancy::handleOrTrue(TNode node, SatValue desiredVal) {
-  Debug("jh-findSplitterRec") << " handleOrTrue (" << node << ", "
-                              << desiredVal << std::endl;
-
-  Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or 
-          (node.getKind() == kind::OR  and desiredVal == SAT_VALUE_TRUE) );
-
-  int n = node.getNumChildren();
-  SatValue desiredValInverted = invertValue(desiredVal);
-  for(int i = 0; i < n; ++i) {
-    if ( tryGetSatValue(node[i]) != desiredValInverted ) {
-      // PRE RELEVANCY return findSplitterRec(node[i], desiredVal);
-      bool ret = findSplitterRec(node[i], desiredVal);
-      if(ret) {
-        // Splitter could be found... so can't justify this node
-        if(!d_multipleBacktrace)
-          return true;
-      }
-      else  {
-        // Splitter couldn't be found... should be justified
-        return false;
-      }
-    }
-  }
-  // Multiple backtrace is on, so must have reached here because
-  // everything had splitter
-  if(d_multipleBacktrace) return true;
-
-  if(Debug.isOn("jh-findSplitterRec")) {
-    Debug("jh-findSplitterRec") << " * ** " << std::endl;
-    Debug("jh-findSplitterRec") << node.getKind() << " "
-                                << node << std::endl;
-    for(unsigned i = 0; i < node.getNumChildren(); ++i) 
-      Debug("jh-findSplitterRec") << "child: " << tryGetSatValue(node[i]) 
-                                  << std::endl;
-    Debug("jh-findSplitterRec") << "node: " << tryGetSatValue(node)
-                                << std::endl;
-  }
-  Assert(false, "No controlling input found");
-  return false;
-}
-
-bool Relevancy::handleITE(TNode node, SatValue desiredVal)
-{
-  Debug("jh-findSplitterRec") << " handleITE (" << node << ", "
-                              << desiredVal << std::endl;
-
-  //[0]: if, [1]: then, [2]: else
-  SatValue ifVal = tryGetSatValue(node[0]);
-  if (ifVal == SAT_VALUE_UNKNOWN) {
-      
-    // are we better off trying false? if not, try true
-    SatValue ifDesiredVal = 
-      (tryGetSatValue(node[2]) == desiredVal ||
-       tryGetSatValue(node[1]) == invertValue(desiredVal))
-      ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
-
-    if(findSplitterRec(node[0], ifDesiredVal)) return true;
-    
-    Assert(false, "No controlling input found (6)");
-  } else {
-
-    // Try to justify 'if'
-    if(findSplitterRec(node[0], ifVal)) return true;
-
-    // If that was successful, we need to go into only one of 'then'
-    // or 'else'
-    int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2;
-    int chVal = tryGetSatValue(node[ch]);
-    if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) &&
-        findSplitterRec(node[ch], desiredVal) ) {
-      return true;
-    }
-  }// else (...ifVal...)
-  return false;
-}//handleITE
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
deleted file mode 100644
index fd16eb0cc..000000000
--- a/src/decision/relevancy.h
+++ /dev/null
@@ -1,421 +0,0 @@
-/*********************                                                        */
-/*! \file relevancy.h
- ** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** 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.
- **
- ** Relevancy
- ** ---------
- **
- ** This class also currently computes the may-relevancy of a node
- **
- ** A node is may-relevant if there is a path from the root of the
- ** formula to the node such that no node on the path is justified. As
- ** contrapositive, a node is not relevant (with the may-notion) if all
- ** path from the root to the node go through a justified node.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__DECISION__RELEVANCY
-#define __CVC4__DECISION__RELEVANCY
-
-#include "decision_engine.h"
-#include "decision_strategy.h"
-#include "decision/options.h"
-
-#include "context/cdhashset.h"
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "prop/sat_solver_types.h"
-
-namespace CVC4 {
-
-namespace decision {
-
-class RelGiveUpException : public Exception {
-public:
-  RelGiveUpException() : 
-    Exception("relevancy: giving up") {
-  }
-};/* class GiveUpException */
-
-class Relevancy : public RelevancyStrategy {
-  typedef std::vector<TNode> IteList;
-  typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
-  typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
-  typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
-
-  // being 'justified' is monotonic with respect to decisions
-  context::CDHashSet<Node, NodeHashFunction> d_justified;
-  context::CDO<unsigned>  d_prvsIndex;
-
-  IntStat d_helfulness;
-  IntStat d_polqueries;
-  IntStat d_polhelp;
-  IntStat d_giveup;
-  IntStat d_expense;          /* Total number of nodes considered over
-                                 all calls to the findSplitter function */
-  TimerStat d_timestat;
-
-  /**
-   * A copy of the assertions that need to be justified
-   * directly. Doesn't have ones introduced during during ITE-removal.
-   */
-  std::vector<TNode> d_assertions;   
-  //TNode is fine since decisionEngine has them too
-
-  /** map from ite-rewrite skolem to a boolean-ite assertion */
-  SkolemMap d_iteAssertions;
-  // 'key' being TNode is fine since if a skolem didn't exist anywhere,
-  // we won't look it up. as for 'value', same reason as d_assertions
-
-  /** Cache for ITE skolems present in a atomic formula */
-  IteCache d_iteCache;
-
-  /**
-   * This is used to prevent infinite loop when trying to find a
-   * splitter. Can happen when exploring assertion corresponding to a
-   * term-ITE.
-   */
-  hash_set<TNode,TNodeHashFunction> d_visited;
-
-  /** 
-   * May-relevancy of a node is an integer. For a node n, it becomes
-   * irrelevant when d_maxRelevancy[n] = d_relevancy[n]
-   */
-  hash_map<TNode,int,TNodeHashFunction> d_maxRelevancy;
-  context::CDHashMap<TNode,int,TNodeHashFunction> d_relevancy;
-  PolarityCache d_polarityCache;
-
-  /**  **** * * *** * * OPTIONS *** *  * ** * * **** */
-
-  /**
-   * do we do "multiple-backtrace" to try to justify a node
-   */
-  bool d_multipleBacktrace;
-  //bool d_computeRelevancy;     // are we in a mode where we compute relevancy?
-
-  static const double secondsPerDecision;
-  static const double secondsPerExpense;
-  static const double EPS;
-
-  /** Maximum time this algorithm should spent as part of whole algorithm */
-  double d_maxTimeAsPercentageOfTotalTime;
-
-  /** current decision for the recursive call */
-  SatLiteral* d_curDecision;
-public:
-  Relevancy(CVC4::DecisionEngine* de, context::Context *c):
-    RelevancyStrategy(de, c),
-    d_justified(c),
-    d_prvsIndex(c, 0),
-    d_helfulness("decision::rel::preventedDecisions", 0),
-    d_polqueries("decision::rel::polarityQueries", 0),
-    d_polhelp("decision::rel::polarityHelp", 0),
-    d_giveup("decision::rel::giveup", 0),
-    d_expense("decision::rel::expense", 0),
-    d_timestat("decision::rel::time"),
-    d_relevancy(c),
-    d_multipleBacktrace(options::decisionComputeRelevancy()),
-    //    d_computeRelevancy(decOpt.computeRelevancy),
-    d_maxTimeAsPercentageOfTotalTime(options::decisionMaxRelTimeAsPermille()*1.0/10.0),
-    d_curDecision(NULL)
-  {
-    Warning() << "There are known bugs in this Relevancy code which we know"
-              << "how to fix (but haven't yet)." << std::endl
-              << "Please bug kshitij if you wish to use." << std::endl;
-
-    StatisticsRegistry::registerStat(&d_helfulness);
-    StatisticsRegistry::registerStat(&d_polqueries);
-    StatisticsRegistry::registerStat(&d_polhelp);
-    StatisticsRegistry::registerStat(&d_giveup);
-    StatisticsRegistry::registerStat(&d_expense);
-    StatisticsRegistry::registerStat(&d_timestat);
-    Trace("decision") << "relevancy enabled with" << std::endl;
-    Trace("decision") << "  * computeRelevancy: " << (options::decisionComputeRelevancy() ? "on" : "off")
-                      << std::endl;
-    Trace("decision") << "  * relevancyLeaves: " << (options::decisionRelevancyLeaves() ? "on" : "off")
-                      << std::endl;
-    Trace("decision") << "  * mustRelevancy [unimplemented]: " << (options::decisionMustRelevancy() ? "on" : "off")
-                      << std::endl;
-  }
-  ~Relevancy() {
-    StatisticsRegistry::unregisterStat(&d_helfulness);
-    StatisticsRegistry::unregisterStat(&d_polqueries);
-    StatisticsRegistry::unregisterStat(&d_polhelp);
-    StatisticsRegistry::unregisterStat(&d_giveup);
-    StatisticsRegistry::unregisterStat(&d_expense);
-    StatisticsRegistry::unregisterStat(&d_timestat);
-  }
-  prop::SatLiteral getNext(bool &stopSearch) {
-    Debug("decision") << std::endl;
-    Trace("decision") << "Relevancy::getNext()" << std::endl;
-    TimerStat::CodeTimer codeTimer(d_timestat);
-
-    if( d_maxTimeAsPercentageOfTotalTime < 100.0 - EPS &&
-        double(d_polqueries.getData())*secondsPerDecision < 
-          d_maxTimeAsPercentageOfTotalTime*double(d_expense.getData())*secondsPerExpense
-      ) {
-      ++d_giveup;
-      return undefSatLiteral;
-    }
-
-    d_visited.clear();
-    d_polarityCache.clear();
-
-    for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
-      Trace("decision") << d_assertions[i] << std::endl;
-
-      // Sanity check: if it was false, aren't we inconsistent?
-      Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
-
-      SatValue desiredVal = SAT_VALUE_TRUE;
-      SatLiteral litDecision = findSplitter(d_assertions[i], desiredVal);
-
-      if(!options::decisionComputeRelevancy() && litDecision != undefSatLiteral) {
-        d_prvsIndex = i;
-        return litDecision;
-      }
-    }
-
-    if(options::decisionComputeRelevancy()) return undefSatLiteral;
-
-    Trace("decision") << "jh: Nothing to split on " << std::endl;
-
-#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
-    bool alljustified = true;
-    for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) {
-      TNode curass = d_assertions[i];
-      while(curass.getKind() == kind::NOT)
-        curass = curass[0];
-      alljustified &= checkJustified(curass);
-
-      if(Debug.isOn("decision")) {
-	if(!checkJustified(curass))
-	  Debug("decision") << "****** Not justified [i="<<i<<"]: " 
-                            << d_assertions[i] << std::endl;
-      }
-    }
-    Assert(alljustified);
-#endif
-
-    // SAT solver can stop...
-    stopSearch = true;
-    d_decisionEngine->setResult(SAT_VALUE_TRUE);
-    return prop::undefSatLiteral;
-  }
-
-  void addAssertions(const std::vector<Node> &assertions,
-                     unsigned assertionsEnd,
-                     IteSkolemMap iteSkolemMap) {
-    Trace("decision")
-      << "Relevancy::addAssertions()" 
-      << " size = " << assertions.size()
-      << " assertionsEnd = " << assertionsEnd
-      << std::endl;
-
-    // Save mapping between ite skolems and ite assertions
-    for(IteSkolemMap::iterator i = iteSkolemMap.begin();
-        i != iteSkolemMap.end(); ++i) {
-      Assert(i->second >= assertionsEnd && i->second < assertions.size());
-      Debug("jh-ite") << " jh-ite: " << (i->first) << " maps to "
-                      << assertions[(i->second)] << std::endl;
-      d_iteAssertions[i->first] = assertions[i->second];
-    }
-
-    // Save the 'real' assertions locally
-    for(unsigned i = 0; i < assertionsEnd; ++i) {
-      d_assertions.push_back(assertions[i]);
-      d_visited.clear();
-      if(options::decisionComputeRelevancy()) increaseMaxRelevancy(assertions[i]);
-      d_visited.clear();
-    }
-
-  }
-
-  bool isRelevant(TNode n) {
-    Trace("decision") << "isRelevant(" << n << "): ";
-
-    if(Debug.isOn("decision")) {
-      if(d_maxRelevancy.find(n) == d_maxRelevancy.end()) {
-        // we are becuase of not getting information about literals
-        // created using newLiteral command... need to figure how to
-        // handle that
-        Message() << "isRelevant: WARNING: didn't find node when we should had" << std::endl;
-      }      
-    }
-
-    if(d_maxRelevancy.find(n) == d_maxRelevancy.end()) {
-      Trace("decision") << "yes [not found in db]" << std::endl;
-      return true;
-    }
-    
-    if(options::decisionRelevancyLeaves() && !isAtomicFormula(n)) {
-      Trace("decision") << "no [not a leaf]" << std::endl;
-      return false;
-    }
-
-    Trace("decision") << (d_maxRelevancy[n] == d_relevancy[n] ? "no":"yes")
-                      << std::endl;
-
-    Debug("decision") << " maxRel: " << (d_maxRelevancy[n] )
-                      << " rel: " << d_relevancy[n].get() << std::endl;
-    // Assert(d_maxRelevancy.find(n) != d_maxRelevancy.end());
-    Assert(0 <= d_relevancy[n] && d_relevancy[n] <= d_maxRelevancy[n]);
-
-    if(d_maxRelevancy[n] == d_relevancy[n]) {
-      ++d_helfulness; // preventedDecisions
-      return false;
-    } else {
-      return true;
-    }
-  }
-
-  SatValue getPolarity(TNode n) {
-    Trace("decision") << "getPolarity([" << n.getId() << "]" << n << "): ";
-    Assert(n.getKind() != kind::NOT);
-    ++d_polqueries;
-    PolarityCache::iterator it = d_polarityCache.find(n);
-    if(it == d_polarityCache.end()) {
-      Trace("decision") << "don't know" << std::endl;
-      return SAT_VALUE_UNKNOWN;
-    } else {
-      ++d_polhelp;
-      Trace("decision") << it->second << std::endl;
-      return it->second;
-    }
-  }
-
-  /* Compute justified */
-  /*bool computeJustified() {
-    
-  }*/
-private:
-  SatLiteral findSplitter(TNode node, SatValue desiredVal)
-  {
-    bool ret;
-    SatLiteral litDecision;
-    try {
-      // init
-      d_curDecision = &litDecision;
-      
-      // solve
-      ret = findSplitterRec(node, desiredVal);
-
-      // post
-      d_curDecision = NULL;
-    }catch(RelGiveUpException &e) {
-      return prop::undefSatLiteral;
-    }
-    if(ret == true) {
-      Trace("decision") << "Yippee!!" << std::endl;
-      return litDecision;
-    } else {
-      return undefSatLiteral;
-    }
-  }
-  
-  /** 
-   * Do all the hardwork. 
-   * Return 'true' if the node cannot be justfied, 'false' it it can be.
-   * Sets 'd_curDecision' if unable to justify (depending on the mode)
-   * If 'd_computeRelevancy' is on does multiple backtrace
-   */ 
-  bool findSplitterRec(TNode node, SatValue value);
-  // Functions to make findSplitterRec modular...
-  bool handleOrFalse(TNode node, SatValue desiredVal);
-  bool handleOrTrue(TNode node, SatValue desiredVal);
-  bool handleITE(TNode node, SatValue desiredVal);
-
-  /* Helper functions */
-  void setJustified(TNode);
-  bool checkJustified(TNode);
-  
-  /* If literal exists corresponding to the node return
-     that. Otherwise an UNKNOWN */
-  SatValue tryGetSatValue(Node n);
-
-  /* Get list of all term-ITEs for the atomic formula v */
-  const Relevancy::IteList& getITEs(TNode n);
-
-  /* Compute all term-ITEs in a node recursively */
-  void computeITEs(TNode n, IteList &l);
-
-  /* Checks whether something is an atomic formula or not */
-  bool isAtomicFormula(TNode n) {
-    return theory::kindToTheoryId(n.getKind()) != theory::THEORY_BOOL;
-  }
-  
-  /** Recursively increase relevancies */
-  void updateRelevancy(TNode n) {
-    if(d_visited.find(n) != d_visited.end()) return;
-
-    Assert(d_relevancy[n] <= d_maxRelevancy[n]);
-
-    if(d_relevancy[n] != d_maxRelevancy[n])
-      return;
-
-    d_visited.insert(n);
-    if(isAtomicFormula(n)) {
-      const IteList& l = getITEs(n);
-      for(unsigned i = 0; i < l.size(); ++i) {
-        if(d_visited.find(l[i]) == d_visited.end()) continue;
-        d_relevancy[l[i]] = d_relevancy[l[i]] + 1;
-        updateRelevancy(l[i]);
-      }
-    } else {
-      for(unsigned i = 0; i < n.getNumChildren(); ++i) {
-        if(d_visited.find(n[i]) == d_visited.end()) continue;
-        d_relevancy[n[i]] = d_relevancy[n[i]] + 1;
-        updateRelevancy(n[i]);
-      }
-    }
-    d_visited.erase(n);
-  }
-
-  /* */
-  void increaseMaxRelevancy(TNode n) {
-
-    Debug("decision") 
-      << "increaseMaxRelevancy([" << n.getId() << "]" << n << ")" 
-      << std::endl;    
-
-    d_maxRelevancy[n]++;
-
-    // don't update children multiple times
-    if(d_visited.find(n) != d_visited.end()) return;
-    
-    d_visited.insert(n);
-    // Part to make the recursive call
-    if(isAtomicFormula(n)) {
-      const IteList& l = getITEs(n);
-      for(unsigned i = 0; i < l.size(); ++i)
-        if(d_visited.find(l[i]) == d_visited.end())
-          increaseMaxRelevancy(l[i]);
-    } else {
-      for(unsigned i = 0; i < n.getNumChildren(); ++i)
-        increaseMaxRelevancy(n[i]);
-    } //else (...atomic formula...)
-  }
-
-};/* class Relevancy */
-
-}/* namespace decision */
-
-}/* namespace CVC4 */
-
-#endif /* __CVC4__DECISION__RELEVANCY */