diff options
23 files changed, 258 insertions, 230 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index e2109cf1e..caad72fd5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -61,6 +61,8 @@ libcvc4_la_SOURCES = \ decision/decision_strategy.h \ decision/justification_heuristic.cpp \ decision/justification_heuristic.h \ + preprocessing/assertion_pipeline.cpp \ + preprocessing/assertion_pipeline.h \ preprocessing/passes/apply_substs.cpp \ preprocessing/passes/apply_substs.h \ preprocessing/passes/apply_to_const.cpp \ @@ -97,10 +99,10 @@ libcvc4_la_SOURCES = \ preprocessing/passes/pseudo_boolean_processor.h \ preprocessing/passes/miplib_trick.cpp \ preprocessing/passes/miplib_trick.h \ - preprocessing/passes/quantifiers_preprocess.cpp \ - preprocessing/passes/quantifiers_preprocess.h \ preprocessing/passes/quantifier_macros.cpp \ preprocessing/passes/quantifier_macros.h \ + preprocessing/passes/quantifiers_preprocess.cpp \ + preprocessing/passes/quantifiers_preprocess.h \ preprocessing/passes/real_to_int.cpp \ preprocessing/passes/real_to_int.h \ preprocessing/passes/rewrite.cpp \ diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 8aed4fb32..013e2165f 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -610,10 +610,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> namespace { -bool isDefinedKind(Kind k) -{ - return k > UNDEFINED_KIND && k < LAST_KIND; -} +bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } bool isDefinedIntKind(CVC4::Kind k) { diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 8e419e768..01f78f2d6 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -98,31 +98,21 @@ SatValue DecisionEngine::getPolarity(SatVariable var) } } -void DecisionEngine::addAssertions(const vector<Node> &assertions) -{ - Assert(false); // doing this so that we revisit what to do - // here. Currently not being used. - - // d_result = SAT_VALUE_UNKNOWN; - // d_assertions.reserve(assertions.size()); - // for(unsigned i = 0; i < assertions.size(); ++i) - // d_assertions.push_back(assertions[i]); -} - -void DecisionEngine::addAssertions(const vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) +void DecisionEngine::addAssertions( + const preprocessing::AssertionPipeline& assertions) { // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; - // d_assertions.reserve(assertions.size()); - for(unsigned i = 0; i < assertions.size(); ++i) - d_assertions.push_back(assertions[i]); + for (const Node& assertion : assertions) + { + d_assertions.push_back(assertion); + } for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) - d_needIteSkolemMap[i]-> - addAssertions(assertions, assertionsEnd, iteSkolemMap); + { + d_needIteSkolemMap[i]->addAssertions(assertions); + } } }/* CVC4 namespace */ diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 838e53b5a..c5325bc9a 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -24,11 +24,12 @@ #include "base/output.h" #include "decision/decision_strategy.h" #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" -#include "smt/term_formula_removal.h" #include "smt/smt_engine_scope.h" +#include "smt/term_formula_removal.h" using namespace std; using namespace CVC4::prop; @@ -173,21 +174,10 @@ public: /* return d_needIteSkolemMap.size() > 0; */ /* } */ - /* add a set of assertions */ - void addAssertions(const vector<Node> &assertions); - /** - * add a set of assertions, while providing a mapping between skolem - * variables and corresponding assertions. It is assumed that all - * assertions after assertionEnd were generated by ite - * removal. Hence, iteSkolemMap maps into only these. + * Add a list of assertions from an AssertionPipeline. */ - void addAssertions(const vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap); - - /* add a single assertion */ - void addAssertion(Node n); + void addAssertions(const preprocessing::AssertionPipeline& assertions); // Interface for Strategies to use stuff stored in Decision Engine // (which was possibly requested by them on initialization) diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index bad80d4ef..d26b28eeb 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -19,6 +19,7 @@ #ifndef __CVC4__DECISION__DECISION_STRATEGY_H #define __CVC4__DECISION__DECISION_STRATEGY_H +#include "preprocessing/assertion_pipeline.h" #include "prop/sat_solver_types.h" #include "smt/term_formula_removal.h" @@ -57,9 +58,8 @@ public: bool needIteSkolemMap() override { return true; } - virtual void addAssertions(const std::vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) = 0; + virtual void addAssertions( + const preprocessing::AssertionPipeline& assertions) = 0; };/* class ITEDecisionStrategy */ class RelevancyStrategy : public ITEDecisionStrategy { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 7d19d3363..b4fbe1cbd 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -163,12 +163,10 @@ inline void computeXorIffDesiredValues } } - - -void JustificationHeuristic::addAssertions -(const std::vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) { +void JustificationHeuristic::addAssertions( + const preprocessing::AssertionPipeline &assertions) +{ + size_t assertionsEnd = assertions.getRealAssertionsEnd(); Trace("decision") << "JustificationHeuristic::addAssertions()" @@ -177,19 +175,19 @@ void JustificationHeuristic::addAssertions << std::endl; // Save the 'real' assertions locally - for(unsigned i = 0; i < assertionsEnd; ++i) + for (size_t i = 0; i < assertionsEnd; i++) + { d_assertions.push_back(assertions[i]); + } // Save mapping between ite skolems and ite assertions - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); - i != iteSkolemMap.end(); ++i) { - - Trace("decision::jh::ite") - << " jh-ite: " << (i->first) << " maps to " - << assertions[(i->second)] << std::endl; - Assert(i->second >= assertionsEnd && i->second < assertions.size()); + for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap()) + { + Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to " + << assertions[(i.second)] << std::endl; + Assert(i.second >= assertionsEnd && i.second < assertions.size()); - d_iteAssertions[i->first] = assertions[i->second]; + d_iteAssertions[i.first] = assertions[i.second]; } // Automatic weight computation diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index a70bee02c..0cd45ada7 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -32,6 +32,7 @@ #include "decision/decision_engine.h" #include "decision/decision_strategy.h" #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" #include "prop/sat_solver_types.h" namespace CVC4 { @@ -119,9 +120,8 @@ public: prop::SatLiteral getNext(bool &stopSearch) override; - void addAssertions(const std::vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) override; + void addAssertions( + const preprocessing::AssertionPipeline &assertions) override; private: /* getNext with an option to specify threshold */ diff --git a/src/include/cvc4_private_library.h b/src/include/cvc4_private_library.h index 92ed555fd..23bf0e01f 100644 --- a/src/include/cvc4_private_library.h +++ b/src/include/cvc4_private_library.h @@ -19,7 +19,10 @@ #ifndef __CVC4_PRIVATE_LIBRARY_H #define __CVC4_PRIVATE_LIBRARY_H -#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4DRIVER)) +#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) \ + || defined(__BUILDING_CVC4PARSERLIB) \ + || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) \ + || defined(__BUILDING_CVC4DRIVER)) # error A "private library" CVC4 header was included when not building the library, driver, or private unit test code. #endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || __BUILDING_CVC4DRIVER) */ diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp new file mode 100644 index 000000000..0bce3b8cd --- /dev/null +++ b/src/preprocessing/assertion_pipeline.cpp @@ -0,0 +1,59 @@ +/********************* */ +/*! \file assertion_pipeline.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief AssertionPipeline stores a list of assertions modified by + ** preprocessing passes + **/ + +#include "preprocessing/assertion_pipeline.h" + +#include "expr/node_manager.h" +#include "proof/proof.h" +#include "proof/proof_manager.h" + +namespace CVC4 { +namespace preprocessing { + +AssertionPipeline::AssertionPipeline() : d_realAssertionsEnd(0) {} + +void AssertionPipeline::replace(size_t i, Node n) +{ + PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);); + d_nodes[i] = n; +} + +void AssertionPipeline::replace(size_t i, + Node n, + const std::vector<Node>& addnDeps) +{ + PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]); + for (const auto& addnDep + : addnDeps) { + ProofManager::currentPM()->addDependence(n, addnDep); + }); + d_nodes[i] = n; +} + +void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns) +{ + PROOF( + for (const auto& n + : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); }); + d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true); + + for (const auto& n : ns) + { + d_nodes.push_back(n); + } +} + +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h new file mode 100644 index 000000000..af7a8dce3 --- /dev/null +++ b/src/preprocessing/assertion_pipeline.h @@ -0,0 +1,101 @@ +/********************* */ +/*! \file assertion_pipeline.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief AssertionPipeline stores a list of assertions modified by + ** preprocessing passes + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H +#define __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H + +#include <vector> + +#include "expr/node.h" +#include "smt/term_formula_removal.h" + +namespace CVC4 { +namespace preprocessing { + +/** + * Assertion Pipeline stores a list of assertions modified by preprocessing + * passes. It is assumed that all assertions after d_realAssertionsEnd were + * generated by ITE removal. Hence, d_iteSkolemMap maps into only these. + */ +class AssertionPipeline +{ + public: + AssertionPipeline(); + + size_t size() const { return d_nodes.size(); } + + void resize(size_t n) { d_nodes.resize(n); } + + void clear() + { + d_nodes.clear(); + d_realAssertionsEnd = 0; + } + + 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); } + + std::vector<Node>& ref() { return d_nodes; } + const std::vector<Node>& ref() const { return d_nodes; } + + std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); } + std::vector<Node>::const_iterator end() const { return d_nodes.cend(); } + + /* + * Replaces assertion i with node n and records the dependency between the + * original assertion and its replacement. + */ + void replace(size_t i, Node n); + + /* + * Replaces assertion i with node n and records that this replacement depends + * on assertion i and the nodes listed in addnDeps. The dependency + * information is used for unsat cores and proofs. + */ + void replace(size_t i, Node n, const std::vector<Node>& addnDeps); + + /* + * Replaces an assertion with a vector of assertions and records the + * dependencies. + */ + void replace(size_t i, const std::vector<Node>& ns); + + IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; } + const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; } + + size_t getRealAssertionsEnd() const { return d_realAssertionsEnd; } + + void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); } + + private: + std::vector<Node> d_nodes; + + /** + * Map from skolem variables to index in d_assertions containing + * corresponding introduced Boolean ite + */ + IteSkolemMap d_iteSkolemMap; + + /** Size of d_nodes when preprocessing starts */ + size_t d_realAssertionsEnd; +}; /* class AssertionPipeline */ + +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */ diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 6fb4b7793..f5c3520d0 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -44,8 +44,9 @@ PreprocessingPassResult ApplySubsts::applyInternal( // When solving incrementally, all substitutions are piled into the // assertion at d_substitutionsIndex: we don't want to apply substitutions // to this assertion or information will be lost. - context::CDO<unsigned>& substs_index = - assertionsToPreprocess->getSubstitutionsIndex(); + unsigned substs_index = d_preprocContext->getSubstitutionsIndex(); + theory::SubstitutionMap& substMap = + d_preprocContext->getTopLevelSubstitutions(); unsigned size = assertionsToPreprocess->size(); unsigned substitutionAssertion = substs_index > 0 ? substs_index : size; for (unsigned i = 0; i < size; ++i) @@ -57,11 +58,9 @@ PreprocessingPassResult ApplySubsts::applyInternal( Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i] << std::endl; d_preprocContext->spendResource(options::preprocessStep()); - assertionsToPreprocess->replace( - i, - theory::Rewriter::rewrite( - assertionsToPreprocess->getTopLevelSubstitutions().apply( - (*assertionsToPreprocess)[i]))); + assertionsToPreprocess->replace(i, + theory::Rewriter::rewrite(substMap.apply( + (*assertionsToPreprocess)[i]))); Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] << std::endl; } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 81588d039..616ecd969 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -188,7 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( propagator->getBackEdges(); unordered_set<unsigned long> removeAssertions; SubstitutionMap& top_level_substs = - assertionsToPreprocess->getTopLevelSubstitutions(); + d_preprocContext->getTopLevelSubstitutions(); NodeManager* nm = NodeManager::currentNM(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index e2ce1c301..653aed8ad 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -76,8 +76,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // Assert all the assertions to the propagator Trace("non-clausal-simplify") << "asserting to propagator" << std::endl; - context::CDO<unsigned>& substs_index = - assertionsToPreprocess->getSubstitutionsIndex(); + unsigned substs_index = d_preprocContext->getSubstitutionsIndex(); for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) @@ -114,7 +113,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << " learned literals." << std::endl; // No conflict, go through the literals and solve them SubstitutionMap& top_level_substs = - assertionsToPreprocess->getTopLevelSubstitutions(); + d_preprocContext->getTopLevelSubstitutions(); SubstitutionMap constantPropagations(d_preprocContext->getUserContext()); SubstitutionMap newSubstitutions(d_preprocContext->getUserContext()); SubstitutionMap::iterator pos; diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 6a7078696..6a1d89d33 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -16,51 +16,12 @@ #include "preprocessing/preprocessing_pass.h" -#include "expr/node_manager.h" -#include "proof/proof.h" #include "smt/dump.h" #include "smt/smt_statistics_registry.h" namespace CVC4 { namespace preprocessing { -AssertionPipeline::AssertionPipeline(context::Context* context) - : d_substitutionsIndex(context, 0), - d_topLevelSubstitutions(context), - d_realAssertionsEnd(0) -{ -} - -void AssertionPipeline::replace(size_t i, Node n) { - PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);); - d_nodes[i] = n; -} - -void AssertionPipeline::replace(size_t i, - Node n, - const std::vector<Node>& addnDeps) -{ - PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]); - for (const auto& addnDep - : addnDeps) { - ProofManager::currentPM()->addDependence(n, addnDep); - }); - d_nodes[i] = n; -} - -void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns) -{ - PROOF( - for (const auto& n - : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); }); - d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true); - - for (const auto& n : ns) - { - d_nodes.push_back(n); - } -} - PreprocessingPassResult PreprocessingPass::apply( AssertionPipeline* assertionsToPreprocess) { TimerStat::CodeTimer codeTimer(d_timer); diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index 4143f2d4b..448cacb87 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -32,103 +32,16 @@ #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H #include <string> -#include <vector> -#include "context/cdo.h" -#include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_engine_scope.h" -#include "smt/term_formula_removal.h" #include "theory/logic_info.h" -#include "theory/substitutions.h" namespace CVC4 { namespace preprocessing { /** - * Assertion Pipeline stores a list of assertions modified by preprocessing - * passes. - */ -class AssertionPipeline -{ - public: - AssertionPipeline(context::Context* context); - - size_t size() const { return d_nodes.size(); } - - void resize(size_t n) { d_nodes.resize(n); } - - void clear() - { - d_nodes.clear(); - d_realAssertionsEnd = 0; - } - - 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); } - - std::vector<Node>& ref() { return d_nodes; } - const std::vector<Node>& ref() const { return d_nodes; } - - std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); } - std::vector<Node>::const_iterator end() const { return d_nodes.cend(); } - - /* - * Replaces assertion i with node n and records the dependency between the - * original assertion and its replacement. - */ - void replace(size_t i, Node n); - - /* - * Replaces assertion i with node n and records that this replacement depends - * on assertion i and the nodes listed in addnDeps. The dependency - * information is used for unsat cores and proofs. - */ - void replace(size_t i, Node n, const std::vector<Node>& addnDeps); - - /* - * Replaces an assertion with a vector of assertions and records the - * dependencies. - */ - void replace(size_t i, const std::vector<Node>& ns); - - IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; } - - context::CDO<unsigned>& getSubstitutionsIndex() - { - return d_substitutionsIndex; - } - - theory::SubstitutionMap& getTopLevelSubstitutions() - { - return d_topLevelSubstitutions; - } - - size_t getRealAssertionsEnd() { return d_realAssertionsEnd; } - - void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); } - - private: - std::vector<Node> d_nodes; - - /** - * Map from skolem variables to index in d_assertions containing - * corresponding introduced Boolean ite - */ - IteSkolemMap d_iteSkolemMap; - - /* Index for where to store substitutions */ - context::CDO<unsigned> d_substitutionsIndex; - - /* The top level substitutions */ - theory::SubstitutionMap d_topLevelSubstitutions; - - /** Size of d_nodes when preprocessing starts */ - size_t d_realAssertionsEnd; -}; /* class AssertionPipeline */ - -/** * Preprocessing passes return a result which indicates whether a conflict has * been detected during preprocessing. */ diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 15f5d3eb0..3f72a4559 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -29,6 +29,8 @@ PreprocessingPassContext::PreprocessingPassContext( : d_smt(smt), d_resourceManager(resourceManager), d_iteRemover(iteRemover), + d_substitutionsIndex(smt->d_userContext, 0), + d_topLevelSubstitutions(smt->d_userContext), d_circuitPropagator(circuitPropagator), d_symsInAssertions(smt->d_userContext) { diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index ae989d700..3eb0f10b5 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -21,6 +21,7 @@ #ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H +#include "context/cdo.h" #include "context/context.h" #include "decision/decision_engine.h" #include "preprocessing/util/ite_utilities.h" @@ -70,6 +71,16 @@ class PreprocessingPassContext /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); + unsigned getSubstitutionsIndex() const { return d_substitutionsIndex.get(); } + + void setSubstitutionsIndex(unsigned i) { d_substitutionsIndex = i; } + + /** Gets a reference to the top-level substitution map */ + theory::SubstitutionMap& getTopLevelSubstitutions() + { + return d_topLevelSubstitutions; + } + /* Enable Integers. */ void enableIntegers(); @@ -90,6 +101,12 @@ class PreprocessingPassContext /** Instance of the ITE remover */ RemoveTermFormulas* d_iteRemover; + /* Index for where to store substitutions */ + context::CDO<unsigned> d_substitutionsIndex; + + /* The top level substitutions */ + theory::SubstitutionMap d_topLevelSubstitutions; + /** Instance of the circuit propagator */ theory::booleans::CircuitPropagator* d_circuitPropagator; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 73264daa5..eeacb9c3f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -568,7 +568,7 @@ class SmtEnginePrivate : public NodeManagerListener { d_managedReplayLog(), d_listenerRegistrations(new ListenerRegistrationList()), d_propagator(true, true), - d_assertions(d_smt.d_userContext), + d_assertions(), d_assertionsProcessed(smt.d_userContext, false), d_fakeContext(), d_abstractValueMap(&d_fakeContext), @@ -715,7 +715,7 @@ class SmtEnginePrivate : public NodeManagerListener { Node applySubstitutions(TNode node) { return Rewriter::rewrite( - d_assertions.getTopLevelSubstitutions().apply(node)); + d_preprocessingPassContext->getTopLevelSubstitutions().apply(node)); } /** @@ -3113,7 +3113,8 @@ void SmtEnginePrivate::processAssertions() { spendResource(options::preprocessStep()); Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); - SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions(); + SubstitutionMap& top_level_substs = + d_preprocessingPassContext->getTopLevelSubstitutions(); // Dump the assertions dumpAssertions("pre-everything", d_assertions); @@ -3138,7 +3139,7 @@ void SmtEnginePrivate::processAssertions() { // proper data structure. // Placeholder for storing substitutions - d_assertions.getSubstitutionsIndex() = d_assertions.size(); + d_preprocessingPassContext->setSubstitutionsIndex(d_assertions.size()); d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true)); } @@ -3478,9 +3479,7 @@ void SmtEnginePrivate::processAssertions() { if(noConflict) { Chat() << "pushing to decision engine..." << endl; Assert(iteRewriteAssertionsEnd == d_assertions.size()); - d_smt.d_decisionEngine->addAssertions(d_assertions.ref(), - d_assertions.getRealAssertionsEnd(), - getIteSkolemMap()); + d_smt.d_decisionEngine->addAssertions(d_assertions); } // end: INVARIANT to maintain: no reordering of assertions or diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index 95a60afac..8c9b39ea4 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -67,10 +67,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) d_check_vts_lemma_lc = false; } -InstStrategyCegqi::~InstStrategyCegqi() -{ - -} +InstStrategyCegqi::~InstStrategyCegqi() {} bool InstStrategyCegqi::needsCheck(Theory::Effort e) { diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 92a355348..95ec24df9 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1194,16 +1194,17 @@ bool MatchGen::reset_round(QuantConflictFind* p) d_qni_gterm_rep[it->first] = p->getRepresentative( it->second ); } if( d_type==typ_ground ){ - //int e = p->evaluate( d_n ); - //if( e==1 ){ + // int e = p->evaluate( d_n ); + // if( e==1 ){ // d_ground_eval[0] = p->d_true; //}else if( e==-1 ){ // d_ground_eval[0] = p->d_false; //} - //modified + // modified TermDb* tdb = p->getTermDatabase(); QuantifiersEngine* qe = p->getQuantifiersEngine(); - for( unsigned i=0; i<2; i++ ){ + for (unsigned i = 0; i < 2; i++) + { if (tdb->isEntailed(d_n, i == 0)) { d_ground_eval[0] = i==0 ? p->d_true : p->d_false; @@ -1220,7 +1221,7 @@ bool MatchGen::reset_round(QuantConflictFind* p) { if (!expr::hasBoundVar(d_n[i])) { - TNode t = tdb->getEntailedTerm(d_n[i]); + TNode t = tdb->getEntailedTerm(d_n[i]); if (qe->inConflict()) { return false; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index fe1dc30a4..09525712f 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -307,8 +307,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, } Trace("cegqi-engine") << "...success:" << std::endl; Trace("cegqi-engine") << ss.str(); - Trace("sygus-repair-const") << "Repaired constants in solution : " - << std::endl; + Trace("sygus-repair-const") + << "Repaired constants in solution : " << std::endl; Trace("sygus-repair-const") << ss.str(); return true; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 37276ac5e..b9c3ccc4e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -29,6 +29,7 @@ #include "options/options.h" #include "options/proof_options.h" #include "options/quantifiers_options.h" +#include "preprocessing/assertion_pipeline.h" #include "proof/cnf_proof.h" #include "proof/lemma_proof.h" #include "proof/proof_manager.h" @@ -53,6 +54,7 @@ using namespace std; +using namespace CVC4::preprocessing; using namespace CVC4::theory; namespace CVC4 { @@ -1818,8 +1820,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr()); } - std::vector<Node> additionalLemmas; - IteSkolemMap iteSkolemMap; + AssertionPipeline additionalLemmas; // Run theory preprocessing, maybe Node ppNode = preprocess ? this->preprocess(node) : Node(node); @@ -1827,9 +1828,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // Remove the ITEs Debug("ite") << "Remove ITE from " << ppNode << std::endl; additionalLemmas.push_back(ppNode); - d_tform_remover.run(additionalLemmas, iteSkolemMap); + additionalLemmas.updateRealAssertionsEnd(); + d_tform_remover.run(additionalLemmas.ref(), + additionalLemmas.getIteSkolemMap()); Debug("ite") << "..done " << additionalLemmas[0] << std::endl; - additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); + additionalLemmas.replace(0, theory::Rewriter::rewrite(additionalLemmas[0])); if(Debug.isOn("lemma-ites")) { Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl; @@ -1846,19 +1849,19 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // assert to prop engine d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { - additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); + additionalLemmas.replace(i, theory::Rewriter::rewrite(additionalLemmas[i])); d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. if(negated) { - additionalLemmas[0] = additionalLemmas[0].notNode(); + additionalLemmas.replace(0, additionalLemmas[0].notNode()); negated = false; } // assert to decision engine if(!removable) { - d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap); + d_decisionEngine->addAssertions(additionalLemmas); } // Mark that we added some lemmas diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index f238ba8be..8ba6da0bf 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -2378,8 +2378,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - context::Context context; - AssertionPipeline apipe(&context); + AssertionPipeline apipe; apipe.push_back(a); passes::BVGauss bgauss(nullptr); std::unordered_map<Node, Node, NodeHashFunction> res; @@ -2461,8 +2460,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - context::Context context; - AssertionPipeline apipe(&context); + AssertionPipeline apipe; apipe.push_back(a); apipe.push_back(eq4); apipe.push_back(eq5); @@ -2513,8 +2511,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_p), d_nine); - context::Context context; - AssertionPipeline apipe(&context); + AssertionPipeline apipe; apipe.push_back(eq1); apipe.push_back(eq2); passes::BVGauss bgauss(nullptr); |