diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-31 07:23:09 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-31 09:23:09 -0500 |
commit | 6a89ff6d106a012442f0ab3b212dc3d26a758da3 (patch) | |
tree | 9cddb0bcaf6afcd5cee2665a2fa41d02d0635b9d /src/preprocessing/assertion_pipeline.h | |
parent | 1955e4b504e95ed64bc7dcc6b1329eb5b796f565 (diff) |
Record assumption info in AssertionPipeline (#2678)
Diffstat (limited to 'src/preprocessing/assertion_pipeline.h')
-rw-r--r-- | src/preprocessing/assertion_pipeline.h | 31 |
1 files changed, 25 insertions, 6 deletions
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index af7a8dce3..77c5c4582 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -40,15 +40,22 @@ class AssertionPipeline void resize(size_t n) { d_nodes.resize(n); } - void clear() - { - d_nodes.clear(); - d_realAssertionsEnd = 0; - } + /** + * Clear the list of assertions and assumptions. + */ + void clear(); Node& operator[](size_t i) { return d_nodes[i]; } const Node& operator[](size_t i) const { return d_nodes[i]; } - void push_back(Node n) { d_nodes.push_back(n); } + + /** + * Adds an assertion/assumption to be preprocessed. + * + * @param n The assertion/assumption + * @param isAssumption If true, records that \p n is an assumption. Note that + * all assumptions have to be added contiguously. + */ + void push_back(Node n, bool isAssumption = false); std::vector<Node>& ref() { return d_nodes; } const std::vector<Node>& ref() const { return d_nodes; } @@ -80,9 +87,16 @@ class AssertionPipeline size_t getRealAssertionsEnd() const { return d_realAssertionsEnd; } + /** @return The index of the first assumption */ + size_t getAssumptionsStart() const { return d_assumptionsStart; } + + /** @return The number of assumptions */ + size_t getNumAssumptions() const { return d_numAssumptions; } + void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); } private: + /** The list of current assertions */ std::vector<Node> d_nodes; /** @@ -93,6 +107,11 @@ class AssertionPipeline /** Size of d_nodes when preprocessing starts */ size_t d_realAssertionsEnd; + + /** Index of the first assumption */ + size_t d_assumptionsStart; + /** The number of assumptions */ + size_t d_numAssumptions; }; /* class AssertionPipeline */ } // namespace preprocessing |