From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 12 Jan 2021 15:42:37 +0000 (-0800)
Subject: Foreign theory rewrite option (#5763)
X-Git-Tag: cvc5-1.0.0~2384
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a38a642eab886d298ea3b658c9823544c3a35f27;p=cvc5.git

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 247559c91..33d21612b 100644
--- 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 5faa2a66c..0bbc2eeae 100644
--- 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 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)