1 /********************* */
2 /*! \file assertion_pipeline.h
4 ** Top contributors (to current version):
5 ** Andres Noetzli, Andrew Reynolds, Justin Xu
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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 AssertionPipeline stores a list of assertions modified by
13 ** preprocessing passes
16 #include "cvc4_private.h"
18 #ifndef CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
19 #define CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
23 #include "expr/node.h"
24 #include "expr/proof_generator.h"
25 #include "expr/proof_node_manager.h"
26 #include "smt/preprocess_proof_generator.h"
27 #include "smt/term_formula_removal.h"
28 #include "theory/trust_node.h"
31 namespace preprocessing
{
34 * Assertion Pipeline stores a list of assertions modified by preprocessing
35 * passes. It is assumed that all assertions after d_realAssertionsEnd were
36 * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
38 class AssertionPipeline
43 size_t size() const { return d_nodes
.size(); }
45 void resize(size_t n
) { d_nodes
.resize(n
); }
48 * Clear the list of assertions and assumptions.
52 const Node
& operator[](size_t i
) const { return d_nodes
[i
]; }
55 * Adds an assertion/assumption to be preprocessed.
57 * @param n The assertion/assumption
58 * @param isAssumption If true, records that \p n is an assumption. Note that
59 * all assumptions have to be added contiguously.
60 * @param isInput If true, n is an input formula (an assumption in the main
61 * body of the overall proof).
62 * @param pg The proof generator who can provide a proof of n. The proof
63 * generator is not required and is ignored if isInput is true.
65 void push_back(Node n
,
66 bool isAssumption
= false,
68 ProofGenerator
* pg
= nullptr);
69 /** Same as above, with TrustNode */
70 void pushBackTrusted(theory::TrustNode trn
);
73 * Get the constant reference to the underlying assertions. It is only
74 * possible to modify these via the replace methods below.
76 const std::vector
<Node
>& ref() const { return d_nodes
; }
78 std::vector
<Node
>::const_iterator
begin() const { return d_nodes
.cbegin(); }
79 std::vector
<Node
>::const_iterator
end() const { return d_nodes
.cend(); }
82 * Replaces assertion i with node n and records the dependency between the
83 * original assertion and its replacement.
85 * @param i The position of the assertion to replace.
86 * @param n The replacement assertion.
87 * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
88 * where d_nodes[i] is the assertion at position i prior to this call.
90 void replace(size_t i
, Node n
, ProofGenerator
* pg
= nullptr);
91 /** Same as above, with TrustNode */
92 void replaceTrusted(size_t i
, theory::TrustNode trn
);
94 IteSkolemMap
& getIteSkolemMap() { return d_iteSkolemMap
; }
95 const IteSkolemMap
& getIteSkolemMap() const { return d_iteSkolemMap
; }
97 size_t getRealAssertionsEnd() const { return d_realAssertionsEnd
; }
99 /** @return The index of the first assumption */
100 size_t getAssumptionsStart() const { return d_assumptionsStart
; }
102 /** @return The number of assumptions */
103 size_t getNumAssumptions() const { return d_numAssumptions
; }
105 void updateRealAssertionsEnd() { d_realAssertionsEnd
= d_nodes
.size(); }
108 * Returns true if substitutions must be stored as assertions. This is for
109 * example the case when we do incremental solving.
111 bool storeSubstsInAsserts() { return d_storeSubstsInAsserts
; }
114 * Enables storing substitutions as assertions.
116 void enableStoreSubstsInAsserts();
119 * Disables storing substitutions as assertions.
121 void disableStoreSubstsInAsserts();
124 * Adds a substitution node of the form (= lhs rhs) to the assertions.
125 * This conjoins n to assertions at a distinguished index given by
128 * @param n The substitution node
129 * @param pg The proof generator that can provide a proof of n.
131 void addSubstitutionNode(Node n
, ProofGenerator
* pg
= nullptr);
134 * Conjoin n to the assertion vector at position i. This replaces
135 * d_nodes[i] with the rewritten form of (AND d_nodes[i] n).
137 * @param i The assertion to replace
138 * @param n The formula to conjoin at position i
139 * @param pg The proof generator that can provide a proof of n
141 void conjoin(size_t i
, Node n
, ProofGenerator
* pg
= nullptr);
144 * Checks whether the assertion at a given index represents substitutions.
146 * @param i The index in question
148 bool isSubstsIndex(size_t i
)
150 return d_storeSubstsInAsserts
&& i
== d_substsIndex
;
152 //------------------------------------ for proofs
153 /** Set proof generator */
154 void setProofGenerator(smt::PreprocessProofGenerator
* pppg
);
155 /** Is proof enabled? */
156 bool isProofEnabled() const;
157 //------------------------------------ end for proofs
159 /** The list of current assertions */
160 std::vector
<Node
> d_nodes
;
163 * Map from skolem variables to index in d_assertions containing
164 * corresponding introduced Boolean ite
166 IteSkolemMap d_iteSkolemMap
;
168 /** Size of d_nodes when preprocessing starts */
169 size_t d_realAssertionsEnd
;
172 * If true, we store the substitutions as assertions. This is necessary when
173 * doing incremental solving because we cannot apply them to existing
174 * assertions while preprocessing new assertions.
176 bool d_storeSubstsInAsserts
;
179 * The index of the assertions that holds the substitutions.
181 * TODO(#2473): replace by separate vector of substitution assertions.
183 size_t d_substsIndex
;
185 /** Index of the first assumption */
186 size_t d_assumptionsStart
;
187 /** The number of assumptions */
188 size_t d_numAssumptions
;
189 /** The proof generator, if one is provided */
190 smt::PreprocessProofGenerator
* d_pppg
;
191 }; /* class AssertionPipeline */
193 } // namespace preprocessing
196 #endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */