Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Morgan Deters
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 : : * SolverEngine: the main public entry point of libcvc5.
14 : : */
15 : :
16 : : #include "cvc5_public.h"
17 : :
18 : : #ifndef CVC5__SMT__SOLVER_ENGINE_H
19 : : #define CVC5__SMT__SOLVER_ENGINE_H
20 : :
21 : : #include <cvc5/cvc5_export.h>
22 : :
23 : : #include <map>
24 : : #include <memory>
25 : : #include <string>
26 : : #include <unordered_set>
27 : : #include <vector>
28 : :
29 : : #include "context/cdhashmap_forward.h"
30 : : #include "options/options.h"
31 : : #include "smt/smt_mode.h"
32 : : #include "theory/logic_info.h"
33 : : #include "util/result.h"
34 : : #include "util/synth_result.h"
35 : :
36 : : namespace cvc5 {
37 : :
38 : : class Solver;
39 : :
40 : : namespace internal {
41 : :
42 : : template <bool ref_count>
43 : : class NodeTemplate;
44 : : typedef NodeTemplate<true> Node;
45 : : typedef NodeTemplate<false> TNode;
46 : : class TypeNode;
47 : : class ProofNode;
48 : :
49 : : class Env;
50 : : class NodeManager;
51 : : class UnsatCore;
52 : : class StatisticsRegistry;
53 : : class Plugin;
54 : : class Printer;
55 : : class ResourceManager;
56 : : struct InstantiationList;
57 : :
58 : : /* -------------------------------------------------------------------------- */
59 : :
60 : : namespace smt {
61 : : /** Utilities */
62 : : class ContextManager;
63 : : class SolverEngineState;
64 : : class ResourceOutListener;
65 : : class CheckModels;
66 : : /** Subsolvers */
67 : : class SmtSolver;
68 : : class SmtDriver;
69 : : class SygusSolver;
70 : : class AbductionSolver;
71 : : class InterpolationSolver;
72 : : class QuantElimSolver;
73 : : class FindSynthSolver;
74 : :
75 : : struct SolverEngineStatistics;
76 : : class PfManager;
77 : : class UnsatCoreManager;
78 : :
79 : : } // namespace smt
80 : :
81 : : /* -------------------------------------------------------------------------- */
82 : :
83 : : namespace theory {
84 : : class TheoryModel;
85 : : class QuantifiersEngine;
86 : : } // namespace theory
87 : :
88 : : /* -------------------------------------------------------------------------- */
89 : :
90 : : class CVC5_EXPORT SolverEngine
91 : : {
92 : : friend class cvc5::Solver;
93 : :
94 : : /* ....................................................................... */
95 : : public:
96 : : /* ....................................................................... */
97 : :
98 : : /**
99 : : * Construct an SolverEngine with the given expression manager.
100 : : * If provided, optr is a pointer to a set of options that should initialize
101 : : * the values of the options object owned by this class.
102 : : */
103 : : SolverEngine(NodeManager* nm, const Options* optr = nullptr);
104 : : /** Destruct the SMT engine. */
105 : : ~SolverEngine();
106 : :
107 : : //--------------------------------------------- concerning the state
108 : :
109 : : /**
110 : : * This is the main initialization procedure of the SolverEngine.
111 : : *
112 : : * Should be called whenever the final options and logic for the problem are
113 : : * set (at least, those options that are not permitted to change after
114 : : * assertions and queries are made).
115 : : *
116 : : * Internally, this creates the theory engine, prop engine, decision engine,
117 : : * and other utilities whose initialization depends on the final set of
118 : : * options being set.
119 : : *
120 : : * This post-construction initialization is automatically triggered by the
121 : : * use of the SolverEngine; e.g. when the first formula is asserted, a call
122 : : * to simplify() is issued, a scope is pushed, etc.
123 : : */
124 : : void finishInit();
125 : : /**
126 : : * Return true if this SolverEngine is fully initialized (post-construction)
127 : : * by the above call.
128 : : */
129 : : bool isFullyInited() const;
130 : : /**
131 : : * @return True if a call to check-sat or check-synth has been made and
132 : : * completed. Other calls (e.g., get-interpolant, get-abduct, get-qe) do not
133 : : * impact this, since they are handled independently via subsolvers.
134 : : */
135 : : bool isQueryMade() const;
136 : : /** Return the user context level. */
137 : : size_t getNumUserLevels() const;
138 : : /** Return the current mode of the solver. */
139 : : SmtMode getSmtMode() const;
140 : : /**
141 : : * Whether the SmtMode allows for get-value, get-model, get-assignment, etc.
142 : : * This is equivalent to:
143 : : * getSmtMode()==SmtMode::SAT || getSmtMode()==SmtMode::SAT_UNKNOWN
144 : : */
145 : : bool isSmtModeSat() const;
146 : : /**
147 : : * Returns the most recent result of checkSat or
148 : : * (set-info :status).
149 : : */
150 : : Result getStatusOfLastCommand() const;
151 : : //--------------------------------------------- end concerning the state
152 : :
153 : : /**
154 : : * Set the logic of the script.
155 : : * @throw ModalException, LogicException
156 : : */
157 : : void setLogic(const std::string& logic);
158 : :
159 : : /**
160 : : * Set the logic of the script.
161 : : * @throw ModalException
162 : : */
163 : : void setLogic(const LogicInfo& logic);
164 : :
165 : : /** Has the logic been set by a call to setLogic? */
166 : : bool isLogicSet() const;
167 : :
168 : : /** Get the logic information currently set. */
169 : : const LogicInfo& getLogicInfo() const;
170 : :
171 : : /** Get the logic information set by the user. */
172 : : LogicInfo getUserLogicInfo() const;
173 : :
174 : : /**
175 : : * Set information about the script executing.
176 : : */
177 : : void setInfo(const std::string& key, const std::string& value);
178 : :
179 : : /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */
180 : : bool isValidGetInfoFlag(const std::string& key) const;
181 : :
182 : : /** Query information about the SMT environment. */
183 : : std::string getInfo(const std::string& key) const;
184 : :
185 : : /**
186 : : * Set an aspect of the current SMT execution environment.
187 : : * @param key The option to set
188 : : * @param value The value to set
189 : : * @param fromUser Whether this option was set by the user. This impacts
190 : : * whether we enable checks e.g. when safe mode is enabled.
191 : : * @throw OptionException, ModalException
192 : : */
193 : : void setOption(const std::string& key,
194 : : const std::string& value,
195 : : bool fromUser = false);
196 : :
197 : : /** Set is internal subsolver.
198 : : *
199 : : * This function is called on SolverEngine objects that are created
200 : : * internally. It is used to mark that this SolverEngine should not
201 : : * perform preprocessing passes that rephrase the input, such as
202 : : * --sygus-rr-synth-input or
203 : : * --sygus-abduct.
204 : : */
205 : : void setIsInternalSubsolver();
206 : : /** Is this an internal subsolver? */
207 : : bool isInternalSubsolver() const;
208 : :
209 : : /**
210 : : * Block the current model. Can be called only if immediately preceded by
211 : : * a SAT or INVALID query. Only permitted if produce-models is on, and the
212 : : * block-models option is set to a mode other than "none".
213 : : *
214 : : * This adds an assertion to the assertion stack that blocks the current
215 : : * model based on the current options configured by cvc5.
216 : : */
217 : : void blockModel(modes::BlockModelsMode mode);
218 : :
219 : : /**
220 : : * Block the current model values of (at least) the values in exprs. Can be
221 : : * called only if immediately preceded by a SAT query. Only permitted if
222 : : * produce-models is on, and the block-models option is set to a mode other
223 : : * than "none".
224 : : *
225 : : * This adds an assertion to the assertion stack of the form:
226 : : * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
227 : : * where M0 ... Mn are the current model values of exprs[0] ... exprs[n].
228 : : */
229 : : void blockModelValues(const std::vector<Node>& exprs);
230 : :
231 : : /**
232 : : * Declare heap. For smt2 inputs, this is called when the command
233 : : * (declare-heap (locT datat)) is invoked by the user. This sets locT as the
234 : : * location type and dataT is the data type for the heap. This command should
235 : : * be executed only once, and must be invoked before solving separation logic
236 : : * inputs.
237 : : */
238 : : void declareSepHeap(TypeNode locT, TypeNode dataT);
239 : :
240 : : /**
241 : : * Get the separation heap types, which extracts which types were passed to
242 : : * the method above.
243 : : *
244 : : * @return true if the separation logic heap types have been declared.
245 : : */
246 : : bool getSepHeapTypes(TypeNode& locT, TypeNode& dataT);
247 : :
248 : : /** When using separation logic, obtain the expression for the heap. */
249 : : Node getSepHeapExpr();
250 : :
251 : : /** When using separation logic, obtain the expression for nil. */
252 : : Node getSepNilExpr();
253 : :
254 : : /**
255 : : * Get the list of top-level learned literals that are entailed by the current
256 : : * set of assertions.
257 : : */
258 : : std::vector<Node> getLearnedLiterals(modes::LearnedLitType t);
259 : :
260 : : /**
261 : : * Get an aspect of the current SMT execution environment.
262 : : * @throw OptionException
263 : : */
264 : : std::string getOption(const std::string& key) const;
265 : :
266 : : /**
267 : : * Notify that a declare-fun or declare-const was made for n. This only
268 : : * impacts the SMT mode.
269 : : */
270 : : void declareConst(const Node& n);
271 : : /**
272 : : * Notify that a declare-sort was made for tn. This only impacts the SMT mode.
273 : : */
274 : : void declareSort(const TypeNode& tn);
275 : : /**
276 : : * Define function func in the current context to be:
277 : : * (lambda (formals) formula)
278 : : * This adds func to the list of defined functions, which indicates that
279 : : * all occurrences of func should be expanded during expandDefinitions.
280 : : *
281 : : * @param func a variable of function type that expects the arguments in
282 : : * formal
283 : : * @param formals a list of BOUND_VARIABLE expressions
284 : : * @param formula The body of the function, must not contain func
285 : : * @param global True if this definition is global (i.e. should persist when
286 : : * popping the user context)
287 : : */
288 : : void defineFunction(Node func,
289 : : const std::vector<Node>& formals,
290 : : Node formula,
291 : : bool global = false);
292 : : /** Same as above, with lambda */
293 : : void defineFunction(Node func, Node lambda, bool global = false);
294 : :
295 : : /**
296 : : * Define functions recursive
297 : : *
298 : : * For each i, this constrains funcs[i] in the current context to be:
299 : : * (lambda (formals[i]) formulas[i])
300 : : * where formulas[i] may contain variables from funcs. Unlike defineFunction
301 : : * above, we do not add funcs[i] to the set of defined functions. Instead,
302 : : * we consider funcs[i] to be a free uninterpreted function, and add:
303 : : * forall formals[i]. f(formals[i]) = formulas[i]
304 : : * to the set of assertions in the current context.
305 : : * This method expects input such that for each i:
306 : : * - func[i] : a variable of function type that expects the arguments in
307 : : * formals[i], and
308 : : * - formals[i] : a list of BOUND_VARIABLE expressions.
309 : : *
310 : : * @param global True if this definition is global (i.e. should persist when
311 : : * popping the user context)
312 : : */
313 : : void defineFunctionsRec(const std::vector<Node>& funcs,
314 : : const std::vector<std::vector<Node>>& formals,
315 : : const std::vector<Node>& formulas,
316 : : bool global = false);
317 : : /**
318 : : * Define function recursive
319 : : * Same as above, but for a single function.
320 : : */
321 : : void defineFunctionRec(Node func,
322 : : const std::vector<Node>& formals,
323 : : Node formula,
324 : : bool global = false);
325 : :
326 : : /**
327 : : * Add a formula to the current context: preprocess, do per-theory
328 : : * setup, use processAssertionList(), asserting to T-solver for
329 : : * literals and conjunction of literals. Note this formula will
330 : : * be included in the unsat core when applicable.
331 : : *
332 : : * @throw TypeCheckingException, LogicException
333 : : */
334 : : void assertFormula(const Node& formula);
335 : :
336 : : /**
337 : : * Assert a formula (if provided) to the current context and call
338 : : * check(). Returns SAT, UNSAT, or UNKNOWN result.
339 : : *
340 : : * @throw Exception
341 : : */
342 : : Result checkSat();
343 : : Result checkSat(const Node& assumption);
344 : : Result checkSat(const std::vector<Node>& assumptions);
345 : :
346 : : /**
347 : : * Get a timeout core, which computes a subset of the current assertions that
348 : : * cause a timeout. Note it does not require being proceeded by a call to
349 : : * checkSat. For details, see Solver::getTimeoutCore.
350 : : *
351 : : * @return The result of the timeout core computation.
352 : : */
353 : : std::pair<Result, std::vector<Node>> getTimeoutCore(
354 : : const std::vector<Node>& assumptions);
355 : : /**
356 : : * Returns a set of so-called "failed" assumptions.
357 : : *
358 : : * The returned set is a subset of the set of assumptions of a previous
359 : : * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability
360 : : * with this set of failed assumptions still produces an unsat answer.
361 : : *
362 : : * Note that the returned set of failed assumptions is not necessarily
363 : : * minimal.
364 : : */
365 : : std::vector<Node> getUnsatAssumptions(void);
366 : :
367 : : /*---------------------------- sygus commands ---------------------------*/
368 : :
369 : : /**
370 : : * Add sygus variable declaration.
371 : : *
372 : : * Declared SyGuS variables may be used in SyGuS constraints, in which they
373 : : * are assumed to be universally quantified.
374 : : *
375 : : * In SyGuS semantics, declared functions are treated in the same manner as
376 : : * declared variables, i.e. as universally quantified (function) variables
377 : : * which can occur in the SyGuS constraints that compose the conjecture to
378 : : * which a function is being synthesized. Thus declared functions should use
379 : : * this method as well.
380 : : */
381 : : void declareSygusVar(Node var);
382 : :
383 : : /**
384 : : * Add a function-to-synthesize declaration.
385 : : *
386 : : * The given sygusType may not correspond to the actual function type of func
387 : : * but to a datatype encoding the syntax restrictions for the
388 : : * function-to-synthesize. In this case this information is stored to be used
389 : : * during solving.
390 : : *
391 : : * vars contains the arguments of the function-to-synthesize. These variables
392 : : * are also stored to be used during solving.
393 : : *
394 : : * isInv determines whether the function-to-synthesize is actually an
395 : : * invariant. This information is necessary if we are dumping a command
396 : : * corresponding to this declaration, so that it can be properly printed.
397 : : */
398 : : void declareSynthFun(Node func,
399 : : TypeNode sygusType,
400 : : bool isInv,
401 : : const std::vector<Node>& vars);
402 : : /**
403 : : * Same as above, without a sygus type.
404 : : */
405 : : void declareSynthFun(Node func, bool isInv, const std::vector<Node>& vars);
406 : :
407 : : /**
408 : : * Add a regular sygus constraint or assumption.
409 : : * @param n The formula
410 : : * @param isAssume True if n is an assumption.
411 : : */
412 : : void assertSygusConstraint(Node n, bool isAssume = false);
413 : :
414 : : /** @return sygus constraints .*/
415 : : std::vector<Node> getSygusConstraints();
416 : :
417 : : /** @return sygus assumptions .*/
418 : : std::vector<Node> getSygusAssumptions();
419 : :
420 : : /**
421 : : * Add an invariant constraint.
422 : : *
423 : : * Invariant constraints are not explicitly declared: they are given in terms
424 : : * of the invariant-to-synthesize, the pre condition, transition relation and
425 : : * post condition. The actual constraint is built based on the inputs of these
426 : : * place holder predicates :
427 : : *
428 : : * PRE(x) -> INV(x)
429 : : * INV() ^ TRANS(x, x') -> INV(x')
430 : : * INV(x) -> POST(x)
431 : : *
432 : : * The regular and primed variables are retrieved from the declaration of the
433 : : * invariant-to-synthesize.
434 : : */
435 : : void assertSygusInvConstraint(Node inv, Node pre, Node trans, Node post);
436 : : /**
437 : : * Assert a synthesis conjecture to the current context and call
438 : : * check(). Returns sat, unsat, or unknown result.
439 : : *
440 : : * The actual synthesis conjecture is built based on the previously
441 : : * communicated information to this module (universal variables, defined
442 : : * functions, functions-to-synthesize, and which constraints compose it). The
443 : : * built conjecture is a higher-order formula of the form
444 : : *
445 : : * exists f1...fn . forall v1...vm . F
446 : : *
447 : : * in which f1...fn are the functions-to-synthesize, v1...vm are the declared
448 : : * universal variables and F is the set of declared constraints.
449 : : *
450 : : * @param isNext Whether we are asking for the next synthesis solution (if
451 : : * using incremental).
452 : : *
453 : : * @throw Exception
454 : : */
455 : : SynthResult checkSynth(bool isNext = false);
456 : : /**
457 : : * Find synth for the given target and grammar.
458 : : */
459 : : Node findSynth(modes::FindSynthTarget fst, const TypeNode& gtn);
460 : : /**
461 : : * Find synth for the given target and grammar.
462 : : */
463 : : Node findSynthNext();
464 : :
465 : : /*------------------------- end of sygus commands ------------------------*/
466 : :
467 : : /**
468 : : * Declare pool whose initial value is the terms in initValue. A pool is
469 : : * a variable of type (Set T) that is used in quantifier annotations and does
470 : : * not occur in constraints.
471 : : *
472 : : * @param p The pool to declare, which should be a variable of type (Set T)
473 : : * for some type T.
474 : : * @param initValue The initial value of p, which should be a vector of terms
475 : : * of type T.
476 : : */
477 : : void declarePool(const Node& p, const std::vector<Node>& initValue);
478 : :
479 : : /**
480 : : * Add an oracle function to the state, also adds an oracle interface
481 : : * defining it.
482 : : *
483 : : * @param var The oracle function symbol
484 : : * @param fn The method for the oracle
485 : : */
486 : : void declareOracleFun(
487 : : Node var, std::function<std::vector<Node>(const std::vector<Node>&)> fn);
488 : : /**
489 : : * Adds plugin to the theory engine of this solver engine.
490 : : *
491 : : * @param p The plugin to add.
492 : : */
493 : : void addPlugin(Plugin* p);
494 : : /**
495 : : * Simplify a term or formula based on rewriting and (optionally) applying
496 : : * substitutions for solved variables.
497 : : *
498 : : * If applySubs is true, then for example, if `(= x 0)` was asserted to this
499 : : * solver, this method may replace occurrences of `x` with `0`.
500 : : *
501 : : * @param t The term to simplify.
502 : : * @param applySubs Whether to apply substitutions for solved variables.
503 : : * @return The simplified term.
504 : : */
505 : : Node simplify(const Node& e, bool applySubs);
506 : :
507 : : /**
508 : : * Get the assigned value of an expr (only if immediately preceded by a SAT
509 : : * query). Only permitted if the SolverEngine is set to operate interactively
510 : : * and produce-models is on.
511 : : *
512 : : * Note that this method may make a subcall to another copy of the SMT solver
513 : : * (if --check-model-subsolver is enabled). We do this only if the call
514 : : * originated from the user (fromUser is true), in which case we insist
515 : : * that we find a concrete value. This means if e is a quantified formula,
516 : : * we must call a subsolver. Other uses of internal subsolvers (e.g. MBQI)
517 : : * do not generally insist that the returned value is concrete.
518 : : *
519 : : * @param e The term to get the value of.
520 : : * @param fromUser Whether the call originated from an external user.
521 : : * @throw ModalException, TypeCheckingException, LogicException
522 : : */
523 : : Node getValue(const Node& e, bool fromUser = false);
524 : :
525 : : /**
526 : : * Same as getValue but for a vector of expressions
527 : : *
528 : : * @param e The term to get the value of.
529 : : * @param fromUser Whether the call originated from an external user.
530 : : */
531 : : std::vector<Node> getValues(const std::vector<Node>& exprs,
532 : : bool fromUser = false);
533 : :
534 : : /**
535 : : * @return the domain elements for uninterpreted sort tn.
536 : : */
537 : : std::vector<Node> getModelDomainElements(TypeNode tn) const;
538 : :
539 : : /**
540 : : * @return true if v is a model core symbol
541 : : */
542 : : bool isModelCoreSymbol(Node v);
543 : :
544 : : /**
545 : : * Get a model (only if immediately preceded by an SAT or unknown query).
546 : : * Only permitted if the model option is on.
547 : : *
548 : : * @param declaredSorts The sorts to print in the model
549 : : * @param declaredFuns The free constants to print in the model. A subset
550 : : * of these may be printed based on isModelCoreSymbol.
551 : : * @return the string corresponding to the model. If the output language is
552 : : * smt2, then this corresponds to a response to the get-model command.
553 : : */
554 : : std::string getModel(const std::vector<TypeNode>& declaredSorts,
555 : : const std::vector<Node>& declaredFuns);
556 : :
557 : : /** print instantiations
558 : : *
559 : : * Print all instantiations for all quantified formulas on out,
560 : : * returns true if at least one instantiation was printed. The type of output
561 : : * (list, num, etc.) is determined by printInstMode.
562 : : */
563 : : void printInstantiations(std::ostream& out);
564 : :
565 : : /**
566 : : * Get synth solution.
567 : : *
568 : : * This method returns true if we are in a state immediately preceded by
569 : : * a successful call to checkSynth.
570 : : *
571 : : * This method adds entries to solMap that map functions-to-synthesize with
572 : : * their solutions, for all active conjectures. This should be called
573 : : * immediately after the solver answers unsat for sygus input.
574 : : *
575 : : * Specifically, given a sygus conjecture of the form
576 : : * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn )
577 : : * where x1...xn are second order bound variables, we map each xi to
578 : : * lambda term in solMap such that
579 : : * forall y1...yn. P( solMap[x1]...solMap[xn], y1...yn )
580 : : * is a valid formula.
581 : : */
582 : : bool getSynthSolutions(std::map<Node, Node>& solMap);
583 : : /**
584 : : * Same as above, but used for getting synthesis solutions from a "subsolver"
585 : : * that has been initialized to assert the synthesis conjecture as a
586 : : * normal assertion.
587 : : *
588 : : * This method returns true if we are in a state immediately preceded by
589 : : * a successful call to checkSat, where this SolverEngine has an asserted
590 : : * synthesis conjecture.
591 : : */
592 : : bool getSubsolverSynthSolutions(std::map<Node, Node>& solMap);
593 : :
594 : : /**
595 : : * Do quantifier elimination.
596 : : *
597 : : * This function takes as input a quantified formula q
598 : : * of the form:
599 : : * Q x1...xn. P( x1...xn, y1...yn )
600 : : * where P( x1...xn, y1...yn ) is a quantifier-free
601 : : * formula in a logic that supports quantifier elimination.
602 : : * Currently, the only logics supported by quantifier
603 : : * elimination is LRA and LIA.
604 : : *
605 : : * This function returns a formula ret such that, given
606 : : * the current set of formulas A asserted to this SolverEngine :
607 : : *
608 : : * If doFull = true, then
609 : : * - ( A ^ q ) and ( A ^ ret ) are equivalent
610 : : * - ret is quantifier-free formula containing
611 : : * only free variables in y1...yn.
612 : : *
613 : : * If doFull = false, then
614 : : * - (A ^ q) => (A ^ ret) if Q is forall or
615 : : * (A ^ ret) => (A ^ q) if Q is exists,
616 : : * - ret is quantifier-free formula containing
617 : : * only free variables in y1...yn,
618 : : * - If Q is exists, let A^Q_n be the formula
619 : : * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
620 : : * where for each i=1,...n, formula ret^Q_i
621 : : * is the result of calling doQuantifierElimination
622 : : * for q with the set of assertions A^Q_{i-1}.
623 : : * Similarly, if Q is forall, then let A^Q_n be
624 : : * A ^ ret^Q_1 ^ ... ^ ret^Q_n
625 : : * where ret^Q_i is the same as above.
626 : : * In either case, we have that ret^Q_j will
627 : : * eventually be true or false, for some finite j.
628 : : *
629 : : * The former feature is quantifier elimination, and
630 : : * is run on invocations of the smt2 extended command get-qe.
631 : : * The latter feature is referred to as partial quantifier
632 : : * elimination, and is run on invocations of the smt2
633 : : * extended command get-qe-disjunct, which can be used
634 : : * for incrementally computing the result of a
635 : : * quantifier elimination.
636 : : */
637 : : Node getQuantifierElimination(Node q, bool doFull);
638 : :
639 : : /**
640 : : * This method asks this SMT engine to find an interpolant with respect to
641 : : * the current assertion stack (call it A) and the conjecture (call it B). If
642 : : * this method returns true, then interpolant is set to a formula I such that
643 : : * A ^ ~I and I ^ ~B are both unsatisfiable.
644 : : *
645 : : * The argument grammarType is a sygus datatype type that encodes the syntax
646 : : * restrictions on the shapes of possible solutions.
647 : : *
648 : : * This method invokes a separate copy of the SMT engine for solving the
649 : : * corresponding sygus problem for generating such a solution.
650 : : */
651 : : Node getInterpolant(const Node& conj, const TypeNode& grammarType);
652 : :
653 : : /**
654 : : * Get next interpolant. This can only be called immediately after a
655 : : * successful call to getInterpolant or getInterpolantNext.
656 : : *
657 : : * Returns the interpolant if one exists, or the null node otherwise.
658 : : */
659 : : Node getInterpolantNext();
660 : :
661 : : /**
662 : : * This method asks this SMT engine to find an abduct with respect to the
663 : : * current assertion stack (call it A) and the conjecture (call it B).
664 : : * If this method returns true, then abd is set to a formula C such that
665 : : * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
666 : : *
667 : : * The argument grammarType is a sygus datatype type that encodes the syntax
668 : : * restrictions on the shape of possible solutions.
669 : : *
670 : : * This method invokes a separate copy of the SMT engine for solving the
671 : : * corresponding sygus problem for generating such a solution.
672 : : */
673 : : Node getAbduct(const Node& conj, const TypeNode& grammarType);
674 : :
675 : : /**
676 : : * Get next abduct. This can only be called immediately after a successful
677 : : * call to getAbduct or getAbductNext.
678 : : *
679 : : * Returns the abduct if one exists, or the null node otherwise.
680 : : */
681 : : Node getAbductNext();
682 : :
683 : : /**
684 : : * Get list of quantified formulas that were instantiated on the last call
685 : : * to check-sat.
686 : : */
687 : : void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
688 : :
689 : : /**
690 : : * Get instantiation term vectors for quantified formula q.
691 : : *
692 : : * This method is similar to above, but in the example above, we return the
693 : : * (vectors of) terms t1, ..., tn instead.
694 : : *
695 : : * Notice that these are not guaranteed to come in the same order as the
696 : : * instantiation lemmas above.
697 : : */
698 : : void getInstantiationTermVectors(Node q,
699 : : std::vector<std::vector<Node>>& tvecs);
700 : : /**
701 : : * Adds the skolemizations and instantiations that were relevant
702 : : * for the refutation.
703 : : * @param insts The relevant instantiations
704 : : * @param sks The relevant skolemizations
705 : : * @param getDebugInfo If true, we add identifiers on instantiations that
706 : : * indicate their source (the strategy that invoked them)
707 : : */
708 : : void getRelevantQuantTermVectors(std::map<Node, InstantiationList>& insts,
709 : : std::map<Node, std::vector<Node>>& sks,
710 : : bool getDebugInfo = false);
711 : : /**
712 : : * Get instantiation term vectors, which maps each instantiated quantified
713 : : * formula to the list of instantiations for that quantified formula. This
714 : : * list is minimized if proofs are enabled, and this call is immediately
715 : : * preceded by an UNSAT query.
716 : : */
717 : : void getInstantiationTermVectors(
718 : : std::map<Node, std::vector<std::vector<Node>>>& insts);
719 : :
720 : : /**
721 : : * Get an unsatisfiable core (only if immediately preceded by an UNSAT
722 : : * query). Only permitted if cvc5 was built with unsat-core support and
723 : : * produce-unsat-cores is on.
724 : : */
725 : : UnsatCore getUnsatCore();
726 : :
727 : : /** Get the lemmas used to derive UNSAT. Only permitted if cvc5 was built with
728 : : * unsat cores support and produce-unsat-core-lemmas is on. */
729 : : std::vector<Node> getUnsatCoreLemmas();
730 : :
731 : : /**
732 : : * Get a refutation proof (only if immediately preceded by an UNSAT query).
733 : : * Only permitted if cvc5 was built with proof support and the proof option
734 : : * is on.
735 : : */
736 : : std::vector<std::shared_ptr<ProofNode>> getProof(
737 : : modes::ProofComponent c = modes::ProofComponent::FULL);
738 : :
739 : : // TODO: this goes away after proof printing went into ProofNode
740 : : void proofToString(std::ostream& out, std::shared_ptr<ProofNode> fp);
741 : :
742 : : /**
743 : : * Get the current set of assertions. Only permitted if the
744 : : * SolverEngine is set to operate interactively.
745 : : */
746 : : std::vector<Node> getAssertions();
747 : :
748 : : /**
749 : : * Get difficulty map, which populates dmap, mapping input assertions
750 : : * to a value that estimates their difficulty for solving the current problem.
751 : : */
752 : : void getDifficultyMap(std::map<Node, Node>& dmap);
753 : :
754 : : /**
755 : : * Push a user-level context.
756 : : * throw@ ModalException, LogicException
757 : : */
758 : : void push();
759 : :
760 : : /**
761 : : * Pop a user-level context. Throws an exception if nothing to pop.
762 : : * @throw ModalException
763 : : */
764 : : void pop();
765 : :
766 : : /** Reset all assertions, global declarations, etc. */
767 : : void resetAssertions();
768 : :
769 : : /**
770 : : * Interrupt a running query. This can be called from another thread
771 : : * or from a signal handler. Throws a ModalException if the SolverEngine
772 : : * isn't currently in a query.
773 : : *
774 : : * @throw ModalException
775 : : */
776 : : void interrupt();
777 : :
778 : : /**
779 : : * Set a resource limit for SolverEngine operations. This is like a time
780 : : * limit, but it's deterministic so that reproducible results can be
781 : : * obtained. Currently, it's based on the number of conflicts.
782 : : * However, please note that the definition may change between different
783 : : * versions of cvc5 (as may the number of conflicts required, anyway),
784 : : * and it might even be different between instances of the same version
785 : : * of cvc5 on different platforms.
786 : : *
787 : : * A cumulative and non-cumulative (per-call) resource limit can be
788 : : * set at the same time. A call to setResourceLimit() with
789 : : * cumulative==true replaces any cumulative resource limit currently
790 : : * in effect; a call with cumulative==false replaces any per-call
791 : : * resource limit currently in effect. Time limits can be set in
792 : : * addition to resource limits; the SolverEngine obeys both. That means
793 : : * that up to four independent limits can control the SolverEngine
794 : : * at the same time.
795 : : *
796 : : * When an SolverEngine is first created, it has no time or resource
797 : : * limits.
798 : : *
799 : : * Currently, these limits only cause the SolverEngine to stop what its
800 : : * doing when the limit expires (or very shortly thereafter); no
801 : : * heuristics are altered by the limits or the threat of them expiring.
802 : : * We reserve the right to change this in the future.
803 : : *
804 : : * @param units the resource limit, or 0 for no limit
805 : : * @param cumulative whether this resource limit is to be a cumulative
806 : : * resource limit for all remaining calls into the SolverEngine (true), or
807 : : * whether it's a per-call resource limit (false); the default is false
808 : : */
809 : : void setResourceLimit(uint64_t units, bool cumulative = false);
810 : :
811 : : /**
812 : : * Set a per-call time limit for SolverEngine operations.
813 : : *
814 : : * A per-call time limit can be set at the same time and replaces
815 : : * any per-call time limit currently in effect.
816 : : * Resource limits (either per-call or cumulative) can be set in
817 : : * addition to a time limit; the SolverEngine obeys all three of them.
818 : : *
819 : : * Note that the per-call timer only ticks away when one of the
820 : : * SolverEngine's workhorse functions (things like assertFormula(),
821 : : * checkSat(), and simplify()) are running.
822 : : * Between calls, the timer is still.
823 : : *
824 : : * When an SolverEngine is first created, it has no time or resource
825 : : * limits.
826 : : *
827 : : * Currently, these limits only cause the SolverEngine to stop what its
828 : : * doing when the limit expires (or very shortly thereafter); no
829 : : * heuristics are altered by the limits or the threat of them expiring.
830 : : * We reserve the right to change this in the future.
831 : : *
832 : : * @param millis the time limit in milliseconds, or 0 for no limit
833 : : */
834 : : void setTimeLimit(uint64_t millis);
835 : :
836 : : /**
837 : : * Get the current resource usage count for this SolverEngine. This
838 : : * function can be used to ascertain reasonable values to pass as
839 : : * resource limits to setResourceLimit().
840 : : */
841 : : unsigned long getResourceUsage() const;
842 : :
843 : : /** Get the current millisecond count for this SolverEngine. */
844 : : unsigned long getTimeUsage() const;
845 : :
846 : : /**
847 : : * Get the remaining resources that can be consumed by this SolverEngine
848 : : * according to the currently-set cumulative resource limit. If there
849 : : * is not a cumulative resource limit set, this function throws a
850 : : * ModalException.
851 : : *
852 : : * @throw ModalException
853 : : */
854 : : unsigned long getResourceRemaining() const;
855 : :
856 : : /**
857 : : * Print statistics from the statistics registry in the env object owned by
858 : : * this SolverEngine. Safe to use in a signal handler.
859 : : */
860 : : void printStatisticsSafe(int fd) const;
861 : :
862 : : /**
863 : : * Print the changes to the statistics from the statistics registry in the
864 : : * env object owned by this SolverEngine since this method was called the last
865 : : * time. Internally prints the diff and then stores a snapshot for the next
866 : : * call.
867 : : */
868 : : void printStatisticsDiff() const;
869 : :
870 : : /** Get the options object (const and non-const versions) */
871 : : Options& getOptions();
872 : : const Options& getOptions() const;
873 : :
874 : : /** Get the resource manager of this SMT engine */
875 : : ResourceManager* getResourceManager() const;
876 : :
877 : : /**
878 : : * Get substituted assertions.
879 : : *
880 : : * Return the set of assertions, after applying top-level substitutions.
881 : : */
882 : : std::vector<Node> getSubstitutedAssertions();
883 : :
884 : : /**
885 : : * Get the enviornment from this solver engine.
886 : : */
887 : : Env& getEnv();
888 : : /* ....................................................................... */
889 : : private:
890 : : /* ....................................................................... */
891 : :
892 : : // disallow copy/assignment
893 : : SolverEngine(const SolverEngine&) = delete;
894 : : SolverEngine& operator=(const SolverEngine&) = delete;
895 : :
896 : : /**
897 : : * Begin call, which is called before any method that requires initializing
898 : : * this solver engine and make the state of the internal solver current.
899 : : *
900 : : * In particular, this ensures the solver is initialized, the pending pops
901 : : * on the context are processed, and optionally calls the resource manager
902 : : * to reset its limits (ResourceManager::beginCall).
903 : : *
904 : : * @param needsRLlimit If true, then beginCall() is called on the resource
905 : : * manager maintained by this class.
906 : : */
907 : : void beginCall(bool needsRLlimit = false);
908 : : /**
909 : : * End call. Should follow after a call to beginCall where needsRLlimit
910 : : * was true.
911 : : */
912 : : void endCall();
913 : :
914 : : /** Set solver instance that owns this SolverEngine. */
915 : 59608 : void setSolver(cvc5::Solver* solver) { d_solver = solver; }
916 : :
917 : : /** Get a pointer to the (new) PfManager owned by this SolverEngine. */
918 : : smt::PfManager* getPfManager() { return d_pfManager.get(); };
919 : :
920 : : /** Get a pointer to the StatisticsRegistry owned by this SolverEngine. */
921 : : StatisticsRegistry& getStatisticsRegistry();
922 : :
923 : : /**
924 : : * Internal method to get an unsatisfiable core (only if immediately preceded
925 : : * by an UNSAT query). Only permitted if cvc5 was built with unsat-core
926 : : * support and produce-unsat-cores is on. Does not dump the command.
927 : : *
928 : : * @param isInternal Whether this call was made internally (not by the user).
929 : : * This impacts whether the unsat core is post-processed.
930 : : */
931 : : UnsatCore getUnsatCoreInternal(bool isInternal = true);
932 : :
933 : : /** Internal version of assertFormula */
934 : : void assertFormulaInternal(const Node& formula);
935 : :
936 : : /**
937 : : * Check that a generated proof checks. This method is the same as getProof,
938 : : * but does not return the proof. Like that method, it should be called
939 : : * after an UNSAT response. It ensures that a well-formed proof of false
940 : : * can be constructed by the combination of the PropEngine and ProofManager.
941 : : */
942 : : void checkProof();
943 : :
944 : : /**
945 : : * Check that an unsatisfiable core is indeed unsatisfiable.
946 : : */
947 : : void checkUnsatCore();
948 : :
949 : : /**
950 : : * Check that a generated Model (via getModel()) actually satisfies
951 : : * all user assertions.
952 : : * @param hardFailure True have a failed model check should result in an
953 : : * InternalError rather than only issue a warning.
954 : : */
955 : : void checkModel(bool hardFailure = true);
956 : :
957 : : /**
958 : : * Check that a solution to an interpolation problem is indeed a solution.
959 : : *
960 : : * The check is made by determining that the assertions imply the solution of
961 : : * the interpolation problem (interpol), and the solution implies the goal
962 : : * (conj). If these criteria are not met, an internal error is thrown.
963 : : */
964 : : void checkInterpol(Node interpol,
965 : : const std::vector<Node>& easserts,
966 : : const Node& conj);
967 : :
968 : : /**
969 : : * This is called by the destructor, just before destroying the
970 : : * PropEngine, TheoryEngine, and DecisionEngine (in that order). It
971 : : * is important because there are destruction ordering issues
972 : : * between PropEngine and Theory.
973 : : */
974 : : void shutdown();
975 : :
976 : : /**
977 : : * Get the (SMT-level) model pointer, if we are in SAT mode. Otherwise,
978 : : * return nullptr.
979 : : *
980 : : * This ensures that the underlying theory model of the SmtSolver maintained
981 : : * by this class is currently available, which means that cvc5 is producing
982 : : * models, and is in "SAT mode", otherwise a recoverable exception is thrown.
983 : : *
984 : : * @param c used for giving an error message to indicate the context
985 : : * this method was called.
986 : : */
987 : : theory::TheoryModel* getAvailableModel(const char* c) const;
988 : : /**
989 : : * Get the available proof, which is that of the prop engine if SAT
990 : : * proof producing, or else a dummy proof SAT_REFUTATION whose assumptions
991 : : * are the preprocessed input formulas.
992 : : */
993 : : std::shared_ptr<ProofNode> getAvailableSatProof();
994 : : /**
995 : : * Get available quantifiers engine, which throws a modal exception if it
996 : : * does not exist. This can happen if a quantifiers-specific call (e.g.
997 : : * getInstantiatedQuantifiedFormulas) is called in a non-quantified logic.
998 : : *
999 : : * @param c used for giving an error message to indicate the context
1000 : : * this method was called.
1001 : : */
1002 : : theory::QuantifiersEngine* getAvailableQuantifiersEngine(const char* c) const;
1003 : :
1004 : : /**
1005 : : * Internally handle the setting of a logic. This function should always
1006 : : * be called when d_logic is updated.
1007 : : */
1008 : : void setLogicInternal();
1009 : :
1010 : : /*
1011 : : * Check satisfiability (used to check satisfiability and entailment).
1012 : : */
1013 : : Result checkSatInternal(const std::vector<Node>& assumptions);
1014 : :
1015 : : /**
1016 : : * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
1017 : : * the function that the formal argument list is for. This method is used
1018 : : * as a helper function when defining (recursive) functions.
1019 : : */
1020 : : void debugCheckFormals(const std::vector<Node>& formals, Node func);
1021 : :
1022 : : /**
1023 : : * Checks whether formula is a valid function body for func whose formal
1024 : : * argument list is stored in formals. This method is
1025 : : * used as a helper function when defining (recursive) functions.
1026 : : */
1027 : : void debugCheckFunctionBody(Node formula,
1028 : : const std::vector<Node>& formals,
1029 : : Node func);
1030 : : /**
1031 : : * Helper method to obtain both the heap and nil from the solver. Returns a
1032 : : * std::pair where the first element is the heap expression and the second
1033 : : * element is the nil expression.
1034 : : */
1035 : : std::pair<Node, Node> getSepHeapAndNilExpr();
1036 : : /**
1037 : : * Get assertions internal, which is only called after initialization. This
1038 : : * should be used internally to get the assertions instead of getAssertions
1039 : : * or getExpandedAssertions, which may trigger initialization and SMT state
1040 : : * changes.
1041 : : */
1042 : : std::vector<Node> getAssertionsInternal() const;
1043 : :
1044 : : /**
1045 : : * Return a reference to options like for `EnvObj`.
1046 : : */
1047 : : const Options& options() const;
1048 : :
1049 : : /**
1050 : : * Return true if the given term is a valid closed term, which can be used as
1051 : : * an argument to, e.g., assert, get-value, block-model-values, etc.
1052 : : *
1053 : : * @param n The node to check
1054 : : * @return true if n is a well formed term.
1055 : : */
1056 : : bool isWellFormedTerm(const Node& n) const;
1057 : : /**
1058 : : * Check that the given term is a valid closed term, which can be used as an
1059 : : * argument to, e.g., assert, get-value, block-model-values, etc.
1060 : : *
1061 : : * @param n The node to check
1062 : : * @param src The source of the check, which is printed in the exception if
1063 : : * this check fails.
1064 : : */
1065 : : void ensureWellFormedTerm(const Node& n, const std::string& src) const;
1066 : : /** Vector version of above. */
1067 : : void ensureWellFormedTerms(const std::vector<Node>& ns,
1068 : : const std::string& src) const;
1069 : :
1070 : : /**
1071 : : * Prints a proof node using a proof format of choice.
1072 : : */
1073 : : void printProof(std::ostream& out,
1074 : : std::shared_ptr<ProofNode> fp,
1075 : : modes::ProofFormat proofFormat,
1076 : : const std::map<Node, std::string>& assertionNames);
1077 : :
1078 : : /* Members -------------------------------------------------------------- */
1079 : :
1080 : : /** Solver instance that owns this SolverEngine instance. */
1081 : : cvc5::Solver* d_solver = nullptr;
1082 : :
1083 : : /**
1084 : : * The environment object, which contains all utilities that are globally
1085 : : * available to internal code.
1086 : : */
1087 : : std::unique_ptr<Env> d_env;
1088 : : /**
1089 : : * The state of this SolverEngine, which is responsible for maintaining which
1090 : : * SMT mode we are in, the last result, etc.
1091 : : */
1092 : : std::unique_ptr<smt::SolverEngineState> d_state;
1093 : : /**
1094 : : * The context manager of this SolverEngine, which is responsible for
1095 : : * maintaining which the contexts.
1096 : : */
1097 : : std::unique_ptr<smt::ContextManager> d_ctxManager;
1098 : :
1099 : : /** Resource out listener */
1100 : : std::unique_ptr<smt::ResourceOutListener> d_routListener;
1101 : :
1102 : : /** The SMT solver */
1103 : : std::unique_ptr<smt::SmtSolver> d_smtSolver;
1104 : : /** The SMT solver driver */
1105 : : std::unique_ptr<smt::SmtDriver> d_smtDriver;
1106 : :
1107 : : /**
1108 : : * The utility used for checking models
1109 : : */
1110 : : std::unique_ptr<smt::CheckModels> d_checkModels;
1111 : :
1112 : : /**
1113 : : * The proof manager, which manages all things related to checking,
1114 : : * processing, and printing proofs.
1115 : : */
1116 : : std::unique_ptr<smt::PfManager> d_pfManager;
1117 : :
1118 : : /**
1119 : : * The unsat core manager, which produces unsat cores and related information
1120 : : * from refutations. */
1121 : : std::unique_ptr<smt::UnsatCoreManager> d_ucManager;
1122 : :
1123 : : /** The solver for sygus queries */
1124 : : std::unique_ptr<smt::SygusSolver> d_sygusSolver;
1125 : : /** The solver for find-synth queries */
1126 : : std::unique_ptr<smt::FindSynthSolver> d_findSynthSolver;
1127 : :
1128 : : /** The solver for abduction queries */
1129 : : std::unique_ptr<smt::AbductionSolver> d_abductSolver;
1130 : : /** The solver for interpolation queries */
1131 : : std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
1132 : : /** The solver for quantifier elimination queries */
1133 : : std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
1134 : :
1135 : : /**
1136 : : * The logic set by the user. The actual logic, which may extend the user's
1137 : : * logic, lives in the Env class.
1138 : : */
1139 : : LogicInfo d_userLogic;
1140 : : /** Has the above logic been initialized? */
1141 : : bool d_userLogicSet;
1142 : :
1143 : : /** Have we set a regular option yet? (for --safe-mode) */
1144 : : bool d_safeOptsSetRegularOption;
1145 : : /** The regular option we set (for --safe-mode) */
1146 : : std::string d_safeOptsRegularOption;
1147 : : /** The value of the regular option we set (for --safe-mode) */
1148 : : std::string d_safeOptsRegularOptionValue;
1149 : : /** Was the option already the default setting */
1150 : : bool d_safeOptsSetRegularOptionToDefault;
1151 : :
1152 : : /** Whether this is an internal subsolver. */
1153 : : bool d_isInternalSubsolver;
1154 : :
1155 : : /** The statistics class */
1156 : : std::unique_ptr<smt::SolverEngineStatistics> d_stats;
1157 : : }; /* class SolverEngine */
1158 : :
1159 : : /* -------------------------------------------------------------------------- */
1160 : :
1161 : : } // namespace internal
1162 : : } // namespace cvc5
1163 : :
1164 : : #endif /* CVC5__SMT_ENGINE_H */
|
