GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/transition_inference.h Lines: 12 12 100.0 %
Date: 2021-03-22 Branches: 4 8 50.0 %

Line Exec Source
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) 2009-2021 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.\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 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
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) 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
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