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
expr_stream.h
kind_map.h
matcher.h
+ match_trie.cpp
+ match_trie.h
node.cpp
node.h
node_algorithm.cpp
pickler.h
symbol_table.cpp
symbol_table.h
+ term_canonize.cpp
+ term_canonize.h
type.cpp
type.h
type_checker.h
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#include <string>
#include <vector>
#include "expr/node.h"
-#include "theory/quantifiers/term_canonize.h"
+#include "expr/term_canonize.h"
namespace CVC4 {
namespace preprocessing {
Node d_falseNode;
/** term canonizer (for quantified formulas) */
- theory::quantifiers::TermCanonize d_tcanon;
+ expr::TermCanonize d_tcanon;
/** Cache for partitions */
std::map<Node, Partition> d_term_partition;
#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"
#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;
std::vector<Node> cterms;
// canonical terms for each type
std::map<TypeNode, std::vector<Node> > t_cterms;
- theory::quantifiers::TermCanonize tcanon;
+ expr::TermCanonize tcanon;
for (unsigned i = 0, nterms = terms.size(); i < nterms; i++)
{
Node n = terms[i];
**/
#include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/term_canonize.h"
using namespace CVC4;
using namespace std;
using namespace CVC4::kind;
struct sortTypeOrder {
- TermCanonize* d_tu;
+ expr::TermCanonize* d_tu;
bool operator() (TypeNode i, TypeNode j) {
return d_tu->getIdForType( i )<d_tu->getIdForType( j );
}
#include "theory/quantifiers_engine.h"
+#include "expr/term_canonize.h"
+
namespace CVC4 {
namespace theory {
namespace quantifiers {
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
/** 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;
};
/**
#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;
namespace quantifiers {
struct sortTypeOrder {
- TermCanonize* d_tu;
+ expr::TermCanonize* d_tu;
bool operator() (TypeNode i, TypeNode j) {
return d_tu->getIdForType( i )<d_tu->getIdForType( j );
}
namespace theory {
namespace quantifiers {
-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("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<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("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<int>(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<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("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<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();
-}
-
// the number of d_drewrite objects we have allocated (to avoid name conflicts)
static unsigned drewrite_counter = 0;
#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
#include <map>
+#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"
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<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;
-};
-
/** candidate rewrite filter
*
* This class is responsible for various filtering techniques for candidate
* prevents matches between terms select( x, y ) and select( z, y ) where
* the type of x and z are different.
*/
- std::map<TypeNode, MatchTrie> d_match_trie;
+ std::map<TypeNode, expr::MatchTrie> d_match_trie;
/** Notify class */
- class CandidateRewriteFilterNotifyMatch : public NotifyMatch
+ class CandidateRewriteFilterNotifyMatch : public expr::NotifyMatch
{
CandidateRewriteFilter& d_sse;
**/
#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"
+++ /dev/null
-/********************* */
-/*! \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 "theory/quantifiers/term_canonize.h"
-
-#include "theory/quantifiers/term_util.h"
-
-using namespace CVC4::kind;
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-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 a.getAttribute(InstVarNumAttribute())
- < b.getAttribute(InstVarNumAttribute());
- }
- 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);
- InstVarNumAttribute ivna;
- x.setAttribute(ivna, d_cn_free_var[tn].size());
- d_cn_free_var[tn].push_back(x);
- }
- return d_cn_free_var[tn][i];
-}
-
-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 && 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 quantifiers
-} // namespace theory
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \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__THEORY__QUANTIFIERS__TERM_CANONIZE_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
-
-#include <map>
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** 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;
- /** 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 quantifiers
-} // namespace theory
-} // namespace CVC4
-
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */
#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"
#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"
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)),
{
return d_term_util.get();
}
-quantifiers::TermCanonize* QuantifiersEngine::getTermCanonize() const
+expr::TermCanonize* QuantifiersEngine::getTermCanonize() const
{
return d_term_canon.get();
}
class TheoryEngine;
+namespace expr {
+class TermCanonize;
+}
+
namespace theory {
class QuantifiersEngine;
class TermDb;
class TermDbSygus;
class TermUtil;
- class TermCanonize;
class Instantiate;
class Skolemize;
class TermEnumeration;
/** 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 */
/** term utilities */
std::unique_ptr<quantifiers::TermUtil> d_term_util;
/** term utilities */
- std::unique_ptr<quantifiers::TermCanonize> d_term_canon;
+ std::unique_ptr<expr::TermCanonize> d_term_canon;
/** term database */
std::unique_ptr<quantifiers::TermDb> d_term_db;
/** sygus term database */
projects / cvc5.git / commitdiff