From b685ed411b6814f0810ce8f61d07aa49bd75ea3b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 29 Jul 2021 11:11:05 -0500 Subject: 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`. --- test/regress/regress0/aufbv/cee-small-shared-eq.smt2 | 8 ++++++++ test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 | 10 ++++++++++ test/regress/regress0/sets/sets-deq-dd.smt2 | 8 ++++++++ 3 files changed, 26 insertions(+) create mode 100644 test/regress/regress0/aufbv/cee-small-shared-eq.smt2 create mode 100644 test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 create mode 100644 test/regress/regress0/sets/sets-deq-dd.smt2 (limited to 'test/regress/regress0') 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) -- cgit v1.2.3