1 /********************* */ 2 /*! \file theory_sep.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 sep 13 ** 14 ** Theory of sep. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__THEORY__SEP__THEORY_SEP_H 20 #define __CVC4__THEORY__SEP__THEORY_SEP_H 21 22 #include "context/cdhashmap.h" 23 #include "context/cdhashset.h" 24 #include "context/cdlist.h" 25 #include "context/cdqueue.h" 26 #include "theory/theory.h" 27 #include "theory/uf/equality_engine.h" 28 #include "util/statistics_registry.h" 29 30 namespace CVC4 { 31 namespace theory { 32 33 class TheoryModel; 34 35 namespace sep { 36 37 class TheorySep : public Theory { 38 typedef context::CDList<Node> NodeList; 39 typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; 40 typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; 41 42 ///////////////////////////////////////////////////////////////////////////// 43 // MISC 44 ///////////////////////////////////////////////////////////////////////////// 45 46 private: 47 /** all lemmas sent */ 48 NodeSet d_lemmas_produced_c; 49 50 /** True node for predicates = true */ 51 Node d_true; 52 53 /** True node for predicates = false */ 54 Node d_false; 55 56 //whether bounds have been initialized 57 bool d_bounds_init; 58 59 Node mkAnd( std::vector< TNode >& assumptions ); 60 61 int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited, 62 std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict, 63 bool pol, bool hasPol, bool underSpatial ); 64 65 public: 66 TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); 67 ~TheorySep(); 68 69 void setMasterEqualityEngine(eq::EqualityEngine* eq) override; 70 identify()71 std::string identify() const override { return std::string("TheorySep"); } 72 73 ///////////////////////////////////////////////////////////////////////////// 74 // PREPROCESSING 75 ///////////////////////////////////////////////////////////////////////////// 76 77 public: 78 PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; 79 Node ppRewrite(TNode atom) override; 80 81 void ppNotifyAssertions(const std::vector<Node>& assertions) override; 82 ///////////////////////////////////////////////////////////////////////////// 83 // T-PROPAGATION / REGISTRATION 84 ///////////////////////////////////////////////////////////////////////////// 85 86 private: 87 /** Should be called to propagate the literal. */ 88 bool propagate(TNode literal); 89 90 /** Explain why this literal is true by adding assumptions */ 91 void explain(TNode literal, std::vector<TNode>& assumptions); 92 93 public: 94 void propagate(Effort e) override; 95 Node explain(TNode n) override; 96 97 public: 98 void addSharedTerm(TNode t) override; 99 EqualityStatus getEqualityStatus(TNode a, TNode b) override; 100 void computeCareGraph() override; 101 102 ///////////////////////////////////////////////////////////////////////////// 103 // MODEL GENERATION 104 ///////////////////////////////////////////////////////////////////////////// 105 106 public: 107 bool collectModelInfo(TheoryModel* m) override; 108 void postProcessModel(TheoryModel* m) override; 109 110 ///////////////////////////////////////////////////////////////////////////// 111 // NOTIFICATIONS 112 ///////////////////////////////////////////////////////////////////////////// 113 114 public: 115 116 void presolve() override; shutdown()117 void shutdown() override {} 118 119 ///////////////////////////////////////////////////////////////////////////// 120 // MAIN SOLVER 121 ///////////////////////////////////////////////////////////////////////////// 122 public: 123 void check(Effort e) override; 124 125 bool needsCheckLastEffort() override; 126 127 private: 128 // NotifyClass: template helper class for d_equalityEngine - handles 129 // call-back from congruence closure module 130 class NotifyClass : public eq::EqualityEngineNotify 131 { 132 TheorySep& d_sep; 133 134 public: NotifyClass(TheorySep & sep)135 NotifyClass(TheorySep& sep) : d_sep(sep) {} 136 eqNotifyTriggerEquality(TNode equality,bool value)137 bool eqNotifyTriggerEquality(TNode equality, bool value) override 138 { 139 Debug("sep::propagate") 140 << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " 141 << (value ? "true" : "false") << ")" << std::endl; 142 // Just forward to sep 143 if (value) 144 { 145 return d_sep.propagate(equality); 146 } 147 else 148 { 149 return d_sep.propagate(equality.notNode()); 150 } 151 } 152 eqNotifyTriggerPredicate(TNode predicate,bool value)153 bool eqNotifyTriggerPredicate(TNode predicate, bool value) override 154 { 155 Unreachable(); 156 } 157 eqNotifyTriggerTermEquality(TheoryId tag,TNode t1,TNode t2,bool value)158 bool eqNotifyTriggerTermEquality(TheoryId tag, 159 TNode t1, 160 TNode t2, 161 bool value) override 162 { 163 Debug("sep::propagate") 164 << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 165 << ", " << (value ? "true" : "false") << ")" << std::endl; 166 if (value) 167 { 168 // Propagate equality between shared terms 169 return d_sep.propagate(t1.eqNode(t2)); 170 } 171 else 172 { 173 return d_sep.propagate(t1.eqNode(t2).notNode()); 174 } 175 return true; 176 } 177 eqNotifyConstantTermMerge(TNode t1,TNode t2)178 void eqNotifyConstantTermMerge(TNode t1, TNode t2) override 179 { 180 Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 181 << ", " << t2 << ")" << std::endl; 182 d_sep.conflict(t1, t2); 183 } 184 eqNotifyNewClass(TNode t)185 void eqNotifyNewClass(TNode t) override {} eqNotifyPreMerge(TNode t1,TNode t2)186 void eqNotifyPreMerge(TNode t1, TNode t2) override 187 { 188 d_sep.eqNotifyPreMerge(t1, t2); 189 } eqNotifyPostMerge(TNode t1,TNode t2)190 void eqNotifyPostMerge(TNode t1, TNode t2) override 191 { 192 d_sep.eqNotifyPostMerge(t1, t2); 193 } eqNotifyDisequal(TNode t1,TNode t2,TNode reason)194 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} 195 }; 196 197 /** The notify class for d_equalityEngine */ 198 NotifyClass d_notify; 199 200 /** Equaltity engine */ 201 eq::EqualityEngine d_equalityEngine; 202 203 /** Are we in conflict? */ 204 context::CDO<bool> d_conflict; 205 std::vector< Node > d_pending_exp; 206 std::vector< Node > d_pending; 207 std::vector< int > d_pending_lem; 208 209 /** list of all refinement lemms */ 210 std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem; 211 212 /** Conflict when merging constants */ 213 void conflict(TNode a, TNode b); 214 215 //cache for positive polarity start reduction 216 NodeSet d_reduce; 217 std::map< Node, std::map< Node, Node > > d_red_conc; 218 std::map< Node, std::map< Node, Node > > d_neg_guard; 219 std::vector< Node > d_neg_guards; 220 /** a (singleton) decision strategy for each negative guard. */ 221 std::map<Node, std::unique_ptr<DecisionStrategySingleton> > 222 d_neg_guard_strategy; 223 std::map< Node, Node > d_guard_to_assertion; 224 /** inferences: maintained to ensure ref count for internally introduced nodes */ 225 NodeList d_infer; 226 NodeList d_infer_exp; 227 NodeList d_spatial_assertions; 228 229 //data,ref type (globally fixed) 230 TypeNode d_type_ref; 231 TypeNode d_type_data; 232 //currently fix one data type for each location type, throw error if using more than one 233 std::map< TypeNode, TypeNode > d_loc_to_data_type; 234 //information about types 235 std::map< TypeNode, Node > d_base_label; 236 std::map< TypeNode, Node > d_nil_ref; 237 //reference bound 238 std::map< TypeNode, Node > d_reference_bound; 239 std::map< TypeNode, Node > d_reference_bound_max; 240 std::map< TypeNode, std::vector< Node > > d_type_references; 241 //kind of bound for reference types 242 enum { 243 bound_strict, 244 bound_default, 245 bound_herbrand, 246 bound_invalid, 247 }; 248 std::map< TypeNode, unsigned > d_bound_kind; 249 250 std::map< TypeNode, std::vector< Node > > d_type_references_card; 251 std::map< Node, unsigned > d_type_ref_card_id; 252 std::map< TypeNode, std::vector< Node > > d_type_references_all; 253 std::map< TypeNode, unsigned > d_card_max; 254 //for empty argument 255 std::map< TypeNode, Node > d_emp_arg; 256 //map from ( atom, label, child index ) -> label 257 std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map; 258 std::map< Node, Node > d_label_map_parent; 259 260 //term model 261 std::map< Node, Node > d_tmodel; 262 std::map< Node, Node > d_pto_model; 263 264 class HeapAssertInfo { 265 public: 266 HeapAssertInfo( context::Context* c ); ~HeapAssertInfo()267 ~HeapAssertInfo(){} 268 context::CDO< Node > d_pto; 269 context::CDO< bool > d_has_neg_pto; 270 }; 271 std::map< Node, HeapAssertInfo * > d_eqc_info; 272 HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false ); 273 274 //get global reference/data type 275 TypeNode getReferenceType( Node n ); 276 TypeNode getDataType( Node n ); 277 void registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ); 278 //get location/data type 279 //get the base label for the spatial assertion 280 Node getBaseLabel( TypeNode tn ); 281 Node getNilRef( TypeNode tn ); 282 void setNilRef( TypeNode tn, Node n ); 283 Node getLabel( Node atom, int child, Node lbl ); 284 Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ); 285 void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels ); 286 287 class HeapInfo { 288 public: HeapInfo()289 HeapInfo() : d_computed(false) {} 290 //information about the model 291 bool d_computed; 292 std::vector< Node > d_heap_locs; 293 std::vector< Node > d_heap_locs_model; 294 //get value 295 Node getValue( TypeNode tn ); 296 }; 297 //heap info ( label -> HeapInfo ) 298 std::map< Node, HeapInfo > d_label_model; 299 // loc -> { data_1, ..., data_n } where (not (pto loc data_1))...(not (pto loc data_n))). 300 std::map< Node, std::vector< Node > > d_heap_locs_nptos; 301 302 void debugPrintHeap( HeapInfo& heap, const char * c ); 303 void validatePto( HeapAssertInfo * ei, Node ei_n ); 304 void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ); 305 void mergePto( Node p1, Node p2 ); 306 void computeLabelModel( Node lbl ); 307 Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, 308 TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 ); 309 void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ); 310 311 Node mkUnion( TypeNode tn, std::vector< Node >& locs ); 312 313 private: 314 Node getRepresentative( Node t ); 315 bool hasTerm( Node a ); 316 bool areEqual( Node a, Node b ); 317 bool areDisequal( Node a, Node b ); 318 void eqNotifyPreMerge(TNode t1, TNode t2); 319 void eqNotifyPostMerge(TNode t1, TNode t2); 320 321 void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false ); 322 void doPendingFacts(); 323 324 public: getEqualityEngine()325 eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } 326 327 void initializeBounds(); 328 };/* class TheorySep */ 329 330 }/* CVC4::theory::sep namespace */ 331 }/* CVC4::theory namespace */ 332 }/* CVC4 namespace */ 333 334 #endif /* __CVC4__THEORY__SEP__THEORY_SEP_H */ 335