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