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

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_interpol.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Ying Sheng, Abdalrhman Mohamed
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 interpolation utility, which transforms an input of axioms and
13
 ** conjecture into an interpolation problem, and solve it.
14
 **/
15
16
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
17
#define CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
18
19
#include <string>
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "expr/type_node.h"
24
#include "smt/smt_engine.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
/**
30
 * This is an utility for the SMT-LIB command (get-interpol <term>).
31
 * The utility turns a set of quantifier-free assertions into a sygus
32
 * conjecture that encodes an interpolation problem, and then solve the
33
 * interpolation problem by synthesizing it. In detail, if our input formula is
34
 * F( x ) for free symbol x, and is partitioned into axioms Fa and conjecture Fc
35
 * then the sygus conjecture we construct is:
36
 *
37
 * (Fa( x ) => A( x )) ^ (A( x ) => Fc( x ))
38
 *
39
 * where A( x ) is a predicate over the free symbols of our input that are
40
 * shared between Fa and Fc. In other words, A( x ) must be implied by our
41
 * axioms Fa( x ) and implies Fc( x ). Then, to solve the interpolation problem,
42
 * we just need to synthesis A( x ).
43
 *
44
 * This class uses a fresh copy of the SMT engine which is used for solving the
45
 * interpolation problem. In particular, consider the input: (assert A)
46
 *   (get-interpol s B)
47
 * In the copy of the SMT engine where these commands are issued, we maintain
48
 * A in the assertion stack. In solving the interpolation problem, we will
49
 * need to call a SMT engine solver with a different assertion stack, which is
50
 * a sygus conjecture build from A and B. Then to solve the interpolation
51
 * problem, instead of modifying the assertion stack to remove A and add the
52
 * sygus conjecture (exists I. ...), we invoke a fresh copy of the SMT engine
53
 * and leave the original assertion stack unchanged. This copy of the SMT
54
 * engine will have the assertion stack with the sygus conjecture. This copy
55
 * of the SMT engine can be further queried for information regarding further
56
 * solutions.
57
 */
58
10
class SygusInterpol
59
{
60
 public:
61
  SygusInterpol();
62
63
  /**
64
   * Returns the sygus conjecture in interpol corresponding to the interpolation
65
   * problem for input problem (F above) given by axioms (Fa above), and conj
66
   * (Fc above). And solve the interpolation by sygus. Note that axioms is
67
   * expected to be a subset of assertions in SMT-LIB.
68
   *
69
   * @param name the name for the interpol-to-synthesize.
70
   * @param axioms the assertions (Fa above)
71
   * @param conj the conjecture (Fc above)
72
   * @param itpGType (if non-null) a sygus datatype type that encodes the
73
   * grammar that should be used for solutions of the interpolation conjecture.
74
   * @interpol the solution to the sygus conjecture.
75
   */
76
  bool solveInterpolation(const std::string& name,
77
                          const std::vector<Node>& axioms,
78
                          const Node& conj,
79
                          const TypeNode& itpGType,
80
                          Node& interpol);
81
82
 private:
83
  /**
84
   * Collects symbols from axioms (axioms) and conjecture (conj), which are
85
   * stored in d_syms, and computes the shared symbols between axioms and
86
   * conjecture, stored in d_symSetShared.
87
   *
88
   * @param axioms the assertions (Fa above)
89
   * @param conj the conjecture (Fc above)
90
   */
91
  void collectSymbols(const std::vector<Node>& axioms, const Node& conj);
92
93
  /**
94
   * Creates free variables and shared free variables from d_syms and
95
   * d_symSetShared, which are stored in d_vars and d_varsShared. And also
96
   * creates the corresponding set of variables for the formal argument list,
97
   * which is stored in d_vlvs and d_vlvsShared. Extracts the types of shared
98
   * variables, which are stored in d_varTypesShared. Creates the formal
99
   * argument list of the interpol-to-synthese, stored in d_ibvlShared.
100
   *
101
   * When using default grammar, the needsShared is true. When using
102
   * user-defined gramar, the needsShared is false.
103
   *
104
   * @param needsShared If it is true, the argument list of the
105
   * interpol-to-synthesis will be restricted to be over shared variables. If it
106
   * is false, the argument list will be over all the variables.
107
   */
108
  void createVariables(bool needsShared);
109
110
  /**
111
   * Get include_cons for mkSygusDefaultType.
112
   * mkSygusDefaultType() is a function to make default grammar. It has an
113
   * arguemnt include_cons, which will restrict what operators we want in the
114
   * grammar. The return value depends on options::produceInterpols(). In
115
   * ASSUMPTIONS option, it will return the operators from axioms. In CONJECTURE
116
   * option, it will return the operators from conj. In SHARED option, it will
117
   * return the oprators shared by axioms and conj. In ALL option, it will
118
   * return the operators from either axioms or conj.
119
   *
120
   * @param axioms input argument
121
   * @param conj input argument
122
   * @param result the return value
123
   */
124
  void getIncludeCons(
125
      const std::vector<Node>& axioms,
126
      const Node& conj,
127
      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result);
128
129
  /**
130
   * Set up the grammar for the interpol-to-synthesis.
131
   *
132
   * The user-defined grammar will be encoded by itpGType. The options for
133
   * grammar is given by options::produceInterpols(). In DEFAULT option, it will
134
   * set up the grammar from itpGType. And if itpGType is null, it will set up
135
   * the default grammar, which is built according to a policy handled by
136
   * getIncludeCons().
137
   *
138
   * @param itpGType (if non-null) a sygus datatype type that encodes the
139
   * grammar that should be used for solutions of the interpolation conjecture.
140
   * @param axioms the assertions (Fa above)
141
   * @param conj the conjecture (Fc above)
142
   */
143
  TypeNode setSynthGrammar(const TypeNode& itpGType,
144
                           const std::vector<Node>& axioms,
145
                           const Node& conj);
146
147
  /**
148
   * Make the interpolation predicate.
149
   *
150
   * @param name the name of the interpol-to-synthesis.
151
   */
152
  Node mkPredicate(const std::string& name);
153
154
  /**
155
   * Make the sygus conjecture to be synthesis.
156
   * The conjecture body is Fa( x ) => A( x ) ^ A( x ) => Fc( x ) as described
157
   * above.
158
   *
159
   * @param itp the interpolation predicate.
160
   * @param axioms the assertions (Fa above)
161
   * @param conj the conjecture (Fc above)
162
   */
163
  void mkSygusConjecture(Node itp,
164
                         const std::vector<Node>& axioms,
165
                         const Node& conj);
166
167
  /**
168
   * Get the synthesis solution, stored in interpol.
169
   *
170
   * @param interpol the solution to the sygus conjecture.
171
   * @param itp the interpolation predicate.
172
   */
173
  bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);
174
175
  /**
176
   * symbols from axioms and conjecture.
177
   */
178
  std::vector<Node> d_syms;
179
  /**
180
   * unordered set for shared symbols between axioms and conjecture.
181
   */
182
  std::unordered_set<Node, NodeHashFunction> d_symSetShared;
183
  /**
184
   * free variables created from d_syms.
185
   */
186
  std::vector<Node> d_vars;
187
  /**
188
   * variables created from d_syms for formal argument list.
189
   */
190
  std::vector<Node> d_vlvs;
191
  /**
192
   * free variables created from d_symSetShared.
193
   */
194
  std::vector<Node> d_varsShared;
195
  /**
196
   * variables created from d_symShared for formal argument list.
197
   */
198
  std::vector<Node> d_vlvsShared;
199
  /**
200
   * types of shared variables between axioms and conjecture.
201
   */
202
  std::vector<TypeNode> d_varTypesShared;
203
  /**
204
   * formal argument list of the interpol-to-synthesis.
205
   */
206
  Node d_ibvlShared;
207
208
  /**
209
   * the sygus conjecture to synthesis for interpolation problem
210
   */
211
  Node d_sygusConj;
212
};
213
214
}  // namespace quantifiers
215
}  // namespace theory
216
}  // namespace CVC4
217
218
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */