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