diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/foreign_theory_rewrite.cpp | 105 | ||||
-rw-r--r-- | src/preprocessing/passes/foreign_theory_rewrite.h | 21 |
2 files changed, 122 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; }; |