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