src/theory/sep/theory_sep.h

   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-2021 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/decision_strategy.h"
  27 #include "theory/inference_manager_buffered.h"
  28 #include "theory/sep/theory_sep_rewriter.h"
  29 #include "theory/theory.h"
  30 #include "theory/theory_state.h"
  31 #include "theory/uf/equality_engine.h"
  32 #include "util/statistics_registry.h"
  33
  34 namespace CVC5 {
  35 namespace theory {
  36
  37 class TheoryModel;
  38
  39 namespace sep {
  40
  41 class TheorySep : public Theory {
  42   typedef context::CDList<Node> NodeList;
  43   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  44   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
  45
  46   /////////////////////////////////////////////////////////////////////////////
  47   // MISC
  48   /////////////////////////////////////////////////////////////////////////////
  49
  50  private:
  51   /** all lemmas sent */
  52   NodeSet d_lemmas_produced_c;
  53
  54   /** True node for predicates = true */
  55   Node d_true;
  56
  57   /** True node for predicates = false */
  58   Node d_false;
  59
  60   //whether bounds have been initialized
  61   bool d_bounds_init;
  62
  63   TheorySepRewriter d_rewriter;
  64   /** A (default) theory state object */
  65   TheoryState d_state;
  66   /** A buffered inference manager */
  67   InferenceManagerBuffered d_im;
  68
  69   Node mkAnd( std::vector< TNode >& assumptions );
  70
  71   int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited,
  72                         std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
  73                         bool pol, bool hasPol, bool underSpatial );
  74
  75  public:
  76   TheorySep(context::Context* c,
  77             context::UserContext* u,
  78             OutputChannel& out,
  79             Valuation valuation,
  80             const LogicInfo& logicInfo,
  81             ProofNodeManager* pnm = nullptr);
  82   ~TheorySep();
  83
  84   /**
  85    * Declare heap. For smt2 inputs, this is called when the command
  86    * (declare-heap (locT datat)) is invoked by the user. This sets locT as the
  87    * location type and dataT is the data type for the heap. This command can be
  88    * executed once only, and must be invoked before solving separation logic
  89    * inputs.
  90    */
  91   void declareSepHeap(TypeNode locT, TypeNode dataT) override;
  92
  93   //--------------------------------- initialization
  94   /** get the official theory rewriter of this theory */
  95   TheoryRewriter* getTheoryRewriter() override;
  96   /**
  97    * Returns true if we need an equality engine. If so, we initialize the
  98    * information regarding how it should be setup. For details, see the
  99    * documentation in Theory::needsEqualityEngine.
 100    */
 101   bool needsEqualityEngine(EeSetupInfo& esi) override;
 102   /** finish initialization */
 103   void finishInit() override;
 104   //--------------------------------- end initialization
 105   /** preregister term */
 106   void preRegisterTerm(TNode n) override;
 107
 108   std::string identify() const override { return std::string("TheorySep"); }
 109
 110   /////////////////////////////////////////////////////////////////////////////
 111   // PREPROCESSING
 112   /////////////////////////////////////////////////////////////////////////////
 113
 114  public:
 115   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
 116   /////////////////////////////////////////////////////////////////////////////
 117   // T-PROPAGATION / REGISTRATION
 118   /////////////////////////////////////////////////////////////////////////////
 119
 120  private:
 121   /** Should be called to propagate the literal.  */
 122   bool propagateLit(TNode literal);
 123   /** Conflict when merging constants */
 124   void conflict(TNode a, TNode b);
 125
 126  public:
 127   TrustNode explain(TNode n) override;
 128
 129  public:
 130   void computeCareGraph() override;
 131
 132   /////////////////////////////////////////////////////////////////////////////
 133   // MODEL GENERATION
 134   /////////////////////////////////////////////////////////////////////////////
 135
 136  public:
 137   void postProcessModel(TheoryModel* m) override;
 138
 139   /////////////////////////////////////////////////////////////////////////////
 140   // NOTIFICATIONS
 141   /////////////////////////////////////////////////////////////////////////////
 142
 143  public:
 144
 145   void presolve() override;
 146   void shutdown() override {}
 147
 148   /////////////////////////////////////////////////////////////////////////////
 149   // MAIN SOLVER
 150   /////////////////////////////////////////////////////////////////////////////
 151
 152   //--------------------------------- standard check
 153   /** Do we need a check call at last call effort? */
 154   bool needsCheckLastEffort() override;
 155   /** Post-check, called after the fact queue of the theory is processed. */
 156   void postCheck(Effort level) override;
 157   /** Pre-notify fact, return true if processed. */
 158   bool preNotifyFact(TNode atom,
 159                      bool pol,
 160                      TNode fact,
 161                      bool isPrereg,
 162                      bool isInternal) override;
 163   /** Notify fact */
 164   void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
 165   //--------------------------------- end standard check
 166
 167  private:
 168   /** Ensures that the reduction has been added for the given fact */
 169   void reduceFact(TNode atom, bool polarity, TNode fact);
 170   /** Is spatial kind? */
 171   bool isSpatialKind(Kind k) const;
 172   // NotifyClass: template helper class for d_equalityEngine - handles
 173   // call-back from congruence closure module
 174   class NotifyClass : public eq::EqualityEngineNotify
 175   {
 176     TheorySep& d_sep;
 177
 178    public:
 179     NotifyClass(TheorySep& sep) : d_sep(sep) {}
 180
 181     bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
 182     {
 183       Debug("sep::propagate")
 184           << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", "
 185           << (value ? "true" : "false") << ")" << std::endl;
 186       Assert(predicate.getKind() == kind::EQUAL);
 187       // Just forward to sep
 188       if (value)
 189       {
 190         return d_sep.propagateLit(predicate);
 191       }
 192       return d_sep.propagateLit(predicate.notNode());
 193     }
 194     bool eqNotifyTriggerTermEquality(TheoryId tag,
 195                                      TNode t1,
 196                                      TNode t2,
 197                                      bool value) override
 198     {
 199       Debug("sep::propagate")
 200           << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2
 201           << ", " << (value ? "true" : "false") << ")" << std::endl;
 202       if (value)
 203       {
 204         // Propagate equality between shared terms
 205         return d_sep.propagateLit(t1.eqNode(t2));
 206       }
 207       return d_sep.propagateLit(t1.eqNode(t2).notNode());
 208     }
 209
 210     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
 211     {
 212       Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
 213                               << ", " << t2 << ")" << std::endl;
 214       d_sep.conflict(t1, t2);
 215     }
 216
 217     void eqNotifyNewClass(TNode t) override {}
 218     void eqNotifyMerge(TNode t1, TNode t2) override
 219     {
 220       d_sep.eqNotifyMerge(t1, t2);
 221     }
 222     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
 223   };
 224
 225   /** The notify class for d_equalityEngine */
 226   NotifyClass d_notify;
 227
 228   /** list of all refinement lemms */
 229   std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem;
 230
 231   //cache for positive polarity start reduction
 232   NodeSet d_reduce;
 233   std::map< Node, std::map< Node, Node > > d_red_conc;
 234   std::map< Node, std::map< Node, Node > > d_neg_guard;
 235   std::vector< Node > d_neg_guards;
 236   /** a (singleton) decision strategy for each negative guard. */
 237   std::map<Node, std::unique_ptr<DecisionStrategySingleton> >
 238       d_neg_guard_strategy;
 239   std::map< Node, Node > d_guard_to_assertion;
 240   NodeList d_spatial_assertions;
 241
 242   //data,ref type (globally fixed)
 243   TypeNode d_type_ref;
 244   TypeNode d_type_data;
 245   //currently fix one data type for each location type, throw error if using more than one
 246   std::map< TypeNode, TypeNode > d_loc_to_data_type;
 247   //information about types
 248   std::map< TypeNode, Node > d_base_label;
 249   std::map< TypeNode, Node > d_nil_ref;
 250   //reference bound
 251   std::map< TypeNode, Node > d_reference_bound;
 252   std::map< TypeNode, Node > d_reference_bound_max;
 253   std::map< TypeNode, std::vector< Node > > d_type_references;
 254   //kind of bound for reference types
 255   enum {
 256     bound_strict,
 257     bound_default,
 258     bound_invalid,
 259   };
 260   std::map< TypeNode, unsigned > d_bound_kind;
 261
 262   std::map< TypeNode, std::vector< Node > > d_type_references_card;
 263   std::map< Node, unsigned > d_type_ref_card_id;
 264   std::map< TypeNode, std::vector< Node > > d_type_references_all;
 265   std::map< TypeNode, unsigned > d_card_max;
 266   //for empty argument
 267   std::map< TypeNode, Node > d_emp_arg;
 268   //map from ( atom, label, child index ) -> label
 269   std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map;
 270   std::map< Node, Node > d_label_map_parent;
 271
 272   //term model
 273   std::map< Node, Node > d_tmodel;
 274   std::map< Node, Node > d_pto_model;
 275
 276   class HeapAssertInfo {
 277   public:
 278     HeapAssertInfo( context::Context* c );
 279     ~HeapAssertInfo(){}
 280     context::CDO< Node > d_pto;
 281     context::CDO< bool > d_has_neg_pto;
 282   };
 283   std::map< Node, HeapAssertInfo * > d_eqc_info;
 284   HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
 285
 286   //get global reference/data type
 287   TypeNode getReferenceType( Node n );
 288   TypeNode getDataType( Node n );
 289   /**
 290    * Register reference data types for atom. Calls the method below for
 291    * the appropriate types.
 292    */
 293   void registerRefDataTypesAtom(Node atom);
 294   /**
 295    * This is called either when:
 296    * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
 297    * (B) an atom specifying the heap type tn1/tn2 is registered to this theory.
 298    * We set the heap type if we are are case (A), and check whether the
 299    * heap type is consistent in the case of (B).
 300    */
 301   void registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom);
 302   //get location/data type
 303   //get the base label for the spatial assertion
 304   Node getBaseLabel( TypeNode tn );
 305   Node getNilRef( TypeNode tn );
 306   void setNilRef( TypeNode tn, Node n );
 307   Node getLabel( Node atom, int child, Node lbl );
 308   Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited );
 309   void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels );
 310
 311   class HeapInfo {
 312   public:
 313     HeapInfo() : d_computed(false) {}
 314     //information about the model
 315     bool d_computed;
 316     std::vector< Node > d_heap_locs;
 317     std::vector< Node > d_heap_locs_model;
 318     //get value
 319     Node getValue( TypeNode tn );
 320   };
 321   //heap info ( label -> HeapInfo )
 322   std::map< Node, HeapInfo > d_label_model;
 323   // loc -> { data_1, ..., data_n } where (not (pto loc data_1))...(not (pto loc data_n))).
 324   std::map< Node, std::vector< Node > > d_heap_locs_nptos;
 325
 326   void debugPrintHeap( HeapInfo& heap, const char * c );
 327   void validatePto( HeapAssertInfo * ei, Node ei_n );
 328   void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
 329   void mergePto( Node p1, Node p2 );
 330   void computeLabelModel( Node lbl );
 331   Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model,
 332                          TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
 333   void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
 334
 335   Node mkUnion( TypeNode tn, std::vector< Node >& locs );
 336
 337  private:
 338   Node getRepresentative( Node t );
 339   bool hasTerm( Node a );
 340   bool areEqual( Node a, Node b );
 341   bool areDisequal( Node a, Node b );
 342   void eqNotifyMerge(TNode t1, TNode t2);
 343
 344   void sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer = false );
 345   void doPending();
 346
 347  public:
 348
 349   void initializeBounds();
 350 };/* class TheorySep */
 351
 352 }  // namespace sep
 353 }  // namespace theory
 354 }  // namespace CVC5
 355
 356 #endif /* CVC4__THEORY__SEP__THEORY_SEP_H */