diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-01 09:26:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-01 09:26:26 -0500 |
commit | c1d9bed7f73db9567f635f59cde134795e65c9ba (patch) | |
tree | cec6839b42cc6c691bbb888bd356f627d973e968 /src/expr | |
parent | 79881c196e29ef341166e7a31c1183e8b537d069 (diff) |
Move some generic utilities out of quantifiers (#3139)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/CMakeLists.txt | 4 | ||||
-rw-r--r-- | src/expr/match_trie.cpp | 199 | ||||
-rw-r--r-- | src/expr/match_trie.h | 82 | ||||
-rw-r--r-- | src/expr/term_canonize.cpp | 210 | ||||
-rw-r--r-- | src/expr/term_canonize.h | 105 |
5 files changed, 600 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 61ab7b3fb..300af8e8c 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -16,6 +16,8 @@ libcvc4_add_sources( expr_stream.h kind_map.h matcher.h + match_trie.cpp + match_trie.h node.cpp node.h node_algorithm.cpp @@ -37,6 +39,8 @@ libcvc4_add_sources( pickler.h symbol_table.cpp symbol_table.h + term_canonize.cpp + term_canonize.h type.cpp type.h type_checker.h diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp new file mode 100644 index 000000000..363c78c9e --- /dev/null +++ b/src/expr/match_trie.cpp @@ -0,0 +1,199 @@ +/********************* */ +/*! \file match_trie.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implements a match trie, also known as a discrimination tree. + **/ + +#include "expr/match_trie.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace expr { + +bool MatchTrie::getMatches(Node n, NotifyMatch* ntm) +{ + std::vector<Node> vars; + std::vector<Node> subs; + std::map<Node, Node> smap; + + std::vector<std::vector<Node> > visit; + std::vector<MatchTrie*> visit_trie; + std::vector<int> visit_var_index; + std::vector<bool> visit_bound_var; + + visit.push_back(std::vector<Node>{n}); + visit_trie.push_back(this); + visit_var_index.push_back(-1); + visit_bound_var.push_back(false); + while (!visit.empty()) + { + std::vector<Node> cvisit = visit.back(); + MatchTrie* curr = visit_trie.back(); + if (cvisit.empty()) + { + Assert(n + == curr->d_data.substitute( + vars.begin(), vars.end(), subs.begin(), subs.end())); + Trace("match-debug") << "notify : " << curr->d_data << std::endl; + if (!ntm->notify(n, curr->d_data, vars, subs)) + { + return false; + } + visit.pop_back(); + visit_trie.pop_back(); + visit_var_index.pop_back(); + visit_bound_var.pop_back(); + } + else + { + Node cn = cvisit.back(); + Trace("match-debug") << "traverse : " << cn << " at depth " + << visit.size() << std::endl; + unsigned index = visit.size() - 1; + int vindex = visit_var_index[index]; + if (vindex == -1) + { + if (!cn.isVar()) + { + Node op = cn.hasOperator() ? cn.getOperator() : cn; + unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0; + std::map<unsigned, MatchTrie>::iterator itu = + curr->d_children[op].find(nchild); + if (itu != curr->d_children[op].end()) + { + // recurse on the operator or self + cvisit.pop_back(); + if (cn.hasOperator()) + { + for (const Node& cnc : cn) + { + cvisit.push_back(cnc); + } + } + Trace("match-debug") << "recurse op : " << op << std::endl; + visit.push_back(cvisit); + visit_trie.push_back(&itu->second); + visit_var_index.push_back(-1); + visit_bound_var.push_back(false); + } + } + visit_var_index[index]++; + } + else + { + // clean up if we previously bound a variable + if (visit_bound_var[index]) + { + Assert(!vars.empty()); + smap.erase(vars.back()); + vars.pop_back(); + subs.pop_back(); + visit_bound_var[index] = false; + } + + if (vindex == static_cast<int>(curr->d_vars.size())) + { + Trace("match-debug") + << "finished checking " << curr->d_vars.size() + << " variables at depth " << visit.size() << std::endl; + // finished + visit.pop_back(); + visit_trie.pop_back(); + visit_var_index.pop_back(); + visit_bound_var.pop_back(); + } + else + { + Trace("match-debug") << "check variable #" << vindex << " at depth " + << visit.size() << std::endl; + Assert(vindex < static_cast<int>(curr->d_vars.size())); + // recurse on variable? + Node var = curr->d_vars[vindex]; + bool recurse = true; + // check if it is already bound + std::map<Node, Node>::iterator its = smap.find(var); + if (its != smap.end()) + { + if (its->second != cn) + { + recurse = false; + } + } + else if (!var.getType().isSubtypeOf(cn.getType())) + { + recurse = false; + } + else + { + vars.push_back(var); + subs.push_back(cn); + smap[var] = cn; + visit_bound_var[index] = true; + } + if (recurse) + { + Trace("match-debug") << "recurse var : " << var << std::endl; + cvisit.pop_back(); + visit.push_back(cvisit); + visit_trie.push_back(&curr->d_children[var][0]); + visit_var_index.push_back(-1); + visit_bound_var.push_back(false); + } + visit_var_index[index]++; + } + } + } + } + return true; +} + +void MatchTrie::addTerm(Node n) +{ + Assert(!n.isNull()); + std::vector<Node> visit; + visit.push_back(n); + MatchTrie* curr = this; + while (!visit.empty()) + { + Node cn = visit.back(); + visit.pop_back(); + if (cn.hasOperator()) + { + curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]); + for (const Node& cnc : cn) + { + visit.push_back(cnc); + } + } + else + { + if (cn.isVar() + && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn) + == curr->d_vars.end()) + { + curr->d_vars.push_back(cn); + } + curr = &(curr->d_children[cn][0]); + } + } + curr->d_data = n; +} + +void MatchTrie::clear() +{ + d_children.clear(); + d_vars.clear(); + d_data = Node::null(); +} + +} // namespace expr +} // namespace CVC4 diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h new file mode 100644 index 000000000..ea8be44d9 --- /dev/null +++ b/src/expr/match_trie.h @@ -0,0 +1,82 @@ +/********************* */ +/*! \file match_trie.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implements a match trie, also known as a discrimination tree. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__MATCH_TRIE_H +#define CVC4__EXPR__MATCH_TRIE_H + +#include <map> +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +/** A virtual class for notifications regarding matches. */ +class NotifyMatch +{ + public: + virtual ~NotifyMatch() {} + /** + * A notification that s is equal to n * { vars -> subs }. This function + * should return false if we do not wish to be notified of further matches. + */ + virtual bool notify(Node s, + Node n, + std::vector<Node>& vars, + std::vector<Node>& subs) = 0; +}; + +/** + * A trie (discrimination tree) storing a set of terms S, that can be used to + * query, for a given term t, all terms s from S that are matchable with t, + * that is s*sigma = t for some substitution sigma. + */ +class MatchTrie +{ + public: + /** Get matches + * + * This calls ntm->notify( n, s, vars, subs ) for each term s stored in this + * trie that is matchable with n where s = n * { vars -> subs } for some + * vars, subs. This function returns false if one of these calls to notify + * returns false. + */ + bool getMatches(Node n, NotifyMatch* ntm); + /** Adds node n to this trie */ + void addTerm(Node n); + /** Clear this trie */ + void clear(); + + private: + /** + * The children of this node in the trie. Terms t are indexed by a + * depth-first (right to left) traversal on its subterms, where the + * top-symbol of t is indexed by: + * - (operator, #children) if t has an operator, or + * - (t, 0) if t does not have an operator. + */ + std::map<Node, std::map<unsigned, MatchTrie> > d_children; + /** The set of variables in the domain of d_children */ + std::vector<Node> d_vars; + /** The data of this node in the trie */ + Node d_data; +}; + +} // namespace expr +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp new file mode 100644 index 000000000..d9a5f6e1a --- /dev/null +++ b/src/expr/term_canonize.cpp @@ -0,0 +1,210 @@ +/********************* */ +/*! \file term_canonize.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 term canonize. + **/ + +#include "expr/term_canonize.h" + +// TODO #1216: move the code in this include +#include "theory/quantifiers/term_util.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace expr { + +TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {} + +int TermCanonize::getIdForOperator(Node op) +{ + std::map<Node, int>::iterator it = d_op_id.find(op); + if (it == d_op_id.end()) + { + d_op_id[op] = d_op_id_count; + d_op_id_count++; + return d_op_id[op]; + } + return it->second; +} + +int TermCanonize::getIdForType(TypeNode t) +{ + std::map<TypeNode, int>::iterator it = d_typ_id.find(t); + if (it == d_typ_id.end()) + { + d_typ_id[t] = d_typ_id_count; + d_typ_id_count++; + return d_typ_id[t]; + } + return it->second; +} + +bool TermCanonize::getTermOrder(Node a, Node b) +{ + if (a.getKind() == BOUND_VARIABLE) + { + if (b.getKind() == BOUND_VARIABLE) + { + return getIndexForFreeVariable(a) < getIndexForFreeVariable(b); + } + return true; + } + if (b.getKind() != BOUND_VARIABLE) + { + Node aop = a.hasOperator() ? a.getOperator() : a; + Node bop = b.hasOperator() ? b.getOperator() : b; + Trace("aeq-debug2") << a << "...op..." << aop << std::endl; + Trace("aeq-debug2") << b << "...op..." << bop << std::endl; + if (aop == bop) + { + if (a.getNumChildren() == b.getNumChildren()) + { + for (unsigned i = 0, size = a.getNumChildren(); i < size; i++) + { + if (a[i] != b[i]) + { + // first distinct child determines the ordering + return getTermOrder(a[i], b[i]); + } + } + } + else + { + return aop.getNumChildren() < bop.getNumChildren(); + } + } + else + { + return getIdForOperator(aop) < getIdForOperator(bop); + } + } + return false; +} + +Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i) +{ + Assert(!tn.isNull()); + NodeManager* nm = NodeManager::currentNM(); + while (d_cn_free_var[tn].size() <= i) + { + std::stringstream oss; + oss << tn; + std::string typ_name = oss.str(); + while (typ_name[0] == '(') + { + typ_name.erase(typ_name.begin()); + } + std::stringstream os; + os << typ_name[0] << i; + Node x = nm->mkBoundVar(os.str().c_str(), tn); + d_fvIndex[x] = d_cn_free_var[tn].size(); + d_cn_free_var[tn].push_back(x); + } + return d_cn_free_var[tn][i]; +} + +size_t TermCanonize::getIndexForFreeVariable(Node v) const +{ + std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v); + if (it == d_fvIndex.end()) + { + return 0; + } + return it->second; +} + +struct sortTermOrder +{ + TermCanonize* d_tu; + bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); } +}; + +Node TermCanonize::getCanonicalTerm(TNode n, + bool apply_torder, + bool doHoVar, + std::map<TypeNode, unsigned>& var_count, + std::map<TNode, Node>& visited) +{ + std::map<TNode, Node>::iterator it = visited.find(n); + if (it != visited.end()) + { + return it->second; + } + + Trace("canon-term-debug") << "Get canonical term for " << n << std::endl; + if (n.getKind() == BOUND_VARIABLE) + { + TypeNode tn = n.getType(); + // allocate variable + unsigned vn = var_count[tn]; + var_count[tn]++; + Node fv = getCanonicalFreeVar(tn, vn); + visited[n] = fv; + Trace("canon-term-debug") << "...allocate variable." << std::endl; + return fv; + } + else if (n.getNumChildren() > 0) + { + // collect children + Trace("canon-term-debug") << "Collect children" << std::endl; + std::vector<Node> cchildren; + for (const Node& cn : n) + { + cchildren.push_back(cn); + } + // if applicable, first sort by term order + if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind())) + { + Trace("canon-term-debug") + << "Sort based on commutative operator " << n.getKind() << std::endl; + sortTermOrder sto; + sto.d_tu = this; + std::sort(cchildren.begin(), cchildren.end(), sto); + } + // now make canonical + Trace("canon-term-debug") << "Make canonical children" << std::endl; + for (unsigned i = 0, size = cchildren.size(); i < size; i++) + { + cchildren[i] = getCanonicalTerm( + cchildren[i], apply_torder, doHoVar, var_count, visited); + } + if (n.getMetaKind() == metakind::PARAMETERIZED) + { + Node op = n.getOperator(); + if (doHoVar) + { + op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited); + } + Trace("canon-term-debug") << "Insert operator " << op << std::endl; + cchildren.insert(cchildren.begin(), op); + } + Trace("canon-term-debug") + << "...constructing for " << n << "." << std::endl; + Node ret = NodeManager::currentNM()->mkNode(n.getKind(), cchildren); + Trace("canon-term-debug") + << "...constructed " << ret << " for " << n << "." << std::endl; + visited[n] = ret; + return ret; + } + Trace("canon-term-debug") << "...return 0-child term." << std::endl; + return n; +} + +Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar) +{ + std::map<TypeNode, unsigned> var_count; + std::map<TNode, Node> visited; + return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited); +} + +} // namespace expr +} // namespace CVC4 diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h new file mode 100644 index 000000000..6049cd804 --- /dev/null +++ b/src/expr/term_canonize.h @@ -0,0 +1,105 @@ +/********************* */ +/*! \file term_canonize.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Utilities for constructing canonical terms. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__TERM_CANONIZE_H +#define CVC4__EXPR__TERM_CANONIZE_H + +#include <map> +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +/** TermCanonize + * + * This class contains utilities for canonizing terms with respect to + * free variables (which are of kind BOUND_VARIABLE). For example, this + * class infers that terms like f(BOUND_VARIABLE_1) and f(BOUND_VARIABLE_2) + * are effectively the same term. + */ +class TermCanonize +{ + public: + TermCanonize(); + ~TermCanonize() {} + + /** Maps operators to an identifier, useful for ordering. */ + int getIdForOperator(Node op); + /** Maps types to an identifier, useful for ordering. */ + int getIdForType(TypeNode t); + /** get term order + * + * Returns true if a <= b in the term ordering used by this class. The + * term order is determined by the leftmost position in a and b whose + * operators o_a and o_b are distinct at that position. Then a <= b iff + * getIdForOperator( o_a ) <= getIdForOperator( o_b ). + */ + bool getTermOrder(Node a, Node b); + /** get canonical free variable #i of type tn */ + Node getCanonicalFreeVar(TypeNode tn, unsigned i); + /** get canonical term + * + * This returns a canonical (alpha-equivalent) version of n, where + * bound variables in n may be replaced by other ones, and arguments of + * commutative operators of n may be sorted (if apply_torder is true). If + * doHoVar is true, we also canonicalize bound variables that occur in + * operators. + * + * In detail, we replace bound variables in n so the the leftmost occurrence + * of a bound variable for type T is the first canonical free variable for T, + * the second leftmost is the second, and so on, for each type T. + */ + Node getCanonicalTerm(TNode n, + bool apply_torder = false, + bool doHoVar = true); + + private: + /** the number of ids we have allocated for operators */ + int d_op_id_count; + /** map from operators to id */ + std::map<Node, int> d_op_id; + /** the number of ids we have allocated for types */ + int d_typ_id_count; + /** map from type to id */ + std::map<TypeNode, int> d_typ_id; + /** free variables for each type */ + std::map<TypeNode, std::vector<Node> > d_cn_free_var; + /** + * Map from each free variable above to their index in their respective vector + */ + std::map<Node, size_t> d_fvIndex; + /** + * Return the range of the free variable in the above map, or 0 if it does not + * exist. + */ + size_t getIndexForFreeVariable(Node v) const; + /** get canonical term + * + * This is a helper function for getCanonicalTerm above. We maintain a + * counter of how many variables we have allocated for each type (var_count), + * and a cache of visited nodes (visited). + */ + Node getCanonicalTerm(TNode n, + bool apply_torder, + bool doHoVar, + std::map<TypeNode, unsigned>& var_count, + std::map<TNode, Node>& visited); +}; + +} // namespace expr +} // namespace CVC4 + +#endif /* CVC4__EXPR__TERM_CANONIZE_H */ |