1 /********************* */ 2 /*! \file theory_datatypes.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Tim King, Mathias Preiner 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 Theory of datatypes. 13 ** 14 ** Theory of datatypes. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H 20 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H 21 22 #include <iostream> 23 #include <map> 24 25 #include "context/cdlist.h" 26 #include "expr/attribute.h" 27 #include "expr/datatype.h" 28 #include "expr/node_trie.h" 29 #include "theory/datatypes/datatypes_sygus.h" 30 #include "theory/theory.h" 31 #include "theory/uf/equality_engine.h" 32 #include "util/hash.h" 33 34 namespace CVC4 { 35 namespace theory { 36 namespace datatypes { 37 38 class TheoryDatatypes : public Theory { 39 private: 40 typedef context::CDList<Node> NodeList; 41 /** maps nodes to an index in a vector */ 42 typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeUIntMap; 43 typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; 44 typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; 45 46 /** inferences */ 47 NodeList d_infer; 48 NodeList d_infer_exp; 49 Node d_true; 50 Node d_zero; 51 /** mkAnd */ 52 Node mkAnd(std::vector<TNode>& assumptions); 53 54 private: 55 //notification class for equality engine 56 class NotifyClass : public eq::EqualityEngineNotify { 57 TheoryDatatypes& d_dt; 58 public: NotifyClass(TheoryDatatypes & dt)59 NotifyClass(TheoryDatatypes& dt): d_dt(dt) {} eqNotifyTriggerEquality(TNode equality,bool value)60 bool eqNotifyTriggerEquality(TNode equality, bool value) override 61 { 62 Debug("dt") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; 63 if (value) { 64 return d_dt.propagate(equality); 65 } else { 66 // We use only literal triggers so taking not is safe 67 return d_dt.propagate(equality.notNode()); 68 } 69 } eqNotifyTriggerPredicate(TNode predicate,bool value)70 bool eqNotifyTriggerPredicate(TNode predicate, bool value) override 71 { 72 Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; 73 if (value) { 74 return d_dt.propagate(predicate); 75 } else { 76 return d_dt.propagate(predicate.notNode()); 77 } 78 } eqNotifyTriggerTermEquality(TheoryId tag,TNode t1,TNode t2,bool value)79 bool eqNotifyTriggerTermEquality(TheoryId tag, 80 TNode t1, 81 TNode t2, 82 bool value) override 83 { 84 Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; 85 if (value) { 86 return d_dt.propagate(t1.eqNode(t2)); 87 } else { 88 return d_dt.propagate(t1.eqNode(t2).notNode()); 89 } 90 } eqNotifyConstantTermMerge(TNode t1,TNode t2)91 void eqNotifyConstantTermMerge(TNode t1, TNode t2) override 92 { 93 Debug("dt") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; 94 d_dt.conflict(t1, t2); 95 } eqNotifyNewClass(TNode t)96 void eqNotifyNewClass(TNode t) override 97 { 98 Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; 99 d_dt.eqNotifyNewClass(t); 100 } eqNotifyPreMerge(TNode t1,TNode t2)101 void eqNotifyPreMerge(TNode t1, TNode t2) override 102 { 103 Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl; 104 d_dt.eqNotifyPreMerge(t1, t2); 105 } eqNotifyPostMerge(TNode t1,TNode t2)106 void eqNotifyPostMerge(TNode t1, TNode t2) override 107 { 108 Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl; 109 d_dt.eqNotifyPostMerge(t1, t2); 110 } eqNotifyDisequal(TNode t1,TNode t2,TNode reason)111 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override 112 { 113 Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl; 114 d_dt.eqNotifyDisequal(t1, t2, reason); 115 } 116 };/* class TheoryDatatypes::NotifyClass */ 117 private: 118 /** equivalence class info 119 * d_inst is whether the instantiate rule has been applied, 120 * d_constructor is a node of kind APPLY_CONSTRUCTOR (if any) in this equivalence class, 121 * d_selectors is whether a selector has been applied to this equivalence class. 122 */ 123 class EqcInfo 124 { 125 public: 126 EqcInfo( context::Context* c ); ~EqcInfo()127 ~EqcInfo(){} 128 //whether we have instantiatied this eqc 129 context::CDO< bool > d_inst; 130 //constructor equal to this eqc 131 context::CDO< Node > d_constructor; 132 //all selectors whose argument is this eqc 133 context::CDO< bool > d_selectors; 134 }; 135 /** does eqc of n have a label (do we know its constructor)? */ 136 bool hasLabel( EqcInfo* eqc, Node n ); 137 /** get the label associated to n */ 138 Node getLabel( Node n ); 139 /** get the index of the label associated to n */ 140 int getLabelIndex( EqcInfo* eqc, Node n ); 141 /** does eqc of n have any testers? */ 142 bool hasTester( Node n ); 143 /** get the possible constructors for n */ 144 void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons ); 145 /** mkExpDefSkolem */ 146 void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ); 147 /** skolems for terms */ 148 NodeMap d_term_sk; 149 Node getTermSkolemFor( Node n ); 150 private: 151 /** The notify class */ 152 NotifyClass d_notify; 153 /** Equaltity engine */ 154 eq::EqualityEngine d_equalityEngine; 155 /** information necessary for equivalence classes */ 156 std::map< Node, EqcInfo* > d_eqc_info; 157 /** map from nodes to their instantiated equivalent for each constructor type */ 158 std::map< Node, std::map< int, Node > > d_inst_map; 159 //---------------------------------labels 160 /** labels for each equivalence class 161 * 162 * For each eqc r, d_labels[r] is testers that hold for this equivalence 163 * class, either: 164 * a list of equations of the form 165 * NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ), each of 166 * which are unique testers, n is less than the number of possible 167 * constructors for t minus one, 168 * or a list of equations of the form 169 * NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ) followed by 170 * is_[constructor_(n+1)]( t{n+1} ), each of which is a unique tester. 171 * In both cases, t1, ..., tn, t{n+1} are terms in the equivalence class of r. 172 * 173 * We store this list in a context-dependent way, using the four data 174 * structures below. The three vectors d_labels_data, d_labels_args, and 175 * d_labels_tindex store the tester applications, their arguments and the 176 * tester index of the application. The map d_labels stores the number of 177 * values in these vectors that is valid in the current context (this is an 178 * optimization that ensures we don't need to pop data when changing SAT 179 * contexts). 180 */ 181 NodeUIntMap d_labels; 182 /** the tester applications */ 183 std::map< Node, std::vector< Node > > d_labels_data; 184 /** the argument of each node in d_labels_data */ 185 std::map<Node, std::vector<Node> > d_labels_args; 186 /** the tester index of each node in d_labels_data */ 187 std::map<Node, std::vector<unsigned> > d_labels_tindex; 188 //---------------------------------end labels 189 /** selector apps for eqch equivalence class */ 190 NodeUIntMap d_selector_apps; 191 std::map< Node, std::vector< Node > > d_selector_apps_data; 192 /** Are we in conflict */ 193 context::CDO<bool> d_conflict; 194 /** added lemma 195 * 196 * This flag is set to true during a full effort check if this theory 197 * called d_out->lemma(...). 198 */ 199 bool d_addedLemma; 200 /** added fact 201 * 202 * This flag is set to true during a full effort check if this theory 203 * added an internal fact to its equality engine. 204 */ 205 bool d_addedFact; 206 /** The conflict node */ 207 Node d_conflictNode; 208 /** cache for which terms we have called collectTerms(...) on */ 209 BoolMap d_collectTermsCache; 210 /** pending assertions/merges */ 211 std::vector< Node > d_pending_lem; 212 std::vector< Node > d_pending; 213 std::map< Node, Node > d_pending_exp; 214 std::vector< Node > d_pending_merge; 215 /** All the function terms that the theory has seen */ 216 context::CDList<TNode> d_functionTerms; 217 /** counter for forcing assignments (ensures fairness) */ 218 unsigned d_dtfCounter; 219 /** expand definition skolem functions */ 220 std::map< TypeNode, std::map< Node, Node > > d_exp_def_skolem; 221 /** uninterpreted constant to variable map */ 222 std::map< Node, Node > d_uc_to_fresh_var; 223 private: 224 /** singleton lemmas (for degenerate co-datatype case) */ 225 std::map< TypeNode, Node > d_singleton_lemma[2]; 226 /** Cache for singleton equalities processed */ 227 BoolMap d_singleton_eq; 228 /** list of all lemmas produced */ 229 BoolMap d_lemmas_produced_c; 230 private: 231 /** assert fact */ 232 void assertFact( Node fact, Node exp ); 233 234 /** flush pending facts */ 235 void flushPendingFacts(); 236 237 /** do pending merged */ 238 void doPendingMerges(); 239 /** do send lemma */ 240 bool doSendLemma( Node lem ); 241 bool doSendLemmas( std::vector< Node >& lem ); 242 /** get or make eqc info */ 243 EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false ); 244 245 /** has eqc info */ hasEqcInfo(TNode n)246 bool hasEqcInfo( TNode n ) { return d_labels.find( n )!=d_labels.end(); } 247 248 /** get eqc constructor */ 249 TNode getEqcConstructor( TNode r ); 250 251 protected: 252 void addCarePairs(TNodeTrie* t1, 253 TNodeTrie* t2, 254 unsigned arity, 255 unsigned depth, 256 unsigned& n_pairs); 257 /** compute care graph */ 258 void computeCareGraph() override; 259 260 public: 261 TheoryDatatypes(context::Context* c, context::UserContext* u, 262 OutputChannel& out, Valuation valuation, 263 const LogicInfo& logicInfo); 264 ~TheoryDatatypes(); 265 266 void setMasterEqualityEngine(eq::EqualityEngine* eq) override; 267 268 /** propagate */ 269 void propagate(Effort effort) override; 270 /** propagate */ 271 bool propagate(TNode literal); 272 /** explain */ 273 void addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ); 274 void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions ); 275 void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ); 276 void explain( TNode literal, std::vector<TNode>& assumptions ); 277 Node explain(TNode literal) override; 278 Node explain( std::vector< Node >& lits ); 279 /** Conflict when merging two constants */ 280 void conflict(TNode a, TNode b); 281 /** called when a new equivalance class is created */ 282 void eqNotifyNewClass(TNode t); 283 /** called when two equivalance classes will merge */ 284 void eqNotifyPreMerge(TNode t1, TNode t2); 285 /** called when two equivalance classes have merged */ 286 void eqNotifyPostMerge(TNode t1, TNode t2); 287 /** called when two equivalence classes are made disequal */ 288 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); 289 290 void check(Effort e) override; 291 bool needsCheckLastEffort() override; 292 void preRegisterTerm(TNode n) override; 293 void finishInit() override; 294 Node expandDefinition(LogicRequest& logicRequest, Node n) override; 295 Node ppRewrite(TNode n) override; 296 void presolve() override; 297 void addSharedTerm(TNode t) override; 298 EqualityStatus getEqualityStatus(TNode a, TNode b) override; 299 bool collectModelInfo(TheoryModel* m) override; shutdown()300 void shutdown() override {} identify()301 std::string identify() const override 302 { 303 return std::string("TheoryDatatypes"); 304 } 305 /** equality engine */ getEqualityEngine()306 eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } 307 bool getCurrentSubstitution(int effort, 308 std::vector<Node>& vars, 309 std::vector<Node>& subs, 310 std::map<Node, std::vector<Node> >& exp) override; 311 /** debug print */ 312 void printModelDebug( const char* c ); 313 /** entailment check */ 314 std::pair<bool, Node> entailmentCheck( 315 TNode lit, 316 const EntailmentCheckParameters* params = NULL, 317 EntailmentCheckSideEffects* out = NULL) override; 318 319 private: 320 /** add tester to equivalence class info */ 321 void addTester(unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg); 322 /** add selector to equivalence class info */ 323 void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true ); 324 /** add constructor */ 325 void addConstructor( Node c, EqcInfo* eqc, Node n ); 326 /** merge the equivalence class info of t1 and t2 */ 327 void merge( Node t1, Node t2 ); 328 /** collapse selector, s is of the form sel( n ) where n = c */ 329 void collapseSelector( Node s, Node c ); 330 /** remove uninterpreted constants */ 331 Node removeUninterpretedConstants( Node n, std::map< Node, Node >& visited ); 332 /** for checking if cycles exist */ 333 void checkCycles(); 334 Node searchForCycle( TNode n, TNode on, 335 std::map< TNode, bool >& visited, std::map< TNode, bool >& proc, 336 std::vector< TNode >& explanation, bool firstTime = true ); 337 /** for checking whether two codatatype terms must be equal */ 338 void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out, 339 std::vector< TNode >& exp, 340 std::map< Node, Node >& cn, 341 std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ); 342 /** build model */ 343 Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ); 344 /** get singleton lemma */ 345 Node getSingletonLemma( TypeNode tn, bool pol ); 346 /** collect terms */ 347 void collectTerms( Node n ); 348 /** get instantiate cons */ 349 Node getInstantiateCons( Node n, const Datatype& dt, int index ); 350 /** check instantiate */ 351 void instantiate( EqcInfo* eqc, Node n ); 352 /** must communicate fact */ 353 bool mustCommunicateFact( Node n, Node exp ); 354 /** get relevant terms */ 355 void getRelevantTerms( std::set<Node>& termSet ); 356 private: 357 //equality queries 358 bool hasTerm( TNode a ); 359 bool areEqual( TNode a, TNode b ); 360 bool areDisequal( TNode a, TNode b ); 361 bool areCareDisequal( TNode x, TNode y ); 362 TNode getRepresentative( TNode a ); 363 private: 364 /** sygus symmetry breaking utility */ 365 SygusSymBreakNew* d_sygus_sym_break; 366 367 };/* class TheoryDatatypes */ 368 369 }/* CVC4::theory::datatypes namespace */ 370 }/* CVC4::theory namespace */ 371 }/* CVC4 namespace */ 372 373 #endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */ 374