diff options
Diffstat (limited to 'src/theory/sep/theory_sep.h')
| -rw-r--r-- | src/theory/sep/theory_sep.h | 15 |
1 files changed, 5 insertions, 10 deletions
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 |