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`.

3 files changed, 26 insertions, 0 deletions

diff --git a/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2
new file mode 100644
index 000000000..fa91fe7de
--- /dev/null
+++ b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Array (_ BitVec 1) (_ BitVec 16)))
+(assert (not (= (_ bv0 16) (select a ((_ extract 14 14) (select a (_ bv0 1)))))))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2
new file mode 100644
index 000000000..d81c3723d
--- /dev/null
+++ b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((T 0)) (((A) (B (proj0B T) (proj1B T)) (C (proj0C T)) (D (proj0D T) ))))
+(declare-fun w () T)
+(declare-fun u () T)
+(assert (= w (B (D u) (B (D u) (C w)))))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-deq-dd.smt2 b/test/regress/regress0/sets/sets-deq-dd.smt2
new file mode 100644
index 000000000..17ca1fce2
--- /dev/null
+++ b/test/regress/regress0/sets/sets-deq-dd.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun S () (Set (_ BitVec 1)))
+(assert (not (= S (as emptyset (Set (_ BitVec 1))))))
+(check-sat)