diff options
Diffstat (limited to 'src/theory/sep/theory_sep.h')
| -rw-r--r-- | src/theory/sep/theory_sep.h | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 935170adf..3685ea063 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -66,7 +66,12 @@ class TheorySep : public Theory { bool pol, bool hasPol, bool underSpatial ); public: - TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheorySep(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); ~TheorySep(); TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } @@ -81,7 +86,6 @@ class TheorySep : public Theory { public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; - Node ppRewrite(TNode atom) override; void ppNotifyAssertions(const std::vector<Node>& assertions) override; ///////////////////////////////////////////////////////////////////////////// @@ -97,7 +101,7 @@ class TheorySep : public Theory { public: void propagate(Effort e) override; - Node explain(TNode n) override; + TrustNode explain(TNode n) override; public: void addSharedTerm(TNode t) override; |