1 /********************* */
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Andres Noetzli
6 ** This file is part of the CVC4 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.\endverbatim
12 ** \brief The module for storing assertions for an SMT engine.
15 #include "cvc4_private.h"
17 #ifndef CVC4__SMT__ASSERTIONS_H
18 #define CVC4__SMT__ASSERTIONS_H
22 #include "context/cdlist.h"
23 #include "expr/node.h"
24 #include "preprocessing/assertion_pipeline.h"
32 * Contains all information pertaining to the assertions of an SMT engine.
34 * This class is responsible for setting up the assertions pipeline for
35 * check-sat calls. It is *not* responsible for the preprocessing itself, and
36 * instead is intended to be the input to a preprocessor utility.
40 /** The type of our internal assertion list */
41 typedef context::CDList
<Node
> AssertionList
;
44 Assertions(context::UserContext
* u
, AbstractValues
& absv
);
47 * Finish initialization, called once after options are finalized. Sets up
48 * the required bookkeeping based on the options.
52 * Clears out the non-context-dependent data in this class. Necessary to
53 * clear out our assertion vectors in case someone does a push-assert-pop
54 * without a check-sat.
58 * Initialize a call to check satisfiability. This adds assumptions to
59 * the list of assumptions maintained by this class, and finalizes the
60 * set of formulas (in the assertions pipeline) that will be used for the
61 * upcoming check-sat call.
63 * @param assumptions The assumptions of the upcoming check-sat call.
64 * @param inUnsatCore Whether assumptions are in the unsat core.
65 * @param isEntailmentCheck Whether we are checking entailment of assumptions
66 * in the upcoming check-sat call.
68 void initializeCheckSat(const std::vector
<Node
>& assumptions
,
70 bool isEntailmentCheck
);
72 * Add a formula to the current context: preprocess, do per-theory
73 * setup, use processAssertionList(), asserting to T-solver for
74 * literals and conjunction of literals. Returns false if
75 * immediately determined to be inconsistent. This version
76 * takes a Boolean flag to determine whether to include this asserted
77 * formula in an unsat core (if one is later requested).
79 * @throw TypeCheckingException, LogicException, UnsafeInterruptException
81 void assertFormula(const Node
& n
, bool inUnsatCore
= true);
83 * Assert that n corresponds to an assertion from a define-fun-rec command.
84 * This assertion is added to the set of assertions maintained by this class.
85 * If this has a global definition, this assertion is persistent for any
86 * subsequent check-sat calls.
88 void addDefineFunRecDefinition(Node n
, bool global
);
90 * Get the assertions pipeline, which contains the set of assertions we are
91 * currently processing.
93 preprocessing::AssertionPipeline
& getAssertionPipeline();
95 * Get assertions list corresponding to the original list of assertions,
96 * before preprocessing.
98 context::CDList
<Node
>* getAssertionList();
100 * Get the list of assumptions, which are those registered to this class
101 * on initializeCheckSat.
103 std::vector
<Node
>& getAssumptions();
105 * Is the set of assertions globally negated? When this flag is true, the
106 * overall result of check-sat should be inverted.
108 bool isGlobalNegated() const;
109 /** Flip the global negation flag. */
110 void flipGlobalNegated();
112 //------------------------------------ for proofs
113 /** Set proof generator */
114 void setProofGenerator(smt::PreprocessProofGenerator
* pppg
);
115 /** Is proof enabled? */
116 bool isProofEnabled() const;
117 //------------------------------------ end for proofs
120 * Fully type-check the argument, and also type-check that it's
122 * throw@ TypeCheckingException
124 void ensureBoolean(const Node
& n
);
126 * Adds a formula to the current context. Action here depends on
127 * the SimplificationMode (in the current Options scope); the
128 * formula might be pushed out to the propositional layer
129 * immediately, or it might be simplified and kept, or it might not
130 * even be simplified.
131 * The arguments isInput and isAssumption are used for bookkeeping for unsat
133 * The argument maybeHasFv should be set to true if the assertion may have
134 * free variables. By construction, assertions from the smt2 parser are
135 * guaranteed not to have free variables. However, other cases such as
136 * assertions from the SyGuS parser may have free variables (say if the
137 * input contains an assert or define-fun-rec command).
139 * @param isAssumption If true, the formula is considered to be an assumption
140 * (this is used to distinguish assertions and assumptions)
142 void addFormula(TNode n
,
147 /** pointer to the user context */
148 context::UserContext
* d_userContext
;
149 /** Reference to the abstract values utility */
150 AbstractValues
& d_absValues
;
152 * The assertion list (before any conversion) for supporting
153 * getAssertions(). Only maintained if in incremental mode.
155 AssertionList
* d_assertionList
;
157 * List of lemmas generated for global recursive function definitions. We
158 * assert this list of definitions in each check-sat call.
160 std::unique_ptr
<std::vector
<Node
>> d_globalDefineFunRecLemmas
;
162 * The list of assumptions from the previous call to checkSatisfiability.
163 * Note that if the last call to checkSatisfiability was an entailment check,
164 * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains
165 * one single assumption ~(a1 AND ... AND an).
167 std::vector
<Node
> d_assumptions
;
168 /** Whether we did a global negation of the formula. */
169 bool d_globalNegation
;
170 /** Assertions in the preprocessing pipeline */
171 preprocessing::AssertionPipeline d_assertions
;