src/theory/sep/theory_sep.h

   1 /*********************                                                        */
   2 /*! \file theory_sep.h
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Dejan Jovanovic, Clark Barrett
   6  ** Minor contributors (to current version): Tim King, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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 "theory/theory.h"
  23 #include "util/statistics_registry.h"
  24 #include "theory/uf/equality_engine.h"
  25 #include "context/cdchunk_list.h"
  26 #include "context/cdhashmap.h"
  27 #include "context/cdhashset.h"
  28 #include "context/cdqueue.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::CDChunkList<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   void processAssertion( Node n, std::map< Node, bool >& visited );
  62
  63   public:
  64
  65   TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
  66   ~TheorySep();
  67
  68   void setMasterEqualityEngine(eq::EqualityEngine* eq);
  69
  70   std::string identify() const { return std::string("TheorySep"); }
  71
  72   /////////////////////////////////////////////////////////////////////////////
  73   // PREPROCESSING
  74   /////////////////////////////////////////////////////////////////////////////
  75
  76   public:
  77
  78   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
  79   Node ppRewrite(TNode atom);
  80
  81   void ppNotifyAssertions( std::vector< Node >& assertions );
  82   /////////////////////////////////////////////////////////////////////////////
  83   // T-PROPAGATION / REGISTRATION
  84   /////////////////////////////////////////////////////////////////////////////
  85
  86   private:
  87
  88   /** Should be called to propagate the literal.  */
  89   bool propagate(TNode literal);
  90
  91   /** Explain why this literal is true by adding assumptions */
  92   void explain(TNode literal, std::vector<TNode>& assumptions);
  93
  94   public:
  95
  96   void propagate(Effort e);
  97   Node explain(TNode n);
  98
  99   public:
 100
 101   void addSharedTerm(TNode t);
 102   EqualityStatus getEqualityStatus(TNode a, TNode b);
 103   void computeCareGraph();
 104
 105   /////////////////////////////////////////////////////////////////////////////
 106   // MODEL GENERATION
 107   /////////////////////////////////////////////////////////////////////////////
 108
 109   public:
 110
 111   void collectModelInfo(TheoryModel* m, bool fullModel);
 112   void postProcessModel(TheoryModel* m);
 113
 114   /////////////////////////////////////////////////////////////////////////////
 115   // NOTIFICATIONS
 116   /////////////////////////////////////////////////////////////////////////////
 117
 118   private:
 119   public:
 120
 121   Node getNextDecisionRequest( unsigned& priority );
 122
 123   void presolve();
 124   void shutdown() { }
 125
 126   /////////////////////////////////////////////////////////////////////////////
 127   // MAIN SOLVER
 128   /////////////////////////////////////////////////////////////////////////////
 129   public:
 130
 131   void check(Effort e);
 132
 133   bool needsCheckLastEffort();
 134
 135   private:
 136
 137   // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
 138   class NotifyClass : public eq::EqualityEngineNotify {
 139     TheorySep& d_sep;
 140   public:
 141     NotifyClass(TheorySep& sep): d_sep(sep) {}
 142
 143     bool eqNotifyTriggerEquality(TNode equality, bool value) {
 144       Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
 145       // Just forward to sep
 146       if (value) {
 147         return d_sep.propagate(equality);
 148       } else {
 149         return d_sep.propagate(equality.notNode());
 150       }
 151     }
 152
 153     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
 154       Unreachable();
 155     }
 156
 157     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 158       Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
 159       if (value) {
 160         // Propagate equality between shared terms
 161         return d_sep.propagate(t1.eqNode(t2));
 162       } else {
 163         return d_sep.propagate(t1.eqNode(t2).notNode());
 164       }
 165       return true;
 166     }
 167
 168     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 169       Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 170       d_sep.conflict(t1, t2);
 171     }
 172
 173     void eqNotifyNewClass(TNode t) { }
 174     void eqNotifyPreMerge(TNode t1, TNode t2) { d_sep.eqNotifyPreMerge( t1, t2 ); }
 175     void eqNotifyPostMerge(TNode t1, TNode t2) { d_sep.eqNotifyPostMerge( t1, t2 ); }
 176     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
 177   };
 178
 179   /** The notify class for d_equalityEngine */
 180   NotifyClass d_notify;
 181
 182   /** Equaltity engine */
 183   eq::EqualityEngine d_equalityEngine;
 184
 185   /** Are we in conflict? */
 186   context::CDO<bool> d_conflict;
 187   std::vector< Node > d_pending_exp;
 188   std::vector< Node > d_pending;
 189   std::vector< int > d_pending_lem;
 190
 191   /** list of all refinement lemms */
 192   std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem;
 193
 194   /** Conflict when merging constants */
 195   void conflict(TNode a, TNode b);
 196
 197   //cache for positive polarity start reduction
 198   NodeSet d_reduce;
 199   std::map< Node, std::map< Node, Node > > d_red_conc;
 200   std::map< Node, std::map< Node, Node > > d_neg_guard;
 201   std::vector< Node > d_neg_guards;
 202   std::map< Node, Node > d_guard_to_assertion;
 203   //cache for references
 204   std::map< Node, std::map< int, TypeNode > > d_reference_type;
 205   std::map< Node, std::map< int, int > > d_reference_type_card;
 206   std::map< Node, std::map< int, std::vector< Node > > > d_references;
 207   /** inferences: maintained to ensure ref count for internally introduced nodes */
 208   NodeList d_infer;
 209   NodeList d_infer_exp;
 210   NodeList d_spatial_assertions;
 211
 212   //data,ref type (globally fixed)
 213   TypeNode d_type_ref;
 214   TypeNode d_type_data;
 215   //currently fix one data type for each location type, throw error if using more than one
 216   std::map< TypeNode, TypeNode > d_loc_to_data_type;
 217   //information about types
 218   std::map< TypeNode, Node > d_base_label;
 219   std::map< TypeNode, Node > d_nil_ref;
 220   //reference bound
 221   std::map< TypeNode, Node > d_reference_bound;
 222   std::map< TypeNode, Node > d_reference_bound_max;
 223   std::map< TypeNode, bool > d_reference_bound_invalid;
 224   std::map< TypeNode, bool > d_reference_bound_fv;
 225   std::map< TypeNode, std::vector< Node > > d_type_references;
 226   std::map< TypeNode, std::vector< Node > > d_type_references_card;
 227   std::map< Node, unsigned > d_type_ref_card_id;
 228   std::map< TypeNode, std::vector< Node > > d_type_references_all;
 229   std::map< TypeNode, unsigned > d_card_max;
 230   //for empty argument
 231   std::map< TypeNode, Node > d_emp_arg;
 232   //map from ( atom, label, child index ) -> label
 233   std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map;
 234   std::map< Node, Node > d_label_map_parent;
 235
 236   //term model
 237   std::map< Node, Node > d_tmodel;
 238   std::map< Node, Node > d_pto_model;
 239
 240   class HeapAssertInfo {
 241   public:
 242     HeapAssertInfo( context::Context* c );
 243     ~HeapAssertInfo(){}
 244     context::CDO< Node > d_pto;
 245     context::CDO< bool > d_has_neg_pto;
 246   };
 247   std::map< Node, HeapAssertInfo * > d_eqc_info;
 248   HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
 249
 250   //get global reference/data type
 251   TypeNode getReferenceType( Node n );
 252   TypeNode getDataType( Node n );
 253   //calculate the element type of the heap for spatial assertions
 254   TypeNode computeReferenceType( Node atom, int& card, int index = -1 );
 255   TypeNode computeReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited);
 256   void registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom );
 257   //get location/data type
 258   //get the base label for the spatial assertion
 259   Node getBaseLabel( TypeNode tn );
 260   Node getNilRef( TypeNode tn );
 261   void setNilRef( TypeNode tn, Node n );
 262   Node getLabel( Node atom, int child, Node lbl );
 263   Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited );
 264   void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels );
 265
 266   class HeapInfo {
 267   public:
 268     HeapInfo() : d_computed(false) {}
 269     //information about the model
 270     bool d_computed;
 271     std::vector< Node > d_heap_locs;
 272     std::vector< Node > d_heap_locs_model;
 273     std::map< Node, std::vector< Node > > d_heap_locs_nptos;
 274     //get value
 275     Node getValue( TypeNode tn );
 276   };
 277   //heap info ( label -> HeapInfo )
 278   std::map< Node, HeapInfo > d_label_model;
 279
 280   void debugPrintHeap( HeapInfo& heap, const char * c );
 281   void validatePto( HeapAssertInfo * ei, Node ei_n );
 282   void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
 283   void mergePto( Node p1, Node p2 );
 284   void computeLabelModel( Node lbl );
 285   Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model,
 286                          TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
 287   void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
 288
 289   Node mkUnion( TypeNode tn, std::vector< Node >& locs );
 290 private:
 291   Node getRepresentative( Node t );
 292   bool hasTerm( Node a );
 293   bool areEqual( Node a, Node b );
 294   bool areDisequal( Node a, Node b );
 295   void eqNotifyPreMerge(TNode t1, TNode t2);
 296   void eqNotifyPostMerge(TNode t1, TNode t2);
 297
 298   void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
 299   void doPendingFacts();
 300 public:
 301   eq::EqualityEngine* getEqualityEngine() {
 302     return &d_equalityEngine;
 303   }
 304
 305   void initializeBounds();
 306 };/* class TheorySep */
 307
 308 }/* CVC4::theory::sep namespace */
 309 }/* CVC4::theory namespace */
 310 }/* CVC4 namespace */
 311
 312 #endif /* __CVC4__THEORY__SEP__THEORY_SEP_H */