GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_eval_unfold.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_eval_unfold.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 sygus_eval_unfold
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
19
20
#include <map>
21
#include "expr/node.h"
22
#include "theory/quantifiers/sygus/sygus_invariance.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
class TermDbSygus;
29
30
/** SygusEvalUnfold
31
 *
32
 * This class implements techniques for eagerly unfolding sygus evaluation
33
 * functions. For example, given sygus datatype type corresponding to grammar:
34
 *   A -> 0 | 1 | A+A
35
 * whose evaluation function is eval, this class adds lemmas that "eagerly
36
 * unfold" applications of eval based on the model values of evaluation heads
37
 * in refinement lemmas.
38
 */
39
class SygusEvalUnfold
40
{
41
 public:
42
  SygusEvalUnfold(TermDbSygus* tds);
43
2188
  ~SygusEvalUnfold() {}
44
  /** register evaluation term
45
   *
46
   * This is called by TermDatabase, during standard effort calls when a term
47
   * n is registered as an equivalence class in the master equality engine.
48
   * If this term is of the form:
49
   *   eval( a, t1, ..., tn )
50
   * where a is a symbolic term of sygus datatype type (not a application of a
51
   * constructor), then we remember that n is an evaluation function application
52
   * for evaluation head a.
53
   */
54
  void registerEvalTerm(Node n);
55
  /** register model value
56
   *
57
   * This notifies this class that the model value M(a) of an anchor term a is
58
   * currently v. Assume in the following that the top symbol of v is some sygus
59
   * datatype constructor C_op.
60
   *
61
   * If we have registered terms eval( a, T1 ), ..., eval( a, Tm ), then we
62
   * ensure that for each i=1,...,m, a lemma of one of the two forms is
63
   * generated:
64
   * [A] a=v => eval( a, Ti ) = [[unfold( eval( v, Ti ) )]]
65
   * [B] is-C_op(v) => eval(a, Ti ) = op(eval( a.1, Ti ), ..., eval( a.k, Ti )),
66
   * where this corresponds to a "one step folding" of the sygus evaluation
67
   * function, i.e. op is a builtin operator encoded by constructor C_op.
68
   *
69
   * We decide which kind of lemma to send ([A] or [B]) based on the symbol
70
   * C_op. If op is an ITE, or if C_op is a Boolean operator, then we add [B].
71
   * Otherwise, we add [A]. The intuition of why [B] is better than [A] for the
72
   * former is that evaluation unfolding can lead to useful conflict analysis.
73
   *
74
   * For each lemma C => eval( a, T ) = T' we infer is necessary, we add C to
75
   * exps, eval( a, T ) to terms, and T' to vals. The caller should send the
76
   * corresponding lemma on the output channel.
77
   *
78
   * We do the above scheme *for each* selector chain (see d_subterms below)
79
   * applied to a.
80
   */
81
  void registerModelValue(Node a,
82
                          Node v,
83
                          std::vector<Node>& exps,
84
                          std::vector<Node>& terms,
85
                          std::vector<Node>& vals);
86
  /** unfold
87
   *
88
   * This method is called when a sygus term d (typically a variable for a SyGuS
89
   * enumerator) has a model value specified by the map vtm. The argument en
90
   * is an application of kind DT_SYGUS_EVAL, i.e. eval( d, c1, ..., cm ).
91
   * Typically, d is a shared selector chain, although it may also be a
92
   * non-constant application of a constructor.
93
   *
94
   * If doRec is false, this method returns the one-step unfolding of this
95
   * evaluation function application. An example of a one step unfolding is:
96
   *    eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) )
97
   *
98
   * This function does this unfolding for a (possibly symbolic) evaluation
99
   * head, where the argument "variable to model" vtm stores the model value of
100
   * variables from this head. This allows us to track an explanation of the
101
   * unfolding in the vector exp when track_exp is true.
102
   *
103
   * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then
104
   * this method applied to eval( d, t ) will return
105
   * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp.
106
   *
107
   * If the argument doRec is true, we do a multi-step unfolding instead of
108
   * a single-step unfolding. For example, if vtm[d] = C_+( C_x(), C_0() ),
109
   * then this method applied to eval(d,5) will return 5+0 = 0.
110
   *
111
   * Furthermore, notice that any-constant constructors are *never* expanded to
112
   * their concrete model values. This means that the multi-step unfolding when
113
   * vtm[d] = C_+( C_x(), any_constant(n) ), then this method applied to
114
   * eval(d,5) will return 5 + d.2.1, where the latter term is a shared selector
115
   * chain. In other words, this unfolding elaborates the connection between
116
   * the builtin integer field d.2.1 of d and the builtin interpretation of
117
   * this sygus term, for the given argument.
118
   */
119
  Node unfold(Node en,
120
              std::map<Node, Node>& vtm,
121
              std::vector<Node>& exp,
122
              bool track_exp = true,
123
              bool doRec = false);
124
  /**
125
   * Same as above, but without explanation tracking. This is used for concrete
126
   * evaluation heads
127
   */
128
  Node unfold(Node en);
129
130
 private:
131
  /** sygus term database associated with this utility */
132
  TermDbSygus* d_tds;
133
  /** the set of evaluation terms we have already processed */
134
  std::unordered_set<Node, NodeHashFunction> d_eval_processed;
135
  /** map from evaluation heads to evaluation function applications */
136
  std::map<Node, std::vector<Node> > d_evals;
137
  /**
138
   * Map from evaluation function applications to their arguments (minus the
139
   * evaluation head). For example, eval(x,0,1) is mapped to { 0, 1 }.
140
   */
141
  std::map<Node, std::vector<std::vector<Node> > > d_eval_args;
142
  /**
143
   * For each (a,M(a)) pair, the number of terms in d_evals that we have added
144
   * lemmas for
145
   */
146
  std::map<Node, std::map<Node, unsigned> > d_node_mv_args_proc;
147
  /** subterms map
148
   *
149
   * This maps anchor terms to the set of shared selector chains with
150
   * them as an anchor, for example x may map to { x, x.1, x.2, x.1.1 }.
151
   */
152
  std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_subterms;
153
};
154
155
}  // namespace quantifiers
156
}  // namespace theory
157
}  // namespace CVC4
158
159
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */