1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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 * ****************************************************************************
13 * SolverEngine: the main public entry point of libcvc5.
16 #include "cvc5_public.h"
18 #ifndef CVC5__SMT__SOLVER_ENGINE_H
19 #define CVC5__SMT__SOLVER_ENGINE_H
26 #include "context/cdhashmap_forward.h"
27 #include "cvc5_export.h"
28 #include "options/options.h"
29 #include "smt/smt_mode.h"
30 #include "theory/logic_info.h"
31 #include "util/result.h"
35 template <bool ref_count
>
37 typedef NodeTemplate
<true> Node
;
38 typedef NodeTemplate
<false> TNode
;
45 class StatisticsRegistry
;
47 class ResourceManager
;
48 struct InstantiationList
;
50 /* -------------------------------------------------------------------------- */
56 /* -------------------------------------------------------------------------- */
61 } // namespace context
63 /* -------------------------------------------------------------------------- */
65 namespace preprocessing
{
66 class PreprocessingPassContext
;
69 /* -------------------------------------------------------------------------- */
75 /* -------------------------------------------------------------------------- */
79 class SolverEngineState
;
82 class ResourceOutListener
;
83 class SmtNodeManagerListener
;
88 class AbductionSolver
;
89 class InterpolationSolver
;
90 class QuantElimSolver
;
92 struct SolverEngineStatistics
;
93 class SolverEngineScope
;
95 class UnsatCoreManager
;
99 /* -------------------------------------------------------------------------- */
104 class QuantifiersEngine
;
105 } // namespace theory
107 /* -------------------------------------------------------------------------- */
109 class CVC5_EXPORT SolverEngine
111 friend class ::cvc5::api::Solver
;
112 friend class ::cvc5::smt::SolverEngineState
;
113 friend class ::cvc5::smt::SolverEngineScope
;
115 /* ....................................................................... */
117 /* ....................................................................... */
120 * Construct an SolverEngine with the given expression manager.
121 * If provided, optr is a pointer to a set of options that should initialize
122 * the values of the options object owned by this class.
124 SolverEngine(NodeManager
* nm
, const Options
* optr
= nullptr);
125 /** Destruct the SMT engine. */
128 //--------------------------------------------- concerning the state
131 * This is the main initialization procedure of the SolverEngine.
133 * Should be called whenever the final options and logic for the problem are
134 * set (at least, those options that are not permitted to change after
135 * assertions and queries are made).
137 * Internally, this creates the theory engine, prop engine, decision engine,
138 * and other utilities whose initialization depends on the final set of
141 * This post-construction initialization is automatically triggered by the
142 * use of the SolverEngine; e.g. when the first formula is asserted, a call
143 * to simplify() is issued, a scope is pushed, etc.
147 * Return true if this SolverEngine is fully initialized (post-construction)
150 bool isFullyInited() const;
152 * Return true if a checkEntailed() or checkSatisfiability() has been made.
154 bool isQueryMade() const;
155 /** Return the user context level. */
156 size_t getNumUserLevels() const;
157 /** Return the current mode of the solver. */
158 SmtMode
getSmtMode() const;
160 * Whether the SmtMode allows for get-value, get-model, get-assignment, etc.
161 * This is equivalent to:
162 * getSmtMode()==SmtMode::SAT || getSmtMode()==SmtMode::SAT_UNKNOWN
164 bool isSmtModeSat() const;
166 * Returns the most recent result of checkSat/checkEntailed or
167 * (set-info :status).
169 Result
getStatusOfLastCommand() const;
170 //--------------------------------------------- end concerning the state
173 * Set the logic of the script.
174 * @throw ModalException, LogicException
176 void setLogic(const std::string
& logic
);
179 * Set the logic of the script.
180 * @throw ModalException, LogicException
182 void setLogic(const char* logic
);
185 * Set the logic of the script.
186 * @throw ModalException
188 void setLogic(const LogicInfo
& logic
);
190 /** Get the logic information currently set. */
191 const LogicInfo
& getLogicInfo() const;
193 /** Get the logic information set by the user. */
194 LogicInfo
getUserLogicInfo() const;
197 * Set information about the script executing.
199 void setInfo(const std::string
& key
, const std::string
& value
);
201 /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */
202 bool isValidGetInfoFlag(const std::string
& key
) const;
204 /** Query information about the SMT environment. */
205 std::string
getInfo(const std::string
& key
) const;
208 * Set an aspect of the current SMT execution environment.
209 * @throw OptionException, ModalException
211 void setOption(const std::string
& key
, const std::string
& value
);
213 /** Set is internal subsolver.
215 * This function is called on SolverEngine objects that are created
216 * internally. It is used to mark that this SolverEngine should not
217 * perform preprocessing passes that rephrase the input, such as
218 * --sygus-rr-synth-input or
221 void setIsInternalSubsolver();
222 /** Is this an internal subsolver? */
223 bool isInternalSubsolver() const;
226 * Block the current model. Can be called only if immediately preceded by
227 * a SAT or INVALID query. Only permitted if produce-models is on, and the
228 * block-models option is set to a mode other than "none".
230 * This adds an assertion to the assertion stack that blocks the current
231 * model based on the current options configured by cvc5.
233 * The return value has the same meaning as that of assertFormula.
238 * Block the current model values of (at least) the values in exprs.
239 * Can be called only if immediately preceded by a SAT or NOT_ENTAILED query.
240 * Only permitted if produce-models is on, and the block-models option is set
241 * to a mode other than "none".
243 * This adds an assertion to the assertion stack of the form:
244 * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
245 * where M0 ... Mn are the current model values of exprs[0] ... exprs[n].
247 * The return value has the same meaning as that of assertFormula.
249 Result
blockModelValues(const std::vector
<Node
>& exprs
);
252 * Declare heap. For smt2 inputs, this is called when the command
253 * (declare-heap (locT datat)) is invoked by the user. This sets locT as the
254 * location type and dataT is the data type for the heap. This command should
255 * be executed only once, and must be invoked before solving separation logic
258 void declareSepHeap(TypeNode locT
, TypeNode dataT
);
261 * Get the separation heap types, which extracts which types were passed to
264 * @return true if the separation logic heap types have been declared.
266 bool getSepHeapTypes(TypeNode
& locT
, TypeNode
& dataT
);
268 /** When using separation logic, obtain the expression for the heap. */
269 Node
getSepHeapExpr();
271 /** When using separation logic, obtain the expression for nil. */
272 Node
getSepNilExpr();
275 * Get an aspect of the current SMT execution environment.
276 * @throw OptionException
278 std::string
getOption(const std::string
& key
) const;
281 * Define function func in the current context to be:
282 * (lambda (formals) formula)
283 * This adds func to the list of defined functions, which indicates that
284 * all occurrences of func should be expanded during expandDefinitions.
286 * @param func a variable of function type that expects the arguments in
288 * @param formals a list of BOUND_VARIABLE expressions
289 * @param formula The body of the function, must not contain func
290 * @param global True if this definition is global (i.e. should persist when
291 * popping the user context)
293 void defineFunction(Node func
,
294 const std::vector
<Node
>& formals
,
296 bool global
= false);
299 * Define functions recursive
301 * For each i, this constrains funcs[i] in the current context to be:
302 * (lambda (formals[i]) formulas[i])
303 * where formulas[i] may contain variables from funcs. Unlike defineFunction
304 * above, we do not add funcs[i] to the set of defined functions. Instead,
305 * we consider funcs[i] to be a free uninterpreted function, and add:
306 * forall formals[i]. f(formals[i]) = formulas[i]
307 * to the set of assertions in the current context.
308 * This method expects input such that for each i:
309 * - func[i] : a variable of function type that expects the arguments in
311 * - formals[i] : a list of BOUND_VARIABLE expressions.
313 * @param global True if this definition is global (i.e. should persist when
314 * popping the user context)
316 void defineFunctionsRec(const std::vector
<Node
>& funcs
,
317 const std::vector
<std::vector
<Node
>>& formals
,
318 const std::vector
<Node
>& formulas
,
319 bool global
= false);
321 * Define function recursive
322 * Same as above, but for a single function.
324 void defineFunctionRec(Node func
,
325 const std::vector
<Node
>& formals
,
327 bool global
= false);
329 * Add a formula to the current context: preprocess, do per-theory
330 * setup, use processAssertionList(), asserting to T-solver for
331 * literals and conjunction of literals. Returns false if
332 * immediately determined to be inconsistent. Note this formula will
333 * be included in the unsat core when applicable.
335 * @throw TypeCheckingException, LogicException, UnsafeInterruptException
337 Result
assertFormula(const Node
& formula
);
340 * Reduce an unsatisfiable core to make it minimal.
342 std::vector
<Node
> reduceUnsatCore(const std::vector
<Node
>& core
);
345 * Check if a given (set of) expression(s) is entailed with respect to the
346 * current set of assertions. We check this by asserting the negation of
347 * the (big AND over the) given (set of) expression(s).
348 * Returns ENTAILED, NOT_ENTAILED, or ENTAILMENT_UNKNOWN result.
352 Result
checkEntailed(const Node
& assumption
);
353 Result
checkEntailed(const std::vector
<Node
>& assumptions
);
356 * Assert a formula (if provided) to the current context and call
357 * check(). Returns SAT, UNSAT, or SAT_UNKNOWN result.
362 Result
checkSat(const Node
& assumption
);
363 Result
checkSat(const std::vector
<Node
>& assumptions
);
366 * Returns a set of so-called "failed" assumptions.
368 * The returned set is a subset of the set of assumptions of a previous
369 * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability
370 * with this set of failed assumptions still produces an unsat answer.
372 * Note that the returned set of failed assumptions is not necessarily
375 std::vector
<Node
> getUnsatAssumptions(void);
377 /*---------------------------- sygus commands ---------------------------*/
380 * Add sygus variable declaration.
382 * Declared SyGuS variables may be used in SyGuS constraints, in which they
383 * are assumed to be universally quantified.
385 * In SyGuS semantics, declared functions are treated in the same manner as
386 * declared variables, i.e. as universally quantified (function) variables
387 * which can occur in the SyGuS constraints that compose the conjecture to
388 * which a function is being synthesized. Thus declared functions should use
389 * this method as well.
391 void declareSygusVar(Node var
);
394 * Add a function-to-synthesize declaration.
396 * The given sygusType may not correspond to the actual function type of func
397 * but to a datatype encoding the syntax restrictions for the
398 * function-to-synthesize. In this case this information is stored to be used
401 * vars contains the arguments of the function-to-synthesize. These variables
402 * are also stored to be used during solving.
404 * isInv determines whether the function-to-synthesize is actually an
405 * invariant. This information is necessary if we are dumping a command
406 * corresponding to this declaration, so that it can be properly printed.
408 void declareSynthFun(Node func
,
411 const std::vector
<Node
>& vars
);
413 * Same as above, without a sygus type.
415 void declareSynthFun(Node func
, bool isInv
, const std::vector
<Node
>& vars
);
418 * Add a regular sygus constraint or assumption.
419 * @param n The formula
420 * @param isAssume True if n is an assumption.
422 void assertSygusConstraint(Node n
, bool isAssume
= false);
425 * Add an invariant constraint.
427 * Invariant constraints are not explicitly declared: they are given in terms
428 * of the invariant-to-synthesize, the pre condition, transition relation and
429 * post condition. The actual constraint is built based on the inputs of these
430 * place holder predicates :
433 * INV() ^ TRANS(x, x') -> INV(x')
436 * The regular and primed variables are retrieved from the declaration of the
437 * invariant-to-synthesize.
439 void assertSygusInvConstraint(Node inv
, Node pre
, Node trans
, Node post
);
441 * Assert a synthesis conjecture to the current context and call
442 * check(). Returns sat, unsat, or unknown result.
444 * The actual synthesis conjecture is built based on the previously
445 * communicated information to this module (universal variables, defined
446 * functions, functions-to-synthesize, and which constraints compose it). The
447 * built conjecture is a higher-order formula of the form
449 * exists f1...fn . forall v1...vm . F
451 * in which f1...fn are the functions-to-synthesize, v1...vm are the declared
452 * universal variables and F is the set of declared constraints.
454 * @param isNext Whether we are asking for the next synthesis solution (if
455 * using incremental).
459 Result
checkSynth(bool isNext
= false);
461 /*------------------------- end of sygus commands ------------------------*/
464 * Declare pool whose initial value is the terms in initValue. A pool is
465 * a variable of type (Set T) that is used in quantifier annotations and does
466 * not occur in constraints.
468 * @param p The pool to declare, which should be a variable of type (Set T)
470 * @param initValue The initial value of p, which should be a vector of terms
473 void declarePool(const Node
& p
, const std::vector
<Node
>& initValue
);
475 * Simplify a formula without doing "much" work. Does not involve
476 * the SAT Engine in the simplification, but uses the current
477 * definitions, assertions, and the current partial model, if one
478 * has been constructed. It also involves theory normalization.
480 * @throw TypeCheckingException, LogicException, UnsafeInterruptException
482 * @todo (design) is this meant to give an equivalent or an
483 * equisatisfiable formula?
485 Node
simplify(const Node
& e
);
488 * Expand the definitions in a term or formula.
490 * @param n The node to expand
492 * @throw TypeCheckingException, LogicException, UnsafeInterruptException
494 Node
expandDefinitions(const Node
& n
);
497 * Get the assigned value of an expr (only if immediately preceded by a SAT
498 * or NOT_ENTAILED query). Only permitted if the SolverEngine is set to
499 * operate interactively and produce-models is on.
501 * @throw ModalException, TypeCheckingException, LogicException,
502 * UnsafeInterruptException
504 Node
getValue(const Node
& e
) const;
507 * Same as getValue but for a vector of expressions
509 std::vector
<Node
> getValues(const std::vector
<Node
>& exprs
) const;
512 * @return the domain elements for uninterpreted sort tn.
514 std::vector
<Node
> getModelDomainElements(TypeNode tn
) const;
517 * @return true if v is a model core symbol
519 bool isModelCoreSymbol(Node v
);
522 * Get a model (only if immediately preceded by an SAT or unknown query).
523 * Only permitted if the model option is on.
525 * @param declaredSorts The sorts to print in the model
526 * @param declaredFuns The free constants to print in the model. A subset
527 * of these may be printed based on isModelCoreSymbol.
528 * @return the string corresponding to the model. If the output language is
529 * smt2, then this corresponds to a response to the get-model command.
531 std::string
getModel(const std::vector
<TypeNode
>& declaredSorts
,
532 const std::vector
<Node
>& declaredFuns
);
534 /** print instantiations
536 * Print all instantiations for all quantified formulas on out,
537 * returns true if at least one instantiation was printed. The type of output
538 * (list, num, etc.) is determined by printInstMode.
540 void printInstantiations(std::ostream
& out
);
542 * Print the current proof. This method should be called after an UNSAT
543 * response. It gets the proof of false from the PropEngine and passes
544 * it to the ProofManager, which post-processes the proof and prints it
545 * in the proper format.
550 * Get synth solution.
552 * This method returns true if we are in a state immediately preceded by
553 * a successful call to checkSynth.
555 * This method adds entries to solMap that map functions-to-synthesize with
556 * their solutions, for all active conjectures. This should be called
557 * immediately after the solver answers unsat for sygus input.
559 * Specifically, given a sygus conjecture of the form
560 * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn )
561 * where x1...xn are second order bound variables, we map each xi to
562 * lambda term in solMap such that
563 * forall y1...yn. P( solMap[x1]...solMap[xn], y1...yn )
564 * is a valid formula.
566 bool getSynthSolutions(std::map
<Node
, Node
>& solMap
);
568 * Same as above, but used for getting synthesis solutions from a "subsolver"
569 * that has been initialized to assert the synthesis conjecture as a
572 * This method returns true if we are in a state immediately preceded by
573 * a successful call to checkSat, where this SolverEngine has an asserted
574 * synthesis conjecture.
576 bool getSubsolverSynthSolutions(std::map
<Node
, Node
>& solMap
);
579 * Do quantifier elimination.
581 * This function takes as input a quantified formula q
583 * Q x1...xn. P( x1...xn, y1...yn )
584 * where P( x1...xn, y1...yn ) is a quantifier-free
585 * formula in a logic that supports quantifier elimination.
586 * Currently, the only logics supported by quantifier
587 * elimination is LRA and LIA.
589 * This function returns a formula ret such that, given
590 * the current set of formulas A asserted to this SolverEngine :
592 * If doFull = true, then
593 * - ( A ^ q ) and ( A ^ ret ) are equivalent
594 * - ret is quantifier-free formula containing
595 * only free variables in y1...yn.
597 * If doFull = false, then
598 * - (A ^ q) => (A ^ ret) if Q is forall or
599 * (A ^ ret) => (A ^ q) if Q is exists,
600 * - ret is quantifier-free formula containing
601 * only free variables in y1...yn,
602 * - If Q is exists, let A^Q_n be the formula
603 * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
604 * where for each i=1,...n, formula ret^Q_i
605 * is the result of calling doQuantifierElimination
606 * for q with the set of assertions A^Q_{i-1}.
607 * Similarly, if Q is forall, then let A^Q_n be
608 * A ^ ret^Q_1 ^ ... ^ ret^Q_n
609 * where ret^Q_i is the same as above.
610 * In either case, we have that ret^Q_j will
611 * eventually be true or false, for some finite j.
613 * The former feature is quantifier elimination, and
614 * is run on invocations of the smt2 extended command get-qe.
615 * The latter feature is referred to as partial quantifier
616 * elimination, and is run on invocations of the smt2
617 * extended command get-qe-disjunct, which can be used
618 * for incrementally computing the result of a
619 * quantifier elimination.
621 * The argument strict is whether to output
622 * warnings, such as when an unexpected logic is used.
626 Node
getQuantifierElimination(Node q
, bool doFull
, bool strict
= true);
629 * This method asks this SMT engine to find an interpolant with respect to
630 * the current assertion stack (call it A) and the conjecture (call it B). If
631 * this method returns true, then interpolant is set to a formula I such that
632 * A ^ ~I and I ^ ~B are both unsatisfiable.
634 * The argument grammarType is a sygus datatype type that encodes the syntax
635 * restrictions on the shapes of possible solutions.
637 * This method invokes a separate copy of the SMT engine for solving the
638 * corresponding sygus problem for generating such a solution.
640 bool getInterpol(const Node
& conj
,
641 const TypeNode
& grammarType
,
644 /** Same as above, but without user-provided grammar restrictions */
645 bool getInterpol(const Node
& conj
, Node
& interpol
);
648 * This method asks this SMT engine to find an abduct with respect to the
649 * current assertion stack (call it A) and the conjecture (call it B).
650 * If this method returns true, then abd is set to a formula C such that
651 * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
653 * The argument grammarType is a sygus datatype type that encodes the syntax
654 * restrictions on the shape of possible solutions.
656 * This method invokes a separate copy of the SMT engine for solving the
657 * corresponding sygus problem for generating such a solution.
659 bool getAbduct(const Node
& conj
, const TypeNode
& grammarType
, Node
& abd
);
662 * Get next abduct. This can only be called immediately after a successful
663 * call to getAbduct or getAbductNext.
665 * Returns true if an abduct was found, and sets abd to the abduct.
667 bool getAbductNext(Node
& abd
);
670 * Get list of quantified formulas that were instantiated on the last call
673 void getInstantiatedQuantifiedFormulas(std::vector
<Node
>& qs
);
676 * Get instantiation term vectors for quantified formula q.
678 * This method is similar to above, but in the example above, we return the
679 * (vectors of) terms t1, ..., tn instead.
681 * Notice that these are not guaranteed to come in the same order as the
682 * instantiation lemmas above.
684 void getInstantiationTermVectors(Node q
,
685 std::vector
<std::vector
<Node
>>& tvecs
);
687 * As above but only the instantiations that were relevant for the
690 void getRelevantInstantiationTermVectors(
691 std::map
<Node
, InstantiationList
>& insts
, bool getDebugInfo
= false);
693 * Get instantiation term vectors, which maps each instantiated quantified
694 * formula to the list of instantiations for that quantified formula. This
695 * list is minimized if proofs are enabled, and this call is immediately
696 * preceded by an UNSAT or ENTAILED query
698 void getInstantiationTermVectors(
699 std::map
<Node
, std::vector
<std::vector
<Node
>>>& insts
);
702 * Get an unsatisfiable core (only if immediately preceded by an UNSAT or
703 * ENTAILED query). Only permitted if cvc5 was built with unsat-core support
704 * and produce-unsat-cores is on.
706 UnsatCore
getUnsatCore();
709 * Get a refutation proof (only if immediately preceded by an UNSAT or
710 * ENTAILED query). Only permitted if cvc5 was built with proof support and
711 * the proof option is on. */
712 std::string
getProof();
715 * Get the current set of assertions. Only permitted if the
716 * SolverEngine is set to operate interactively.
718 std::vector
<Node
> getAssertions();
721 * Get difficulty map, which populates dmap, mapping input assertions
722 * to a value that estimates their difficulty for solving the current problem.
724 void getDifficultyMap(std::map
<Node
, Node
>& dmap
);
727 * Push a user-level context.
728 * throw@ ModalException, LogicException, UnsafeInterruptException
733 * Pop a user-level context. Throws an exception if nothing to pop.
734 * @throw ModalException
738 /** Reset all assertions, global declarations, etc. */
739 void resetAssertions();
742 * Interrupt a running query. This can be called from another thread
743 * or from a signal handler. Throws a ModalException if the SolverEngine
744 * isn't currently in a query.
746 * @throw ModalException
751 * Set a resource limit for SolverEngine operations. This is like a time
752 * limit, but it's deterministic so that reproducible results can be
753 * obtained. Currently, it's based on the number of conflicts.
754 * However, please note that the definition may change between different
755 * versions of cvc5 (as may the number of conflicts required, anyway),
756 * and it might even be different between instances of the same version
757 * of cvc5 on different platforms.
759 * A cumulative and non-cumulative (per-call) resource limit can be
760 * set at the same time. A call to setResourceLimit() with
761 * cumulative==true replaces any cumulative resource limit currently
762 * in effect; a call with cumulative==false replaces any per-call
763 * resource limit currently in effect. Time limits can be set in
764 * addition to resource limits; the SolverEngine obeys both. That means
765 * that up to four independent limits can control the SolverEngine
768 * When an SolverEngine is first created, it has no time or resource
771 * Currently, these limits only cause the SolverEngine to stop what its
772 * doing when the limit expires (or very shortly thereafter); no
773 * heuristics are altered by the limits or the threat of them expiring.
774 * We reserve the right to change this in the future.
776 * @param units the resource limit, or 0 for no limit
777 * @param cumulative whether this resource limit is to be a cumulative
778 * resource limit for all remaining calls into the SolverEngine (true), or
779 * whether it's a per-call resource limit (false); the default is false
781 void setResourceLimit(uint64_t units
, bool cumulative
= false);
784 * Set a per-call time limit for SolverEngine operations.
786 * A per-call time limit can be set at the same time and replaces
787 * any per-call time limit currently in effect.
788 * Resource limits (either per-call or cumulative) can be set in
789 * addition to a time limit; the SolverEngine obeys all three of them.
791 * Note that the per-call timer only ticks away when one of the
792 * SolverEngine's workhorse functions (things like assertFormula(),
793 * checkEntailed(), checkSat(), and simplify()) are running.
794 * Between calls, the timer is still.
796 * When an SolverEngine is first created, it has no time or resource
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.
804 * @param millis the time limit in milliseconds, or 0 for no limit
806 void setTimeLimit(uint64_t millis
);
809 * Get the current resource usage count for this SolverEngine. This
810 * function can be used to ascertain reasonable values to pass as
811 * resource limits to setResourceLimit().
813 unsigned long getResourceUsage() const;
815 /** Get the current millisecond count for this SolverEngine. */
816 unsigned long getTimeUsage() const;
819 * Get the remaining resources that can be consumed by this SolverEngine
820 * according to the currently-set cumulative resource limit. If there
821 * is not a cumulative resource limit set, this function throws a
824 * @throw ModalException
826 unsigned long getResourceRemaining() const;
828 /** Permit access to the underlying NodeManager. */
829 NodeManager
* getNodeManager() const;
832 * Print statistics from the statistics registry in the env object owned by
833 * this SolverEngine. Safe to use in a signal handler.
835 void printStatisticsSafe(int fd
) const;
838 * Print the changes to the statistics from the statistics registry in the
839 * env object owned by this SolverEngine since this method was called the last
840 * time. Internally prints the diff and then stores a snapshot for the next
843 void printStatisticsDiff() const;
845 /** Get the options object (const and non-const versions) */
846 Options
& getOptions();
847 const Options
& getOptions() const;
849 /** Get a pointer to the UserContext owned by this SolverEngine. */
850 context::UserContext
* getUserContext();
852 /** Get a pointer to the Context owned by this SolverEngine. */
853 context::Context
* getContext();
855 /** Get a pointer to the TheoryEngine owned by this SolverEngine. */
856 TheoryEngine
* getTheoryEngine();
858 /** Get a pointer to the PropEngine owned by this SolverEngine. */
859 prop::PropEngine
* getPropEngine();
861 /** Get the resource manager of this SMT engine */
862 ResourceManager
* getResourceManager() const;
864 /** Get the printer used by this SMT engine */
865 const Printer
& getPrinter() const;
867 /** Get a pointer to the Rewriter owned by this SolverEngine. */
868 theory::Rewriter
* getRewriter();
870 * Get expanded assertions.
872 * Return the set of assertions, after expanding definitions.
874 std::vector
<Node
> getExpandedAssertions();
877 * !!!!! temporary, until the environment is passsed to all classes that
881 /* ....................................................................... */
883 /* ....................................................................... */
885 // disallow copy/assignment
886 SolverEngine(const SolverEngine
&) = delete;
887 SolverEngine
& operator=(const SolverEngine
&) = delete;
889 /** Set solver instance that owns this SolverEngine. */
890 void setSolver(api::Solver
* solver
) { d_solver
= solver
; }
892 /** Get a pointer to the (new) PfManager owned by this SolverEngine. */
893 smt::PfManager
* getPfManager() { return d_pfManager
.get(); };
895 /** Get a pointer to the StatisticsRegistry owned by this SolverEngine. */
896 StatisticsRegistry
& getStatisticsRegistry();
899 * Internal method to get an unsatisfiable core (only if immediately preceded
900 * by an UNSAT or ENTAILED query). Only permitted if cvc5 was built with
901 * unsat-core support and produce-unsat-cores is on. Does not dump the
904 UnsatCore
getUnsatCoreInternal();
907 * Check that a generated proof checks. This method is the same as printProof,
908 * but does not print the proof. Like that method, it should be called
909 * after an UNSAT response. It ensures that a well-formed proof of false
910 * can be constructed by the combination of the PropEngine and ProofManager.
915 * Check that an unsatisfiable core is indeed unsatisfiable.
917 void checkUnsatCore();
920 * Check that a generated Model (via getModel()) actually satisfies
921 * all user assertions.
923 void checkModel(bool hardFailure
= true);
926 * Check that a solution to an interpolation problem is indeed a solution.
928 * The check is made by determining that the assertions imply the solution of
929 * the interpolation problem (interpol), and the solution implies the goal
930 * (conj). If these criteria are not met, an internal error is thrown.
932 void checkInterpol(Node interpol
,
933 const std::vector
<Node
>& easserts
,
937 * This is called by the destructor, just before destroying the
938 * PropEngine, TheoryEngine, and DecisionEngine (in that order). It
939 * is important because there are destruction ordering issues
940 * between PropEngine and Theory.
945 * Quick check of consistency in current context: calls
946 * processAssertionList() then look for inconsistency (based only on
952 * Get the (SMT-level) model pointer, if we are in SAT mode. Otherwise,
955 * This ensures that the underlying theory model of the SmtSolver maintained
956 * by this class is currently available, which means that cvc5 is producing
957 * models, and is in "SAT mode", otherwise a recoverable exception is thrown.
959 * @param c used for giving an error message to indicate the context
960 * this method was called.
962 theory::TheoryModel
* getAvailableModel(const char* c
) const;
964 * Get available quantifiers engine, which throws a modal exception if it
965 * does not exist. This can happen if a quantifiers-specific call (e.g.
966 * getInstantiatedQuantifiedFormulas) is called in a non-quantified logic.
968 * @param c used for giving an error message to indicate the context
969 * this method was called.
971 theory::QuantifiersEngine
* getAvailableQuantifiersEngine(const char* c
) const;
973 // --------------------------------------- callbacks from the state
975 * Notify push pre, which is called just before the user context of the state
976 * pushes. This processes all pending assertions.
978 void notifyPushPre();
980 * Notify push post, which is called just after the user context of the state
981 * pushes. This performs a push on the underlying prop engine.
983 void notifyPushPost();
985 * Notify pop pre, which is called just before the user context of the state
986 * pops. This performs a pop on the underlying prop engine.
990 * Notify post solve pre, which is called once per check-sat query. It
991 * is triggered when the first d_state.doPendingPops() is issued after the
992 * check-sat. This method is called before the contexts pop in the method
995 void notifyPostSolvePre();
997 * Same as above, but after contexts are popped. This calls the postsolve
998 * method of the underlying TheoryEngine.
1000 void notifyPostSolvePost();
1001 // --------------------------------------- end callbacks from the state
1004 * Internally handle the setting of a logic. This function should always
1005 * be called when d_logic is updated.
1007 void setLogicInternal();
1010 * Check satisfiability (used to check satisfiability and entailment).
1012 Result
checkSatInternal(const std::vector
<Node
>& assumptions
,
1013 bool isEntailmentCheck
);
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.
1020 void debugCheckFormals(const std::vector
<Node
>& formals
, Node func
);
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.
1027 void debugCheckFunctionBody(Node formula
,
1028 const std::vector
<Node
>& formals
,
1032 * Helper method to obtain both the heap and nil from the solver. Returns a
1033 * std::pair where the first element is the heap expression and the second
1034 * element is the nil expression.
1036 std::pair
<Node
, Node
> getSepHeapAndNilExpr();
1038 * Get assertions internal, which is only called after initialization. This
1039 * should be used internally to get the assertions instead of getAssertions
1040 * or getExpandedAssertions, which may trigger initialization and SMT state
1043 std::vector
<Node
> getAssertionsInternal();
1046 * Return a reference to options like for `EnvObj`.
1048 const Options
& options() const;
1050 /* Members -------------------------------------------------------------- */
1052 /** Solver instance that owns this SolverEngine instance. */
1053 api::Solver
* d_solver
= nullptr;
1056 * The environment object, which contains all utilities that are globally
1057 * available to internal code.
1059 std::unique_ptr
<Env
> d_env
;
1061 * The state of this SolverEngine, which is responsible for maintaining which
1062 * SMT mode we are in, the contexts, the last result, etc.
1064 std::unique_ptr
<smt::SolverEngineState
> d_state
;
1066 /** Abstract values */
1067 std::unique_ptr
<smt::AbstractValues
> d_absValues
;
1068 /** Assertions manager */
1069 std::unique_ptr
<smt::Assertions
> d_asserts
;
1070 /** Resource out listener */
1071 std::unique_ptr
<smt::ResourceOutListener
> d_routListener
;
1073 /** The SMT solver */
1074 std::unique_ptr
<smt::SmtSolver
> d_smtSolver
;
1077 * The utility used for checking models
1079 std::unique_ptr
<smt::CheckModels
> d_checkModels
;
1082 * The proof manager, which manages all things related to checking,
1083 * processing, and printing proofs.
1085 std::unique_ptr
<smt::PfManager
> d_pfManager
;
1088 * The unsat core manager, which produces unsat cores and related information
1089 * from refutations. */
1090 std::unique_ptr
<smt::UnsatCoreManager
> d_ucManager
;
1092 /** The solver for sygus queries */
1093 std::unique_ptr
<smt::SygusSolver
> d_sygusSolver
;
1095 /** The solver for abduction queries */
1096 std::unique_ptr
<smt::AbductionSolver
> d_abductSolver
;
1097 /** The solver for interpolation queries */
1098 std::unique_ptr
<smt::InterpolationSolver
> d_interpolSolver
;
1099 /** The solver for quantifier elimination queries */
1100 std::unique_ptr
<smt::QuantElimSolver
> d_quantElimSolver
;
1103 * The logic set by the user. The actual logic, which may extend the user's
1104 * logic, lives in the Env class.
1106 LogicInfo d_userLogic
;
1108 /** Whether this is an internal subsolver. */
1109 bool d_isInternalSubsolver
;
1111 /** The statistics class */
1112 std::unique_ptr
<smt::SolverEngineStatistics
> d_stats
;
1115 * The global scope object. Upon creation of this SolverEngine, it becomes the
1116 * SolverEngine in scope. It says the SolverEngine in scope until it is
1117 * destructed, or another SolverEngine is created.
1119 std::unique_ptr
<smt::SolverEngineScope
> d_scope
;
1120 }; /* class SolverEngine */
1122 /* -------------------------------------------------------------------------- */
1126 #endif /* CVC5__SMT_ENGINE_H */