diff options
Diffstat (limited to 'src/decision/justification_heuristic.h')
-rw-r--r-- | src/decision/justification_heuristic.h | 58 |
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 */ |