1 /********************* */ 2 /*! \file justification_heuristic.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Kshitij Bansal, Tim King, Morgan Deters 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Justification heuristic for decision making 13 ** 14 ** A ATGP-inspired justification-based decision heuristic. See 15 ** [insert reference] for more details. This code is, or not, based 16 ** on the CVC3 implementation of the same heuristic. 17 ** 18 ** It needs access to the simplified but non-clausal formula. 19 **/ 20 21 #include "cvc4_private.h" 22 23 #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC 24 #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC 25 26 #include <unordered_set> 27 28 #include "context/cdhashmap.h" 29 #include "context/cdhashset.h" 30 #include "context/cdlist.h" 31 #include "decision/decision_attributes.h" 32 #include "decision/decision_engine.h" 33 #include "decision/decision_strategy.h" 34 #include "expr/node.h" 35 #include "preprocessing/assertion_pipeline.h" 36 #include "prop/sat_solver_types.h" 37 38 namespace CVC4 { 39 namespace decision { 40 41 class JustificationHeuristic : public ITEDecisionStrategy { 42 // TRUE FALSE MEH 43 enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW}; 44 45 typedef std::vector<pair<TNode,TNode> > IteList; 46 typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache; 47 typedef std::vector<TNode> ChildList; 48 typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache; 49 typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap; 50 typedef context::CDHashMap<TNode,pair<DecisionWeight,DecisionWeight>,TNodeHashFunction> WeightCache; 51 52 // being 'justified' is monotonic with respect to decisions 53 typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet; 54 JustifiedSet d_justified; 55 typedef context::CDHashMap<Node,DecisionWeight,NodeHashFunction> ExploredThreshold; 56 ExploredThreshold d_exploredThreshold; 57 context::CDO<unsigned> d_prvsIndex; 58 context::CDO<unsigned> d_threshPrvsIndex; 59 60 IntStat d_helfulness; 61 IntStat d_giveup; 62 TimerStat d_timestat; 63 64 /** 65 * A copy of the assertions that need to be justified 66 * directly. Doesn't have ones introduced during during ITE-removal. 67 */ 68 context::CDList<TNode> d_assertions; 69 //TNode is fine since decisionEngine has them too 70 71 /** map from ite-rewrite skolem to a boolean-ite assertion */ 72 SkolemMap d_iteAssertions; 73 // 'key' being TNode is fine since if a skolem didn't exist anywhere, 74 // we won't look it up. as for 'value', same reason as d_assertions 75 76 /** Cache for ITE skolems present in a atomic formula */ 77 IteCache d_iteCache; 78 79 /** 80 * This is used to prevent infinite loop when trying to find a 81 * splitter. Can happen when exploring assertion corresponding to a 82 * term-ITE. 83 */ 84 std::unordered_set<TNode,TNodeHashFunction> d_visited; 85 86 /** 87 * Set to track visited nodes in a dfs search done in computeITE 88 * function 89 */ 90 std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE; 91 92 /** current decision for the recursive call */ 93 SatLiteral d_curDecision; 94 /** current threshold for the recursive call */ 95 DecisionWeight d_curThreshold; 96 97 /** child cache */ 98 ChildCache d_childCache; 99 100 /** computed polarized weight cache */ 101 WeightCache d_weightCache; 102 103 104 class myCompareClass { 105 JustificationHeuristic* d_jh; 106 bool d_b; 107 public: myCompareClass(JustificationHeuristic * jh,bool b)108 myCompareClass(JustificationHeuristic* jh, bool b):d_jh(jh),d_b(b) {}; operator()109 bool operator() (TNode n1, TNode n2) { 110 return d_jh->getWeightPolarized(n1, d_b) < d_jh->getWeightPolarized(n2, d_b); 111 } 112 }; 113 114 public: 115 JustificationHeuristic(CVC4::DecisionEngine* de, 116 context::UserContext *uc, 117 context::Context *c); 118 119 ~JustificationHeuristic(); 120 121 prop::SatLiteral getNext(bool &stopSearch) override; 122 123 void addAssertions( 124 const preprocessing::AssertionPipeline &assertions) override; 125 126 private: 127 /* getNext with an option to specify threshold */ 128 prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold); 129 130 SatLiteral findSplitter(TNode node, SatValue desiredVal); 131 132 /** 133 * Do all the hard work. 134 */ 135 SearchResult findSplitterRec(TNode node, SatValue value); 136 137 /* Helper functions */ 138 void setJustified(TNode); 139 bool checkJustified(TNode); 140 DecisionWeight getExploredThreshold(TNode); 141 void setExploredThreshold(TNode); 142 void setPrvsIndex(int); 143 int getPrvsIndex(); 144 DecisionWeight getWeightPolarized(TNode n, bool polarity); 145 DecisionWeight getWeightPolarized(TNode n, SatValue); 146 static DecisionWeight getWeight(TNode); 147 bool compareByWeightFalse(TNode, TNode); 148 bool compareByWeightTrue(TNode, TNode); 149 TNode getChildByWeight(TNode n, int i, bool polarity); 150 151 /* If literal exists corresponding to the node return 152 that. Otherwise an UNKNOWN */ 153 SatValue tryGetSatValue(Node n); 154 155 /* Get list of all term-ITEs for the atomic formula v */ 156 JustificationHeuristic::IteList getITEs(TNode n); 157 158 159 /** 160 * For big and/or nodes, a cache to save starting index into children 161 * for efficiently. 162 */ 163 typedef context::CDHashMap<TNode, int, TNodeHashFunction> StartIndexCache; 164 StartIndexCache d_startIndexCache; 165 int getStartIndex(TNode node); 166 void saveStartIndex(TNode node, int val); 167 168 /* Compute all term-ITEs in a node recursively */ 169 void computeITEs(TNode n, IteList &l); 170 171 SearchResult handleAndOrEasy(TNode node, SatValue desiredVal); 172 SearchResult handleAndOrHard(TNode node, SatValue desiredVal); 173 SearchResult handleBinaryEasy(TNode node1, SatValue desiredVal1, 174 TNode node2, SatValue desiredVal2); 175 SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1, 176 TNode node2, SatValue desiredVal2); 177 SearchResult handleITE(TNode node, SatValue desiredVal); 178 SearchResult handleEmbeddedITEs(TNode node); 179 };/* class JustificationHeuristic */ 180 181 }/* namespace decision */ 182 }/* namespace CVC4 */ 183 184 #endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */ 185