Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Ying Sheng, Andrew Reynolds, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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/quantifiers_options.h"
25 : : #include "options/smt_options.h"
26 : : #include "smt/env.h"
27 : : #include "smt/set_defaults.h"
28 : : #include "theory/datatypes/sygus_datatype_utils.h"
29 : : #include "theory/quantifiers/quantifiers_attributes.h"
30 : : #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
31 : : #include "theory/quantifiers/sygus/sygus_utils.h"
32 : : #include "theory/smt_engine_subsolver.h"
33 : :
34 : : namespace cvc5::internal {
35 : : namespace theory {
36 : : namespace quantifiers {
37 : :
38 : 616 : SygusInterpol::SygusInterpol(Env& env) : EnvObj(env) {}
39 : :
40 : 616 : void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
41 : : const Node& conj)
42 : : {
43 [ + - ]: 616 : Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl;
44 : 1232 : std::unordered_set<Node> symSetAxioms;
45 : 616 : std::unordered_set<Node> symSetConj;
46 [ + + ]: 1234 : for (size_t i = 0, size = axioms.size(); i < size; i++)
47 : : {
48 : 618 : expr::getSymbols(axioms[i], symSetAxioms);
49 : : }
50 : 616 : expr::getSymbols(conj, symSetConj);
51 : 616 : d_syms.insert(d_syms.end(), symSetAxioms.begin(), symSetAxioms.end());
52 [ + + ]: 997 : for (const Node& elem : symSetConj)
53 : : {
54 [ + + ]: 381 : if (symSetAxioms.find(elem) != symSetAxioms.end())
55 : : {
56 : 193 : d_symSetShared.insert(elem);
57 : : }
58 : : else
59 : : {
60 : 188 : d_syms.push_back(elem);
61 : : }
62 : : }
63 [ + - ]: 1232 : Trace("sygus-interpol-debug")
64 : 0 : << "...finish, got " << d_syms.size() << " symbols in total. And "
65 : 616 : << d_symSetShared.size() << " shared symbols." << std::endl;
66 : 616 : }
67 : :
68 : 616 : void SygusInterpol::createVariables(bool needsShared)
69 : : {
70 : 616 : NodeManager* nm = nodeManager();
71 [ + + ]: 1414 : for (const Node& s : d_syms)
72 : : {
73 : 798 : TypeNode tn = s.getType();
74 [ + - ]: 1596 : if (tn.isDatatypeConstructor() || tn.isDatatypeSelector()
75 [ + - ][ + - ]: 1596 : || tn.isDatatypeTester() || tn.isDatatypeUpdater())
[ - + ][ - + ]
76 : : {
77 : : // datatype symbols should be considered interpreted symbols here, not
78 : : // (higher-order) variables.
79 : 0 : continue;
80 : : }
81 : : // Notice that we allow for non-first class (e.g. function) variables here.
82 : 1596 : std::stringstream ss;
83 : 798 : ss << s;
84 : 1596 : Node var = NodeManager::mkBoundVar(tn);
85 : 798 : d_vars.push_back(var);
86 : 1596 : Node vlv = NodeManager::mkBoundVar(ss.str(), tn);
87 : : // set that this variable encodes the term s
88 : : SygusVarToTermAttribute sta;
89 : 798 : vlv.setAttribute(sta, s);
90 : 798 : d_vlvs.push_back(vlv);
91 [ + + ][ + + ]: 798 : if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end())
[ + + ]
92 : : {
93 : 373 : d_varsShared.push_back(var);
94 : 373 : d_vlvsShared.push_back(vlv);
95 : 373 : d_varTypesShared.push_back(tn);
96 : : }
97 : : }
98 : : // make the sygus variable list
99 [ + + ]: 616 : if (!d_vlvsShared.empty())
100 : : {
101 : 274 : d_ibvlShared = nm->mkNode(Kind::BOUND_VAR_LIST, d_vlvsShared);
102 : : }
103 [ + - ]: 616 : Trace("sygus-interpol-debug") << "...finish" << std::endl;
104 : 616 : }
105 : :
106 : 2 : void SygusInterpol::getIncludeCons(
107 : : const std::vector<Node>& axioms,
108 : : const Node& conj,
109 : : std::map<TypeNode, std::unordered_set<Node>>& result)
110 : : {
111 : 2 : NodeManager* nm = nodeManager();
112 [ - + ][ - + ]: 2 : Assert(options().smt.produceInterpolants);
[ - - ]
113 : : // ASSUMPTIONS
114 [ + + ]: 2 : if (options().smt.interpolantsMode == options::InterpolantsMode::ASSUMPTIONS)
115 : : {
116 : : Node tmpAssumptions =
117 [ - + ]: 1 : (axioms.size() == 1 ? axioms[0] : nm->mkNode(Kind::AND, axioms));
118 : 1 : expr::getOperatorsMap(tmpAssumptions, result);
119 : : }
120 : : // CONJECTURE
121 : 1 : else if (options().smt.interpolantsMode
122 [ + - ]: 1 : == options::InterpolantsMode::CONJECTURE)
123 : : {
124 : 1 : expr::getOperatorsMap(conj, result);
125 : : }
126 : : // SHARED
127 [ - - ]: 0 : else if (options().smt.interpolantsMode == options::InterpolantsMode::SHARED)
128 : : {
129 : : // Get operators from axioms
130 : 0 : std::map<TypeNode, std::unordered_set<Node>> include_cons_axioms;
131 : : Node tmpAssumptions =
132 [ - - ]: 0 : (axioms.size() == 1 ? axioms[0] : nm->mkNode(Kind::AND, axioms));
133 : 0 : expr::getOperatorsMap(tmpAssumptions, include_cons_axioms);
134 : :
135 : : // Get operators from conj
136 : 0 : std::map<TypeNode, std::unordered_set<Node>> include_cons_conj;
137 : 0 : expr::getOperatorsMap(conj, include_cons_conj);
138 : :
139 : : // Compute intersection
140 : 0 : for (std::map<TypeNode, std::unordered_set<Node>>::iterator it =
141 : 0 : include_cons_axioms.begin();
142 [ - - ]: 0 : it != include_cons_axioms.end();
143 : 0 : it++)
144 : : {
145 : 0 : TypeNode tn = it->first;
146 : 0 : std::unordered_set<Node> axiomsOps = it->second;
147 : : std::map<TypeNode, std::unordered_set<Node>>::iterator concIter =
148 : 0 : include_cons_conj.find(tn);
149 [ - - ]: 0 : if (concIter != include_cons_conj.end())
150 : : {
151 : 0 : std::unordered_set<Node> conjOps = concIter->second;
152 [ - - ]: 0 : for (const Node& n : axiomsOps)
153 : : {
154 [ - - ]: 0 : if (conjOps.find(n) != conjOps.end())
155 : : {
156 [ - - ]: 0 : if (result.find(tn) == result.end())
157 : : {
158 : 0 : result[tn] = std::unordered_set<Node>();
159 : : }
160 : 0 : result[tn].insert(n);
161 : : }
162 : : }
163 : : }
164 : : }
165 : : }
166 : : // ALL
167 [ - - ]: 0 : else if (options().smt.interpolantsMode == options::InterpolantsMode::ALL)
168 : : {
169 : : Node tmpAssumptions =
170 [ - - ]: 0 : (axioms.size() == 1 ? axioms[0] : nm->mkNode(Kind::AND, axioms));
171 : 0 : Node tmpAll = nm->mkNode(Kind::AND, tmpAssumptions, conj);
172 : 0 : expr::getOperatorsMap(tmpAll, result);
173 : : }
174 : 2 : }
175 : :
176 : 616 : TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType,
177 : : const std::vector<Node>& axioms,
178 : : const Node& conj)
179 : : {
180 [ + - ]: 616 : Trace("sygus-interpol-debug") << "Setup grammar..." << std::endl;
181 : 616 : TypeNode itpGTypeS;
182 [ + + ]: 616 : if (!itpGType.isNull())
183 : : {
184 : : // set user-defined grammar
185 [ + - ][ + - ]: 680 : Assert(itpGType.isDatatype() && itpGType.getDType().isSygus());
[ - + ][ - - ]
186 : 680 : itpGTypeS = datatypes::utils::substituteAndGeneralizeSygusType(
187 : 680 : itpGType, d_syms, d_vlvs);
188 [ + - ][ + - ]: 680 : Assert(itpGTypeS.isDatatype() && itpGTypeS.getDType().isSygus());
[ - + ][ - - ]
189 : : // TODO(Ying Sheng) check if the vars in user-defined grammar, are
190 : : // consistent with the shared vars
191 : : }
192 [ + + ]: 276 : else if (options().smt.interpolantsMode != options::InterpolantsMode::DEFAULT)
193 : : {
194 : : // set default grammar, unless in DEFAULT mode, in which case we will
195 : : // provide no grammar in this module.
196 : 4 : TypeNode btype = nodeManager()->booleanType();
197 : : SygusGrammar g =
198 : 4 : SygusGrammarCons::mkDefaultGrammar(d_env, btype, d_ibvlShared);
199 : : // exclude rules that don't appear in operators
200 : 2 : std::map<TypeNode, std::unordered_set<Node>> include_cons;
201 : 2 : getIncludeCons(axioms, conj, include_cons);
202 : 2 : const std::vector<Node>& ntSyms = g.getNtSyms();
203 [ + + ]: 4 : for (const Node& ntSym : ntSyms)
204 : : {
205 : 2 : std::vector<Node> rules = g.getRulesFor(ntSym);
206 : 2 : TypeNode stype = ntSym.getType();
207 [ - + ]: 2 : if (include_cons.find(stype) == include_cons.end())
208 : : {
209 : 0 : continue;
210 : : }
211 : 2 : const std::unordered_set<Node>& icons = include_cons[stype];
212 [ + + ]: 6 : for (const Node& r : rules)
213 : : {
214 [ - + ][ - - ]: 4 : if (r.hasOperator() && icons.find(r.getOperator()) == icons.end())
[ - + ][ - + ]
[ - - ]
215 : : {
216 : 0 : g.removeRule(ntSym, r);
217 : : }
218 : : }
219 : : }
220 : 2 : itpGTypeS = g.resolve(true);
221 : : }
222 [ + - ]: 616 : Trace("sygus-interpol-debug") << "...finish setting up grammar" << std::endl;
223 : 616 : return itpGTypeS;
224 : : }
225 : :
226 : 616 : Node SygusInterpol::mkPredicate(const std::string& name)
227 : : {
228 : 616 : NodeManager* nm = nodeManager();
229 : : // make the interpolation predicate to synthesize
230 [ + - ]: 1232 : Trace("sygus-interpol-debug")
231 : 616 : << "Make interpolation predicate..." << std::endl;
232 : 616 : TypeNode itpType = d_varTypesShared.empty()
233 : : ? nm->booleanType()
234 [ + + ]: 1232 : : nm->mkPredicateType(d_varTypesShared);
235 : 1232 : Node itp = NodeManager::mkBoundVar(name.c_str(), itpType);
236 [ + - ]: 616 : Trace("sygus-interpol-debug") << "...finish" << std::endl;
237 : 1232 : return itp;
238 : : }
239 : :
240 : 616 : void SygusInterpol::mkSygusConjecture(Node itp,
241 : : const std::vector<Node>& axioms,
242 : : const Node& conj)
243 : : {
244 : 616 : NodeManager* nm = nodeManager();
245 : : // make the interpolation application to synthesize
246 [ + - ]: 1232 : Trace("sygus-interpol-debug")
247 : 616 : << "Make interpolation predicate app..." << std::endl;
248 : 1232 : std::vector<Node> ichildren;
249 : 616 : ichildren.push_back(itp);
250 : 616 : ichildren.insert(ichildren.end(), d_varsShared.begin(), d_varsShared.end());
251 : : Node itpApp =
252 [ + + ]: 1232 : d_varsShared.empty() ? itp : nm->mkNode(Kind::APPLY_UF, ichildren);
253 [ + - ]: 1232 : Trace("sygus-interpol-debug") << "itpApp: " << itpApp << std::endl
254 : 616 : << std::endl;
255 [ + - ]: 616 : Trace("sygus-interpol-debug") << "...finish" << std::endl;
256 : :
257 : : // set the sygus bound variable list
258 [ + - ]: 616 : Trace("sygus-interpol-debug") << "Set attributes..." << std::endl;
259 [ + + ]: 616 : if (!d_ibvlShared.isNull())
260 : : {
261 : 274 : SygusUtils::setSygusArgumentList(itp, d_ibvlShared);
262 : : }
263 [ + - ]: 616 : Trace("sygus-interpol-debug") << "...finish" << std::endl;
264 : :
265 : : // Fa( x )
266 [ + - ]: 616 : Trace("sygus-interpol-debug") << "Make conjecture body..." << std::endl;
267 : 1232 : Node Fa = nm->mkAnd(axioms);
268 : : // Fa( x ) => A( x )
269 : 1848 : Node firstImplication = nm->mkNode(Kind::IMPLIES, Fa, itpApp);
270 [ + - ]: 1232 : Trace("sygus-interpol-debug")
271 : 0 : << "first implication: " << firstImplication << std::endl
272 : 616 : << std::endl;
273 : : // A( x ) => Fc( x )
274 : 1232 : Node Fc = conj;
275 : 1848 : Node secondImplication = nm->mkNode(Kind::IMPLIES, itpApp, Fc);
276 [ + - ]: 1232 : Trace("sygus-interpol-debug")
277 : 0 : << "second implication: " << secondImplication << std::endl
278 : 616 : << std::endl;
279 : : // Fa( x ) => A( x ) ^ A( x ) => Fc( x )
280 : 1232 : Node constraint = nm->mkNode(Kind::AND, firstImplication, secondImplication);
281 : 1232 : constraint = constraint.substitute(
282 : 616 : d_syms.begin(), d_syms.end(), d_vars.begin(), d_vars.end());
283 [ + - ]: 616 : Trace("sygus-interpol-debug") << constraint << "...finish" << std::endl;
284 : 616 : constraint = rewrite(constraint);
285 : :
286 : 616 : d_sygusConj = constraint;
287 [ + - ]: 616 : Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
288 : 616 : }
289 : :
290 : 693 : bool SygusInterpol::findInterpol(SolverEngine* subSolver,
291 : : Node& interpol,
292 : : Node itp)
293 : : {
294 : : // get the synthesis solution
295 : 1386 : std::map<Node, Node> sols;
296 [ + + ]: 693 : if (!subSolver->getSynthSolutions(sols))
297 : : {
298 : 1 : return false;
299 : : }
300 [ - + ][ - + ]: 692 : Assert(sols.size() == 1);
[ - - ]
301 : 692 : std::map<Node, Node>::iterator its = sols.find(itp);
302 [ - + ]: 692 : if (its == sols.end())
303 : : {
304 [ - - ]: 0 : Trace("sygus-interpol")
305 : 0 : << "SolverEngine::getInterpol: could not find solution!" << std::endl;
306 : : throw RecoverableModalException(
307 : 0 : "Could not find solution for get-interpolant.");
308 : : return false;
309 : : }
310 [ + - ]: 1384 : Trace("sygus-interpol") << "SolverEngine::getInterpol: solution is "
311 : 692 : << its->second << std::endl;
312 : 692 : interpol = its->second;
313 : : // replace back the created variables to original symbols.
314 [ + + ]: 692 : if (interpol.getKind() == Kind::LAMBDA)
315 : : {
316 : 357 : interpol = interpol[1];
317 : : }
318 : :
319 : : // get the grammar type for the interpolant
320 : 1384 : Node igdtbv = SygusUtils::getOrMkSygusArgumentList(itp);
321 : : // could have no variables, in which case there is nothing to do
322 [ + + ]: 692 : if (igdtbv.isNull())
323 : : {
324 : 335 : return true;
325 : : }
326 [ - + ][ - + ]: 357 : Assert(igdtbv.getKind() == Kind::BOUND_VAR_LIST);
[ - - ]
327 : : // convert back to original
328 : : // must replace formal arguments of itp with the free variables in the
329 : : // input problem that they correspond to.
330 : 714 : std::vector<Node> vars;
331 : 357 : std::vector<Node> syms;
332 : : SygusVarToTermAttribute sta;
333 [ + + ]: 812 : for (const Node& bv : igdtbv)
334 : : {
335 : 455 : vars.push_back(bv);
336 [ + - ]: 455 : syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
337 : : }
338 : : interpol =
339 : 357 : interpol.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
340 : :
341 : 357 : return true;
342 : : }
343 : :
344 : 616 : bool SygusInterpol::solveInterpolation(const std::string& name,
345 : : const std::vector<Node>& axioms,
346 : : const Node& conj,
347 : : const TypeNode& itpGType,
348 : : Node& interpol)
349 : : {
350 : : // Some instructions in setSynthGrammar and mkSygusConjecture need a fully
351 : : // initialized solver to work properly. Notice, however, that the sub-solver
352 : : // created below is not fully initialized by the time those two methods are
353 : : // needed. Therefore, we call them while the current parent solver is in scope
354 : : // (i.e., before creating the sub-solver).
355 : 616 : collectSymbols(axioms, conj);
356 : 616 : createVariables(itpGType.isNull());
357 : 1232 : TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj);
358 : :
359 : 616 : d_itp = mkPredicate(name);
360 : 616 : mkSygusConjecture(d_itp, axioms, conj);
361 : :
362 : 1232 : Options subOptions;
363 : 616 : subOptions.copyValues(d_env.getOptions());
364 : 616 : subOptions.write_quantifiers().sygus = true;
365 : 616 : smt::SetDefaults::disableChecking(subOptions);
366 : 1232 : SubsolverSetupInfo ssi(d_env, subOptions);
367 : 616 : initializeSubsolver(d_subSolver, ssi);
368 : :
369 [ + + ]: 1414 : for (const Node& var : d_vars)
370 : : {
371 : 798 : d_subSolver->declareSygusVar(var);
372 : : }
373 : 1232 : std::vector<Node> vars_empty;
374 : 616 : d_subSolver->declareSynthFun(d_itp, grammarType, false, vars_empty);
375 [ + - ]: 1232 : Trace("sygus-interpol")
376 : 0 : << "SygusInterpol::solveInterpolation: made conjecture : " << d_sygusConj
377 : 616 : << std::endl;
378 : 616 : d_subSolver->assertSygusConstraint(d_sygusConj);
379 : :
380 [ + - ]: 1232 : Trace("sygus-interpol")
381 : 616 : << " SygusInterpol::solveInterpolation check synth..." << std::endl;
382 : 616 : SynthResult r = d_subSolver->checkSynth();
383 [ + - ]: 1232 : Trace("sygus-interpol") << " SygusInterpol::solveInterpolation result: " << r
384 : 616 : << std::endl;
385 [ + + ]: 616 : if (r.getStatus() == SynthResult::SOLUTION)
386 : : {
387 : 609 : return findInterpol(d_subSolver.get(), interpol, d_itp);
388 : : }
389 : 7 : return false;
390 : : }
391 : :
392 : 84 : bool SygusInterpol::solveInterpolationNext(Node& interpol)
393 : : {
394 [ + - ]: 168 : Trace("sygus-interpol")
395 : 84 : << " SygusInterpol::solveInterpolationNext check synth..." << std::endl;
396 : : // invoke the check-synth with isNext = true.
397 : 84 : SynthResult r = d_subSolver->checkSynth(true);
398 [ + - ]: 168 : Trace("sygus-interpol") << " SygusInterpol::solveInterpolationNext result: "
399 : 84 : << r << std::endl;
400 [ + - ]: 84 : if (r.getStatus() == SynthResult::SOLUTION)
401 : : {
402 : 84 : return findInterpol(d_subSolver.get(), interpol, d_itp);
403 : : }
404 : 0 : return false;
405 : : }
406 : :
407 : : } // namespace quantifiers
408 : : } // namespace theory
409 : : } // namespace cvc5::internal
|
