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.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 247559c9199233fd1d01ceac3d2ca16f54fe2cd1..33d21612b683064702b879e35807feb9843523a2 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -680,6 +680,16 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "Force no CPU limit when dumping models and proofs"
 
+[[option]]
+  name       = "foreignTheoryRewrite"
+  category   = "regular"
+  long       = "foreign-theory-rewrite"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "Cross-theory rewrites"
+
+
 [[option]]
   name       = "solveBVAsInt"
   category   = "undocumented"

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 5faa2a66c51182e63f29b8dd2137fbb8da738177..0bbc2eeae868e257c220f436163f74b1655c9bba 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -204,6 +204,10 @@ bool ProcessAssertions::apply(Assertions& as)
   {
     d_passes["bv-to-int"]->apply(&assertions);
   }
+  if (options::foreignTheoryRewrite())
+  {
+    d_passes["foreign-theory-rewrite"]->apply(&assertions);
+  }
 
   // Since this pass is not robust for the information tracking necessary for
   // unsat cores, it's only applied if we are not doing unsat core computation

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index dd6956b0900665afe62d0da3494215c7acbbbdfd..ea0b3b9e34d72eeb307047c2c2a9b89b87684a7f 100644 (file)
--- 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 (file)
index 0000000..a77ec1e
--- /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)