diff options
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/kinds | 2 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 13 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 15 |
3 files changed, 10 insertions, 20 deletions
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 235b61172..7a3fb00a4 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -8,7 +8,7 @@ theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h" typechecker "theory/sep/theory_sep_type_rules.h" properties polite stable-infinite parametric -properties check propagate presolve +properties check presolve rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index f75eb4472..cf3cf2f9a 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -111,13 +111,13 @@ Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstit // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// - -bool TheorySep::propagate(TNode literal) +bool TheorySep::propagateLit(TNode literal) { - Debug("sep") << "TheorySep::propagate(" << literal << ")" << std::endl; + Debug("sep") << "TheorySep::propagateLit(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("sep") << "TheorySep::propagate(" << literal << "): already in conflict" << std::endl; + Debug("sep") << "TheorySep::propagateLit(" << literal + << "): already in conflict" << std::endl; return false; } bool ok = d_out->propagate(literal); @@ -146,11 +146,6 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) { } } - -void TheorySep::propagate(Effort e){ - -} - TrustNode TheorySep::explain(TNode literal) { Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index b178b97db..bbb37a3a2 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -105,13 +105,12 @@ class TheorySep : public Theory { private: /** Should be called to propagate the literal. */ - bool propagate(TNode literal); + bool propagateLit(TNode literal); /** Explain why this literal is true by adding assumptions */ void explain(TNode literal, std::vector<TNode>& assumptions); public: - void propagate(Effort e) override; TrustNode explain(TNode n) override; public: @@ -163,9 +162,9 @@ class TheorySep : public Theory { // Just forward to sep if (value) { - return d_sep.propagate(predicate); + return d_sep.propagateLit(predicate); } - return d_sep.propagate(predicate.notNode()); + return d_sep.propagateLit(predicate.notNode()); } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, @@ -178,13 +177,9 @@ class TheorySep : public Theory { if (value) { // Propagate equality between shared terms - return d_sep.propagate(t1.eqNode(t2)); + return d_sep.propagateLit(t1.eqNode(t2)); } - else - { - return d_sep.propagate(t1.eqNode(t2).notNode()); - } - return true; + return d_sep.propagateLit(t1.eqNode(t2).notNode()); } void eqNotifyConstantTermMerge(TNode t1, TNode t2) override |