From: yoni206 Date: Sat, 9 Jan 2021 14:35:18 +0000 (-0800) Subject: Strings arith checks preprocessing pass: step 2 (#5750) X-Git-Tag: cvc5-1.0.0~2388 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fcac065b47ea73aecb90f019c07dc6fa09cd914f;p=cvc5.git 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. --- 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 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 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 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 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 + +#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(0); + Node geq1 = d_nm->mkNode(kind::GEQ, len_x, zero); + Node tt = d_nm->mkConst(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; +};