There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
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
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
*/
void conflict(TNode n, std::unique_ptr<Proof> 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;
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;
#include <vector>
#include "expr/node.h"
#include "theory/arith/nl/inference.h"
+#include "theory/output_channel.h"
namespace CVC4 {
namespace theory {
* Cimatti et al., CADE 2017.
*/
std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint;
+ /** get lemma property (preprocess or none) */
+ LemmaProperty getLemmaProperty() const;
};
/**
* Writes a non-linear lemma to a stream.
#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"
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);
}
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;
}
std::vector<Node>& 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
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;
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() ){
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;
}
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;
}
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)
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)
++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
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;
* 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:
/**
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;
}
}
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;
--- /dev/null
+/********************* */
+/*! \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<LemmaProperty>(static_cast<uint32_t>(lhs)
+ | static_cast<uint32_t>(rhs));
+}
+LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs)
+{
+ lhs = lhs | rhs;
+ return lhs;
+}
+LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs)
+{
+ return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
+ & static_cast<uint32_t>(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
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;
/**
*/
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;
*
* @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
*
* @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;
* 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
* 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 */
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);
}
}
}
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{
Trace("quantifiers-sk-debug")
<< "Skolemize lemma : " << slem << std::endl;
}
- getOutputChannel().lemma(lem, false, true);
+ getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
}
return;
}
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;
d_hasAddedLemma = true;
for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
- getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
+ getOutputChannel().lemma(d_lemmas_waiting[i], LemmaProperty::PREPROCESS);
}
d_lemmas_waiting.clear();
}
}
Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
d_lemmas_produced.insert(lem);
- d_parent.getOutputChannel()->lemma(lem, false, preprocess);
+ LemmaProperty p =
+ preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE;
+ d_parent.getOutputChannel()->lemma(lem, p);
d_sentLemma = true;
}
#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"
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
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();
Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
<< CheckSatCommand(n.toExpr());
}
+ bool removable = isLemmaPropertyRemovable(p);
+ bool preprocess = isLemmaPropertyPreprocess(p);
// call preprocessor
std::vector<TrustNode> newLemmas;
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));
ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
});
- lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
+ lemma(conflict, RULE_CONFLICT, true, LemmaProperty::REMOVABLE, THEORY_LAST);
}
PROOF({
* 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 */
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);
}
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(); }
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);
}
projects / cvc5.git / commitdiff