summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/sets/theory_sets.cpp41
-rw-r--r--src/theory/sets/theory_sets.h17
-rw-r--r--src/theory/sets/theory_sets_private.cpp199
-rw-r--r--src/theory/sets/theory_sets_private.h15
4 files changed, 124 insertions, 148 deletions
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 0bf2ed2ea..cb42f09d5 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -67,12 +67,12 @@ void TheorySets::finishInit()
d_valuation.setUnevaluatedKind(WITNESS);
// functions we are doing congruence over
- d_equalityEngine->addFunctionKind(kind::SINGLETON);
- d_equalityEngine->addFunctionKind(kind::UNION);
- d_equalityEngine->addFunctionKind(kind::INTERSECTION);
- d_equalityEngine->addFunctionKind(kind::SETMINUS);
- d_equalityEngine->addFunctionKind(kind::MEMBER);
- d_equalityEngine->addFunctionKind(kind::SUBSET);
+ d_equalityEngine->addFunctionKind(SINGLETON);
+ d_equalityEngine->addFunctionKind(UNION);
+ d_equalityEngine->addFunctionKind(INTERSECTION);
+ d_equalityEngine->addFunctionKind(SETMINUS);
+ d_equalityEngine->addFunctionKind(MEMBER);
+ d_equalityEngine->addFunctionKind(SUBSET);
// relation operators
d_equalityEngine->addFunctionKind(PRODUCT);
d_equalityEngine->addFunctionKind(JOIN);
@@ -88,14 +88,20 @@ void TheorySets::finishInit()
d_internal->finishInit();
}
-void TheorySets::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); }
+void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
-void TheorySets::check(Effort e) {
- if (done() && e < Theory::EFFORT_FULL) {
- return;
- }
- TimerStat::CodeTimer checkTimer(d_checkTime);
- d_internal->check(e);
+bool TheorySets::preNotifyFact(
+ TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
+{
+ return d_internal->preNotifyFact(atom, polarity, fact);
+}
+
+void TheorySets::notifyFact(TNode atom,
+ bool polarity,
+ TNode fact,
+ bool isInternal)
+{
+ d_internal->notifyFact(atom, polarity, fact);
}
bool TheorySets::collectModelValues(TheoryModel* m,
@@ -114,15 +120,12 @@ TrustNode TheorySets::explain(TNode node)
return TrustNode::mkTrustPropExp(node, exp, nullptr);
}
-EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) {
- return d_internal->getEqualityStatus(a, b);
-}
-
Node TheorySets::getModelValue(TNode node) {
return Node::null();
}
-void TheorySets::preRegisterTerm(TNode node) {
+void TheorySets::preRegisterTerm(TNode node)
+{
d_internal->preRegisterTerm(node);
}
@@ -158,7 +161,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubsti
Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
// this is based off of Theory::ppAssert
- if (in.getKind() == kind::EQUAL)
+ if (in.getKind() == EQUAL)
{
if (in[0].isVar() && isLegalElimination(in[0], in[1]))
{
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index a826a43af..7787c0f9b 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -58,13 +58,23 @@ class TheorySets : public Theory
void finishInit() override;
//--------------------------------- end initialization
- void notifySharedTerm(TNode) override;
- void check(Effort) override;
+ //--------------------------------- standard check
+ /** Post-check, called after the fact queue of the theory is processed. */
+ void postCheck(Effort level) override;
+ /** Pre-notify fact, return true if processed. */
+ bool preNotifyFact(TNode atom,
+ bool pol,
+ TNode fact,
+ bool isPrereg,
+ bool isInternal) override;
+ /** Notify fact */
+ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+ //--------------------------------- end standard check
+ /** Collect model values in m based on the relevant terms given by termSet */
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
void computeCareGraph() override;
TrustNode explain(TNode) override;
- EqualityStatus getEqualityStatus(TNode a, TNode b) override;
Node getModelValue(TNode) override;
std::string identify() const override { return "THEORY_SETS"; }
void preRegisterTerm(TNode node) override;
@@ -72,6 +82,7 @@ class TheorySets : public Theory
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
void presolve() override;
bool isEntailed(Node n, bool pol);
+
private:
/** Functions to handle callbacks from equality engine */
class NotifyClass : public eq::EqualityEngineNotify
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 78824636a..c432c8039 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -276,74 +276,21 @@ bool TheorySetsPrivate::assertFact(Node fact, Node exp)
<< ", exp = " << exp << std::endl;
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
- if (!d_state.isEntailed(atom, polarity))
+ if (d_state.isEntailed(atom, polarity))
{
- if (atom.getKind() == kind::EQUAL)
- {
- d_equalityEngine->assertEquality(atom, polarity, exp);
- }
- else
- {
- d_equalityEngine->assertPredicate(atom, polarity, exp);
- }
- if (!d_state.isInConflict())
- {
- if (atom.getKind() == kind::MEMBER && polarity)
- {
- // check if set has a value, if so, we can propagate
- Node r = d_equalityEngine->getRepresentative(atom[1]);
- EqcInfo* e = getOrMakeEqcInfo(r, true);
- if (e)
- {
- Node s = e->d_singleton;
- if (!s.isNull())
- {
- Node pexp = NodeManager::currentNM()->mkNode(
- kind::AND, atom, atom[1].eqNode(s));
- d_keep.insert(pexp);
- if (s.getKind() == kind::SINGLETON)
- {
- if (s[0] != atom[0])
- {
- Trace("sets-prop")
- << "Propagate mem-eq : " << pexp << std::endl;
- Node eq = s[0].eqNode(atom[0]);
- d_keep.insert(eq);
- assertFact(eq, pexp);
- }
- }
- else
- {
- Trace("sets-prop")
- << "Propagate mem-eq conflict : " << pexp << std::endl;
- d_im.conflict(pexp);
- }
- }
- }
- // add to membership list
- NodeIntMap::iterator mem_i = d_members.find(r);
- int n_members = 0;
- if (mem_i != d_members.end())
- {
- n_members = (*mem_i).second;
- }
- d_members[r] = n_members + 1;
- if (n_members < (int)d_members_data[r].size())
- {
- d_members_data[r][n_members] = atom;
- }
- else
- {
- d_members_data[r].push_back(atom);
- }
- }
- }
- return true;
+ return false;
+ }
+ if (atom.getKind() == kind::EQUAL)
+ {
+ d_equalityEngine->assertEquality(atom, polarity, exp);
}
else
{
- return false;
+ d_equalityEngine->assertPredicate(atom, polarity, exp);
}
+ // call the notify new fact method
+ notifyFact(atom, polarity, exp);
+ return true;
}
void TheorySetsPrivate::fullEffortReset()
@@ -950,26 +897,10 @@ void TheorySetsPrivate::checkReduceComprehensions()
}
}
-/**************************** TheorySetsPrivate *****************************/
-/**************************** TheorySetsPrivate *****************************/
-/**************************** TheorySetsPrivate *****************************/
+//--------------------------------- standard check
-void TheorySetsPrivate::check(Theory::Effort level)
+void TheorySetsPrivate::postCheck(Theory::Effort level)
{
- Trace("sets-check") << "Sets check effort " << level << std::endl;
- if (level == Theory::EFFORT_LAST_CALL)
- {
- return;
- }
- while (!d_external.done() && !d_state.isInConflict())
- {
- // Get all the assertions
- Assertion assertion = d_external.get();
- TNode fact = assertion.d_assertion;
- Trace("sets-assert") << "Assert from input " << fact << std::endl;
- // assert the fact
- assertFact(fact, fact);
- }
Trace("sets-check") << "Sets finished assertions effort " << level
<< std::endl;
// invoke full effort check, relations check
@@ -989,18 +920,75 @@ void TheorySetsPrivate::check(Theory::Effort level)
}
}
Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
-} /* TheorySetsPrivate::check() */
+}
-/************************ Sharing ************************/
-/************************ Sharing ************************/
-/************************ Sharing ************************/
+bool TheorySetsPrivate::preNotifyFact(TNode atom, bool polarity, TNode fact)
+{
+ // use entailment check (is this necessary?)
+ return d_state.isEntailed(atom, polarity);
+}
-void TheorySetsPrivate::addSharedTerm(TNode n)
+void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
{
- Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n << ")"
- << std::endl;
- d_equalityEngine->addTriggerTerm(n, THEORY_SETS);
+ if (d_state.isInConflict())
+ {
+ return;
+ }
+ if (atom.getKind() == kind::MEMBER && polarity)
+ {
+ // check if set has a value, if so, we can propagate
+ Node r = d_equalityEngine->getRepresentative(atom[1]);
+ EqcInfo* e = getOrMakeEqcInfo(r, true);
+ if (e)
+ {
+ Node s = e->d_singleton;
+ if (!s.isNull())
+ {
+ Node pexp = NodeManager::currentNM()->mkNode(
+ kind::AND, atom, atom[1].eqNode(s));
+ d_keep.insert(pexp);
+ if (s.getKind() == kind::SINGLETON)
+ {
+ if (s[0] != atom[0])
+ {
+ Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl;
+ Node eq = s[0].eqNode(atom[0]);
+ d_keep.insert(eq);
+ // triggers an internal inference
+ assertFact(eq, pexp);
+ }
+ }
+ else
+ {
+ Trace("sets-prop")
+ << "Propagate mem-eq conflict : " << pexp << std::endl;
+ d_im.conflict(pexp);
+ }
+ }
+ }
+ // add to membership list
+ NodeIntMap::iterator mem_i = d_members.find(r);
+ int n_members = 0;
+ if (mem_i != d_members.end())
+ {
+ n_members = (*mem_i).second;
+ }
+ d_members[r] = n_members + 1;
+ if (n_members < (int)d_members_data[r].size())
+ {
+ d_members_data[r][n_members] = atom;
+ }
+ else
+ {
+ d_members_data[r].push_back(atom);
+ }
+ }
}
+//--------------------------------- end standard check
+
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+/************************ Sharing ************************/
void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
TNodeTrie* t2,
@@ -1193,37 +1181,6 @@ bool TheorySetsPrivate::isCareArg(Node n, unsigned a)
}
}
-EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b)
-{
- Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
- if (d_equalityEngine->areEqual(a, b))
- {
- // The terms are implied to be equal
- return EQUALITY_TRUE;
- }
- if (d_equalityEngine->areDisequal(a, b, false))
- {
- // The terms are implied to be dis-equal
- return EQUALITY_FALSE;
- }
- return EQUALITY_UNKNOWN;
- /*
- Node aModelValue = d_external.d_valuation.getModelValue(a);
- if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; }
- Node bModelValue = d_external.d_valuation.getModelValue(b);
- if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; }
- if( aModelValue == bModelValue ) {
- // The term are true in current model
- return EQUALITY_TRUE_IN_MODEL;
- } else {
- return EQUALITY_FALSE_IN_MODEL;
- }
- */
- // }
- // //TODO: can we be more precise sometimes?
- // return EQUALITY_UNKNOWN;
-}
-
/******************** Model generation ********************/
/******************** Model generation ********************/
/******************** Model generation ********************/
@@ -1261,7 +1218,7 @@ std::string traceElements(const Node& set)
bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
const std::set<Node>& termSet)
{
- Trace("sets-model") << "Set collect model info" << std::endl;
+ Trace("sets-model") << "Set collect model values" << std::endl;
NodeManager* nm = NodeManager::currentNM();
std::map<Node, Node> mvals;
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 387d56de9..0df1eabc5 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -172,18 +172,23 @@ class TheorySetsPrivate {
*/
void finishInit();
+ //--------------------------------- standard check
+ /** Post-check, called after the fact queue of the theory is processed. */
+ void postCheck(Theory::Effort level);
+ /** Preprocess fact, return true if processed. */
+ bool preNotifyFact(TNode atom, bool polarity, TNode fact);
+ /** Notify new fact */
+ void notifyFact(TNode atom, bool polarity, TNode fact);
+ //--------------------------------- end standard check
+
+ /** Collect model values in m based on the relevant terms given by termSet */
void addSharedTerm(TNode);
-
- void check(Theory::Effort);
-
bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet);
void computeCareGraph();
Node explain(TNode);
- EqualityStatus getEqualityStatus(TNode a, TNode b);
-
void preRegisterTerm(TNode node);
/** expandDefinition
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback