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