This makes the shared terms database use a proof equality engine as a layer on top of its equality engine, analogous to how this done in theories.
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm)
: d_te(te),
+ d_pnm(pnm),
d_logicInfo(te.getLogicInfo()),
d_paraTheories(paraTheories),
d_eemanager(nullptr),
if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
{
// use the distributed shared solver
- d_sharedSolver.reset(new SharedSolverDistributed(d_te));
+ d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
// make the distributed equality engine manager
d_eemanager.reset(
new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
void sendLemma(TrustNode trn, TheoryId atomsTo);
/** Reference to the theory engine */
TheoryEngine& d_te;
+ /** The proof node manager */
+ ProofNodeManager* d_pnm;
/** Logic info of theory engine (cached) */
const LogicInfo& d_logicInfo;
/** List of parametric theories of theory engine */
// In distributed equality engine management, shared terms database also
// maintains an equality engine. In central equality engine management,
// it does not.
-SharedSolver::SharedSolver(TheoryEngine& te)
+SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm)
: d_te(te),
d_logicInfo(te.getLogicInfo()),
- d_sharedTerms(&d_te, d_te.getSatContext()),
+ d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm),
d_sharedTermsVisitor(d_sharedTerms)
{
}
#define CVC4__THEORY__SHARED_SOLVER__H
#include "expr/node.h"
+#include "expr/proof_node_manager.h"
#include "theory/ee_setup_info.h"
#include "theory/logic_info.h"
#include "theory/shared_terms_database.h"
class SharedSolver
{
public:
- SharedSolver(TheoryEngine& te);
+ SharedSolver(TheoryEngine& te, ProofNodeManager* pnm);
virtual ~SharedSolver() {}
//------------------------------------- initialization
/**
namespace CVC4 {
namespace theory {
-SharedSolverDistributed::SharedSolverDistributed(TheoryEngine& te)
- : SharedSolver(te)
+SharedSolverDistributed::SharedSolverDistributed(TheoryEngine& te,
+ ProofNodeManager* pnm)
+ : SharedSolver(te, pnm)
{
}
TrustNode texp;
if (id == THEORY_BUILTIN)
{
- // explanation based on the specific solver
+ // explanation using the shared terms database
texp = d_sharedTerms.explain(literal);
Trace("shared-solver")
<< "\tTerm was propagated by THEORY_BUILTIN. Explanation: "
class SharedSolverDistributed : public SharedSolver
{
public:
- SharedSolverDistributed(TheoryEngine& te);
+ SharedSolverDistributed(TheoryEngine& te, ProofNodeManager* pnm);
virtual ~SharedSolverDistributed() {}
//------------------------------------- initialization
/**
namespace CVC4 {
SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
- context::Context* context)
+ context::Context* context,
+ context::UserContext* userContext,
+ ProofNodeManager* pnm)
: ContextNotifyObj(context),
d_statSharedTerms("theory::shared_terms", 0),
d_addedSharedTermsSize(context, 0),
d_theoryEngine(theoryEngine),
d_inConflict(context, false),
d_conflictPolarity(),
- d_equalityEngine(nullptr)
+ d_satContext(context),
+ d_userContext(userContext),
+ d_equalityEngine(nullptr),
+ d_pfee(nullptr),
+ d_pnm(pnm)
{
smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
}
void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
{
+ Assert(ee != nullptr);
d_equalityEngine = ee;
+ // if proofs are enabled, make the proof equality engine
+ if (d_pnm != nullptr)
+ {
+ d_pfee.reset(
+ new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm));
+ }
}
bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi)
return true;
}
-static Node mkAnd(const std::vector<TNode>& conjunctions) {
- Assert(conjunctions.size() > 0);
-
- std::set<TNode> all;
- all.insert(conjunctions.begin(), conjunctions.end());
-
- if (all.size() == 1) {
- // All the same, or just one
- return conjunctions[0];
+void SharedTermsDatabase::checkForConflict()
+{
+ if (!d_inConflict)
+ {
+ return;
}
-
- NodeBuilder<> conjunction(kind::AND);
- std::set<TNode>::const_iterator it = all.begin();
- std::set<TNode>::const_iterator it_end = all.end();
- while (it != it_end) {
- conjunction << *it;
- ++ it;
+ d_inConflict = false;
+ TrustNode trnc;
+ if (d_pfee != nullptr)
+ {
+ Node conflict = d_conflictLHS.eqNode(d_conflictRHS);
+ conflict = d_conflictPolarity ? conflict : conflict.notNode();
+ trnc = d_pfee->assertConflict(conflict);
}
-
- return conjunction;
-}
-
-void SharedTermsDatabase::checkForConflict() {
- Assert(d_equalityEngine != nullptr);
- if (d_inConflict) {
- d_inConflict = false;
+ else
+ {
+ // standard explain
std::vector<TNode> assumptions;
d_equalityEngine->explainEquality(
d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
- Node conflict = mkAnd(assumptions);
- TrustNode tconf = TrustNode::mkTrustConflict(conflict);
- d_theoryEngine->conflict(tconf, THEORY_BUILTIN);
- d_conflictLHS = d_conflictRHS = Node::null();
+ Node conflictNode = NodeManager::currentNM()->mkAnd(assumptions);
+ trnc = TrustNode::mkTrustConflict(conflictNode, nullptr);
}
+ d_theoryEngine->conflict(trnc, THEORY_BUILTIN);
+ d_conflictLHS = d_conflictRHS = Node::null();
}
bool SharedTermsDatabase::isKnown(TNode literal) const {
}
}
-TrustNode SharedTermsDatabase::explain(TNode literal) const
+theory::TrustNode SharedTermsDatabase::explain(TNode literal) const
{
- Assert(d_equalityEngine != nullptr);
- bool polarity = literal.getKind() != kind::NOT;
- TNode atom = polarity ? literal : literal[0];
- Assert(atom.getKind() == kind::EQUAL);
- std::vector<TNode> assumptions;
- d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
- Node exp = mkAnd(assumptions);
+ if (d_pfee != nullptr)
+ {
+ // use the proof equality engine if it exists
+ return d_pfee->explain(literal);
+ }
+ // otherwise, explain without proofs
+ Node exp = d_equalityEngine->mkExplainLit(literal);
+ // no proof generator
return TrustNode::mkTrustPropExp(literal, exp, nullptr);
}
#include "context/cdhashset.h"
#include "expr/node.h"
+#include "expr/proof_node_manager.h"
#include "theory/ee_setup_info.h"
#include "theory/theory_id.h"
+#include "theory/trust_node.h"
#include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
#include "util/statistics_registry.h"
namespace CVC4 {
class TheoryEngine;
class SharedTermsDatabase : public context::ContextNotifyObj {
-
-public:
-
+ public:
/** A container for a list of shared terms */
typedef std::vector<TNode> shared_terms_list;
/** The iterator to go through the shared terms list */
typedef shared_terms_list::const_iterator shared_terms_iterator;
-private:
-
+ private:
/** Some statistics */
IntStat d_statSharedTerms;
typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet;
RegisteredEqualitiesSet d_registeredEqualities;
-private:
-
+ private:
/** This method removes all the un-necessary stuff from the maps */
void backtrack();
*/
void checkForConflict();
-public:
-
- SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
+ public:
+ /**
+ * @param theoryEngine The parent theory engine
+ * @param context The SAT context
+ * @param userContext The user context
+ * @param pnm The proof node manager to use, which is non-null if proofs
+ * are enabled.
+ */
+ SharedTermsDatabase(TheoryEngine* theoryEngine,
+ context::Context* context,
+ context::UserContext* userContext,
+ ProofNodeManager* pnm);
~SharedTermsDatabase();
//-------------------------------------------- initialization
* This method gets called on backtracks from the context manager.
*/
void contextNotifyPop() override { backtrack(); }
-
+ /** The SAT search context. */
+ context::Context* d_satContext;
+ /** The user level assertion context. */
+ context::UserContext* d_userContext;
/** Equality engine */
theory::eq::EqualityEngine* d_equalityEngine;
+ /** Proof equality engine */
+ std::unique_ptr<theory::eq::ProofEqEngine> d_pfee;
+ /** The proof node manager */
+ ProofNodeManager* d_pnm;
};
}
projects / cvc5.git / commitdiff