diff options
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/theory/theory.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory.h | 7 | ||||
-rw-r--r-- | src/theory/theory_inference_manager.cpp | 147 | ||||
-rw-r--r-- | src/theory/theory_inference_manager.h | 148 |
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 */ |