diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-14 12:49:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-14 12:49:58 -0500 |
| commit | 92a007b4a35a925c92eafc29df5bacacac75f6f9 (patch) | |
| tree | af69c6aa8cf3ff5470c25aca27d8d340d9d0b141 /test/regress | |
| parent | c82d061abb0c011da2700051b7a0548f5d59904b (diff) | |
Refactoring the rewriter of sets (#4856)
Changes it so that we don't flatten unions if at least one child is non-constant, since this may lead to children that are non-constant by mixing constant/non-constant elements and is generally expensive for large unions of singleton elements.
The previous rewriting policy was causing an incorrect model in a separation logic benchmark reported by Andrew Jones, due to unions of constant elements that were unsorted (and hence not considered constants). We now have the invariant that all subterms that are unions of constant elements are set constants.
Note this PR changes the normal form of set constants to be (union (singleton c1) ... (union (singleton cn-1) (singleton cn) ... ) not (union ... (union (singleton c1) (singleton c2)) ... (singleton cn)).
It changes a unit test which was impacted by this change which was failing due to hardcoding the enumeration order in the unit test. The test is now agnostic to the order of elements.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sep/simple-080420-const-sets.smt2 | 14 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ed07c7474..d784a1ced 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -858,6 +858,7 @@ set(regress_0_tests regress0/sep/sep-01.smt2 regress0/sep/sep-plus1.smt2 regress0/sep/sep-simp-unsat-emp.smt2 + regress0/sep/simple-080420-const-sets.smt2 regress0/sep/skolem_emp.smt2 regress0/sep/trees-1.smt2 regress0/sep/wand-crash.smt2 diff --git a/test/regress/regress0/sep/simple-080420-const-sets.smt2 b/test/regress/regress0/sep/simple-080420-const-sets.smt2 new file mode 100644 index 000000000..1d85fb133 --- /dev/null +++ b/test/regress/regress0/sep/simple-080420-const-sets.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic QF_ALL_SUPPORTED) +(set-option :produce-models true) +(set-info :status sat) +(declare-fun x () Int) + +; works +;(assert (sep (pto 1 2) (pto 5 6) (pto x 8))) + +; didn't work due to sets rewriter +(assert (sep (pto 1 2) (pto 5 6) (pto 7 8))) + +(check-sat) |