diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-01 09:44:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-01 14:44:13 +0000 |
| commit | 3bcc47a3c03f7bb1c3d00f0978296232b7e0aaf5 (patch) | |
| tree | f8757035f966a1b0ce72388d1ddb6dff7ee5302d /test | |
| parent | c8887627fab0a7f8395bb6434b624df028b8ef46 (diff) | |
Fix upwards closure for relations (#7515)
This PR fixes an issue where we did compute upwards closure (for join, product, etc.) on equivalence classes whose membership cache had already been initialized (perhaps recursively from the computation of upwards/downwards closures on other terms).
It also generalizes the fix from #7511. Instead of doing explicit splitting, we mark shared terms and let theory combination (when necessary) do splitting. This is required to fix a more general version of the benchmark from the previous PR, where instead now a term c+1 is used in a position that is relevant to a join.
It disables a regression that times out after these fixes, and does further cleanup.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 5 | ||||
| -rw-r--r-- | test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 | 8 | ||||
| -rw-r--r-- | test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 | 11 |
3 files changed, 23 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5d1ff9b49..f64768965 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1037,7 +1037,6 @@ set(regress_0_tests regress0/rels/rel_tc_2_1.cvc.smt2 regress0/rels/rel_tc_3_1.cvc.smt2 regress0/rels/rel_tc_3.cvc.smt2 - regress0/rels/rel_tc_7.cvc.smt2 regress0/rels/rel_tc_8.cvc.smt2 regress0/rels/rel_tp_3_1.cvc.smt2 regress0/rels/rel_tp_join_0.cvc.smt2 @@ -2075,6 +2074,8 @@ set(regress_1_tests regress1/rels/joinImg_2_1.cvc.smt2 regress1/rels/prod-mod-eq.cvc.smt2 regress1/rels/prod-mod-eq2.cvc.smt2 + regress1/rels/qgu-fuzz-relations-2.smt2 + regress1/rels/qgu-fuzz-relations-3-upwards.smt2 regress1/rels/rel_complex_3.cvc.smt2 regress1/rels/rel_complex_4.cvc.smt2 regress1/rels/rel_complex_5.cvc.smt2 @@ -2775,6 +2776,8 @@ set(regression_disabled_tests regress0/auflia/fuzz01.smtv1.smt2 ### regress0/bv/test00.smtv1.smt2 + # timeout after fixing upwards closure for relations + regress0/rels/rel_tc_7.cvc.smt2 # timeout after changes to equality rewriting policy in strings regress0/strings/quad-028-2-2-unsat.smt2 # FIXME #1649 diff --git a/test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 b/test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 new file mode 100644 index 000000000..185c06502 --- /dev/null +++ b/test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun a () (Set (Tuple Int Int))) +(declare-fun b () (Set (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) +(assert (and (= a (singleton (tuple (+ c 1) 1))) (= (tclosure b) (join a a)))) +(check-sat) diff --git a/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 b/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 new file mode 100644 index 000000000..1cb91e94c --- /dev/null +++ b/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun b () (Set (Tuple Int Int))) +(assert +(= (join b (tclosure (join b b))) (as emptyset (Set (Tuple Int Int)))) +) +(assert +(distinct b (as emptyset (Set (Tuple Int Int)))) +) +(assert (= (join b b) (as emptyset (Set (Tuple Int Int))))) +(check-sat) |