Strings arith checks preprocessing pass: step 2 (#5750)

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 second step. It includes the implementation of the main function, as well as unit tests for it.

A subsequent PR will add a user-level option that will turn on this preprocessing pass, as well as regression tests.

4 files changed, 190 insertions, 4 deletions

diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
index 74183d518..c7bed4d31 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.cpp
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -24,12 +24,113 @@ 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); }
+Node ForeignTheoryRewrite::simplify(Node n)
+{
+  std::vector<Node> toVisit;
+  n = Rewriter::rewrite(n);
+  toVisit.push_back(n);
+  // traverse n and rewrite until fixpoint
+  while (!toVisit.empty())
+  {
+    Node current = toVisit.back();
+    // split according to three cases:
+    // 1. We have not visited this node
+    // 2. We visited it but did not process it
+    // 3. We already processed and cached the node
+    if (d_cache.find(current) == d_cache.end())
+    {
+      // current is seen for the first time.
+      // mark it by assigning a null node
+      // and add its children to toVisit
+      d_cache[current] = Node();
+      toVisit.insert(toVisit.end(), current.begin(), current.end());
+    }
+    else if (d_cache[current].get().isNull())
+    {
+      // current was seen but was not processed.
+      // (a) remove from toVisit
+      toVisit.pop_back();
+      // (b) Reconstruct it with processed children
+      std::vector<Node> processedChildren;
+      for (Node child : current)
+      {
+        Assert(d_cache.find(child) != d_cache.end());
+        Assert(!d_cache[child].get().isNull());
+        processedChildren.push_back(d_cache[child]);
+      }
+      Node reconstruction = reconstructNode(current, processedChildren);
+      // (c) process the node and store the result in the cache
+      Node result = foreignRewrite(reconstruction);
+      d_cache[current] = result;
+      // (d) add the result to toVisit, unless it is the same as current
+      if (current != result)
+      {
+        toVisit.push_back(result);
+      }
+    }
+    else
+    {
+      // current was already processed
+      // remove from toVisit and skip
+      toVisit.pop_back();
+    }
+  }
+  return d_cache[n];
+}
+
+Node ForeignTheoryRewrite::foreignRewrite(Node n)
+{
+  // n is a rewritten node, and so GT, LT, LEQ
+  // should have been eliminated
+  Assert(n.getKind() != kind::GT);
+  Assert(n.getKind() != kind::LT);
+  Assert(n.getKind() != kind::LEQ);
+  // apply rewrites according to the structure of n
+  if (n.getKind() == kind::GEQ)
+  {
+    return rewriteStringsGeq(n);
+  }
+  return n;
+}
+
+Node ForeignTheoryRewrite::rewriteStringsGeq(Node n)
+{
+  // check if the node can be simplified to true
+  if (theory::strings::ArithEntail::check(n[0], n[1], false))
+  {
+    return NodeManager::currentNM()->mkConst(true);
+  }
+  return n;
+}
+
+Node ForeignTheoryRewrite::reconstructNode(Node originalNode,
+                                           std::vector<Node> newChildren)
+{
+  // Nodes with no children are reconstructed to themselves
+  if (originalNode.getNumChildren() == 0)
+  {
+    Assert(newChildren.empty());
+    return originalNode;
+  }
+  // re-build the node with the same kind and new children
+  kind::Kind_t k = originalNode.getKind();
+  NodeBuilder<> builder(k);
+  // special case for parameterized nodes
+  if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
+    builder << originalNode.getOperator();
+  }
+  // reconstruction
+  for (Node child : newChildren)
+  {
+    builder << child;
+  }
+  return builder.constructNode();
+}
 
 PreprocessingPassResult ForeignTheoryRewrite::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h
index 9b7f71b50..2a882641e 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.h
+++ b/src/preprocessing/passes/foreign_theory_rewrite.h
@@ -39,9 +39,26 @@ class ForeignTheoryRewrite : public PreprocessingPass
  protected:
   PreprocessingPassResult applyInternal(
       AssertionPipeline* assertionsToPreprocess) override;
-  // the main function that simplifies n
+  /** the main function that simplifies n.
+   * does a traversal on n and call rewriting fucntions.
+   */
   Node simplify(Node n);
-  // A cache to store the simplified nodes
+  /** A specific simplification function specific for GEQ
+   * constraints in strings.
+   */
+  static Node rewriteStringsGeq(Node n);
+  /** invoke rewrite functions for n.
+   * based on the structure of n (typically its kind)
+   * we invoke rewrites from other theories.
+   * For example: when encountering a `>=` node,
+   * we invoke rewrites from the theory of strings.
+   */
+  static Node foreignRewrite(Node n);
+  /** construct a node with the same operator as originalNode whose children are
+   * processedChildren
+   */
+  static Node reconstructNode(Node originalNode, vector<Node> newChildren);
+  /** A cache to store the simplified nodes */
   CDNodeMap d_cache;
 };
 
diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt
index f2dc0ce79..f9518bd2e 100644
--- a/test/unit/preprocessing/CMakeLists.txt
+++ b/test/unit/preprocessing/CMakeLists.txt
@@ -12,3 +12,4 @@
 # Add unit tests
 
 cvc4_add_cxx_unit_test_white(pass_bv_gauss_white preprocessing)
+cvc4_add_cxx_unit_test_white(pass_foreign_theory_rewrite_white preprocessing)
diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.h b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.h
new file mode 100644
index 000000000..5416cf304
--- /dev/null
+++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.h
@@ -0,0 +1,67 @@
+/*********************                                                        */
+/*! \file pass_foreign_theory_rewrite.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Mathias Preiner, Andres Noetzli
+ ** 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 Unit tests for Foreign Theory Rerwrite prepricessing pass
+ ** Unit tests for Foreign Theory Rerwrite prepricessing pass
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "expr/node_manager.h"
+#include "preprocessing/passes/foreign_theory_rewrite.h"
+#include "smt/smt_engine.h"
+#include "test_utils.h"
+
+using namespace CVC4;
+using namespace CVC4::preprocessing::passes;
+
+class ForeignTheoryRewriteWhite : public CxxTest::TestSuite
+{
+ public:
+  ForeignTheoryRewriteWhite() {}
+
+  void setUp() override
+  {
+    d_em = new ExprManager();
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm);
+    d_smt->finishInit();
+  }
+
+  void tearDown() override
+  {
+    delete d_smt;
+    delete d_em;
+  }
+
+  void testSimplify()
+  {
+    std::cout << "len(x) >= 0 is simplified to true" << std::endl;
+    Node x = d_nm->mkVar("x", d_nm->stringType());
+    Node len_x = d_nm->mkNode(kind::STRING_LENGTH, x);
+    Node zero = d_nm->mkConst<Rational>(0);
+    Node geq1 = d_nm->mkNode(kind::GEQ, len_x, zero);
+    Node tt = d_nm->mkConst<bool>(true);
+    Node simplified1 = ForeignTheoryRewrite::foreignRewrite(geq1);
+    TS_ASSERT_EQUALS(simplified1, tt);
+
+    std::cout << "len(x) >= n is not simplified to true" << std::endl;
+    Node n = d_nm->mkVar("n", d_nm->integerType());
+    Node geq2 = d_nm->mkNode(kind::GEQ, len_x, n);
+    Node simplified2 = ForeignTheoryRewrite::foreignRewrite(geq2);
+    TS_ASSERT(simplified2 != tt);
+  }
+
+ private:
+  ExprManager* d_em;
+  NodeManager* d_nm;
+  SmtEngine* d_smt;
+};