summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/theory_uf.cpp95
-rw-r--r--src/theory/uf/theory_uf.h19
2 files changed, 68 insertions, 46 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 862a906a0..4f9c3bed5 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -54,16 +54,12 @@ TheoryUF::TheoryUF(context::Context* c,
* so make sure it's initialized first. */
d_thss(nullptr),
d_ho(nullptr),
- d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true),
d_conflict(c, false),
d_functionsTerms(c),
d_symb(u, instanceName)
{
d_true = NodeManager::currentNM()->mkConst( true );
- // The kinds we are treating as function application in congruence
- d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo());
-
ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
if (pc != nullptr)
{
@@ -74,11 +70,17 @@ TheoryUF::TheoryUF(context::Context* c,
TheoryUF::~TheoryUF() {
}
-void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_equalityEngine.setMasterEqualityEngine(eq);
+TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = d_instanceName + "theory::uf::ee";
+ return true;
}
void TheoryUF::finishInit() {
+ Assert(d_equalityEngine != nullptr);
// combined cardinality constraints are not evaluated in getModelValue
d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT);
// Initialize the cardinality constraints solver if the logic includes UF,
@@ -90,9 +92,11 @@ void TheoryUF::finishInit() {
d_thss.reset(new CardinalityExtension(
getSatContext(), getUserContext(), *d_out, this));
}
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
if (options::ufHo())
{
- d_equalityEngine.addFunctionKind(kind::HO_APPLY);
+ d_equalityEngine->addFunctionKind(kind::HO_APPLY);
d_ho.reset(new HoExtension(*this, getSatContext(), getUserContext()));
}
}
@@ -148,7 +152,7 @@ void TheoryUF::check(Effort level) {
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.assertEquality(atom, polarity, fact);
+ d_equalityEngine->assertEquality(atom, polarity, fact);
if( options::ufHo() && options::ufHoExt() ){
if( !polarity && !d_conflict && atom[0].getType().isFunction() ){
// apply extensionality eagerly using the ho extension
@@ -169,10 +173,10 @@ void TheoryUF::check(Effort level) {
}
//needed for models
if( options::produceModels() ){
- d_equalityEngine.assertPredicate(atom, polarity, fact);
+ d_equalityEngine->assertPredicate(atom, polarity, fact);
}
} else {
- d_equalityEngine.assertPredicate(atom, polarity, fact);
+ d_equalityEngine->assertPredicate(atom, polarity, fact);
}
}
@@ -198,7 +202,7 @@ Node TheoryUF::getOperatorForApplyTerm( TNode node ) {
if( node.getKind()==kind::APPLY_UF ){
return node.getOperator();
}else{
- return d_equalityEngine.getRepresentative( node[0] );
+ return d_equalityEngine->getRepresentative(node[0]);
}
}
@@ -242,17 +246,17 @@ void TheoryUF::preRegisterTerm(TNode node) {
switch (node.getKind()) {
case kind::EQUAL:
// Add the trigger for equality
- d_equalityEngine.addTriggerEquality(node);
+ d_equalityEngine->addTriggerEquality(node);
break;
case kind::APPLY_UF:
case kind::HO_APPLY:
// Maybe it's a predicate
if (node.getType().isBoolean()) {
// Get triggered for both equal and dis-equal
- d_equalityEngine.addTriggerPredicate(node);
+ d_equalityEngine->addTriggerPredicate(node);
} else {
// Function applications/predicates
- d_equalityEngine.addTerm(node);
+ d_equalityEngine->addTerm(node);
}
// Remember the function and predicate terms
d_functionsTerms.push_back(node);
@@ -263,7 +267,7 @@ void TheoryUF::preRegisterTerm(TNode node) {
break;
default:
// Variables etc
- d_equalityEngine.addTerm(node);
+ d_equalityEngine->addTerm(node);
break;
}
}/* TheoryUF::preRegisterTerm() */
@@ -294,9 +298,10 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
+ d_equalityEngine->explainEquality(
+ atom[0], atom[1], polarity, assumptions, pf);
} else {
- d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
+ d_equalityEngine->explainPredicate(atom, polarity, assumptions, pf);
}
if( pf ){
Debug("pf::uf") << std::endl;
@@ -331,7 +336,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m)
// Compute terms appearing in assertions and shared terms
computeRelevantTerms(termSet);
- if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
{
Trace("uf") << "Collect model info fail UF" << std::endl;
return false;
@@ -495,13 +500,15 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
// Check for equality (simplest)
- if (d_equalityEngine.areEqual(a, b)) {
+ if (d_equalityEngine->areEqual(a, b))
+ {
// The terms are implied to be equal
return EQUALITY_TRUE;
}
// Check for disequality
- if (d_equalityEngine.areDisequal(a, b, false)) {
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
// The terms are implied to be dis-equal
return EQUALITY_FALSE;
}
@@ -512,15 +519,19 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
void TheoryUF::addSharedTerm(TNode t) {
Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
- d_equalityEngine.addTriggerTerm(t, THEORY_UF);
+ d_equalityEngine->addTriggerTerm(t, THEORY_UF);
}
bool TheoryUF::areCareDisequal(TNode x, TNode y){
- Assert(d_equalityEngine.hasTerm(x));
- Assert(d_equalityEngine.hasTerm(y));
- if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
+ if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
+ && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
+ {
+ TNode x_shared =
+ d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
+ TNode y_shared =
+ d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
return true;
@@ -538,21 +549,27 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
if( t2!=NULL ){
Node f1 = t1->getData();
Node f2 = t2->getData();
- if( !d_equalityEngine.areEqual( f1, f2 ) ){
+ if (!d_equalityEngine->areEqual(f1, f2))
+ {
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > currentPairs;
unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) {
TNode x = f1[k];
TNode y = f2[k];
- Assert(d_equalityEngine.hasTerm(x));
- Assert(d_equalityEngine.hasTerm(y));
- Assert(!d_equalityEngine.areDisequal(x, y, false));
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
+ Assert(!d_equalityEngine->areDisequal(x, y, false));
Assert(!areCareDisequal(x, y));
- if( !d_equalityEngine.areEqual( x, y ) ){
- if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
+ if (!d_equalityEngine->areEqual(x, y))
+ {
+ if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
+ && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
+ {
+ TNode x_shared =
+ d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
+ TNode y_shared =
+ d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
currentPairs.push_back(make_pair(x_shared, y_shared));
}
}
@@ -580,7 +597,8 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
std::map<TNode, TNodeTrie>::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
- if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+ if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
+ {
if( !areCareDisequal(it->first, it2->first) ){
addCarePairs( &it->second, &it2->second, arity, depth+1 );
}
@@ -593,7 +611,7 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
{
for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
{
- if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+ if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
{
if (!areCareDisequal(tt1.first, tt2.first))
{
@@ -621,8 +639,9 @@ void TheoryUF::computeCareGraph() {
std::vector< TNode > reps;
bool has_trigger_arg = false;
for( unsigned j=arg_start_index; j<f1.getNumChildren(); j++ ){
- reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
- if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_UF ) ){
+ reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
+ if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_UF))
+ {
has_trigger_arg = true;
}
}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 345547301..001c947e9 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -116,9 +116,6 @@ private:
/** the higher-order solver extension (or nullptr if it does not exist) */
std::unique_ptr<HoExtension> d_ho;
- /** Equaltity engine */
- eq::EqualityEngine d_equalityEngine;
-
/** Are we in conflict */
context::CDO<bool> d_conflict;
@@ -186,10 +183,18 @@ private:
~TheoryUF();
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
void finishInit() override;
+ //--------------------------------- end initialization
void check(Effort) override;
TrustNode expandDefinition(Node node) override;
@@ -210,8 +215,6 @@ private:
std::string identify() const override { return "THEORY_UF"; }
- eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
-
/** get a pointer to the uf with cardinality */
CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
/** are we in conflict? */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback