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

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 */