From 6a89ff6d106a012442f0ab3b212dc3d26a758da3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 31 Oct 2018 07:23:09 -0700 Subject: [PATCH] Record assumption info in AssertionPipeline (#2678) --- src/preprocessing/assertion_pipeline.cpp | 31 +++++++++++++++++++++++- src/preprocessing/assertion_pipeline.h | 31 +++++++++++++++++++----- src/smt/smt_engine.cpp | 25 ++++++++++++++----- 3 files changed, 74 insertions(+), 13 deletions(-) diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 0bce3b8cd..7d4351baa 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -22,7 +22,36 @@ namespace CVC4 { namespace preprocessing { -AssertionPipeline::AssertionPipeline() : d_realAssertionsEnd(0) {} +AssertionPipeline::AssertionPipeline() + : d_realAssertionsEnd(0), d_assumptionsStart(0), d_numAssumptions(0) +{ +} + +void AssertionPipeline::clear() +{ + d_nodes.clear(); + d_realAssertionsEnd = 0; + d_assumptionsStart = 0; + d_numAssumptions = 0; +} + +void AssertionPipeline::push_back(Node n, bool isAssumption) +{ + d_nodes.push_back(n); + if (isAssumption) + { + if (d_numAssumptions == 0) + { + d_assumptionsStart = d_nodes.size() - 1; + } + // Currently, we assume that assumptions are all added one after another + // and that we store them in the same vector as the assertions. Once we + // split the assertions up into multiple vectors (see issue #2473), we will + // not have this limitation anymore. + Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1); + d_numAssumptions++; + } +} void AssertionPipeline::replace(size_t i, Node n) { 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& ref() { return d_nodes; } const std::vector& 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 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9a0d969d8..cb7766c2d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -756,8 +756,14 @@ class SmtEnginePrivate : public NodeManagerListener { * immediately, or it might be simplified and kept, or it might not * even be simplified. * the 2nd and 3rd arguments added for bookkeeping for proofs + * + * @param isAssumption If true, the formula is considered to be an assumption + * (this is used to distinguish assertions and assumptions) */ - void addFormula(TNode n, bool inUnsatCore, bool inInput = true); + void addFormula(TNode n, + bool inUnsatCore, + bool inInput = true, + bool isAssumption = false); /** Expand definitions in n. */ Node expandDefinitions(TNode n, @@ -3071,7 +3077,8 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl; Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + Debug("smt") << "#Assertions : " << d_assertions.size() << endl; + Debug("smt") << "#Assumptions: " << d_assertions.getNumAssumptions() << endl; if (d_assertions.size() == 0) { // nothing to do @@ -3450,14 +3457,20 @@ void SmtEnginePrivate::processAssertions() { getIteSkolemMap().clear(); } -void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) +void SmtEnginePrivate::addFormula(TNode n, + bool inUnsatCore, + bool inInput, + bool isAssumption) { if (n == d_true) { // nothing to do return; } - Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl; + Trace("smt") << "SmtEnginePrivate::addFormula(" << n + << "), inUnsatCore = " << inUnsatCore + << ", inInput = " << inInput + << ", isAssumption = " << isAssumption << endl; // Give it to proof manager PROOF( @@ -3480,7 +3493,7 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) ); // Add the normalized formula to the queue - d_assertions.push_back(n); + d_assertions.push_back(n, isAssumption); //d_assertions.push_back(Rewriter::rewrite(n)); } @@ -3602,7 +3615,7 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, { d_assertionList->push_back(e); } - d_private->addFormula(e.getNode(), inUnsatCore); + d_private->addFormula(e.getNode(), inUnsatCore, true, true); } r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult(); -- 2.30.2