From 7efd777609f7fbc20701402ad949971cbc251f8f Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 4 Dec 2012 21:41:51 +0000
Subject: * Add support for --decision=justification + incremental (bug 437)  -
 Fix a destruction order issue this triggered in DE

(this commit was certified error- and warning-free by the test-and-commit script.)
---
 src/decision/justification_heuristic.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'src/decision/justification_heuristic.cpp')

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index ba8ab91b7..494da72bf 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -73,7 +73,7 @@ void JustificationHeuristic::computeITEs(TNode n, IteList &l)
   for(unsigned i=0; i<n.getNumChildren(); ++i) {
     SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
     if(it2 != d_iteAssertions.end()) {
-      l.push_back(make_pair(n[i], it2->second));
+      l.push_back(make_pair(n[i], (*it2).second));
       Assert(n[i].getNumChildren() == 0);
     }
     computeITEs(n[i], l);
@@ -98,6 +98,15 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
                                              SatValue desiredVal,
                                              SatLiteral* litDecision)
 {
+  /**
+   * Main idea
+   *
+   * Given a boolean formula "node", the goal is to try to make it
+   * evaluate to "desiredVal" (true/false). for instance if "node" is a AND
+   * formula we want to make it evaluate to true, we'd like one of the
+   * children to be true. this is done recursively.
+   */
+
   Trace("jh-findSplitterRec") 
     << "findSplitterRec(" << node << ", " 
     << desiredVal << ", .. )" << std::endl; 
-- 
cgit v1.2.3