diff options
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 30de7bbad..ad3b91b07 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -55,19 +55,28 @@ class TheoryArith : public Theory { ProofNodeManager* pnm = nullptr); virtual ~TheoryArith(); + //--------------------------------- initialization + /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** + * Returns true if this theory needs an equality engine, which is assigned + * to it (d_equalityEngine) by the equality engine manager during + * TheoryEngine::finishInit, prior to calling finishInit for this theory. + * If this method returns true, it stores instructions for the notifications + * this Theory wishes to receive from its equality engine. + */ + bool needsEqualityEngine(EeSetupInfo& esi) override; + /** finish initialization */ + void finishInit() override; + //--------------------------------- end initialization /** * Does non-context dependent setup for a node connected to a theory. */ void preRegisterTerm(TNode n) override; - void finishInit() override; - TrustNode expandDefinition(Node node) override; - void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - void check(Effort e) override; bool needsCheckLastEffort() override; void propagate(Effort e) override; |