Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Tim King, Haniel Barbosa
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Theory of separation logic.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__SEP__THEORY_SEP_H
19 : : #define CVC5__THEORY__SEP__THEORY_SEP_H
20 : :
21 : : #include "context/cdhashmap.h"
22 : : #include "context/cdhashset.h"
23 : : #include "context/cdlist.h"
24 : : #include "context/cdqueue.h"
25 : : #include "theory/decision_strategy.h"
26 : : #include "theory/inference_manager_buffered.h"
27 : : #include "theory/sep/theory_sep_rewriter.h"
28 : : #include "theory/theory.h"
29 : : #include "theory/theory_state.h"
30 : : #include "theory/uf/equality_engine.h"
31 : : #include "util/statistics_stats.h"
32 : :
33 : : namespace cvc5::internal {
34 : : namespace theory {
35 : :
36 : : class TheoryModel;
37 : :
38 : : namespace sep {
39 : :
40 : : class TheorySep : public Theory {
41 : : typedef context::CDList<Node> NodeList;
42 : : typedef context::CDHashSet<Node> NodeSet;
43 : : typedef context::CDHashMap<Node, Node> NodeNodeMap;
44 : :
45 : : /////////////////////////////////////////////////////////////////////////////
46 : : // MISC
47 : : /////////////////////////////////////////////////////////////////////////////
48 : :
49 : : private:
50 : : /** True node for predicates = true */
51 : : Node d_true;
52 : :
53 : : /** True node for predicates = false */
54 : : Node d_false;
55 : :
56 : : /** Trust id (for proofs) */
57 : : Node d_tiid;
58 : :
59 : : //whether bounds have been initialized
60 : : bool d_bounds_init;
61 : :
62 : : TheorySepRewriter d_rewriter;
63 : : /** A (default) theory state object */
64 : : TheoryState d_state;
65 : : /** A buffered inference manager */
66 : : InferenceManagerBuffered d_im;
67 : :
68 : : size_t processAssertion(
69 : : Node n,
70 : : std::map<int, std::map<Node, size_t> >& visited,
71 : : std::map<int, std::map<Node, std::vector<Node> > >& references,
72 : : std::map<int, std::map<Node, bool> >& references_strict,
73 : : bool pol,
74 : : bool hasPol,
75 : : bool underSpatial);
76 : :
77 : : public:
78 : : TheorySep(Env& env, OutputChannel& out, Valuation valuation);
79 : : ~TheorySep();
80 : :
81 : : //--------------------------------- initialization
82 : : /** get the official theory rewriter of this theory */
83 : : TheoryRewriter* getTheoryRewriter() override;
84 : : /** get the proof checker of this theory */
85 : : ProofRuleChecker* getProofChecker() override;
86 : : /**
87 : : * Returns true if we need an equality engine. If so, we initialize the
88 : : * information regarding how it should be setup. For details, see the
89 : : * documentation in Theory::needsEqualityEngine.
90 : : */
91 : : bool needsEqualityEngine(EeSetupInfo& esi) override;
92 : : /** finish initialization */
93 : : void finishInit() override;
94 : : //--------------------------------- end initialization
95 : : /** preregister term */
96 : : void preRegisterTerm(TNode n) override;
97 : :
98 : 0 : std::string identify() const override { return std::string("TheorySep"); }
99 : :
100 : : void ppNotifyAssertions(const std::vector<Node>& assertions) override;
101 : :
102 : : TrustNode explain(TNode n) override;
103 : :
104 : : void postProcessModel(TheoryModel* m) override;
105 : :
106 : : private:
107 : : /**
108 : : * Initialize heap. For smt2 inputs, this will initialize the heap types
109 : : * based on if a command (declare-heap (locT datat)) was used. This command
110 : : * can be executed once only, and must be invoked before solving separation
111 : : * logic inputs, which is controlled by the solver engine.
112 : : */
113 : : void initializeHeapTypes();
114 : : /** Should be called to propagate the literal. */
115 : : bool propagateLit(TNode literal);
116 : : /** Conflict when merging constants */
117 : : void conflict(TNode a, TNode b);
118 : :
119 : : public:
120 : :
121 : : void presolve() override;
122 : :
123 : : /////////////////////////////////////////////////////////////////////////////
124 : : // MAIN SOLVER
125 : : /////////////////////////////////////////////////////////////////////////////
126 : :
127 : : //--------------------------------- standard check
128 : : /** Do we need a check call at last call effort? */
129 : : bool needsCheckLastEffort() override;
130 : : /** Post-check, called after the fact queue of the theory is processed. */
131 : : void postCheck(Effort level) override;
132 : : /** Pre-notify fact, return true if processed. */
133 : : bool preNotifyFact(TNode atom,
134 : : bool pol,
135 : : TNode fact,
136 : : bool isPrereg,
137 : : bool isInternal) override;
138 : : /** Notify fact */
139 : : void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
140 : : //--------------------------------- end standard check
141 : :
142 : : private:
143 : : /** Ensures that the reduction has been added for the given fact */
144 : : void reduceFact(TNode atom, bool polarity, TNode fact);
145 : : /** Is spatial kind? */
146 : : bool isSpatialKind(Kind k) const;
147 : : // NotifyClass: template helper class for d_equalityEngine - handles
148 : : // call-back from congruence closure module
149 : : class NotifyClass : public eq::EqualityEngineNotify
150 : : {
151 : : TheorySep& d_sep;
152 : :
153 : : public:
154 : 49899 : NotifyClass(TheorySep& sep) : d_sep(sep) {}
155 : :
156 : 0 : bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
157 : : {
158 [ - - ]: 0 : Trace("sep::propagate")
159 : 0 : << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", "
160 [ - - ]: 0 : << (value ? "true" : "false") << ")" << std::endl;
161 : 0 : Assert(predicate.getKind() == Kind::EQUAL);
162 : : // Just forward to sep
163 [ - - ]: 0 : if (value)
164 : : {
165 : 0 : return d_sep.propagateLit(predicate);
166 : : }
167 : 0 : return d_sep.propagateLit(predicate.notNode());
168 : : }
169 : 17429 : bool eqNotifyTriggerTermEquality(CVC5_UNUSED TheoryId tag,
170 : : TNode t1,
171 : : TNode t2,
172 : : bool value) override
173 : : {
174 [ + - ]: 34858 : Trace("sep::propagate")
175 : 0 : << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2
176 [ - - ]: 17429 : << ", " << (value ? "true" : "false") << ")" << std::endl;
177 [ + + ]: 17429 : if (value)
178 : : {
179 : : // Propagate equality between shared terms
180 : 8140 : return d_sep.propagateLit(t1.eqNode(t2));
181 : : }
182 : 9289 : return d_sep.propagateLit(t1.eqNode(t2).notNode());
183 : : }
184 : :
185 : 0 : void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
186 : : {
187 [ - - ]: 0 : Trace("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
188 : 0 : << ", " << t2 << ")" << std::endl;
189 : 0 : d_sep.conflict(t1, t2);
190 : 0 : }
191 : :
192 : 16890 : void eqNotifyNewClass(CVC5_UNUSED TNode t) override {}
193 : 28553 : void eqNotifyMerge(TNode t1, TNode t2) override
194 : : {
195 : 28553 : d_sep.eqNotifyMerge(t1, t2);
196 : 28553 : }
197 : 9289 : void eqNotifyDisequal(CVC5_UNUSED TNode t1,
198 : : CVC5_UNUSED TNode t2,
199 : : CVC5_UNUSED TNode reason) override
200 : : {
201 : 9289 : }
202 : : };
203 : :
204 : : /** The notify class for d_equalityEngine */
205 : : NotifyClass d_notify;
206 : :
207 : : /** list of all refinement lemms */
208 : : std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem;
209 : :
210 : : //cache for positive polarity start reduction
211 : : NodeSet d_reduce;
212 : : std::map< Node, std::map< Node, Node > > d_red_conc;
213 : : std::map< Node, std::map< Node, Node > > d_neg_guard;
214 : : std::vector< Node > d_neg_guards;
215 : : /** a (singleton) decision strategy for each negative guard. */
216 : : std::map<Node, std::unique_ptr<DecisionStrategySingleton> >
217 : : d_neg_guard_strategy;
218 : : std::map< Node, Node > d_guard_to_assertion;
219 : : NodeList d_spatial_assertions;
220 : :
221 : : //data,ref type (globally fixed)
222 : : TypeNode d_type_ref;
223 : : TypeNode d_type_data;
224 : : //information about types
225 : : Node d_base_label;
226 : : Node d_nil_ref;
227 : : //reference bound
228 : : Node d_reference_bound;
229 : : Node d_reference_bound_max;
230 : : std::vector<Node> d_type_references;
231 : : //kind of bound for reference types
232 : : enum {
233 : : bound_strict,
234 : : bound_default,
235 : : bound_invalid,
236 : : };
237 : : unsigned d_bound_kind;
238 : :
239 : : std::vector<Node> d_type_references_card;
240 : : std::map< Node, unsigned > d_type_ref_card_id;
241 : : std::vector<Node> d_type_references_all;
242 : : size_t d_card_max;
243 : : //for empty argument
244 : : Node d_emp_arg;
245 : : //map from ( atom, label, child index ) -> label
246 : : std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map;
247 : :
248 : : /**
249 : : * Maps label sets to their direct parents. A set may have multiple parents
250 : : * if sep.wand constraints are present.
251 : : */
252 : : std::map<Node, std::vector<Node> > d_parentMap;
253 : : /**
254 : : * Maps label sets to their direct children. This map is only stored for
255 : : * labels with children that do not share a root label with the base label.
256 : : */
257 : : std::map<Node, std::vector<Node> > d_childrenMap;
258 : :
259 : : /**
260 : : * This sends the lemmas:
261 : : * parent = (set.union children)
262 : : * (set.inter children_i children_j) = empty, for each i != j
263 : : * It also stores these relationships in d_parentMap.
264 : : */
265 : : void makeDisjointHeap(Node parent, const std::vector<Node>& children);
266 : : /**
267 : : * Get the sets that are parents of p and are roots in the graph induced
268 : : * by d_parentMap.
269 : : */
270 : : std::vector<Node> getRootLabels(Node p) const;
271 : : /**
272 : : * Do p and q have a root label in common?
273 : : */
274 : : bool sharesRootLabel(Node p, Node q) const;
275 : :
276 : : //term model
277 : : std::map< Node, Node > d_tmodel;
278 : : std::map< Node, Node > d_pto_model;
279 : :
280 : : /**
281 : : * A heap assert info is maintained per set equivalence class. It is
282 : : * used to ensure that list of positive and negative pto constraints for
283 : : * all label sets that are equal to a given one are satisfied.
284 : : *
285 : : * Note that sets referring to subsets of different heaps may become equated,
286 : : * e.g. if wand constraints are present. Thus, we keep a list of pto
287 : : * constraints, which track their labels. In the checkPto method, we
288 : : * distinguish whether the pto constraints refer to the same heap.
289 : : */
290 : : class HeapAssertInfo {
291 : : public:
292 : : HeapAssertInfo(context::Context* c);
293 : 1496 : ~HeapAssertInfo() {}
294 : : /** List of positive pto */
295 : : NodeList d_posPto;
296 : : /** List of negative pto */
297 : : NodeList d_negPto;
298 : : };
299 : : std::map< Node, HeapAssertInfo * > d_eqc_info;
300 : : HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
301 : :
302 : : /**
303 : : * Ensure that reference and data types have been set to something that is
304 : : * non-null, and compatible with separation logic constraint atom.
305 : : */
306 : : void ensureHeapTypesFor(Node atom) const;
307 : : /**
308 : : * This is called either when:
309 : : * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
310 : : * (B) an atom specifying the heap type tn1/tn2 is registered to this theory.
311 : : * We set the heap type if we are are case (A), and check whether the
312 : : * heap type is consistent in the case of (B).
313 : : */
314 : : void registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom);
315 : : //get location/data type
316 : : //get the base label for the spatial assertion
317 : : Node getBaseLabel();
318 : : Node getLabel( Node atom, int child, Node lbl );
319 : : /**
320 : : * Apply label lbl to all top-level spatial assertions, recursively, in n.
321 : : */
322 : : Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited );
323 : : void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels );
324 : :
325 : : class HeapInfo {
326 : : public:
327 : 1398 : HeapInfo() : d_computed(false) {}
328 : : //information about the model
329 : : bool d_computed;
330 : : std::vector< Node > d_heap_locs;
331 : : std::vector< Node > d_heap_locs_model;
332 : : //get value
333 : : Node getValue(NodeManager* nm, TypeNode tn);
334 : : };
335 : : //heap info ( label -> HeapInfo )
336 : : std::map< Node, HeapInfo > d_label_model;
337 : : /**
338 : : * This checks the impact of adding the pto assertion p to heap assert info e,
339 : : * where p has been asserted with the given polarity.
340 : : *
341 : : * This method implements two propagation schemes for pairs of
342 : : * positive/positive and positive/negative pto constraints.
343 : : *
344 : : * @param e The heap assert info
345 : : * @param p The (label) pto constraint
346 : : * @param polarity Its asserted polarity
347 : : * @return true if p should be added to the list of constraints in e, false
348 : : * if the constraint was redundant.
349 : : */
350 : : bool checkPto(HeapAssertInfo* e, Node p, bool polarity);
351 : : void computeLabelModel( Node lbl );
352 : : Node instantiateLabel(Node n,
353 : : Node o_lbl,
354 : : Node lbl,
355 : : Node lbl_v,
356 : : std::map<Node, Node>& visited,
357 : : std::map<Node, Node>& pto_model,
358 : : TypeNode rtn,
359 : : std::map<Node, bool>& active_lbl,
360 : : unsigned ind = 0);
361 : : void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
362 : :
363 : : Node mkUnion( TypeNode tn, std::vector< Node >& locs );
364 : :
365 : : Node getRepresentative( Node t );
366 : : bool hasTerm( Node a );
367 : : bool areEqual( Node a, Node b );
368 : : bool areDisequal( Node a, Node b );
369 : : void eqNotifyMerge(TNode t1, TNode t2);
370 : :
371 : : void sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer = false );
372 : : void doPending();
373 : :
374 : : void initializeBounds();
375 : : };/* class TheorySep */
376 : :
377 : : } // namespace sep
378 : : } // namespace theory
379 : : } // namespace cvc5::internal
380 : :
381 : : #endif /* CVC5__THEORY__SEP__THEORY_SEP_H */
|
