Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Oracle engine
11 : : */
12 : :
13 : : #include "theory/quantifiers/oracle_engine.h"
14 : :
15 : : #include "expr/attribute.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "options/quantifiers_options.h"
18 : : #include "theory/decision_manager.h"
19 : : #include "theory/quantifiers/first_order_model.h"
20 : : #include "theory/quantifiers/quantifiers_attributes.h"
21 : : #include "theory/quantifiers/quantifiers_inference_manager.h"
22 : : #include "theory/quantifiers/quantifiers_registry.h"
23 : : #include "theory/quantifiers/term_registry.h"
24 : : #include "theory/quantifiers/term_tuple_enumerator.h"
25 : : #include "theory/trust_substitutions.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : : using namespace cvc5::context;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace quantifiers {
33 : :
34 : : /** Attribute true for input variables */
35 : : struct OracleInputVarAttributeId
36 : : {
37 : : };
38 : : typedef expr::Attribute<OracleInputVarAttributeId, bool>
39 : : OracleInputVarAttribute;
40 : : /** Attribute true for output variables */
41 : : struct OracleOutputVarAttributeId
42 : : {
43 : : };
44 : : typedef expr::Attribute<OracleOutputVarAttributeId, bool>
45 : : OracleOutputVarAttribute;
46 : :
47 : 535 : OracleEngine::OracleEngine(Env& env,
48 : : QuantifiersState& qs,
49 : : QuantifiersInferenceManager& qim,
50 : : QuantifiersRegistry& qr,
51 : 535 : TermRegistry& tr)
52 : : : QuantifiersModule(env, qs, qim, qr, tr),
53 : 535 : d_oracleFuns(userContext()),
54 : 535 : d_ochecker(env.getOracleChecker()),
55 : 535 : d_consistencyCheckPassed(false),
56 : 1070 : d_dstrat(env, "OracleArgValue", qs.getValuation())
57 : : {
58 [ - + ][ - + ]: 535 : Assert(d_ochecker != nullptr);
[ - - ]
59 : 535 : }
60 : :
61 : 326 : void OracleEngine::presolve()
62 : : {
63 : : // Ensure all oracle functions in top-level substitutions occur in
64 : : // lemmas. Otherwise the oracles will not be invoked for those values
65 : : // and the model will be inaccurate.
66 : : std::unordered_map<Node, Node> subs =
67 : 326 : d_env.getTopLevelSubstitutions().get().getSubstitutions();
68 : 326 : std::unordered_set<Node> visited;
69 : 326 : std::vector<TNode> visit;
70 [ - + ]: 326 : for (const std::pair<const Node, Node>& s : subs)
71 : : {
72 : 0 : visit.push_back(s.second);
73 : : }
74 : 326 : TNode cur;
75 [ - + ]: 326 : while (!visit.empty())
76 : : {
77 : 0 : cur = visit.back();
78 : 0 : visit.pop_back();
79 [ - - ]: 0 : if (visited.find(cur) == visited.end())
80 : : {
81 : 0 : visited.insert(cur);
82 [ - - ]: 0 : if (OracleCaller::isOracleFunctionApp(cur))
83 : : {
84 : 0 : Node k = SkolemManager::mkPurifySkolem(cur);
85 : 0 : Node eq = k.eqNode(cur);
86 : 0 : d_qim.lemma(eq, InferenceId::QUANTIFIERS_ORACLE_PURIFY_SUBS);
87 : 0 : }
88 [ - - ]: 0 : if (cur.getNumChildren() > 0)
89 : : {
90 : 0 : visit.insert(visit.end(), cur.begin(), cur.end());
91 : : }
92 : : }
93 : : }
94 : : // register the decision strategy which will insist that arguments are
95 : : // decided to be equal to values.
96 : 326 : d_qim.getDecisionManager()->registerStrategy(
97 : : DecisionManager::STRAT_ORACLE_ARG_VALUE,
98 : : &d_dstrat,
99 : : DecisionManager::STRAT_SCOPE_LOCAL_SOLVE);
100 : 326 : }
101 : :
102 : 2690 : bool OracleEngine::needsCheck(Theory::Effort e)
103 : : {
104 : 2690 : return e == Theory::Effort::EFFORT_LAST_CALL;
105 : : }
106 : :
107 : : // the model is built at this effort level
108 : 1182 : OracleEngine::QEffort OracleEngine::needsModel(CVC5_UNUSED Theory::Effort e)
109 : : {
110 : 1182 : return QEFFORT_MODEL;
111 : : }
112 : :
113 : 2364 : void OracleEngine::reset_round(CVC5_UNUSED Theory::Effort e)
114 : : {
115 : 2364 : d_consistencyCheckPassed = false;
116 : 2364 : }
117 : :
118 : 326 : void OracleEngine::registerQuantifier(CVC5_UNUSED Node q) {}
119 : :
120 : 3546 : void OracleEngine::check(CVC5_UNUSED Theory::Effort e, QEffort quant_e)
121 : : {
122 [ + + ]: 3546 : if (quant_e != QEFFORT_MODEL)
123 : : {
124 : 2364 : return;
125 : : }
126 : :
127 : 1182 : FirstOrderModel* fm = d_treg.getModel();
128 : 1182 : TermDb* termDatabase = d_treg.getTermDatabase();
129 : 1182 : NodeManager* nm = nodeManager();
130 : 1182 : unsigned nquant = fm->getNumAssertedQuantifiers();
131 : 1182 : std::vector<Node> currInterfaces;
132 [ + + ]: 2364 : for (unsigned i = 0; i < nquant; i++)
133 : : {
134 : 1182 : Node q = fm->getAssertedQuantifier(i);
135 [ - + ]: 1182 : if (d_qreg.getOwner(q) != this)
136 : : {
137 : 0 : continue;
138 : : }
139 : 1182 : currInterfaces.push_back(q);
140 [ + - ]: 1182 : }
141 [ - + ][ - - ]: 1182 : if (d_oracleFuns.empty() && currInterfaces.empty())
[ - + ]
142 : : {
143 : 0 : return;
144 : : }
145 : 1182 : beginCallDebug();
146 : : // Note that we currently ignore oracle interface quantified formulas, and
147 : : // look directly at the oracle functions. Note that:
148 : : // (1) The lemmas with InferenceId QUANTIFIERS_ORACLE_INTERFACE are not
149 : : // guarded by a quantified formula. This means that we are assuming that all
150 : : // oracle interface quantified formulas are top-level assertions. This is
151 : : // correct because we do not expose a way of embedding oracle interfaces into
152 : : // formulas at the user level.
153 : : // (2) We assume that oracle functions have associated oracle interface
154 : : // quantified formulas that are in currInterfaces.
155 : : // (3) We currently ignore oracle interface quantified formulas that are
156 : : // not associated with oracle functions.
157 : : //
158 : : // The current design choices above are due to the fact that our support is
159 : : // limited to "definitional SMTO" (see Polgreen et al 2022). In particular,
160 : : // we only support oracles that define I/O equalities for oracle functions
161 : : // only. The net effect of this class hence is to check the consistency of
162 : : // oracle functions, and allow "sat" or otherwise add a lemma with id
163 : : // QUANTIFIERS_ORACLE_INTERFACE.
164 : 1182 : std::vector<Node> learnedLemmas;
165 : 1182 : bool allFappsConsistent = true;
166 : : // iterate over oracle functions
167 [ + + ]: 2362 : for (const Node& f : d_oracleFuns)
168 : : {
169 : 1182 : TNodeTrie* tat = termDatabase->getTermArgTrie(f);
170 [ - + ]: 1182 : if (!tat)
171 : : {
172 : 0 : continue;
173 : : }
174 : 2364 : std::vector<Node> apps = tat->getLeaves(f.getType().getArgTypes().size());
175 [ + - ]: 2364 : Trace("oracle-calls") << "Oracle fun " << f << " with " << apps.size()
176 : 1182 : << " applications." << std::endl;
177 [ + + ]: 2362 : for (const auto& fapp : apps)
178 : : {
179 : 1182 : std::vector<Node> arguments;
180 : 1182 : arguments.push_back(f);
181 : : // evaluate arguments
182 [ + + ]: 2578 : for (const auto& arg : fapp)
183 : : {
184 : 1396 : arguments.push_back(fm->getValue(arg));
185 : 1396 : }
186 : : // call oracle
187 : 1182 : Node fappWithValues = nm->mkNode(Kind::APPLY_UF, arguments);
188 : 1182 : Node predictedResponse = fm->getValue(fapp);
189 : : Node result =
190 : 2366 : d_ochecker->checkConsistent(fappWithValues, predictedResponse);
191 [ + + ]: 1180 : if (!result.isNull())
192 : : {
193 : : // Note that we add (=> (= args values) (= (f args) result))
194 : : // instead of (= (f values) result) here. The latter may be more
195 : : // compact, but we require introducing literals for (= args values)
196 : : // so that they can be preferred by the decision strategy.
197 : 966 : std::vector<Node> disj;
198 : 1932 : Node conc = nm->mkNode(Kind::EQUAL, fapp, result);
199 : 966 : disj.push_back(conc);
200 [ + + ]: 2039 : for (size_t i = 0, nchild = fapp.getNumChildren(); i < nchild; i++)
201 : : {
202 : 1073 : Node eqa = fapp[i].eqNode(arguments[i + 1]);
203 : 1073 : eqa = rewrite(eqa);
204 : : // Insist that the decision strategy tries to make (= args values)
205 : : // true first. This is to ensure that the value of the oracle can be
206 : : // used.
207 : 1073 : d_dstrat.addLiteral(eqa);
208 : 1073 : disj.push_back(eqa.notNode());
209 : 1073 : }
210 : 966 : Node lem = nm->mkOr(disj);
211 : 966 : learnedLemmas.push_back(lem);
212 : 966 : allFappsConsistent = false;
213 : 966 : }
214 : 1186 : }
215 : 1182 : }
216 : : // if all were consistent, we can terminate
217 [ + + ]: 1180 : if (allFappsConsistent)
218 : : {
219 [ + - ]: 428 : Trace("oracle-engine-state")
220 : 214 : << "All responses consistent, no lemmas added" << std::endl;
221 : 214 : d_consistencyCheckPassed = true;
222 : : }
223 : : else
224 : : {
225 [ + + ]: 1932 : for (const Node& l : learnedLemmas)
226 : : {
227 [ + - ]: 966 : Trace("oracle-engine-state") << "adding lemma " << l << std::endl;
228 : 966 : d_qim.lemma(l, InferenceId::QUANTIFIERS_ORACLE_INTERFACE);
229 : : }
230 : : }
231 : : // general SMTO: call constraint generators and assumption generators here
232 : :
233 : 1180 : endCallDebug();
234 [ + - ]: 1184 : }
235 : :
236 : 214 : bool OracleEngine::checkCompleteFor(Node q)
237 : : {
238 [ - + ]: 214 : if (d_qreg.getOwner(q) != this)
239 : : {
240 : 0 : return false;
241 : : }
242 : : // Only true if oracle consistency check was successful. Notice that
243 : : // we can say true for *all* oracle interface quantified formulas in the
244 : : // case that the consistency check passed. In particular, the invocation
245 : : // of oracle interfaces does not need to be complete.
246 : 214 : return d_consistencyCheckPassed;
247 : : }
248 : :
249 : 326 : void OracleEngine::checkOwnership(Node q)
250 : : {
251 : : // take ownership of quantified formulas that are oracle interfaces
252 : 326 : QuantAttributes& qa = d_qreg.getQuantAttributes();
253 [ - + ]: 326 : if (!qa.isOracleInterface(q))
254 : : {
255 : 0 : return;
256 : : }
257 : 326 : d_qreg.setOwner(q, this);
258 : : // We expect oracle interfaces to be limited to definitional SMTO currently.
259 [ + - ]: 326 : if (Configuration::isAssertionBuild())
260 : : {
261 : 326 : std::vector<Node> inputs, outputs;
262 : 326 : Node assume, constraint, oracle;
263 [ - + ]: 326 : if (!getOracleInterface(q, inputs, outputs, assume, constraint, oracle))
264 : : {
265 : 0 : DebugUnhandled() << "Not an oracle interface " << q;
266 : : }
267 : : else
268 : : {
269 : 326 : Assert(outputs.size() == 1) << "Unhandled oracle constraint " << q;
270 : 326 : Assert(constraint.isConst() && constraint.getConst<bool>())
271 : 0 : << "Unhandled oracle constraint " << q;
272 : : }
273 : 326 : CVC5_UNUSED bool isOracleFun = false;
274 [ + - ]: 326 : if (assume.getKind() == Kind::EQUAL)
275 : : {
276 [ + + ]: 978 : for (size_t i = 0; i < 2; i++)
277 : : {
278 [ + + ][ - - ]: 652 : if (OracleCaller::isOracleFunctionApp(assume[i])
279 [ + + ][ + - ]: 652 : && assume[1 - i] == outputs[0])
[ + + ][ + - ]
[ - - ]
280 : : {
281 : 326 : isOracleFun = true;
282 : : }
283 : : }
284 : : }
285 : 326 : Assert(isOracleFun)
286 : 0 : << "Non-definitional oracle interface quantified formula " << q;
287 : 326 : }
288 : : }
289 : :
290 : 0 : std::string OracleEngine::identify() const
291 : : {
292 : 0 : return std::string("OracleEngine");
293 : : }
294 : :
295 : 535 : void OracleEngine::declareOracleFun(Node f) { d_oracleFuns.push_back(f); }
296 : :
297 : 0 : std::vector<Node> OracleEngine::getOracleFuns() const
298 : : {
299 : 0 : std::vector<Node> ofuns;
300 [ - - ]: 0 : for (const Node& f : d_oracleFuns)
301 : : {
302 : 0 : ofuns.push_back(f);
303 : : }
304 : 0 : return ofuns;
305 : 0 : }
306 : :
307 : 535 : Node OracleEngine::mkOracleInterface(const std::vector<Node>& inputs,
308 : : const std::vector<Node>& outputs,
309 : : Node assume,
310 : : Node constraint,
311 : : Node oracleNode)
312 : : {
313 [ - + ][ - + ]: 535 : Assert(!assume.isNull());
[ - - ]
314 [ - + ][ - + ]: 535 : Assert(!constraint.isNull());
[ - - ]
315 [ - + ][ - + ]: 535 : Assert(oracleNode.getKind() == Kind::ORACLE);
[ - - ]
316 : 535 : NodeManager* nm = oracleNode.getNodeManager();
317 : : Node ipl = nm->mkNode(Kind::INST_PATTERN_LIST,
318 : 1070 : nm->mkNode(Kind::INST_ATTRIBUTE, oracleNode));
319 : 535 : std::vector<Node> vars;
320 : : OracleInputVarAttribute oiva;
321 [ + + ]: 1280 : for (Node v : inputs)
322 : : {
323 : 745 : v.setAttribute(oiva, true);
324 : 745 : vars.push_back(v);
325 : 745 : }
326 : : OracleOutputVarAttribute oova;
327 [ + + ]: 1070 : for (Node v : outputs)
328 : : {
329 : 535 : v.setAttribute(oova, true);
330 : 535 : vars.push_back(v);
331 : 535 : }
332 : 535 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, vars);
333 : 1070 : Node body = nm->mkNode(Kind::ORACLE_FORMULA_GEN, assume, constraint);
334 : 1070 : return nm->mkNode(Kind::FORALL, bvl, body, ipl);
335 : 535 : }
336 : :
337 : 326 : bool OracleEngine::getOracleInterface(Node q,
338 : : std::vector<Node>& inputs,
339 : : std::vector<Node>& outputs,
340 : : Node& assume,
341 : : Node& constraint,
342 : : Node& oracleNode) const
343 : : {
344 : 326 : QuantAttributes& qa = d_qreg.getQuantAttributes();
345 [ + - ]: 326 : if (qa.isOracleInterface(q))
346 : : {
347 : : // fill in data
348 : : OracleInputVarAttribute oiva;
349 [ + + ]: 1085 : for (const Node& v : q[0])
350 : : {
351 [ + + ]: 759 : if (v.getAttribute(oiva))
352 : : {
353 : 433 : inputs.push_back(v);
354 : : }
355 : : else
356 : : {
357 [ - + ][ - + ]: 326 : Assert(v.getAttribute(OracleOutputVarAttribute()));
[ - - ]
358 : 326 : outputs.push_back(v);
359 : : }
360 : 1085 : }
361 [ - + ][ - + ]: 326 : Assert(q[1].getKind() == Kind::ORACLE_FORMULA_GEN);
[ - - ]
362 : 326 : assume = q[1][0];
363 : 326 : constraint = q[1][1];
364 [ - + ][ - + ]: 326 : Assert(q.getNumChildren() == 3);
[ - - ]
365 [ - + ][ - + ]: 326 : Assert(q[2].getNumChildren() == 1);
[ - - ]
366 [ - + ][ - + ]: 326 : Assert(q[2][0].getNumChildren() == 1);
[ - - ]
367 [ - + ][ - + ]: 326 : Assert(q[2][0][0].getKind() == Kind::ORACLE);
[ - - ]
368 : 326 : oracleNode = q[2][0][0];
369 : 326 : return true;
370 : : }
371 : 0 : return false;
372 : : }
373 : :
374 : : } // namespace quantifiers
375 : : } // namespace theory
376 : : } // namespace cvc5::internal
|
