From c1d9bed7f73db9567f635f59cde134795e65c9ba Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Aug 2019 09:26:26 -0500 Subject: [PATCH] Move some generic utilities out of quantifiers (#3139) --- src/CMakeLists.txt | 2 - src/expr/CMakeLists.txt | 4 + src/expr/match_trie.cpp | 199 ++++++++++++++++++ src/expr/match_trie.h | 82 ++++++++ .../quantifiers => expr}/term_canonize.cpp | 27 ++- .../quantifiers => expr}/term_canonize.h | 21 +- src/preprocessing/passes/symmetry_detect.h | 4 +- src/preprocessing/passes/synth_rew_rules.cpp | 4 +- src/theory/quantifiers/alpha_equivalence.cpp | 3 +- src/theory/quantifiers/alpha_equivalence.h | 6 +- src/theory/quantifiers/anti_skolem.cpp | 4 +- .../quantifiers/candidate_rewrite_filter.cpp | 176 ---------------- .../quantifiers/candidate_rewrite_filter.h | 56 +---- .../quantifiers/conjecture_generator.cpp | 2 +- src/theory/quantifiers_engine.cpp | 6 +- src/theory/quantifiers_engine.h | 9 +- 16 files changed, 340 insertions(+), 265 deletions(-) create mode 100644 src/expr/match_trie.cpp create mode 100644 src/expr/match_trie.h rename src/{theory/quantifiers => expr}/term_canonize.cpp (91%) rename src/{theory/quantifiers => expr}/term_canonize.h (88%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 028a5ab21..68c22daef 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -591,8 +591,6 @@ libcvc4_add_sources( theory/quantifiers/sygus/term_database_sygus.h theory/quantifiers/sygus_sampler.cpp theory/quantifiers/sygus_sampler.h - theory/quantifiers/term_canonize.cpp - theory/quantifiers/term_canonize.h theory/quantifiers/term_database.cpp theory/quantifiers/term_database.h theory/quantifiers/term_enumeration.cpp 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 vars; + std::vector subs; + std::map smap; + + std::vector > visit; + std::vector visit_trie; + std::vector visit_var_index; + std::vector visit_bound_var; + + visit.push_back(std::vector{n}); + visit_trie.push_back(this); + visit_var_index.push_back(-1); + visit_bound_var.push_back(false); + while (!visit.empty()) + { + std::vector 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::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(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(curr->d_vars.size())); + // recurse on variable? + Node var = curr->d_vars[vindex]; + bool recurse = true; + // check if it is already bound + std::map::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 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 +#include + +#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& vars, + std::vector& 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 > d_children; + /** The set of variables in the domain of d_children */ + std::vector 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/theory/quantifiers/term_canonize.cpp b/src/expr/term_canonize.cpp similarity index 91% rename from src/theory/quantifiers/term_canonize.cpp rename to src/expr/term_canonize.cpp index 2e9c1d286..d9a5f6e1a 100644 --- a/src/theory/quantifiers/term_canonize.cpp +++ b/src/expr/term_canonize.cpp @@ -12,15 +12,15 @@ ** \brief Implementation of term canonize. **/ -#include "theory/quantifiers/term_canonize.h" +#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 theory { -namespace quantifiers { +namespace expr { TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {} @@ -54,8 +54,7 @@ bool TermCanonize::getTermOrder(Node a, Node b) { if (b.getKind() == BOUND_VARIABLE) { - return a.getAttribute(InstVarNumAttribute()) - < b.getAttribute(InstVarNumAttribute()); + return getIndexForFreeVariable(a) < getIndexForFreeVariable(b); } return true; } @@ -107,13 +106,22 @@ Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i) std::stringstream os; os << typ_name[0] << i; Node x = nm->mkBoundVar(os.str().c_str(), tn); - InstVarNumAttribute ivna; - x.setAttribute(ivna, d_cn_free_var[tn].size()); + 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::const_iterator it = d_fvIndex.find(v); + if (it == d_fvIndex.end()) + { + return 0; + } + return it->second; +} + struct sortTermOrder { TermCanonize* d_tu; @@ -154,7 +162,7 @@ Node TermCanonize::getCanonicalTerm(TNode n, cchildren.push_back(cn); } // if applicable, first sort by term order - if (apply_torder && TermUtil::isComm(n.getKind())) + if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind())) { Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl; @@ -198,6 +206,5 @@ Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar) return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited); } -} // namespace quantifiers -} // namespace theory +} // namespace expr } // namespace CVC4 diff --git a/src/theory/quantifiers/term_canonize.h b/src/expr/term_canonize.h similarity index 88% rename from src/theory/quantifiers/term_canonize.h rename to src/expr/term_canonize.h index 207e6150c..6049cd804 100644 --- a/src/theory/quantifiers/term_canonize.h +++ b/src/expr/term_canonize.h @@ -14,15 +14,14 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H -#define CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H +#ifndef CVC4__EXPR__TERM_CANONIZE_H +#define CVC4__EXPR__TERM_CANONIZE_H #include #include "expr/node.h" namespace CVC4 { -namespace theory { -namespace quantifiers { +namespace expr { /** TermCanonize * @@ -78,6 +77,15 @@ class TermCanonize std::map d_typ_id; /** free variables for each type */ std::map > d_cn_free_var; + /** + * Map from each free variable above to their index in their respective vector + */ + std::map 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 @@ -91,8 +99,7 @@ class TermCanonize std::map& visited); }; -} // namespace quantifiers -} // namespace theory +} // namespace expr } // namespace CVC4 -#endif /* CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */ +#endif /* CVC4__EXPR__TERM_CANONIZE_H */ diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h index 07a545723..deb1accd7 100644 --- a/src/preprocessing/passes/symmetry_detect.h +++ b/src/preprocessing/passes/symmetry_detect.h @@ -21,7 +21,7 @@ #include #include #include "expr/node.h" -#include "theory/quantifiers/term_canonize.h" +#include "expr/term_canonize.h" namespace CVC4 { namespace preprocessing { @@ -242,7 +242,7 @@ class SymmetryDetect Node d_falseNode; /** term canonizer (for quantified formulas) */ - theory::quantifiers::TermCanonize d_tcanon; + expr::TermCanonize d_tcanon; /** Cache for partitions */ std::map d_term_partition; diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 3eb27c2f7..6d6e8fb27 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -15,6 +15,7 @@ #include "preprocessing/passes/synth_rew_rules.h" +#include "expr/term_canonize.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -22,7 +23,6 @@ #include "theory/quantifiers/candidate_rewrite_database.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" -#include "theory/quantifiers/term_canonize.h" #include "theory/quantifiers/term_util.h" using namespace std; @@ -218,7 +218,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( std::vector cterms; // canonical terms for each type std::map > t_cterms; - theory::quantifiers::TermCanonize tcanon; + expr::TermCanonize tcanon; for (unsigned i = 0, nterms = terms.size(); i < nterms; i++) { Node n = terms[i]; diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index bb0cdde83..f7d433078 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -14,7 +14,6 @@ **/ #include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers/term_canonize.h" using namespace CVC4; using namespace std; @@ -23,7 +22,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; struct sortTypeOrder { - TermCanonize* d_tu; + expr::TermCanonize* d_tu; bool operator() (TypeNode i, TypeNode j) { return d_tu->getIdForType( i )getIdForType( j ); } diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index b5d68f233..5ef778b8d 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -20,6 +20,8 @@ #include "theory/quantifiers_engine.h" +#include "expr/term_canonize.h" + namespace CVC4 { namespace theory { namespace quantifiers { @@ -78,7 +80,7 @@ public: class AlphaEquivalenceDb { public: - AlphaEquivalenceDb(TermCanonize* tc) : d_tc(tc) {} + AlphaEquivalenceDb(expr::TermCanonize* tc) : d_tc(tc) {} /** adds quantified formula q to this database * * This function returns a quantified formula q' that is alpha-equivalent to @@ -91,7 +93,7 @@ class AlphaEquivalenceDb /** a trie per # of variables per type */ AlphaEquivalenceTypeNode d_ae_typ_trie; /** pointer to the term canonize utility */ - TermCanonize* d_tc; + expr::TermCanonize* d_tc; }; /** diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index 5d1967bb4..d972f2a1c 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -15,9 +15,9 @@ #include "theory/quantifiers/anti_skolem.h" +#include "expr/term_canonize.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_canonize.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -29,7 +29,7 @@ namespace theory { namespace quantifiers { struct sortTypeOrder { - TermCanonize* d_tu; + expr::TermCanonize* d_tu; bool operator() (TypeNode i, TypeNode j) { return d_tu->getIdForType( i )getIdForType( j ); } diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index c07cae51d..8db0501f5 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -26,182 +26,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -bool MatchTrie::getMatches(Node n, NotifyMatch* ntm) -{ - std::vector vars; - std::vector subs; - std::map smap; - - std::vector > visit; - std::vector visit_trie; - std::vector visit_var_index; - std::vector visit_bound_var; - - visit.push_back(std::vector{n}); - visit_trie.push_back(this); - visit_var_index.push_back(-1); - visit_bound_var.push_back(false); - while (!visit.empty()) - { - std::vector 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("crf-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("crf-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::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("crf-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(curr->d_vars.size())) - { - Trace("crf-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("crf-match-debug") << "check variable #" << vindex - << " at depth " << visit.size() << std::endl; - Assert(vindex < static_cast(curr->d_vars.size())); - // recurse on variable? - Node var = curr->d_vars[vindex]; - bool recurse = true; - // check if it is already bound - std::map::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("crf-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 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(); -} - // the number of d_drewrite objects we have allocated (to avoid name conflicts) static unsigned drewrite_counter = 0; diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index af9ac6d87..8f5fa029f 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -20,6 +20,7 @@ #define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H #include +#include "expr/match_trie.h" #include "theory/quantifiers/dynamic_rewrite.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/sygus_sampler.h" @@ -28,57 +29,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -/** 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& vars, - std::vector& 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 > d_children; - /** The set of variables in the domain of d_children */ - std::vector d_vars; - /** The data of this node in the trie */ - Node d_data; -}; - /** candidate rewrite filter * * This class is responsible for various filtering techniques for candidate @@ -174,9 +124,9 @@ class CandidateRewriteFilter * prevents matches between terms select( x, y ) and select( z, y ) where * the type of x and z are different. */ - std::map d_match_trie; + std::map d_match_trie; /** Notify class */ - class CandidateRewriteFilterNotifyMatch : public NotifyMatch + class CandidateRewriteFilterNotifyMatch : public expr::NotifyMatch { CandidateRewriteFilter& d_sse; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 1d9ed1639..2dbc2627b 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -14,11 +14,11 @@ **/ #include "theory/quantifiers/conjecture_generator.h" +#include "expr/term_canonize.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/term_canonize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f86d82874..0281f50ec 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers_engine.h" +#include "expr/term_canonize.h" #include "options/quantifiers_options.h" #include "options/uf_options.h" #include "smt/smt_statistics_registry.h" @@ -49,7 +50,6 @@ #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_canonize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" @@ -81,7 +81,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_builder(nullptr), d_qepr(nullptr), d_term_util(new quantifiers::TermUtil(this)), - d_term_canon(new quantifiers::TermCanonize), + d_term_canon(new expr::TermCanonize), d_term_db(new quantifiers::TermDb(c, u, this)), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), @@ -330,7 +330,7 @@ quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const { return d_term_util.get(); } -quantifiers::TermCanonize* QuantifiersEngine::getTermCanonize() const +expr::TermCanonize* QuantifiersEngine::getTermCanonize() const { return d_term_canon.get(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 61e9053f5..da207c58a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -36,6 +36,10 @@ namespace CVC4 { class TheoryEngine; +namespace expr { +class TermCanonize; +} + namespace theory { class QuantifiersEngine; @@ -47,7 +51,6 @@ namespace quantifiers { class TermDb; class TermDbSygus; class TermUtil; - class TermCanonize; class Instantiate; class Skolemize; class TermEnumeration; @@ -130,7 +133,7 @@ public: /** get term utilities */ quantifiers::TermUtil* getTermUtil() const; /** get term canonizer */ - quantifiers::TermCanonize* getTermCanonize() const; + expr::TermCanonize* getTermCanonize() const; /** get quantifiers attributes */ quantifiers::QuantAttributes* getQuantAttributes() const; /** get instantiate utility */ @@ -345,7 +348,7 @@ public: /** term utilities */ std::unique_ptr d_term_util; /** term utilities */ - std::unique_ptr d_term_canon; + std::unique_ptr d_term_canon; /** term database */ std::unique_ptr d_term_db; /** sygus term database */ -- 2.30.2