diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-01-12 07:42:37 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-12 09:42:37 -0600 |
| commit | a38a642eab886d298ea3b658c9823544c3a35f27 (patch) | |
| tree | ca0769ce5cad74fbff11e4dea6a5288a0be4ddd0 /test | |
| parent | 8c04f1639607b34b56e3eaa8d3188b27e1454b41 (diff) | |
Foreign theory rewrite option (#5763)
We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.
This PR is the third and final step. It adds the user-facing option that turn this feature on, as well as regression tests.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/seq/len_simplify.smt2 | 5 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index dd6956b09..ea0b3b9e3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -965,6 +965,7 @@ set(regress_0_tests regress0/seq/issue5543-unit-cmv.smt2 regress0/seq/issue5547-seq-len-unit.smt2 regress0/seq/issue5547-small-seq-len-unit.smt2 + regress0/seq/len_simplify.smt2 regress0/seq/seq-2var.smt2 regress0/seq/seq-ex1.smt2 regress0/seq/seq-ex2.smt2 diff --git a/test/regress/regress0/seq/len_simplify.smt2 b/test/regress/regress0/seq/len_simplify.smt2 new file mode 100644 index 000000000..a77ec1ed2 --- /dev/null +++ b/test/regress/regress0/seq/len_simplify.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --foreign-theory-rewrite -q +; EXPECT: sat +(set-logic ALL) +(assert (forall ((x (Seq Int)) ) (>= (seq.len x) 0))) +(check-sat) |