1 

/********************* */ 
2 

/*! \file transition_inference.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief Utility for inferring whether a synthesis conjecture encodes a 
13 

** transition system. 
14 

**/ 
15 


16 

#include "cvc4_private.h" 
17 


18 

#ifndef CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H 
19 

#define CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H 
20 


21 

#include <map> 
22 

#include <vector> 
23 


24 

#include "expr/node.h" 
25 


26 

#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" 
27 

#include "theory/quantifiers/inst_match_trie.h" 
28 

#include "theory/quantifiers/single_inv_partition.h" 
29 


30 

namespace CVC4 { 
31 

namespace theory { 
32 

namespace quantifiers { 
33 


34 

/** 
35 

* Utility for storing a deterministic trace of a transition system. A trace 
36 

* is stored as a collection of vectors of values that have been taken by 
37 

* the variables of transition system. For example, say we have a transition 
38 

* system with variables x,y,z. Say the precondition constrains these variables 
39 

* to x=1,y=2,z=3, and say that the transition relation admits the single 
40 

* trace: [1,2,3], [2,3,4], [3,4,5]. We store these three vectors of variables 
41 

* in the trie within this class. 
42 

* 
43 

* This utility is used for determining whether a transition system has a 
44 

* deterministic terminating trace and hence a trivial invariant. 
45 

*/ 
46 
94 
class DetTrace 
47 

{ 
48 

public: 
49 

/** The current value of the trace */ 
50 

std::vector<Node> d_curr; 
51 

/** 
52 

* Increment the trace: index the current values, if successful (they are 
53 

* not a duplicate of a previous value), update the current values to vals. 
54 

* Returns true if the increment was successful. 
55 

*/ 
56 

bool increment(Node loc, std::vector<Node>& vals); 
57 

/** 
58 

* Construct the formula that this trace represents with respect to variables 
59 

* in vars. For details, see DetTraceTrie::constructFormula below. 
60 

*/ 
61 

Node constructFormula(const std::vector<Node>& vars); 
62 

/** Debug print this trace on trace message c */ 
63 

void print(const char* c) const; 
64 


65 

private: 
66 

/** 
67 

* A trie of value vectors for the variables of a transition system. Nodes 
68 

* are stored as data in tries with no children at the leaves of this trie. 
69 

*/ 
70 
3270 
class DetTraceTrie 
71 

{ 
72 

public: 
73 

/** the children of this trie */ 
74 

std::map<Node, DetTraceTrie> d_children; 
75 

/** Add data loc to this trie, indexed by val. */ 
76 

bool add(Node loc, const std::vector<Node>& val); 
77 

/** clear the trie */ 
78 
534 
void clear() { d_children.clear(); } 
79 

/** 
80 

* Construct the formula corresponding to this trie with respect to 
81 

* variables in vars. For example, if we have indexed [1,2,3] and [2,3,4] 
82 

* and vars is [x,y,z], then this method returns: 
83 

* ( x=1 ^ y=2 ^ z=3 ) V ( x=2 ^ y=3 ^ z=4 ). 
84 

*/ 
85 

Node constructFormula(const std::vector<Node>& vars, 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 postcondition) 
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 invarianttosynthesize can either be explicitly given, via a call 
111 

* to initialize( f, vars ), or otherwise inferred if this method is not called. 
112 

*/ 
113 
2206 
class TransitionInference 
114 

{ 
115 

public: 
116 
2208 
TransitionInference() : 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 
119 
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 
10 
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) invarianttosynthesis, 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 "toplevel", 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 
6618 
class Component 
294 

{ 
295 

public: 
296 
6624 
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 
574 
bool has(Node c) const 
308 

{ 
309 
1148 
return std::find(d_conjuncts.begin(), d_conjuncts.end(), c) 
310 
1722 
!= 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 CVC4 */ 
336 


337 

#endif 