1 /********************* */ 2 /*! \file theory_uf.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Dejan Jovanovic, 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 This is the interface to TheoryUF implementations 13 ** 14 ** This is the interface to TheoryUF implementations. All 15 ** implementations of TheoryUF should inherit from this class. 16 **/ 17 18 #include "cvc4_private.h" 19 20 #ifndef __CVC4__THEORY__UF__THEORY_UF_H 21 #define __CVC4__THEORY__UF__THEORY_UF_H 22 23 #include "context/cdhashset.h" 24 #include "context/cdo.h" 25 #include "expr/node.h" 26 #include "expr/node_trie.h" 27 #include "theory/theory.h" 28 #include "theory/uf/equality_engine.h" 29 #include "theory/uf/symmetry_breaker.h" 30 31 namespace CVC4 { 32 namespace theory { 33 namespace uf { 34 35 class UfTermDb; 36 class StrongSolverTheoryUF; 37 38 class TheoryUF : public Theory { 39 40 friend class StrongSolverTheoryUF; 41 typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; 42 typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; 43 public: 44 45 class NotifyClass : public eq::EqualityEngineNotify { 46 TheoryUF& d_uf; 47 public: NotifyClass(TheoryUF & uf)48 NotifyClass(TheoryUF& uf): d_uf(uf) {} 49 eqNotifyTriggerEquality(TNode equality,bool value)50 bool eqNotifyTriggerEquality(TNode equality, bool value) override 51 { 52 Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; 53 if (value) { 54 return d_uf.propagate(equality); 55 } else { 56 // We use only literal triggers so taking not is safe 57 return d_uf.propagate(equality.notNode()); 58 } 59 } 60 eqNotifyTriggerPredicate(TNode predicate,bool value)61 bool eqNotifyTriggerPredicate(TNode predicate, bool value) override 62 { 63 Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; 64 if (value) { 65 return d_uf.propagate(predicate); 66 } else { 67 return d_uf.propagate(predicate.notNode()); 68 } 69 } 70 eqNotifyTriggerTermEquality(TheoryId tag,TNode t1,TNode t2,bool value)71 bool eqNotifyTriggerTermEquality(TheoryId tag, 72 TNode t1, 73 TNode t2, 74 bool value) override 75 { 76 Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; 77 if (value) { 78 return d_uf.propagate(t1.eqNode(t2)); 79 } else { 80 return d_uf.propagate(t1.eqNode(t2).notNode()); 81 } 82 } 83 eqNotifyConstantTermMerge(TNode t1,TNode t2)84 void eqNotifyConstantTermMerge(TNode t1, TNode t2) override 85 { 86 Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; 87 d_uf.conflict(t1, t2); 88 } 89 eqNotifyNewClass(TNode t)90 void eqNotifyNewClass(TNode t) override 91 { 92 Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; 93 d_uf.eqNotifyNewClass(t); 94 } 95 eqNotifyPreMerge(TNode t1,TNode t2)96 void eqNotifyPreMerge(TNode t1, TNode t2) override 97 { 98 Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl; 99 d_uf.eqNotifyPreMerge(t1, t2); 100 } 101 eqNotifyPostMerge(TNode t1,TNode t2)102 void eqNotifyPostMerge(TNode t1, TNode t2) override 103 { 104 Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl; 105 d_uf.eqNotifyPostMerge(t1, t2); 106 } 107 eqNotifyDisequal(TNode t1,TNode t2,TNode reason)108 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override 109 { 110 Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl; 111 d_uf.eqNotifyDisequal(t1, t2, reason); 112 } 113 114 };/* class TheoryUF::NotifyClass */ 115 116 private: 117 118 /** The notify class */ 119 NotifyClass d_notify; 120 121 /** The associated theory strong solver (or NULL if none) */ 122 StrongSolverTheoryUF* d_thss; 123 124 /** Equaltity engine */ 125 eq::EqualityEngine d_equalityEngine; 126 127 /** Are we in conflict */ 128 context::CDO<bool> d_conflict; 129 130 /** The conflict node */ 131 Node d_conflictNode; 132 133 /** extensionality has been applied to these disequalities */ 134 NodeSet d_extensionality; 135 136 /** cache of getExtensionalityDeq below */ 137 std::map<Node, Node> d_extensionality_deq; 138 139 /** map from non-standard operators to their skolems */ 140 NodeNodeMap d_uf_std_skolem; 141 142 /** node for true */ 143 Node d_true; 144 145 /** 146 * Should be called to propagate the literal. We use a node here 147 * since some of the propagated literals are not kept anywhere. 148 */ 149 bool propagate(TNode literal); 150 151 /** 152 * Explain why this literal is true by adding assumptions 153 * with proof (if "pf" is non-NULL). 154 */ 155 void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf); 156 157 /** 158 * Explain a literal, with proof (if "pf" is non-NULL). 159 */ 160 Node explain(TNode literal, eq::EqProof* pf); 161 162 /** All the function terms that the theory has seen */ 163 context::CDList<TNode> d_functionsTerms; 164 165 /** Symmetry analyzer */ 166 SymmetryBreaker d_symb; 167 168 /** Conflict when merging two constants */ 169 void conflict(TNode a, TNode b); 170 171 /** called when a new equivalance class is created */ 172 void eqNotifyNewClass(TNode t); 173 174 /** called when two equivalance classes will merge */ 175 void eqNotifyPreMerge(TNode t1, TNode t2); 176 177 /** called when two equivalance classes have merged */ 178 void eqNotifyPostMerge(TNode t1, TNode t2); 179 180 /** called when two equivalence classes are made disequal */ 181 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); 182 183 private: // for higher-order 184 /** get extensionality disequality 185 * 186 * Given disequality deq f != g, this returns the disequality: 187 * (f k) != (g k) for fresh constant(s) k. 188 */ 189 Node getExtensionalityDeq(TNode deq); 190 191 /** applyExtensionality 192 * 193 * Given disequality deq f != g, if not already cached, this sends a lemma of 194 * the form: 195 * f = g V (f k) != (g k) for fresh constant k. 196 * on the output channel. This is an "extensionality lemma". 197 * Return value is the number of lemmas of this form sent on the output 198 * channel. 199 */ 200 unsigned applyExtensionality(TNode deq); 201 202 /** 203 * Check whether extensionality should be applied for any pair of terms in the 204 * equality engine. 205 * 206 * If we pass a null model m to this function, then we add extensionality 207 * lemmas to the output channel and return the total number of lemmas added. 208 * We only add lemmas for functions whose type is finite, since pairs of 209 * functions whose types are infinite can be made disequal in a model by 210 * witnessing a point they are disequal. 211 * 212 * If we pass a non-null model m to this function, then we add disequalities 213 * that correspond to the conclusion of extensionality lemmas to the model's 214 * equality engine. We return 0 if the equality engine of m is consistent 215 * after this call, and 1 otherwise. We only add disequalities for functions 216 * whose type is infinite, since our decision procedure guarantees that 217 * extensionality lemmas are added for all pairs of functions whose types are 218 * finite. 219 */ 220 unsigned checkExtensionality(TheoryModel* m = nullptr); 221 222 /** applyAppCompletion 223 * This infers a correspondence between APPLY_UF and HO_APPLY 224 * versions of terms for higher-order. 225 * Given APPLY_UF node e.g. (f a b c), this adds the equality to its 226 * HO_APPLY equivalent: 227 * (f a b c) == (@ (@ (@ f a) b) c) 228 * to equality engine, if not already equal. 229 * Return value is the number of equalities added. 230 */ 231 unsigned applyAppCompletion(TNode n); 232 233 /** check whether app-completion should be applied for any 234 * pair of terms in the equality engine. 235 */ 236 unsigned checkAppCompletion(); 237 238 /** check higher order 239 * This is called at full effort and infers facts and sends lemmas 240 * based on higher-order reasoning (specifically, extentionality and 241 * app completion above). It returns the number of lemmas plus facts 242 * added to the equality engine. 243 */ 244 unsigned checkHigherOrder(); 245 246 /** collect model info for higher-order term 247 * 248 * This adds required constraints to m for term n. In particular, if n is 249 * an APPLY_UF term, we add its HO_APPLY equivalent in this call. We return 250 * true if the model m is consistent after this call. 251 */ 252 bool collectModelInfoHoTerm(Node n, TheoryModel* m); 253 254 /** get apply uf for ho apply 255 * This returns the APPLY_UF equivalent for the HO_APPLY term node, where 256 * node has non-functional return type (that is, it corresponds to a fully 257 * applied function term). 258 * This call may introduce a skolem for the head operator and send out a lemma 259 * specifying the definition. 260 */ 261 Node getApplyUfForHoApply(Node node); 262 /** get the operator for this node (node should be either APPLY_UF or 263 * HO_APPLY) 264 */ 265 Node getOperatorForApplyTerm(TNode node); 266 /** get the starting index of the arguments for node (node should be either 267 * APPLY_UF or HO_APPLY) */ 268 unsigned getArgumentStartIndexForApplyTerm(TNode node); 269 270 public: 271 272 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ 273 TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, 274 Valuation valuation, const LogicInfo& logicInfo, 275 std::string instanceName = ""); 276 277 ~TheoryUF(); 278 279 void setMasterEqualityEngine(eq::EqualityEngine* eq) override; 280 void finishInit() override; 281 282 void check(Effort) override; 283 Node expandDefinition(LogicRequest& logicRequest, Node node) override; 284 void preRegisterTerm(TNode term) override; 285 Node explain(TNode n) override; 286 287 bool collectModelInfo(TheoryModel* m) override; 288 289 void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; 290 void presolve() override; 291 292 void addSharedTerm(TNode n) override; 293 void computeCareGraph() override; 294 295 void propagate(Effort effort) override; 296 297 EqualityStatus getEqualityStatus(TNode a, TNode b) override; 298 identify()299 std::string identify() const override { return "THEORY_UF"; } 300 getEqualityEngine()301 eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } 302 getStrongSolver()303 StrongSolverTheoryUF* getStrongSolver() { 304 return d_thss; 305 } 306 private: 307 bool areCareDisequal(TNode x, TNode y); 308 void addCarePairs(TNodeTrie* t1, 309 TNodeTrie* t2, 310 unsigned arity, 311 unsigned depth); 312 };/* class TheoryUF */ 313 314 }/* CVC4::theory::uf namespace */ 315 }/* CVC4::theory namespace */ 316 }/* CVC4 namespace */ 317 318 #endif /* __CVC4__THEORY__UF__THEORY_UF_H */ 319