Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Abdalrhman Mohamed, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Class for verifying queries for synthesis solutions
14 : : */
15 : :
16 : : #include "theory/quantifiers/sygus/synth_verify.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "options/arith_options.h"
20 : : #include "options/base_options.h"
21 : : #include "options/datatypes_options.h"
22 : : #include "options/quantifiers_options.h"
23 : : #include "smt/set_defaults.h"
24 : : #include "theory/quantifiers/first_order_model.h"
25 : : #include "theory/quantifiers/sygus/term_database_sygus.h"
26 : : #include "theory/rewriter.h"
27 : : #include "theory/smt_engine_subsolver.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : : using namespace std;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace quantifiers {
35 : :
36 : 6664 : SynthVerify::SynthVerify(Env& env, TermDbSygus* tds)
37 : 6664 : : EnvObj(env), d_tds(tds), d_subLogicInfo(logicInfo())
38 : : {
39 : : // determine the options to use for the verification subsolvers we spawn
40 : : // we start with the provided options
41 : 6664 : d_subOptions.copyValues(options());
42 : : // limit the number of instantiation rounds on subcalls
43 : 13328 : d_subOptions.write_quantifiers().instMaxRounds =
44 : 6664 : d_subOptions.quantifiers.sygusVerifyInstMaxRounds;
45 : : // Disable sygus on the subsolver. This is particularly important since it
46 : : // ensures that recursive function definitions have the standard ownership
47 : : // instead of being claimed by sygus in the subsolver.
48 : 6664 : d_subOptions.write_base().inputLanguage = Language::LANG_SMTLIB_V2_6;
49 : 6664 : d_subOptions.write_quantifiers().sygus = false;
50 : : // use tangent planes by default, since we want to put effort into
51 : : // the verification step for sygus queries with non-linear arithmetic
52 [ + + ]: 6664 : if (!d_subOptions.arith.nlExtTangentPlanesWasSetByUser)
53 : : {
54 : 6652 : d_subOptions.write_arith().nlExtTangentPlanes = true;
55 : : }
56 : : // we must use the same setting for datatype selectors, since shared selectors
57 : : // can appear in solutions
58 : 13328 : d_subOptions.write_datatypes().dtSharedSelectors =
59 : 6664 : options().datatypes.dtSharedSelectors;
60 : 6664 : d_subOptions.write_datatypes().dtSharedSelectorsWasSetByUser = true;
61 : : // disable checking
62 : 6664 : smt::SetDefaults::disableChecking(d_subOptions);
63 : 6664 : }
64 : :
65 : 6518 : SynthVerify::~SynthVerify() {}
66 : :
67 : 5991 : Result SynthVerify::verify(Node query,
68 : : const std::vector<Node>& vars,
69 : : std::vector<Node>& mvs)
70 : : {
71 : 11982 : Node queryp = preprocessQueryInternal(query);
72 : : bool finished;
73 : 11982 : Result r;
74 : 0 : do
75 : : {
76 [ + - ]: 5991 : Trace("sygus-engine") << " *** Verify with subcall..." << std::endl;
77 [ + + ]: 5991 : if (queryp.isConst())
78 : : {
79 [ + + ]: 2626 : if (!queryp.getConst<bool>())
80 : : {
81 : 1231 : return Result(Result::UNSAT);
82 : : }
83 [ + + ]: 1395 : else if (vars.empty())
84 : : {
85 : 1365 : return Result(Result::SAT);
86 : : }
87 : : // sat, but we need to get arbtirary model values below
88 : : }
89 : 3395 : SubsolverSetupInfo ssi(d_subOptions,
90 : : d_subLogicInfo,
91 : 6790 : d_env.getSepLocType(),
92 : 10185 : d_env.getSepDataType());
93 : 6790 : r = checkWithSubsolver(queryp,
94 : : vars,
95 : : mvs,
96 : : ssi,
97 : 3395 : options().quantifiers.sygusVerifyTimeout != 0,
98 : 6790 : options().quantifiers.sygusVerifyTimeout);
99 : 3395 : finished = true;
100 [ + - ]: 3395 : Trace("sygus-engine") << " ...got " << r << std::endl;
101 : : // we try to learn models for "sat" and "unknown" here
102 [ + + ]: 3395 : if (r.getStatus() != Result::UNSAT)
103 : : {
104 [ - + ]: 2279 : if (TraceIsOn("sygus-engine"))
105 : : {
106 [ - - ]: 0 : Trace("sygus-engine") << " * Verification lemma failed for:\n ";
107 [ - - ]: 0 : for (unsigned i = 0, size = vars.size(); i < size; i++)
108 : : {
109 [ - - ]: 0 : Trace("sygus-engine") << vars[i] << " -> " << mvs[i] << " ";
110 : : }
111 [ - - ]: 0 : Trace("sygus-engine") << std::endl;
112 : : }
113 : : // check whether the query is satisfied by the model
114 [ + - ][ + - ]: 2279 : if (options().quantifiers.oracles || Configuration::isAssertionBuild())
[ + - ]
115 : : {
116 [ - + ][ - + ]: 2279 : Assert(vars.size() == mvs.size());
[ - - ]
117 : : // the values for the query should be a complete model
118 : : Node squery =
119 : 4558 : query.substitute(vars.begin(), vars.end(), mvs.begin(), mvs.end());
120 [ + - ]: 2279 : Trace("cegqi-debug") << "...squery : " << squery << std::endl;
121 : : // Rewrite the node. Notice that if squery contains oracle function
122 : : // symbols, then this may trigger new calls to oracles.
123 : 2279 : squery = d_tds->rewriteNode(squery);
124 [ + - ]: 2279 : Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
125 [ + + ][ + + ]: 2279 : if (!squery.isConst() || !squery.getConst<bool>())
[ + + ]
126 : : {
127 : : // If the query did not simplify to true, then it may be that the
128 : : // value for an oracle function was not what we expected.
129 [ - + ]: 1134 : if (options().quantifiers.oracles)
130 : : {
131 : : // In this case, we reconstruct the query, which may include more
132 : : // information about oracles than we had previously, due to the
133 : : // call to rewriteNode above. We rerun the satisfiability check
134 : : // above, which now may conjoin more I/O pairs to the preprocessed
135 : : // query.
136 : 0 : Node nextQueryp = preprocessQueryInternal(query);
137 [ - - ]: 0 : if (nextQueryp != queryp)
138 : : {
139 : 0 : queryp = nextQueryp;
140 : 0 : finished = false;
141 : : }
142 : : }
143 [ + + ]: 1134 : else if (squery.isConst())
144 : : {
145 : : // simplified to false, the result should have been unknown, or
146 : : // else this indicates a check-model failure. We check this only
147 : : // if oracles are disabled.
148 [ - + ][ - + ]: 114 : Assert(r.getStatus() == Result::UNKNOWN)
[ - - ]
149 : 0 : << "Expected model from verification step to satisfy query";
150 : : }
151 : : }
152 : : }
153 : : }
154 [ - + ]: 3395 : } while (!finished);
155 : 3395 : return r;
156 : : }
157 : :
158 : 1870 : Result SynthVerify::verify(Node query)
159 : : {
160 : 3740 : std::vector<Node> vars;
161 : 1870 : std::vector<Node> mvs;
162 : 3740 : return verify(query, vars, mvs);
163 : : }
164 : :
165 : 5991 : Node SynthVerify::preprocessQueryInternal(Node query)
166 : : {
167 : 5991 : NodeManager* nm = nodeManager();
168 [ + - ]: 5991 : Trace("cegqi-debug") << "pre-rewritten query : " << query << std::endl;
169 : : // simplify the lemma based on the term database sygus utility
170 : 5991 : query = d_tds->rewriteNode(query);
171 : : // eagerly unfold applications of evaluation function
172 [ + - ]: 5991 : Trace("cegqi-debug") << "post-rewritten query : " << query << std::endl;
173 [ + + ]: 5991 : if (!query.isConst())
174 : : {
175 : : // if non-constant, we may need to add recursive function definitions
176 : 3365 : FunDefEvaluator* feval = d_tds->getFunDefEvaluator();
177 : 3365 : OracleChecker* ochecker = d_env.getOracleChecker();
178 : 3365 : const std::vector<Node>& fdefs = feval->getDefinitions();
179 [ + + ][ - + ]: 3365 : if (!fdefs.empty() || (ochecker != nullptr && ochecker->hasOracles()))
[ - - ][ + + ]
180 : : {
181 : : // Get the relevant definitions based on the symbols in the query.
182 : : // Notice in some cases, this may have the effect of making the subcall
183 : : // involve no recursive function definitions at all, in which case the
184 : : // subcall to verification may be decidable, in which case the call
185 : : // below is guaranteed to generate a new counterexample point.
186 : 248 : std::unordered_set<Node> syms;
187 : 124 : expr::getSymbols(query, syms);
188 : 124 : std::vector<Node> qconj;
189 : 124 : qconj.push_back(query);
190 [ + + ]: 739 : for (const Node& f : syms)
191 : : {
192 : : // get the function definition
193 : 1230 : Node q = feval->getDefinitionFor(f);
194 [ + + ]: 615 : if (!q.isNull())
195 : : {
196 : 126 : qconj.push_back(q);
197 : : }
198 : : // Get the relevant cached oracle calls.
199 : : // In contrast to the presentation in Polgreen et al VMCAI 2022,
200 : : // we do not use SMTO as a subsolver for SyMO here. Instead, we
201 : : // conjoin the set of I/O pairs known about each oracle function
202 : : // to the query.
203 [ - + ][ - - ]: 615 : if (ochecker != nullptr && ochecker->hasOracleCalls(f))
[ - + ][ - + ]
[ - - ]
204 : : {
205 : : const std::map<Node, std::vector<Node>>& ocalls =
206 : 0 : ochecker->getOracleCalls(f);
207 [ - - ]: 0 : for (const std::pair<const Node, std::vector<Node>>& oc : ocalls)
208 : : {
209 : : // we ignore calls that had a size other than one
210 [ - - ]: 0 : if (oc.second.size() == 1)
211 : : {
212 : 0 : qconj.push_back(oc.first.eqNode(oc.second[0]));
213 : : }
214 : : }
215 : : }
216 : : }
217 : 124 : query = nm->mkAnd(qconj);
218 [ + - ]: 248 : Trace("cegqi-debug")
219 : 0 : << "after function definitions + oracle calls, query is " << query
220 : 124 : << std::endl;
221 : : }
222 : : }
223 : 5991 : return query;
224 : : }
225 : :
226 : : } // namespace quantifiers
227 : : } // namespace theory
228 : : } // namespace cvc5::internal
|
