From ccfe07f8daba372d2d88b249aa27fe78ad22ed54 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Jun 2021 01:29:10 -0500 Subject: Make TheoryUF compatible with central equality engine (#6695) Work towards central equality engine. This does some minor reorganization to TheoryUF, related to UF+cardinality constraints that makes it compatible with central equality engine. In particular, preNotifyFact is removed in favor of adding conflicts after cardinality constraints are added to the equality engine. This ensures that the central equality engine can explain conflicts that involve cardinality constraints (which will no longer be the responsibility of UF when --ee-mode=central). --- src/theory/uf/theory_uf.h | 6 ------ 1 file changed, 6 deletions(-) (limited to 'src/theory/uf/theory_uf.h') diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index c811e08e8..c953cfe5c 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -128,12 +128,6 @@ private: bool needsCheckLastEffort() override; /** 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 -- cgit v1.2.3