strings arith checks preprocessing pass: step 1 (#5747)

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 first step. It only includes the preprocessing pass infrastructure, with an empty implementation of the main function StrLenSimplify::simplify. It also adds the pass to the registry.
The implementation of this function is not complicated, but is left for a future PR in order to keep the PR short.

Future PRs will include an implementation of the main function, tests, and a command line option to turn on the pass.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 08404ce7367e5fcfaddda6e3d75dbbd4a933c6b0..f01c948db40ab035c1dc25b0fc5e5d04449ee1af 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -102,6 +102,8 @@ libcvc4_add_sources(
   preprocessing/passes/sort_infer.h
   preprocessing/passes/static_learning.cpp
   preprocessing/passes/static_learning.h
+  preprocessing/passes/foreign_theory_rewrite.cpp
+  preprocessing/passes/foreign_theory_rewrite.h
   preprocessing/passes/sygus_inference.cpp
   preprocessing/passes/sygus_inference.h
   preprocessing/passes/synth_rew_rules.cpp

diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
new file mode 100644 (file)
index 0000000..74183d5
--- /dev/null
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -0,0 +1,48 @@
+/*********************                                                        */
+/*! \file foreign_theory_rewrite.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The foreign_theory_rewrite preprocessing pass
+ **
+ ** Simplifies nodes of one theory using rewrites from another.
+ **/
+
+#include "preprocessing/passes/foreign_theory_rewrite.h"
+
+#include "expr/node_traversal.h"
+#include "theory/strings/arith_entail.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+ForeignTheoryRewrite::ForeignTheoryRewrite(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "foreign-theory-rewrite"),
+      d_cache(preprocContext->getUserContext()){};
+
+Node ForeignTheoryRewrite::simplify(Node n) { assert(false); }
+
+PreprocessingPassResult ForeignTheoryRewrite::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+  {
+    assertionsToPreprocess->replace(
+        i, Rewriter::rewrite(simplify((*assertionsToPreprocess)[i])));
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4

diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h
new file mode 100644 (file)
index 0000000..9b7f71b
--- /dev/null
+++ b/src/preprocessing/passes/foreign_theory_rewrite.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file foreign_theory_rewrite.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The foreign_theory_rewrite preprocessing pass
+ ** 
+ ** Simplifies nodes of one theory using rewrites from another.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
+#define CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
+
+#include "context/cdhashmap.h"
+#include "context/cdo.h"
+#include "context/context.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+
+class ForeignTheoryRewrite : public PreprocessingPass
+{
+ public:
+  ForeignTheoryRewrite(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+  // the main function that simplifies n
+  Node simplify(Node n);
+  // A cache to store the simplified nodes
+  CDNodeMap d_cache;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */

diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index b21d4e30c9065a76448c7fa3a52f9a41e10aeddd..da09f63633f73112c53557977ca38921a0a99b16 100644 (file)
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -50,6 +50,7 @@
 #include "preprocessing/passes/sep_skolem_emp.h"
 #include "preprocessing/passes/sort_infer.h"
 #include "preprocessing/passes/static_learning.h"
+#include "preprocessing/passes/foreign_theory_rewrite.h"
 #include "preprocessing/passes/sygus_inference.h"
 #include "preprocessing/passes/synth_rew_rules.h"
 #include "preprocessing/passes/theory_preprocess.h"
@@ -124,6 +125,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("global-negate", callCtor<GlobalNegate>);
   registerPassInfo("int-to-bv", callCtor<IntToBV>);
   registerPassInfo("bv-to-int", callCtor<BVToInt>);
+  registerPassInfo("foreign-theory-rewrite", callCtor<ForeignTheoryRewrite>);
   registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);
   registerPassInfo("real-to-int", callCtor<RealToInt>);
   registerPassInfo("sygus-infer", callCtor<SygusInference>);