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