This class is a wrapper around OutputChannel and EqualityEngine. It is preferred that the Theory use this interface when asserting "internal facts" to the equality engine, and for sending lemmas, conflicts and propagations on the output channel.
This class will be useful when trying new methods for theory combination, where all theories behavior can be modified in a standard way based on modifications to the base inference manager class.
theory/theory_engine_proof_generator.h
theory/theory_id.cpp
theory/theory_id.h
+ theory/theory_inference_manager.cpp
+ theory/theory_inference_manager.h
theory/theory_model.cpp
theory/theory_model.h
theory/theory_model_builder.cpp
d_equalityEngine(nullptr),
d_allocEqualityEngine(nullptr),
d_theoryState(nullptr),
+ d_inferManager(nullptr),
d_proofsEnabled(false)
{
smtStatisticsRegistry()->registerStat(&d_checkTime);
{
d_theoryState->setEqualityEngine(ee);
}
+ if (d_inferManager != nullptr)
+ {
+ d_inferManager->setEqualityEngine(ee);
+ }
}
void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
#include "theory/logic_info.h"
#include "theory/output_channel.h"
#include "theory/theory_id.h"
+#include "theory/theory_inference_manager.h"
#include "theory/theory_rewriter.h"
#include "theory/theory_state.h"
#include "theory/trust_node.h"
* Notice the theory is responsible for memory management of this class.
*/
TheoryState* d_theoryState;
+ /**
+ * The theory inference manager. This is a wrapper around the equality
+ * engine and the output channel. It ensures that the output channel and
+ * the equality engine are used properly.
+ */
+ TheoryInferenceManager* d_inferManager;
/**
* Whether proofs are enabled
*
--- /dev/null
+/********************* */
+/*! \file theory_inference_manager.cpp
+ ** \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 An inference manager for Theory
+ **/
+
+#include "theory/theory_inference_manager.h"
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+TheoryInferenceManager::TheoryInferenceManager(Theory& t,
+ TheoryState& state,
+ ProofNodeManager* pnm)
+ : d_theory(t),
+ d_theoryState(state),
+ d_out(t.getOutputChannel()),
+ d_ee(nullptr),
+ d_pnm(pnm),
+ d_keep(t.getSatContext())
+{
+}
+
+void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
+{
+ d_ee = ee;
+}
+
+void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
+{
+ if (!d_theoryState.isInConflict())
+ {
+ TrustNode tconf = explainConflictEqConstantMerge(a, b);
+ d_theoryState.notifyInConflict();
+ d_out.trustedConflict(tconf);
+ }
+}
+
+void TheoryInferenceManager::conflict(TNode conf)
+{
+ if (!d_theoryState.isInConflict())
+ {
+ d_theoryState.notifyInConflict();
+ d_out.conflict(conf);
+ }
+}
+
+void TheoryInferenceManager::trustedConflict(TrustNode tconf)
+{
+ if (!d_theoryState.isInConflict())
+ {
+ d_theoryState.notifyInConflict();
+ d_out.trustedConflict(tconf);
+ }
+}
+
+bool TheoryInferenceManager::propagateLit(TNode lit)
+{
+ // If already in conflict, no more propagation
+ if (d_theoryState.isInConflict())
+ {
+ return false;
+ }
+ // Propagate out
+ bool ok = d_out.propagate(lit);
+ if (!ok)
+ {
+ d_theoryState.notifyInConflict();
+ }
+ return ok;
+}
+
+TrustNode TheoryInferenceManager::explainLit(TNode lit)
+{
+ // TODO (project #37): use proof equality engine if it exists
+ if (d_ee != nullptr)
+ {
+ Node exp = d_ee->mkExplainLit(lit);
+ return TrustNode::mkTrustPropExp(lit, exp, nullptr);
+ }
+ Unimplemented() << "Inference manager for " << d_theory.getId()
+ << " was asked to explain a propagation but doesn't have an "
+ "equality engine or implement the "
+ "TheoryInferenceManager::explainLit interface!";
+}
+
+TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
+ TNode b)
+{
+ // TODO (project #37): use proof equality engine if it exists
+ if (d_ee != nullptr)
+ {
+ Node lit = a.eqNode(b);
+ Node conf = d_ee->mkExplainLit(lit);
+ return TrustNode::mkTrustConflict(conf, nullptr);
+ }
+ Unimplemented() << "Inference manager for " << d_theory.getId()
+ << " mkTrustedConflictEqConstantMerge";
+}
+
+void TheoryInferenceManager::assertInternalFact(TNode atom,
+ bool pol,
+ TNode fact)
+{
+ // call the pre-notify fact method with preReg = false, isInternal = true
+ if (d_theory.preNotifyFact(atom, pol, fact, false, true))
+ {
+ // handled in a theory-specific way that doesn't require equality engine
+ return;
+ }
+ Assert(d_ee != nullptr);
+ Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
+ << fact << std::endl;
+ if (atom.getKind() == kind::EQUAL)
+ {
+ d_ee->assertEquality(atom, pol, fact);
+ }
+ else
+ {
+ d_ee->assertPredicate(atom, pol, fact);
+ }
+ // call the notify fact method with isInternal = true
+ d_theory.notifyFact(atom, pol, fact, true);
+ Trace("infer-manager")
+ << "TheoryInferenceManager::finished assertInternalFact" << std::endl;
+ // Must reference count the equality and its explanation, which is not done
+ // by the equality engine. Notice that we do *not* need to do this for
+ // external assertions, which enter as facts in theory check.
+ d_keep.insert(atom);
+ d_keep.insert(fact);
+}
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file theory_inference_manager.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 An inference manager for Theory
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
+#define CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
+
+#include "context/cdhashset.h"
+#include "expr/node.h"
+#include "theory/output_channel.h"
+#include "theory/theory_state.h"
+#include "theory/trust_node.h"
+
+namespace CVC4 {
+
+class ProofNodeManager;
+
+namespace theory {
+
+class Theory;
+namespace eq {
+class EqualityEngine;
+}
+
+/**
+ * The base class for inference manager. An inference manager is a wrapper
+ * around the output channel and the official equality engine of a Theory.
+ * It is used for ensuring that the equality engine and output channel
+ * are used properly. This includes the following invariants:
+ *
+ * (1) The state tracks conflicts.
+ * In particular, TheoryState::isInConflict returns true whenever we have
+ * called OutputChannel::conflict in the current context, which we enforce
+ * by always setting d_state.notifyInConflict at the same time we send
+ * conflicts on the output channel.
+ *
+ * (2) The theory is notified of (internal) facts.
+ * In particular, Theory::preNotifyFact and Theory::notifyFact are called
+ * (with isInternal = true) whenever we assert internal facts using
+ * assertFactInernal below, mirroring what is done for facts from the fact
+ * queue (where isInternal = false).
+ */
+class TheoryInferenceManager
+{
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+ /**
+ * Constructor, note that state should be the official state of theory t.
+ */
+ TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
+ virtual ~TheoryInferenceManager() {}
+ //--------------------------------------- initialization
+ /**
+ * Set equality engine, ee is a pointer to the official equality engine
+ * of theory.
+ */
+ void setEqualityEngine(eq::EqualityEngine* ee);
+ //--------------------------------------- end initialization
+ /**
+ * T-propagate literal lit, possibly encountered by equality engine,
+ * returns false if we are in conflict.
+ *
+ * Note that this is the preferred method to call on
+ * EqualityEngineNotify::eqNotifyTriggerPredicate and
+ * EqualityEngineNotify::eqNotifyTriggerTermEquality.
+ */
+ bool propagateLit(TNode lit);
+ /**
+ * Return an explanation for the literal represented by parameter lit
+ * (which was previously propagated by this theory). By default, this
+ * returns the explanation given by the official equality engine of the
+ * Theory, if it exists.
+ */
+ virtual TrustNode explainLit(TNode lit);
+ /**
+ * Raise conflict, called when constants a and b merge. Sends the conflict
+ * on the output channel corresponding to the equality engine's explanation
+ * of (= a b). The proof equality engine (if it exists) will be used as the
+ * proof generator.
+ *
+ * Note that this is the preferred method to call on
+ * EqualityEngineNotify::eqNotifyConstantTermMerge.
+ */
+ void conflictEqConstantMerge(TNode a, TNode b);
+ /**
+ * Raise conflict conf (of any form), without proofs. This method should
+ * only be called if there is not yet proof support in the given theory.
+ */
+ void conflict(TNode conf);
+ /**
+ * Raise trusted conflict tconf (of any form) where a proof generator has
+ * been provided in a custom way.
+ */
+ void trustedConflict(TrustNode tconf);
+ /**
+ * Assert internal fact. This is recommended method for asserting "internal"
+ * facts into the equality engine of the theory. In particular, this method
+ * should be used for anything the theory infers that is not sent on the
+ * output channel as a propagation or lemma. This method ensures that the
+ * Theory's preNotifyFact and notifyFact method have been called with
+ * isInternal = true.
+ */
+ void assertInternalFact(TNode atom, bool pol, TNode fact);
+
+ protected:
+ /**
+ * Explain conflict from constants merging in the equality engine. This
+ * method is called by conflictEqConstantMerge. By default, it returns
+ * the explanation of the official equality engine of the theory, if it
+ * exists.
+ */
+ virtual TrustNode explainConflictEqConstantMerge(TNode a, TNode b);
+ /** The theory object */
+ Theory& d_theory;
+ /** Reference to the state of theory */
+ TheoryState& d_theoryState;
+ /** Reference to the output channel of the theory */
+ OutputChannel& d_out;
+ /** Pointer to equality engine of the theory. */
+ eq::EqualityEngine* d_ee;
+ /** The proof node manager of the theory */
+ ProofNodeManager* d_pnm;
+ /**
+ * The keep set of this class. This set is maintained to ensure that
+ * facts and their explanations are ref-counted. Since facts and their
+ * explanations are SAT-context-dependent, this set is also
+ * SAT-context-dependent.
+ */
+ NodeSet d_keep;
+};
+
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__THEORY_INFERENCE_MANAGER_H */
projects / cvc5.git / commitdiff