1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Ying Sheng, Abdalrhman Mohamed, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of sygus interpolation utility, which transforms an input of |
14 |
|
* axioms and conjecture into an interpolation problem, and solve it. |
15 |
|
*/ |
16 |
|
|
17 |
|
#include "theory/quantifiers/sygus/sygus_interpol.h" |
18 |
|
|
19 |
|
#include <sstream> |
20 |
|
|
21 |
|
#include "base/modal_exception.h" |
22 |
|
#include "expr/dtype.h" |
23 |
|
#include "expr/node_algorithm.h" |
24 |
|
#include "options/smt_options.h" |
25 |
|
#include "smt/env.h" |
26 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
27 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
28 |
|
#include "theory/quantifiers/sygus/sygus_grammar_cons.h" |
29 |
|
#include "theory/smt_engine_subsolver.h" |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
namespace theory { |
33 |
|
namespace quantifiers { |
34 |
|
|
35 |
10 |
SygusInterpol::SygusInterpol(Env& env) : EnvObj(env) {} |
36 |
|
|
37 |
10 |
void SygusInterpol::collectSymbols(const std::vector<Node>& axioms, |
38 |
|
const Node& conj) |
39 |
|
{ |
40 |
10 |
Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl; |
41 |
20 |
std::unordered_set<Node> symSetAxioms; |
42 |
20 |
std::unordered_set<Node> symSetConj; |
43 |
35 |
for (size_t i = 0, size = axioms.size(); i < size; i++) |
44 |
|
{ |
45 |
25 |
expr::getSymbols(axioms[i], symSetAxioms); |
46 |
|
} |
47 |
10 |
expr::getSymbols(conj, symSetConj); |
48 |
10 |
d_syms.insert(d_syms.end(), symSetAxioms.begin(), symSetAxioms.end()); |
49 |
10 |
d_syms.insert(d_syms.end(), symSetConj.begin(), symSetConj.end()); |
50 |
36 |
for (const Node& elem : symSetConj) |
51 |
|
{ |
52 |
26 |
if (symSetAxioms.find(elem) != symSetAxioms.end()) |
53 |
|
{ |
54 |
16 |
d_symSetShared.insert(elem); |
55 |
|
} |
56 |
|
} |
57 |
20 |
Trace("sygus-interpol-debug") |
58 |
20 |
<< "...finish, got " << d_syms.size() << " symbols in total. And " |
59 |
10 |
<< d_symSetShared.size() << " shared symbols." << std::endl; |
60 |
10 |
} |
61 |
|
|
62 |
10 |
void SygusInterpol::createVariables(bool needsShared) |
63 |
|
{ |
64 |
10 |
NodeManager* nm = NodeManager::currentNM(); |
65 |
113 |
for (const Node& s : d_syms) |
66 |
|
{ |
67 |
206 |
TypeNode tn = s.getType(); |
68 |
103 |
if (tn.isConstructor() || tn.isSelector() || tn.isTester()) |
69 |
|
{ |
70 |
|
// datatype symbols should be considered interpreted symbols here, not |
71 |
|
// (higher-order) variables. |
72 |
|
continue; |
73 |
|
} |
74 |
|
// Notice that we allow for non-first class (e.g. function) variables here. |
75 |
206 |
std::stringstream ss; |
76 |
103 |
ss << s; |
77 |
206 |
Node var = nm->mkBoundVar(tn); |
78 |
103 |
d_vars.push_back(var); |
79 |
206 |
Node vlv = nm->mkBoundVar(ss.str(), tn); |
80 |
|
// set that this variable encodes the term s |
81 |
|
SygusVarToTermAttribute sta; |
82 |
103 |
vlv.setAttribute(sta, s); |
83 |
103 |
d_vlvs.push_back(vlv); |
84 |
103 |
if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end()) |
85 |
|
{ |
86 |
34 |
d_varsShared.push_back(var); |
87 |
34 |
d_vlvsShared.push_back(vlv); |
88 |
34 |
d_varTypesShared.push_back(tn); |
89 |
|
} |
90 |
|
} |
91 |
|
// make the sygus variable list |
92 |
10 |
d_ibvlShared = nm->mkNode(kind::BOUND_VAR_LIST, d_vlvsShared); |
93 |
10 |
Trace("sygus-interpol-debug") << "...finish" << std::endl; |
94 |
10 |
} |
95 |
|
|
96 |
9 |
void SygusInterpol::getIncludeCons( |
97 |
|
const std::vector<Node>& axioms, |
98 |
|
const Node& conj, |
99 |
|
std::map<TypeNode, std::unordered_set<Node>>& result) |
100 |
|
{ |
101 |
9 |
NodeManager* nm = NodeManager::currentNM(); |
102 |
9 |
Assert(options::produceInterpols() != options::ProduceInterpols::NONE); |
103 |
|
// ASSUMPTIONS |
104 |
9 |
if (options::produceInterpols() == options::ProduceInterpols::ASSUMPTIONS) |
105 |
|
{ |
106 |
|
Node tmpAssumptions = |
107 |
|
(axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); |
108 |
|
expr::getOperatorsMap(tmpAssumptions, result); |
109 |
|
} |
110 |
|
// CONJECTURE |
111 |
9 |
else if (options::produceInterpols() == options::ProduceInterpols::CONJECTURE) |
112 |
|
{ |
113 |
1 |
expr::getOperatorsMap(conj, result); |
114 |
|
} |
115 |
|
// SHARED |
116 |
8 |
else if (options::produceInterpols() == options::ProduceInterpols::SHARED) |
117 |
|
{ |
118 |
|
// Get operators from axioms |
119 |
|
std::map<TypeNode, std::unordered_set<Node>> include_cons_axioms; |
120 |
|
Node tmpAssumptions = |
121 |
|
(axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); |
122 |
|
expr::getOperatorsMap(tmpAssumptions, include_cons_axioms); |
123 |
|
|
124 |
|
// Get operators from conj |
125 |
|
std::map<TypeNode, std::unordered_set<Node>> include_cons_conj; |
126 |
|
expr::getOperatorsMap(conj, include_cons_conj); |
127 |
|
|
128 |
|
// Compute intersection |
129 |
|
for (std::map<TypeNode, std::unordered_set<Node>>::iterator it = |
130 |
|
include_cons_axioms.begin(); |
131 |
|
it != include_cons_axioms.end(); |
132 |
|
it++) |
133 |
|
{ |
134 |
|
TypeNode tn = it->first; |
135 |
|
std::unordered_set<Node> axiomsOps = it->second; |
136 |
|
std::map<TypeNode, std::unordered_set<Node>>::iterator concIter = |
137 |
|
include_cons_conj.find(tn); |
138 |
|
if (concIter != include_cons_conj.end()) |
139 |
|
{ |
140 |
|
std::unordered_set<Node> conjOps = concIter->second; |
141 |
|
for (const Node& n : axiomsOps) |
142 |
|
{ |
143 |
|
if (conjOps.find(n) != conjOps.end()) |
144 |
|
{ |
145 |
|
if (result.find(tn) == result.end()) |
146 |
|
{ |
147 |
|
result[tn] = std::unordered_set<Node>(); |
148 |
|
} |
149 |
|
result[tn].insert(n); |
150 |
|
} |
151 |
|
} |
152 |
|
} |
153 |
|
} |
154 |
|
} |
155 |
|
// ALL |
156 |
8 |
else if (options::produceInterpols() == options::ProduceInterpols::ALL) |
157 |
|
{ |
158 |
|
Node tmpAssumptions = |
159 |
|
(axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); |
160 |
|
Node tmpAll = nm->mkNode(kind::AND, tmpAssumptions, conj); |
161 |
|
expr::getOperatorsMap(tmpAll, result); |
162 |
|
} |
163 |
9 |
} |
164 |
|
|
165 |
10 |
TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType, |
166 |
|
const std::vector<Node>& axioms, |
167 |
|
const Node& conj) |
168 |
|
{ |
169 |
10 |
Trace("sygus-interpol-debug") << "Setup grammar..." << std::endl; |
170 |
10 |
TypeNode itpGTypeS; |
171 |
10 |
if (!itpGType.isNull()) |
172 |
|
{ |
173 |
|
// set user-defined grammar |
174 |
1 |
Assert(itpGType.isDatatype() && itpGType.getDType().isSygus()); |
175 |
1 |
itpGTypeS = datatypes::utils::substituteAndGeneralizeSygusType( |
176 |
|
itpGType, d_syms, d_vlvs); |
177 |
1 |
Assert(itpGTypeS.isDatatype() && itpGTypeS.getDType().isSygus()); |
178 |
|
// TODO(Ying Sheng) check if the vars in user-defined grammar, are |
179 |
|
// consistent with the shared vars |
180 |
|
} |
181 |
|
else |
182 |
|
{ |
183 |
|
// set default grammar |
184 |
18 |
std::map<TypeNode, std::unordered_set<Node>> extra_cons; |
185 |
18 |
std::map<TypeNode, std::unordered_set<Node>> exclude_cons; |
186 |
18 |
std::map<TypeNode, std::unordered_set<Node>> include_cons; |
187 |
9 |
getIncludeCons(axioms, conj, include_cons); |
188 |
18 |
std::unordered_set<Node> terms_irrelevant; |
189 |
27 |
itpGTypeS = CegGrammarConstructor::mkSygusDefaultType( |
190 |
18 |
NodeManager::currentNM()->booleanType(), |
191 |
|
d_ibvlShared, |
192 |
|
"interpolation_grammar", |
193 |
|
extra_cons, |
194 |
|
exclude_cons, |
195 |
|
include_cons, |
196 |
|
terms_irrelevant); |
197 |
|
} |
198 |
10 |
Trace("sygus-interpol-debug") << "...finish setting up grammar" << std::endl; |
199 |
10 |
return itpGTypeS; |
200 |
|
} |
201 |
|
|
202 |
10 |
Node SygusInterpol::mkPredicate(const std::string& name) |
203 |
|
{ |
204 |
10 |
NodeManager* nm = NodeManager::currentNM(); |
205 |
|
// make the interpolation predicate to synthesize |
206 |
20 |
Trace("sygus-interpol-debug") |
207 |
10 |
<< "Make interpolation predicate..." << std::endl; |
208 |
10 |
TypeNode itpType = d_varTypesShared.empty() |
209 |
|
? nm->booleanType() |
210 |
20 |
: nm->mkPredicateType(d_varTypesShared); |
211 |
10 |
Node itp = nm->mkBoundVar(name.c_str(), itpType); |
212 |
10 |
Trace("sygus-interpol-debug") << "...finish" << std::endl; |
213 |
20 |
return itp; |
214 |
|
} |
215 |
|
|
216 |
10 |
void SygusInterpol::mkSygusConjecture(Node itp, |
217 |
|
const std::vector<Node>& axioms, |
218 |
|
const Node& conj) |
219 |
|
{ |
220 |
10 |
NodeManager* nm = NodeManager::currentNM(); |
221 |
|
// make the interpolation application to synthesize |
222 |
20 |
Trace("sygus-interpol-debug") |
223 |
10 |
<< "Make interpolation predicate app..." << std::endl; |
224 |
20 |
std::vector<Node> ichildren; |
225 |
10 |
ichildren.push_back(itp); |
226 |
10 |
ichildren.insert(ichildren.end(), d_varsShared.begin(), d_varsShared.end()); |
227 |
|
Node itpApp = |
228 |
20 |
d_varsShared.empty() ? itp : nm->mkNode(kind::APPLY_UF, ichildren); |
229 |
20 |
Trace("sygus-interpol-debug") << "itpApp: " << itpApp << std::endl |
230 |
10 |
<< std::endl; |
231 |
10 |
Trace("sygus-interpol-debug") << "...finish" << std::endl; |
232 |
|
|
233 |
|
// set the sygus bound variable list |
234 |
10 |
Trace("sygus-interpol-debug") << "Set attributes..." << std::endl; |
235 |
10 |
itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared); |
236 |
10 |
Trace("sygus-interpol-debug") << "...finish" << std::endl; |
237 |
|
|
238 |
|
// Fa( x ) |
239 |
10 |
Trace("sygus-interpol-debug") << "Make conjecture body..." << std::endl; |
240 |
20 |
Node Fa = axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms); |
241 |
|
// Fa( x ) => A( x ) |
242 |
20 |
Node firstImplication = nm->mkNode(kind::IMPLIES, Fa, itpApp); |
243 |
20 |
Trace("sygus-interpol-debug") |
244 |
10 |
<< "first implication: " << firstImplication << std::endl |
245 |
10 |
<< std::endl; |
246 |
|
// A( x ) => Fc( x ) |
247 |
20 |
Node Fc = conj; |
248 |
20 |
Node secondImplication = nm->mkNode(kind::IMPLIES, itpApp, Fc); |
249 |
20 |
Trace("sygus-interpol-debug") |
250 |
10 |
<< "second implication: " << secondImplication << std::endl |
251 |
10 |
<< std::endl; |
252 |
|
// Fa( x ) => A( x ) ^ A( x ) => Fc( x ) |
253 |
20 |
Node constraint = nm->mkNode(kind::AND, firstImplication, secondImplication); |
254 |
10 |
constraint = constraint.substitute( |
255 |
|
d_syms.begin(), d_syms.end(), d_vars.begin(), d_vars.end()); |
256 |
10 |
Trace("sygus-interpol-debug") << constraint << "...finish" << std::endl; |
257 |
10 |
constraint = rewrite(constraint); |
258 |
|
|
259 |
10 |
d_sygusConj = constraint; |
260 |
10 |
Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl; |
261 |
10 |
} |
262 |
|
|
263 |
10 |
bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp) |
264 |
|
{ |
265 |
|
// get the synthesis solution |
266 |
20 |
std::map<Node, Node> sols; |
267 |
10 |
subSolver->getSynthSolutions(sols); |
268 |
10 |
Assert(sols.size() == 1); |
269 |
10 |
std::map<Node, Node>::iterator its = sols.find(itp); |
270 |
10 |
if (its == sols.end()) |
271 |
|
{ |
272 |
|
Trace("sygus-interpol") |
273 |
|
<< "SmtEngine::getInterpol: could not find solution!" << std::endl; |
274 |
|
throw RecoverableModalException( |
275 |
|
"Could not find solution for get-interpol."); |
276 |
|
return false; |
277 |
|
} |
278 |
20 |
Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is " |
279 |
10 |
<< its->second << std::endl; |
280 |
10 |
interpol = its->second; |
281 |
|
// replace back the created variables to original symbols. |
282 |
10 |
if (interpol.getKind() == kind::LAMBDA) |
283 |
|
{ |
284 |
10 |
interpol = interpol[1]; |
285 |
|
} |
286 |
|
|
287 |
|
// get the grammar type for the interpolant |
288 |
20 |
Node igdtbv = itp.getAttribute(SygusSynthFunVarListAttribute()); |
289 |
10 |
Assert(!igdtbv.isNull()); |
290 |
10 |
Assert(igdtbv.getKind() == kind::BOUND_VAR_LIST); |
291 |
|
// convert back to original |
292 |
|
// must replace formal arguments of itp with the free variables in the |
293 |
|
// input problem that they correspond to. |
294 |
20 |
std::vector<Node> vars; |
295 |
20 |
std::vector<Node> syms; |
296 |
|
SygusVarToTermAttribute sta; |
297 |
44 |
for (const Node& bv : igdtbv) |
298 |
|
{ |
299 |
34 |
vars.push_back(bv); |
300 |
34 |
syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv); |
301 |
|
} |
302 |
10 |
interpol = |
303 |
20 |
interpol.substitute(vars.begin(), vars.end(), syms.begin(), syms.end()); |
304 |
|
|
305 |
10 |
return true; |
306 |
|
} |
307 |
|
|
308 |
10 |
bool SygusInterpol::solveInterpolation(const std::string& name, |
309 |
|
const std::vector<Node>& axioms, |
310 |
|
const Node& conj, |
311 |
|
const TypeNode& itpGType, |
312 |
|
Node& interpol) |
313 |
|
{ |
314 |
|
// Some instructions in setSynthGrammar and mkSygusConjecture need a fully |
315 |
|
// initialized solver to work properly. Notice, however, that the sub-solver |
316 |
|
// created below is not fully initialized by the time those two methods are |
317 |
|
// needed. Therefore, we call them while the current parent solver is in scope |
318 |
|
// (i.e., before creating the sub-solver). |
319 |
10 |
collectSymbols(axioms, conj); |
320 |
10 |
createVariables(itpGType.isNull()); |
321 |
20 |
TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj); |
322 |
|
|
323 |
20 |
Node itp = mkPredicate(name); |
324 |
10 |
mkSygusConjecture(itp, axioms, conj); |
325 |
|
|
326 |
20 |
std::unique_ptr<SmtEngine> subSolver; |
327 |
10 |
initializeSubsolver(subSolver, d_env); |
328 |
|
// get the logic |
329 |
20 |
LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy(); |
330 |
|
// enable everything needed for sygus |
331 |
10 |
l.enableSygus(); |
332 |
10 |
subSolver->setLogic(l); |
333 |
|
|
334 |
113 |
for (const Node& var : d_vars) |
335 |
|
{ |
336 |
103 |
subSolver->declareSygusVar(var); |
337 |
|
} |
338 |
20 |
std::vector<Node> vars_empty; |
339 |
10 |
subSolver->declareSynthFun(itp, grammarType, false, vars_empty); |
340 |
20 |
Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : " |
341 |
10 |
<< d_sygusConj << ", solving for " |
342 |
10 |
<< d_sygusConj[0][0] << std::endl; |
343 |
10 |
subSolver->assertSygusConstraint(d_sygusConj); |
344 |
|
|
345 |
20 |
Trace("sygus-interpol") << " SmtEngine::getInterpol check sat..." |
346 |
10 |
<< std::endl; |
347 |
20 |
Result r = subSolver->checkSynth(); |
348 |
20 |
Trace("sygus-interpol") << " SmtEngine::getInterpol result: " << r |
349 |
10 |
<< std::endl; |
350 |
10 |
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) |
351 |
|
{ |
352 |
10 |
return findInterpol(subSolver.get(), interpol, itp); |
353 |
|
} |
354 |
|
return false; |
355 |
|
} |
356 |
|
|
357 |
|
} // namespace quantifiers |
358 |
|
} // namespace theory |
359 |
29574 |
} // namespace cvc5 |