summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/theory/theory.cpp5
-rw-r--r--src/theory/theory.h7
-rw-r--r--src/theory/theory_inference_manager.cpp147
-rw-r--r--src/theory/theory_inference_manager.h148
5 files changed, 309 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c55c29ed4..df981db2d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -823,6 +823,8 @@ libcvc4_add_sources(
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
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 50a5c4493..66541a63e 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -81,6 +81,7 @@ Theory::Theory(TheoryId id,
d_equalityEngine(nullptr),
d_allocEqualityEngine(nullptr),
d_theoryState(nullptr),
+ d_inferManager(nullptr),
d_proofsEnabled(false)
{
smtStatisticsRegistry()->registerStat(&d_checkTime);
@@ -106,6 +107,10 @@ void Theory::setEqualityEngine(eq::EqualityEngine* ee)
{
d_theoryState->setEqualityEngine(ee);
}
+ if (d_inferManager != nullptr)
+ {
+ d_inferManager->setEqualityEngine(ee);
+ }
}
void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1fdf96331..29a3a0998 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -43,6 +43,7 @@
#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"
@@ -257,6 +258,12 @@ class Theory {
*/
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
*
*/
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
new file mode 100644
index 000000000..54f33f6e7
--- /dev/null
+++ b/src/theory/theory_inference_manager.cpp
@@ -0,0 +1,147 @@
+/********************* */
+/*! \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
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
new file mode 100644
index 000000000..914c87d19
--- /dev/null
+++ b/src/theory/theory_inference_manager.h
@@ -0,0 +1,148 @@
+/********************* */
+/*! \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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback