From c38f35164adc5ab255803765a568ef820fa8f3b2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 28 Jul 2020 11:03:33 -0500 Subject: Use lemma property enum for OutputChannel::lemma (#4755) There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance. This makes them into a enum. --- src/CMakeLists.txt | 1 + src/proof/proof_output_channel.cpp | 6 +- src/proof/proof_output_channel.h | 4 +- src/theory/arith/nl/nl_lemma_utils.cpp | 5 + src/theory/arith/nl/nl_lemma_utils.h | 3 + src/theory/arith/nl/nonlinear_extension.cpp | 12 ++- src/theory/arith/nl/nonlinear_extension.h | 3 - src/theory/arrays/theory_arrays.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 2 +- src/theory/engine_output_channel.cpp | 48 +++++----- src/theory/engine_output_channel.h | 8 +- src/theory/ext_theory.cpp | 2 +- src/theory/fp/theory_fp.cpp | 5 +- src/theory/output_channel.cpp | 111 ++++++++++++++++++++++ src/theory/output_channel.h | 75 +++++++++------ src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 2 +- src/theory/quantifiers/fmf/bounded_integers.cpp | 2 +- src/theory/quantifiers_engine.cpp | 5 +- src/theory/sets/inference_manager.cpp | 4 +- src/theory/theory_engine.cpp | 21 ++-- src/theory/theory_engine.h | 6 +- src/theory/theory_test_utils.h | 4 +- test/unit/theory/theory_engine_white.h | 6 +- test/unit/theory/theory_white.h | 6 +- 24 files changed, 244 insertions(+), 99 deletions(-) create mode 100644 src/theory/output_channel.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 422888e73..992da9a85 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -475,6 +475,7 @@ libcvc4_add_sources( theory/interrupted.h theory/logic_info.cpp theory/logic_info.h + theory/output_channel.cpp theory/output_channel.h theory/quantifiers/alpha_equivalence.cpp theory/quantifiers/alpha_equivalence.h diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp index 1e6e759e3..88467aea6 100644 --- a/src/proof/proof_output_channel.cpp +++ b/src/proof/proof_output_channel.cpp @@ -48,8 +48,10 @@ bool ProofOutputChannel::propagate(TNode x) { return true; } -theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, - bool, bool) { +theory::LemmaStatus ProofOutputChannel::lemma(TNode n, + ProofRule rule, + theory::LemmaProperty p) +{ Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl; // TODO(#1231): We should transition to supporting multiple lemmas. The // following assertion cannot be enabled due to diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index 6a91bad7c..b68abd44b 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -38,7 +38,9 @@ class ProofOutputChannel : public theory::OutputChannel { */ void conflict(TNode n, std::unique_ptr pf) override; bool propagate(TNode x) override; - theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) override; + theory::LemmaStatus lemma(TNode n, + ProofRule rule, + theory::LemmaProperty p) override; theory::LemmaStatus splitLemma(TNode, bool) override; void requirePhase(TNode n, bool b) override; void setIncomplete() override; diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index 0497b5822..49eec186e 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -21,6 +21,11 @@ namespace theory { namespace arith { namespace nl { +LemmaProperty NlLemma::getLemmaProperty() const +{ + return d_preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE; +} + std::ostream& operator<<(std::ostream& out, NlLemma& n) { out << n.d_lemma; diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index 2b5158f18..f40857fda 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -19,6 +19,7 @@ #include #include "expr/node.h" #include "theory/arith/nl/inference.h" +#include "theory/output_channel.h" namespace CVC4 { namespace theory { @@ -61,6 +62,8 @@ struct NlLemma * Cimatti et al., CADE 2017. */ std::vector > d_secantPoint; + /** get lemma property (preprocess or none) */ + LemmaProperty getLemmaProperty() const; }; /** * Writes a non-linear lemma to a stream. diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 432c25f27..4cb1c9fe6 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -18,6 +18,7 @@ #include "theory/arith/nl/nonlinear_extension.h" #include "options/arith_options.h" +#include "options/theory_options.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" @@ -164,14 +165,14 @@ void NonlinearExtension::sendLemmas(const std::vector& out) for (const NlLemma& nlem : out) { Node lem = nlem.d_lemma; - bool preprocess = nlem.d_preprocess; + LemmaProperty p = nlem.getLemmaProperty(); Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_id << " : " << lem << std::endl; - d_containing.getOutputChannel().lemma(lem, false, preprocess); + d_containing.getOutputChannel().lemma(lem, p); // process the side effect processSideEffect(nlem); - // add to cache if not preprocess - if (preprocess) + // add to cache based on preprocess + if (isLemmaPropertyPreprocess(p)) { d_lemmasPp.insert(lem); } @@ -408,7 +409,8 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, Trace("nl-ext-cm") << "-----" << std::endl; unsigned tdegree = d_trSlv.getTaylorDegree(); - bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs); + bool ret = + d_model.checkModel(passertions, tdegree, lemmas, gs); return ret; } diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 36875d8a3..6cc5c29d4 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -257,9 +257,6 @@ class NonlinearExtension std::vector& gs); //---------------------------end check model - /** Is n entailed with polarity pol in the current context? */ - bool isEntailed(Node n, bool pol); - /** * Potentially adds lemmas to the set out and clears lemmas. Returns * the number of lemmas added to out. We do not add lemmas that have already diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 37443c070..f008dc2a1 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1522,7 +1522,7 @@ void TheoryArrays::check(Effort e) { lemma = mkAnd(conjunctions, true); // LSH FIXME: which kind of arrays lemma is this Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n"; - d_out->lemma(lemma, RULE_INVALID, false, false, true); + d_out->lemma(lemma, RULE_INVALID, LemmaProperty::SEND_ATOMS); d_readTableContext->pop(); Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; return; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 505d08c38..9b8badc5e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -320,7 +320,7 @@ void TheoryDatatypes::check(Effort e) { Trace("dt-split") << "*************Split for constructors on " << n << endl; Node lemma = utils::mkSplit(n, dt); Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; - d_out->lemma( lemma, false, false, true ); + d_out->lemma(lemma, LemmaProperty::SEND_ATOMS); d_addedLemma = true; } if( !options::dtBlastSplits() ){ diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index d83d2ba62..a271d6d9c 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -73,26 +73,26 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r) theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, ProofRule rule, - bool removable, - bool preprocess, - bool sendAtoms) + LemmaProperty p) { Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" - << ", preprocess = " << preprocess << std::endl; + << ", properties = " << p << std::endl; ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); + PROOF({ + bool preprocess = isLemmaPropertyPreprocess(p); + registerLemmaRecipe(lemma, lemma, preprocess, d_theory); + }); TrustNode tlem = TrustNode::mkTrustLemma(lemma); - theory::LemmaStatus result = - d_engine->lemma(tlem.getNode(), - rule, - false, - removable, - preprocess, - sendAtoms ? d_theory : theory::THEORY_LAST); + theory::LemmaStatus result = d_engine->lemma( + tlem.getNode(), + rule, + false, + p, + isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST); return result; } @@ -236,8 +236,9 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; TrustNode tlem = TrustNode::mkTrustLemma(lemma); - theory::LemmaStatus result = d_engine->lemma( - tlem.getNode(), RULE_SPLIT, false, removable, false, d_theory); + LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE; + theory::LemmaStatus result = + d_engine->lemma(tlem.getNode(), RULE_SPLIT, false, p, d_theory); return result; } @@ -273,7 +274,7 @@ void EngineOutputChannel::demandRestart() Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl; ++d_statistics.restartDemands; - lemma(restartVar, RULE_INVALID, true); + lemma(restartVar, RULE_INVALID, LemmaProperty::REMOVABLE); } void EngineOutputChannel::requirePhase(TNode n, bool phase) @@ -316,10 +317,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf) d_engine->conflict(pconf.getNode(), d_theory); } -LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, - bool removable, - bool preprocess, - bool sendAtoms) +LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) { Assert(plem.getKind() == TrustNodeKind::LEMMA); if (plem.getGenerator() != nullptr) @@ -329,12 +327,12 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; // now, call the normal interface for lemma - return d_engine->lemma(plem.getNode(), - RULE_INVALID, - false, - removable, - preprocess, - sendAtoms ? d_theory : theory::THEORY_LAST); + return d_engine->lemma( + plem.getNode(), + RULE_INVALID, + false, + p, + isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST); } } // namespace theory diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index d7b26928d..3e959898f 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -51,9 +51,7 @@ class EngineOutputChannel : public theory::OutputChannel theory::LemmaStatus lemma(TNode lemma, ProofRule rule, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false) override; + LemmaProperty p = LemmaProperty::NONE) override; theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override; @@ -81,9 +79,7 @@ class EngineOutputChannel : public theory::OutputChannel * the same as calling OutputChannel::lemma on lem. */ LemmaStatus trustedLemma(TrustNode plem, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false) override; + LemmaProperty p = LemmaProperty::NONE) override; protected: /** diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index f84153c06..bdcd5dcff 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -344,7 +344,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess) if (d_pp_lemmas.find(lem) == d_pp_lemmas.end()) { d_pp_lemmas.insert(lem); - d_parent->getOutputChannel().lemma(lem, false, true); + d_parent->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); return true; } } diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index bffcda7bc..a4cff8c95 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -902,9 +902,8 @@ void TheoryFp::addSharedTerm(TNode node) { void TheoryFp::handleLemma(Node node) { Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl; - - d_out->lemma(node, false, - true); // Has to be true because it contains embedded ITEs + // Preprocess has to be true because it contains embedded ITEs + d_out->lemma(node, LemmaProperty::PREPROCESS); // Ignore the LemmaStatus structure for now... return; diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp new file mode 100644 index 000000000..9fe973569 --- /dev/null +++ b/src/theory/output_channel.cpp @@ -0,0 +1,111 @@ +/********************* */ +/*! \file output_channel.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 The theory output channel interface + **/ + +#include "theory/output_channel.h" + +namespace CVC4 { +namespace theory { + +LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs) +{ + return static_cast(static_cast(lhs) + | static_cast(rhs)); +} +LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs) +{ + lhs = lhs | rhs; + return lhs; +} +LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs) +{ + return static_cast(static_cast(lhs) + & static_cast(rhs)); +} +LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs) +{ + lhs = lhs & rhs; + return lhs; +} +bool isLemmaPropertyRemovable(LemmaProperty p) +{ + return (p & LemmaProperty::REMOVABLE) != LemmaProperty::NONE; +} +bool isLemmaPropertyPreprocess(LemmaProperty p) +{ + return (p & LemmaProperty::PREPROCESS) != LemmaProperty::NONE; +} +bool isLemmaPropertySendAtoms(LemmaProperty p) +{ + return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE; +} + +std::ostream& operator<<(std::ostream& out, LemmaProperty p) +{ + if (p == LemmaProperty::NONE) + { + out << "NONE"; + } + else + { + out << "{"; + if (isLemmaPropertyRemovable(p)) + { + out << " REMOVABLE"; + } + if (isLemmaPropertyPreprocess(p)) + { + out << " PREPROCESS"; + } + if (isLemmaPropertySendAtoms(p)) + { + out << " SEND_ATOMS"; + } + out << " }"; + } + return out; +} + +LemmaStatus::LemmaStatus(TNode rewrittenLemma, unsigned level) + : d_rewrittenLemma(rewrittenLemma), d_level(level) +{ +} + +TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; } + +unsigned LemmaStatus::getLevel() const { return d_level; } + +LemmaStatus OutputChannel::lemma(TNode n, LemmaProperty p) +{ + return lemma(n, RULE_INVALID, p); +} + +LemmaStatus OutputChannel::split(TNode n) +{ + return splitLemma(n.orNode(n.notNode())); +} + +void OutputChannel::trustedConflict(TrustNode pconf) +{ + Unreachable() << "OutputChannel::trustedConflict: no implementation" + << std::endl; +} + +LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p) +{ + Unreachable() << "OutputChannel::trustedLemma: no implementation" + << std::endl; +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index ff13d1b6b..d65d4fc53 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -32,6 +32,42 @@ namespace CVC4 { namespace theory { +/** Properties of lemmas */ +enum class LemmaProperty : uint32_t +{ + // default + NONE = 0, + // whether the lemma is removable + REMOVABLE = 1, + // whether the lemma needs preprocessing + PREPROCESS = 2, + // whether the processing of the lemma should send atoms to the caller + SEND_ATOMS = 4 +}; +/** Define operator lhs | rhs */ +LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs); +/** Define operator lhs |= rhs */ +LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs); +/** Define operator lhs & rhs */ +LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs); +/** Define operator lhs &= rhs */ +LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs); +/** is the removable bit set on p? */ +bool isLemmaPropertyRemovable(LemmaProperty p); +/** is the preprocess bit set on p? */ +bool isLemmaPropertyPreprocess(LemmaProperty p); +/** is the send atoms bit set on p? */ +bool isLemmaPropertySendAtoms(LemmaProperty p); + +/** + * Writes an lemma property name to a stream. + * + * @param out The stream to write to + * @param p The lemma property to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, LemmaProperty p); + class Theory; /** @@ -41,17 +77,17 @@ class Theory; */ class LemmaStatus { public: - LemmaStatus(TNode rewrittenLemma, unsigned level) - : d_rewrittenLemma(rewrittenLemma), d_level(level) {} + LemmaStatus(TNode rewrittenLemma, unsigned level); /** Get the T-rewritten form of the lemma. */ - TNode getRewrittenLemma() const { return d_rewrittenLemma; } + TNode getRewrittenLemma() const; /** * Get the user-level at which the lemma resides. After this user level * is popped, the lemma is un-asserted from the SAT layer. This level * will be 0 if the lemma didn't reach the SAT layer at all. */ - unsigned getLevel() const { return d_level; } + unsigned getLevel() const; + private: Node d_rewrittenLemma; unsigned d_level; @@ -114,23 +150,18 @@ class OutputChannel { * * @param n - a theory lemma valid at decision level 0 * @param rule - the proof rule for this lemma - * @param removable - whether the lemma can be removed at any point - * @param preprocess - whether to apply more aggressive preprocessing - * @param sendAtoms - whether to ensure atoms are sent to the theory + * @param p The properties of the lemma * @return the "status" of the lemma, including user level at which * the lemma resides; the lemma will be removed when this user level pops */ - virtual LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false, - bool preprocess = false, - bool sendAtoms = false) = 0; + virtual LemmaStatus lemma(TNode n, + ProofRule rule, + LemmaProperty p = LemmaProperty::NONE) = 0; /** * Variant of the lemma function that does not require providing a proof rule. */ - virtual LemmaStatus lemma(TNode n, bool removable = false, - bool preprocess = false, bool sendAtoms = false) { - return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms); - } + virtual LemmaStatus lemma(TNode n, LemmaProperty p = LemmaProperty::NONE); /** * Request a split on a new theory atom. This is equivalent to @@ -138,7 +169,7 @@ class OutputChannel { * * @param n - a theory atom; must be of Boolean type */ - LemmaStatus split(TNode n) { return splitLemma(n.orNode(n.notNode())); } + LemmaStatus split(TNode n); virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0; @@ -197,11 +228,7 @@ class OutputChannel { * by the generator pfg. Apart from pfg, the interface for this method is * the same as OutputChannel. */ - virtual void trustedConflict(TrustNode pconf) - { - Unreachable() << "OutputChannel::trustedConflict: no implementation" - << std::endl; - } + virtual void trustedConflict(TrustNode pconf); /** * Let plem be the pair (Node lem, ProofGenerator * pfg). * Send lem on the output channel of this class whose proof can be generated @@ -209,13 +236,7 @@ class OutputChannel { * the same as OutputChannel. */ virtual LemmaStatus trustedLemma(TrustNode lem, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false) - { - Unreachable() << "OutputChannel::trustedLemma: no implementation" - << std::endl; - } + LemmaProperty p = LemmaProperty::NONE); //---------------------------- end new proof }; /* class OutputChannel */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 7f0e93997..5a50bc99a 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1394,7 +1394,7 @@ void CegInstantiator::presolve( Node q ) { lem = NodeManager::currentNM()->mkNode( OR, g, lem ); Trace("cegqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; Assert(!expr::hasFreeVar(lem)); - d_qe->getOutputChannel().lemma( lem, false, true ); + d_qe->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); } } } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index b3ea69dbc..84f4bb83b 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -723,7 +723,7 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] ); Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma(lem, false, true); + d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); } return false; }else{ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6dcf1a980..bb5950c5e 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -970,7 +970,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } - getOutputChannel().lemma(lem, false, true); + getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); } return; } @@ -1021,7 +1021,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl; BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem ); if( itp==d_lemmas_produced_c.end() || !(*itp).second ){ - //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); Trace("inst-add-debug") << "Added lemma" << std::endl; @@ -1122,7 +1121,7 @@ void QuantifiersEngine::flushLemmas(){ d_hasAddedLemma = true; for( unsigned i=0; ilemma(lem, false, preprocess); + LemmaProperty p = + preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE; + d_parent.getOutputChannel()->lemma(lem, p); d_sentLemma = true; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9955be850..ef237e76d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -41,6 +41,7 @@ #include "theory/arith/arith_ite_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/care_graph.h" +#include "theory/decision_manager.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/theory_quantifiers.h" @@ -621,8 +622,7 @@ void TheoryEngine::combineTheories() { lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, - false, - false, + LemmaProperty::NONE, carePair.d_theory); // This code is supposed to force preference to follow what the theory models already have @@ -1587,9 +1587,9 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector& atoms, theory::The theory::LemmaStatus TheoryEngine::lemma(TNode node, ProofRule rule, bool negated, - bool removable, - bool preprocess, - theory::TheoryId atomsTo) { + theory::LemmaProperty p, + theory::TheoryId atomsTo) +{ // For resource-limiting (also does a time check). // spendResource(); @@ -1609,6 +1609,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << CheckSatCommand(n.toExpr()); } + bool removable = isLemmaPropertyRemovable(p); + bool preprocess = isLemmaPropertyPreprocess(p); // call preprocessor std::vector newLemmas; @@ -1705,8 +1707,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST); - + lemma(fullConflict, + RULE_CONFLICT, + true, + LemmaProperty::REMOVABLE, + THEORY_LAST); } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); @@ -1735,7 +1740,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { ProofManager::getCnfProof()->setProofRecipe(proofRecipe); }); - lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST); + lemma(conflict, RULE_CONFLICT, true, LemmaProperty::REMOVABLE, THEORY_LAST); } PROOF({ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 8c0ce6dbf..5b04e49a8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -330,14 +330,12 @@ class TheoryEngine { * Adds a new lemma, returning its status. * @param node the lemma * @param negated should the lemma be asserted negated - * @param removable can the lemma be remove (restrictions apply) - * @param needAtoms if not THEORY_LAST, then + * @param p the properties of the lemma. */ theory::LemmaStatus lemma(TNode node, ProofRule rule, bool negated, - bool removable, - bool preprocess, + theory::LemmaProperty p, theory::TheoryId atomsTo); /** Enusre that the given atoms are send to the given theory */ diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 61caca82a..2593b11a6 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -79,8 +79,8 @@ public: return true; } - LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false, - bool preprocess = false, bool sendAtoms = false) override { + LemmaStatus lemma(TNode n, ProofRule rule, LemmaProperty p) override + { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 5a16fdc20..fbcfbdb37 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -60,8 +60,10 @@ class FakeOutputChannel : public OutputChannel { Unimplemented(); } bool propagate(TNode n) override { Unimplemented(); } - LemmaStatus lemma(TNode n, ProofRule rule, bool removable, bool preprocess, - bool sendAtoms) override { + LemmaStatus lemma(TNode n, + ProofRule rule, + LemmaProperty p = LemmaProperty::NONE) override + { Unimplemented(); } void requirePhase(TNode, bool) override { Unimplemented(); } diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 0ff4e918b..5ed7afbe1 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -58,8 +58,10 @@ class TestOutputChannel : public OutputChannel { return true; } - LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false, - bool preprocess = false, bool sendAtoms = false) override { + LemmaStatus lemma(TNode n, + ProofRule rule, + LemmaProperty p = LemmaProperty::NONE) override + { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } -- cgit v1.2.3