Merge experimental decisionweight branch

None of these are enabled by default, so any performance impact
counts as a bug

Options added are:

--decision-threshold=N :default 0
+ ignore all nodes greater than threshold in first attempt to pick decision

--decision-use-weight bool :default false
+ use the weight nodes (locally, by looking at children) to direct recursive search

--decision-random-weight=N int :default 0
+ assign random weights to nodes between 0 and N-1 (0: disable)

--decision-weight-internal=HOW
+ computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving)

Squashed commit of the following:

commit 0dbae066c19abde37092517b50f23255398539db
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Fri Apr 26 16:42:36 2013 -0400

    contentless cleanup

commit 62bb99b33deceb803ba5afc563fd322b4b5d1b7e
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Apr 16 21:43:55 2013 -0400

    bugfixes in usr1 auto weight computation

commit 9f039cba805bfd722466734920e758d48ae3b23e
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Fri Mar 29 15:01:33 2013 -0400

    DECISION_WEIGHT_INTERNAL_USR1

commit 744e16d514594e5f1c69b36473b03cf501d9b9d1
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Mar 27 11:05:43 2013 -0400

    split theory and decision requests

commit f379d8a821df31c74b42a7722e891abc5c944f16
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Mar 27 09:51:58 2013 -0400

    fix potential bug with threshold

commit 3dcb45eb5ee648d3edbeddf76b838076afea3d12
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Feb 27 20:29:38 2013 -0500

    stat bv::weightComputationTimer

commit 2ab97d063e221357d2bb017af4589105777fd5a3
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Sat Feb 23 17:02:43 2013 -0500

    decision: option to auto compute weight of boolean structure

commit 0a8c29e699ad96d5f73bc14d31ad9254f6711ae8
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Sat Feb 23 14:53:50 2013 -0500

    decision: fix design to do partial explorations

    * make findSplitterRec and all related helper functions' return
      type trivalued, to be able to distinguish between
      "partial exploration" vs "done exploration but found nothing"

    * keep additional data structure to remember to what extent the
      partial exploration has been completed so not to repeat it. we
      can use this to make multiple passes on formula with arbritrary
      order of thresholds for exploration

commit 0815991fc1b0f1d63f0e8124d4672d782e89d671
Author: lianah <lianahady@gmail.com>
Date:   Fri Feb 22 17:55:40 2013 -0500

    added simple node weight computation for bv.

commit e4c507e2e2fdc8794fd04c31093660a80c7f44c3
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Feb 20 02:35:21 2013 -0500

    --decision-use-weight, --decision-random-weight=N

commit 0624177d66d6ed2b3cc7fdb13df775990cfe50c2
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Feb 19 23:36:49 2013 -0500

    decisionThreshold option

commit ac3579a52e452e3118ce116ff1823d6c6885544b
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Feb 19 20:22:51 2013 -0500

    DecisionWeightAttr

1 files changed, 50 insertions, 8 deletions

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 503f6c2af..01458d9ea 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -37,14 +37,23 @@ namespace CVC4 {
 namespace decision {
 
 class JustificationHeuristic : public ITEDecisionStrategy {
+  //                   TRUE           FALSE         MEH
+  enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
+
   typedef std::vector<pair<TNode,TNode> > IteList;
   typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache;
+  typedef std::vector<TNode> ChildList;
+  typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache;
   typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
+  typedef context::CDHashMap<TNode,pair<DecisionWeight,DecisionWeight>,TNodeHashFunction> WeightCache;
 
   // being 'justified' is monotonic with respect to decisions
   typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
   JustifiedSet d_justified;
+  typedef context::CDHashMap<Node,DecisionWeight,NodeHashFunction> ExploredThreshold;
+  ExploredThreshold d_exploredThreshold;
   context::CDO<unsigned>  d_prvsIndex;
+  context::CDO<unsigned>  d_threshPrvsIndex;
 
   IntStat d_helfulness;
   IntStat d_giveup;
@@ -80,6 +89,26 @@ class JustificationHeuristic : public ITEDecisionStrategy {
 
   /** current decision for the recursive call */
   SatLiteral d_curDecision;
+  /** current threshold for the recursive call */
+  DecisionWeight d_curThreshold;
+
+  /** child cache */
+  ChildCache d_childCache;
+
+  /** computed polarized weight cache */
+  WeightCache d_weightCache;
+
+
+  class myCompareClass {
+    JustificationHeuristic* d_jh;
+    bool d_b;
+  public:
+    myCompareClass(JustificationHeuristic* jh, bool b):d_jh(jh),d_b(b) {};
+    bool operator() (TNode n1, TNode n2) {
+      return d_jh->getWeightPolarized(n1, d_b) < d_jh->getWeightPolarized(n2, d_b);
+    }
+  };
+
 public:
   JustificationHeuristic(CVC4::DecisionEngine* de,
                          context::UserContext *uc,
@@ -94,17 +123,30 @@ public:
                      IteSkolemMap iteSkolemMap);
 
 private:
+  /* getNext with an option to specify threshold */
+  prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold);
+
   SatLiteral findSplitter(TNode node, SatValue desiredVal);
   
   /** 
    * Do all the hard work. 
    */ 
-  bool findSplitterRec(TNode node, SatValue value);
+  SearchResult findSplitterRec(TNode node, SatValue value);
 
   /* Helper functions */
   void setJustified(TNode);
   bool checkJustified(TNode);
-  
+  DecisionWeight getExploredThreshold(TNode);
+  void setExploredThreshold(TNode);
+  void setPrvsIndex(int);
+  int  getPrvsIndex();
+  DecisionWeight getWeightPolarized(TNode n, bool polarity);
+  DecisionWeight getWeightPolarized(TNode n, SatValue);
+  static DecisionWeight getWeight(TNode);
+  bool compareByWeightFalse(TNode, TNode);
+  bool compareByWeightTrue(TNode, TNode);
+  TNode getChildByWeight(TNode n, int i, bool polarity);
+
   /* If literal exists corresponding to the node return
      that. Otherwise an UNKNOWN */
   SatValue tryGetSatValue(Node n);
@@ -115,14 +157,14 @@ private:
   /* Compute all term-ITEs in a node recursively */
   void computeITEs(TNode n, IteList &l);
 
-  bool handleAndOrEasy(TNode node, SatValue desiredVal);
-  bool handleAndOrHard(TNode node, SatValue desiredVal);
-  bool handleBinaryEasy(TNode node1, SatValue desiredVal1,
+  SearchResult handleAndOrEasy(TNode node, SatValue desiredVal);
+  SearchResult handleAndOrHard(TNode node, SatValue desiredVal);
+  SearchResult handleBinaryEasy(TNode node1, SatValue desiredVal1,
                         TNode node2, SatValue desiredVal2);
-  bool handleBinaryHard(TNode node1, SatValue desiredVal1,
+  SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1,
                         TNode node2, SatValue desiredVal2);
-  bool handleITE(TNode node, SatValue desiredVal);
-  bool handleEmbeddedITEs(TNode node);
+  SearchResult handleITE(TNode node, SatValue desiredVal);
+  SearchResult handleEmbeddedITEs(TNode node);
 };/* class JustificationHeuristic */
 
 }/* namespace decision */