diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-09 15:08:11 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-09 15:08:11 -0600 |
commit | 4316ad4be1f9bd9fb0842a84804f2642318cb893 (patch) | |
tree | b90a14f42649c333391a49dcd9ff1ad32e9ed65f /src/theory/quantifiers/dynamic_rewrite.cpp | |
parent | a7f08481352ea1c45091b681e990ccc513ae175f (diff) |
Class to reduce printing of redundant candidate rewrites (#1588)
Diffstat (limited to 'src/theory/quantifiers/dynamic_rewrite.cpp')
-rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.cpp | 140 |
1 files changed, 140 insertions, 0 deletions
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp new file mode 100644 index 000000000..a19695770 --- /dev/null +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -0,0 +1,140 @@ +/********************* */ +/*! \file dynamic_rewriter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Implementation of dynamic_rewriter + **/ + +#include "theory/quantifiers/dynamic_rewrite.h" + +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe) + : d_qe(qe), + d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true) +{ + d_equalityEngine.addFunctionKind(kind::APPLY_UF); +} + +bool DynamicRewriter::addRewrite(Node a, Node b) +{ + Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl; + if (a == b) + { + Trace("dyn-rewrite") << "...fail, equal." << std::endl; + return false; + } + + // add to the equality engine + Node ai = toInternal(a); + Node bi = toInternal(b); + d_equalityEngine.addTerm(ai); + d_equalityEngine.addTerm(bi); + + // may already be equal by congruence + Node air = d_equalityEngine.getRepresentative(ai); + Node bir = d_equalityEngine.getRepresentative(bi); + if (air == bir) + { + Trace("dyn-rewrite") << "...fail, congruent." << std::endl; + return false; + } + + Node eq = ai.eqNode(bi); + d_equalityEngine.assertEquality(eq, true, eq); + return true; +} + +Node DynamicRewriter::toInternal(Node a) +{ + std::map<Node, Node>::iterator it = d_term_to_internal.find(a); + if (it != d_term_to_internal.end()) + { + return it->second; + } + Node ret = a; + + if (!a.isVar()) + { + std::vector<Node> children; + if (a.hasOperator()) + { + Node op = a.getOperator(); + if (a.getKind() != APPLY_UF) + { + op = d_ois_trie[op].getSymbol(a); + } + children.push_back(op); + } + for (const Node& ca : a) + { + Node cai = toInternal(ca); + children.push_back(cai); + } + if (!children.empty()) + { + if (children.size() == 1) + { + ret = children[0]; + } + else + { + ret = NodeManager::currentNM()->mkNode(APPLY_UF, children); + } + } + } + d_term_to_internal[a] = ret; + return ret; +} + +Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n) +{ + std::vector<TypeNode> ctypes; + for (const Node& cn : n) + { + ctypes.push_back(cn.getType()); + } + ctypes.push_back(n.getType()); + + OpInternalSymTrie* curr = this; + for (unsigned i = 0, size = ctypes.size(); i < size; i++) + { + curr = &(curr->d_children[ctypes[i]]); + } + if (!curr->d_sym.isNull()) + { + return curr->d_sym; + } + // make UF operator + TypeNode utype; + if (ctypes.size() == 1) + { + utype = ctypes[0]; + } + else + { + utype = NodeManager::currentNM()->mkFunctionType(ctypes); + } + Node f = NodeManager::currentNM()->mkSkolem( + "ufd", utype, "internal op for dynamic_rewriter"); + curr->d_sym = f; + return f; +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ |