Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Daniel Larraz, Aina Niemetz
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 : : * Utility for inferring whether a synthesis conjecture encodes a
14 : : * transition system.
15 : : */
16 : :
17 : : #include "cvc5_private.h"
18 : :
19 : : #ifndef CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
20 : : #define CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
21 : :
22 : : #include <map>
23 : : #include <vector>
24 : :
25 : : #include "expr/node.h"
26 : : #include "smt/env_obj.h"
27 : : #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
28 : : #include "theory/quantifiers/inst_match_trie.h"
29 : : #include "theory/quantifiers/single_inv_partition.h"
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace quantifiers {
34 : :
35 : : /**
36 : : * Utility for storing a deterministic trace of a transition system. A trace
37 : : * is stored as a collection of vectors of values that have been taken by
38 : : * the variables of transition system. For example, say we have a transition
39 : : * system with variables x,y,z. Say the precondition constrains these variables
40 : : * to x=1,y=2,z=3, and say that the transition relation admits the single
41 : : * trace: [1,2,3], [2,3,4], [3,4,5]. We store these three vectors of variables
42 : : * in the trie within this class.
43 : : *
44 : : * This utility is used for determining whether a transition system has a
45 : : * deterministic terminating trace and hence a trivial invariant.
46 : : */
47 : : class DetTrace
48 : : {
49 : : public:
50 : : /** The current value of the trace */
51 : : std::vector<Node> d_curr;
52 : : /**
53 : : * Increment the trace: index the current values, if successful (they are
54 : : * not a duplicate of a previous value), update the current values to vals.
55 : : * Returns true if the increment was successful.
56 : : */
57 : : bool increment(Node loc, std::vector<Node>& vals);
58 : : /**
59 : : * Construct the formula that this trace represents with respect to variables
60 : : * in vars. For details, see DetTraceTrie::constructFormula below.
61 : : */
62 : : Node constructFormula(NodeManager* nm, const std::vector<Node>& vars);
63 : : /** Debug print this trace on trace message c */
64 : : void print(const char* c) const;
65 : :
66 : : private:
67 : : /**
68 : : * A trie of value vectors for the variables of a transition system. Nodes
69 : : * are stored as data in tries with no children at the leaves of this trie.
70 : : */
71 : : class DetTraceTrie
72 : : {
73 : : public:
74 : : /** the children of this trie */
75 : : std::map<Node, DetTraceTrie> d_children;
76 : : /** Add data loc to this trie, indexed by val. */
77 : : bool add(Node loc, const std::vector<Node>& val);
78 : : /** clear the trie */
79 : 630 : void clear() { d_children.clear(); }
80 : : /**
81 : : * Construct the formula corresponding to this trie with respect to
82 : : * variables in vars. For example, if we have indexed [1,2,3] and [2,3,4]
83 : : * and vars is [x,y,z], then this method returns:
84 : : * ( x=1 ^ y=2 ^ z=3 ) V ( x=2 ^ y=3 ^ z=4 ).
85 : : */
86 : : Node constructFormula(NodeManager* nm,
87 : : const std::vector<Node>& vars,
88 : : unsigned index = 0);
89 : : };
90 : : /** The above trie data structure for this class */
91 : : DetTraceTrie d_trie;
92 : : };
93 : :
94 : : /**
95 : : * Trace increment status, used for incrementTrace below.
96 : : */
97 : : enum TraceIncStatus
98 : : {
99 : : // the trace was successfully incremented to a new value
100 : : TRACE_INC_SUCCESS,
101 : : // the trace terminated
102 : : TRACE_INC_TERMINATE,
103 : : // the trace encountered a bad state (violating the post-condition)
104 : : TRACE_INC_CEX,
105 : : // the trace was invalid
106 : : TRACE_INC_INVALID
107 : : };
108 : :
109 : : /**
110 : : * This class is used for inferring that an arbitrary synthesis conjecture
111 : : * corresponds to an invariant synthesis problem for some predicate (d_func).
112 : : *
113 : : * The invariant-to-synthesize can either be explicitly given, via a call
114 : : * to initialize( f, vars ), or otherwise inferred if this method is not called.
115 : : */
116 : : class TransitionInference : protected EnvObj
117 : : {
118 : : public:
119 : 9087 : TransitionInference(Env& env) : EnvObj(env), d_complete(false) {}
120 : : /** Process the conjecture n
121 : : *
122 : : * This initializes this class with information related to viewing it as a
123 : : * transition system. This means we infer a function, the state variables,
124 : : * the pre/post condition and transition relation.
125 : : *
126 : : * The node n should be the inner body of the negated synthesis conjecture,
127 : : * prior to generating the deep embedding. That is, given:
128 : : * forall f. ~forall x. P( f, x ),
129 : : * this method expects n to be P( f, x ), and the argument f to be the
130 : : * function f above.
131 : : */
132 : : void process(Node n, Node f);
133 : : /**
134 : : * Same as above, without specifying f. This will try to infer a function f
135 : : * based on the body of n.
136 : : */
137 : : void process(Node n);
138 : : /**
139 : : * Get the function that is the subject of the synthesis problem we are
140 : : * analyzing.
141 : : */
142 : : Node getFunction() const;
143 : : /**
144 : : * Get the variables that the function is applied to. These are the free
145 : : * variables of the pre/post condition, and transition relation. These are
146 : : * fresh (Skolem) variables allocated by this class.
147 : : */
148 : : void getVariables(std::vector<Node>& vars) const;
149 : : /**
150 : : * Get the pre/post condition, or transition relation that was inferred by
151 : : * this class.
152 : : */
153 : : Node getPreCondition() const;
154 : : Node getPostCondition() const;
155 : : Node getTransitionRelation() const;
156 : : /**
157 : : * Was the analysis of the conjecture complete?
158 : : *
159 : : * If this is false, then the system we have inferred does not take into
160 : : * account all of the synthesis conjecture. This is the case when process(...)
161 : : * was called on formula that does not have the shape of a transition system.
162 : : */
163 : 2001 : bool isComplete() const { return d_complete; }
164 : : /**
165 : : * Was the analysis of the conjecture trivial? This is true if the function
166 : : * did not occur in the conjecture.
167 : : */
168 : 1135 : bool isTrivial() const { return d_trivial; }
169 : :
170 : : /**
171 : : * The following two functions are used for computing whether this transition
172 : : * relation is deterministic and terminating.
173 : : *
174 : : * The argument fwd is whether we are going in the forward direction of the
175 : : * transition system (starting from the precondition).
176 : : *
177 : : * If fwd is true, the initializeTrace method returns TRACE_INC_SUCCESS if the
178 : : * precondition consists of a single conjunct of the form
179 : : * ( x1 = t1 ^ ... ^ xn = tn )
180 : : * where x1...xn are the state variables of the transition system. Otherwise
181 : : * it returns TRACE_INC_INVALID.
182 : : */
183 : : TraceIncStatus initializeTrace(DetTrace& dt, bool fwd = true);
184 : : /**
185 : : * Increment the trace dt in direction fwd.
186 : : *
187 : : * If fwd is true, the incrementTrace method returns TRACE_INC_INVALID if the
188 : : * transition relation is not of the form
189 : : * ( x1' = t1[X] ^ ... ^ xn' = tn[X] ^ Q[X] ^ P(x1...xn) ) => P( x1'...xn' )
190 : : * Otherwise, it returns TRACE_INC_TERMINATE if the values of
191 : : * x1' = t1[dt.d_curr] ^ ... ^ xn' = tn[dt.d_curr] have already been executed
192 : : * on trace dt (the trace has looped), or if
193 : : * x1' = t1[dt.d_curr] ^ ... ^ xn' = tn[dt.d_curr] ^ Q[dt.d_curr] is unsat
194 : : * (the trace has terminated). It returns TRACE_INC_CEX if the postcondition
195 : : * is false for the values t1[dt.d_curr] ^ ... ^ tn[dt.d_curr]. Otherwise,
196 : : * it returns TRACE_INC_SUCCESS.
197 : : */
198 : : TraceIncStatus incrementTrace(DetTrace& dt, bool fwd = true);
199 : : /**
200 : : * Constructs the formula corresponding to trace dt with respect to the
201 : : * variables of this class.
202 : : */
203 : : Node constructFormulaTrace(DetTrace& dt) const;
204 : :
205 : : private:
206 : : /**
207 : : * The function (predicate) that is the subject of the invariant synthesis
208 : : * problem we are inferring.
209 : : */
210 : : Node d_func;
211 : : /** The variables that the function is applied to */
212 : : std::vector<Node> d_vars;
213 : : /**
214 : : * The variables that the function is applied to in the next state of the
215 : : * inferred transition relation.
216 : : */
217 : : std::vector<Node> d_prime_vars;
218 : : /**
219 : : * Was the analysis of the synthesis conjecture passed to the process method
220 : : * of this class complete?
221 : : */
222 : : bool d_complete;
223 : : /** Was the analyis trivial? */
224 : : bool d_trivial;
225 : :
226 : : /** process disjunct
227 : : *
228 : : * The purpose of this function is to infer pre/post/transition conditions
229 : : * for a (possibly unknown) invariant-to-synthesis, given a conjunct from
230 : : * an arbitrary synthesis conjecture.
231 : : *
232 : : * Assume our negated synthesis conjecture is of the form:
233 : : * forall f. exists x. (and (or F11 ... F1{m_1}) ... (or Fn1 ... Fn{m_n}))
234 : : * This method is called on each (or Fi1 ... Fi{m_i}), where topLevel is true
235 : : * for each of Fi1...F1{m_i} and false otherwise. It adds each of Fi1..Fi{m_i}
236 : : * to disjuncts.
237 : : *
238 : : * If this method returns true, then (1) all applications of free function
239 : : * symbols have operator d_func. Note this function may set d_func to a
240 : : * function symbol in n if d_func was null prior to this call. In other words,
241 : : * this method may infer the subject of the invariant synthesis problem;
242 : : * (2) all occurrences of d_func are "top-level", that is, each Fij may be
243 : : * of the form (not) <d_func>( tj ), but otherwise d_func does not occur in
244 : : * (or Fi1 ... Fi{m_i}); (3) there exists at most one occurrence of
245 : : * <d_func>( tj ), and (not <d_func>( tk )).
246 : : *
247 : : * If the above conditions are met, then terms[true] is set to <d_func>( tj )
248 : : * if Fij is <d_func>( tj ) for some j, and likewise terms[false]
249 : : * is set to <d_func>( tk ) if Fik is (not <d_func>( tk )) for some k.
250 : : *
251 : : * The argument visited caches the results of this function for (topLevel, n).
252 : : */
253 : : bool processDisjunct(Node n,
254 : : std::map<bool, Node>& terms,
255 : : std::vector<Node>& disjuncts,
256 : : std::map<bool, std::map<Node, bool> >& visited,
257 : : bool topLevel);
258 : : /**
259 : : * This method infers if the conjunction of disjuncts is equivalent to a
260 : : * conjunction of the form
261 : : * (~) const_var[1] = const_subs[1] ... (~) const_var[n] = const_subs[n]
262 : : * where the above equalities are negated iff reqPol is false, and
263 : : * const_var[1] ... const_var[n]
264 : : * are distinct members of vars
265 : : */
266 : : void getConstantSubstitution(const std::vector<Node>& vars,
267 : : const std::vector<Node>& disjuncts,
268 : : std::vector<Node>& const_var,
269 : : std::vector<Node>& const_subs,
270 : : bool reqPol);
271 : : /** get normalized substitution
272 : : *
273 : : * This method takes as input a node curr of the form I( t1, ..., tn ) and
274 : : * a vector of variables pvars, where pvars.size()=n. For each ti that is
275 : : * a variable, it adds ti to vars, and pvars[i] to subs. For each ti that is
276 : : * not a variable, it adds the disequality ti != pvars[i] to disjuncts.
277 : : *
278 : : * This function is used for instance to normalize an arbitrary application of
279 : : * I so that is over arguments pvars. For instance if curr is I(3,5,y) and
280 : : * pvars = { x1,x2,x3 }, then the formula:
281 : : * I(3,5,y) ^ P(y)
282 : : * is equivalent to:
283 : : * x1 != 3 V x2 != 5 V I(x1,x2,x3) V P( y ) { y -> x3 }
284 : : * Here, we add y and x3 to vars and subs respectively, and x1!=3 and x2!=5
285 : : * to disjuncts.
286 : : */
287 : : void getNormalizedSubstitution(Node curr,
288 : : const std::vector<Node>& pvars,
289 : : std::vector<Node>& vars,
290 : : std::vector<Node>& subs,
291 : : std::vector<Node>& disjuncts);
292 : : /**
293 : : * Stores one of the components of the inferred form of the synthesis
294 : : * conjecture (precondition, postcondition, or transition relation).
295 : : */
296 : : class Component
297 : : {
298 : : public:
299 : 27261 : Component() {}
300 : : /** The formula that was inferred for this component */
301 : : Node d_this;
302 : : /** The list of conjuncts of the above formula */
303 : : std::vector<Node> d_conjuncts;
304 : : /**
305 : : * Maps formulas to the constant equality substitution that it entails.
306 : : * For example, the formula (x=4 ^ y=x+5) may map to { x -> 4, y -> 9 }.
307 : : */
308 : : std::map<Node, std::map<Node, Node> > d_const_eq;
309 : : /** Does this component have conjunct c? */
310 : 666 : bool has(Node c) const
311 : : {
312 : 666 : return std::find(d_conjuncts.begin(), d_conjuncts.end(), c)
313 : 1332 : != d_conjuncts.end();
314 : : }
315 : : };
316 : : /** Components for the pre/post condition and transition relation. */
317 : : Component d_pre;
318 : : Component d_post;
319 : : Component d_trans;
320 : : /**
321 : : * Initialize trace dt, loc is a node to identify the trace, fwd is whether
322 : : * we are going in the forward direction of the transition system (starting
323 : : * from the precondition).
324 : : *
325 : : * The argument loc is a conjunct of transition relation that entails that the
326 : : * trace dt has executed in its last step to its current value. For example,
327 : : * if the transition relation is ( x'=x+1 ^ P( x ) ) => P(x'), and our trace's
328 : : * current value was last updated [x:=1] -> [x:=2] based on x'=x+1, then loc
329 : : * is the node x'=x+1.
330 : : */
331 : : TraceIncStatus initializeTrace(DetTrace& dt, Node loc, bool fwd = true);
332 : : /** Same as above, for incrementing the trace dt */
333 : : TraceIncStatus incrementTrace(DetTrace& dt, Node loc, bool fwd = true);
334 : : };
335 : :
336 : : } // namespace quantifiers
337 : : } // namespace theory
338 : : } // namespace cvc5::internal
339 : :
340 : : #endif
|
