1 /********************* */ 2 /*! \file bv_subtheory_algebraic.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Liana Hadarean, Mathias Preiner, Tim King 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 Algebraic solver. 13 ** 14 ** Algebraic solver. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #pragma once 20 21 #include <unordered_map> 22 #include <unordered_set> 23 24 #include "theory/bv/bv_subtheory.h" 25 #include "theory/bv/slicer.h" 26 #include "theory/substitutions.h" 27 28 namespace CVC4 { 29 namespace theory { 30 namespace bv { 31 32 class AlgebraicSolver; 33 34 35 Node mergeExplanations(TNode expl1, TNode expl2); 36 Node mergeExplanations(const std::vector<Node>& expls); 37 38 39 /** 40 * Non-context dependent substitution with explanations. 41 * 42 */ 43 class SubstitutionEx { 44 struct SubstitutionElement { 45 Node to; 46 Node reason; SubstitutionElementSubstitutionElement47 SubstitutionElement() 48 : to() 49 , reason() 50 {} 51 SubstitutionElementSubstitutionElement52 SubstitutionElement(TNode t, TNode r) 53 : to(t) 54 , reason(r) 55 {} 56 }; 57 58 struct SubstitutionStackElement { 59 TNode node; 60 bool childrenAdded; 61 SubstitutionStackElement(TNode n, bool ca = false) nodeSubstitutionStackElement62 : node(n) 63 , childrenAdded(ca) 64 {} 65 }; 66 67 typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions; 68 typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache; 69 70 Substitutions d_substitutions; 71 SubstitutionsCache d_cache; 72 bool d_cacheInvalid; 73 theory::SubstitutionMap* d_modelMap; 74 75 76 Node getReason(TNode node) const; 77 bool hasCache(TNode node) const; 78 Node getCache(TNode node) const; 79 void storeCache(TNode from, TNode to, Node rason); 80 Node internalApply(TNode node); 81 82 public: 83 SubstitutionEx(theory::SubstitutionMap* modelMap); 84 /** 85 * Returnst true if the substitution map did not contain from. 86 * 87 * @param from 88 * @param to 89 * @param reason 90 * 91 * @return 92 */ 93 bool addSubstitution(TNode from, TNode to, TNode reason); 94 Node apply(TNode node); 95 Node explain(TNode node) const; 96 }; 97 98 /** 99 * In-processing worklist element, id keeps track of 100 * original assertion. 101 * 102 */ 103 struct WorklistElement { 104 Node node; 105 unsigned id; WorklistElementWorklistElement106 WorklistElement(Node n, unsigned i) : node(n), id(i) {} WorklistElementWorklistElement107 WorklistElement() : node(), id(-1) {} 108 }; 109 110 111 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; 112 typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap; 113 typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; 114 115 116 class ExtractSkolemizer { 117 struct Extract { 118 unsigned high; 119 unsigned low; ExtractExtract120 Extract(unsigned h, unsigned l) : high(h), low(l) {} 121 }; 122 123 struct ExtractList { 124 Base base; 125 std::vector<Extract> extracts; ExtractListExtractList126 ExtractList(unsigned bitwidth) : base(bitwidth), extracts() {} ExtractListExtractList127 ExtractList() : base(1), extracts() {} 128 void addExtract(Extract& e); 129 }; 130 typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap; 131 context::Context d_emptyContext; 132 VarExtractMap d_varToExtract; 133 theory::SubstitutionMap* d_modelMap; 134 theory::SubstitutionMap d_skolemSubst; 135 theory::SubstitutionMap d_skolemSubstRev; 136 137 void storeSkolem(TNode node, TNode skolem); 138 void storeExtract(TNode var, unsigned high, unsigned low); 139 void collectExtracts(TNode node, TNodeSet& seen); 140 Node skolemize(TNode); 141 Node unSkolemize(TNode); 142 143 Node mkSkolem(Node node); 144 public: 145 ExtractSkolemizer(theory::SubstitutionMap* modelMap); 146 void skolemize(std::vector<WorklistElement>&); 147 void unSkolemize(std::vector<WorklistElement>&); 148 ~ExtractSkolemizer(); 149 }; 150 151 class BVQuickCheck; 152 class QuickXPlain; 153 154 /** 155 * AlgebraicSolver 156 */ 157 class AlgebraicSolver : public SubtheorySolver { 158 159 struct Statistics { 160 IntStat d_numCallstoCheck; 161 IntStat d_numSimplifiesToTrue; 162 IntStat d_numSimplifiesToFalse; 163 IntStat d_numUnsat; 164 IntStat d_numSat; 165 IntStat d_numUnknown; 166 TimerStat d_solveTime; 167 BackedStat<double> d_useHeuristic; 168 Statistics(); 169 ~Statistics(); 170 }; 171 172 std::unique_ptr<SubstitutionMap> d_modelMap; 173 std::unique_ptr<BVQuickCheck> d_quickSolver; 174 context::CDO<bool> d_isComplete; 175 context::CDO<bool> d_isDifficult; /**< flag to indicate whether the current assertions contain expensive BV operators */ 176 177 unsigned long d_budget; 178 std::vector<Node> d_explanations; /**< explanations for assertions indexed by assertion id */ 179 TNodeSet d_inputAssertions; /**< assertions in current context (for debugging purposes only) */ 180 NodeIdMap d_ids; /**< map from assertions to ids */ 181 uint64_t d_numSolved; 182 uint64_t d_numCalls; 183 184 /** separate quickXplain module as it can reuse the current SAT solver */ 185 std::unique_ptr<QuickXPlain> d_quickXplain; 186 187 Statistics d_statistics; 188 bool useHeuristic(); 189 void setConflict(TNode conflict); 190 bool isSubstitutableIn(TNode node, TNode in); 191 bool checkExplanation(TNode expl); 192 void storeExplanation(TNode expl); 193 void storeExplanation(unsigned id, TNode expl); 194 /** 195 * Apply substitutions and rewriting to the worklist assertions to a fixpoint. 196 * Subsitutions learned store in subst. 197 * 198 * @param worklist 199 * @param subst 200 */ 201 void processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst); 202 /** 203 * Attempt to solve the equation in fact, and if successful 204 * add a substitution to subst. 205 * 206 * @param fact equation we are trying to solve 207 * @param reason the reason in terms of original assertions 208 * @param subst substitution map 209 * 210 * @return true if added a substitution to subst 211 */ 212 bool solve(TNode fact, TNode reason, SubstitutionEx& subst); 213 /** 214 * Run a SAT solver on the given facts with the given budget. 215 * Sets the isComplete flag and conflict accordingly. 216 * 217 * @param facts 218 * 219 * @return true if no conflict was detected. 220 */ 221 bool quickCheck(std::vector<Node>& facts); 222 223 public: 224 AlgebraicSolver(context::Context* c, TheoryBV* bv); 225 ~AlgebraicSolver(); 226 preRegister(TNode node)227 void preRegister(TNode node) override {} 228 bool check(Theory::Effort e) override; explain(TNode literal,std::vector<TNode> & assumptions)229 void explain(TNode literal, std::vector<TNode>& assumptions) override 230 { 231 Unreachable("AlgebraicSolver does not propagate.\n"); 232 } 233 EqualityStatus getEqualityStatus(TNode a, TNode b) override; 234 bool collectModelInfo(TheoryModel* m, bool fullModel) override; 235 Node getModelValue(TNode node) override; 236 bool isComplete() override; 237 void assertFact(TNode fact) override; 238 }; 239 240 } // namespace bv 241 } // namespace theory 242 } // namespace CVC4 243