diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-29 11:11:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-29 16:11:05 +0000 |
| commit | b685ed411b6814f0810ce8f61d07aa49bd75ea3b (patch) | |
| tree | 75029fdd0b7b8d82f6296047c10818cb745c9cdb /src/theory/theory.h | |
| parent | f2672e53fae29abe40fc69b004d1df5be0ce1e8b (diff) | |
Integrate central equality engine approach into theory engine, add option and regressions (#6943)
This commit makes TheoryEngine take into account whether theories are using the central equality engine.
With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
Diffstat (limited to 'src/theory/theory.h')
| -rw-r--r-- | src/theory/theory.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 7149d8e3f..41f35601b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -877,10 +877,12 @@ class Theory { */ virtual std::pair<bool, Node> entailmentCheck(TNode lit); - /** uses central equality engine */ + /** Return true if this theory uses central equality engine */ bool usesCentralEqualityEngine() const; /** uses central equality engine (static) */ static bool usesCentralEqualityEngine(TheoryId id); + /** Explains/propagates via central equality engine only */ + static bool expUsingCentralEqualityEngine(TheoryId id); };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); |