theory/quantifiers/bv_inverter.h \
theory/quantifiers/candidate_rewrite_database.cpp \
theory/quantifiers/candidate_rewrite_database.h \
+ theory/quantifiers/candidate_rewrite_filter.cpp \
+ theory/quantifiers/candidate_rewrite_filter.h \
theory/quantifiers/cegqi/ceg_instantiator.cpp \
theory/quantifiers/cegqi/ceg_instantiator.h \
theory/quantifiers/cegqi/ceg_arith_instantiator.cpp \
namespace theory {
namespace quantifiers {
-// the number of d_drewrite objects we have allocated (to avoid name conflicts)
-static unsigned drewrite_counter = 0;
-
CandidateRewriteDatabase::CandidateRewriteDatabase()
: d_qe(nullptr),
d_tds(nullptr),
d_ext_rewrite(nullptr),
d_using_sygus(false)
{
- if (options::sygusRewSynthFilterCong())
- {
- // initialize the dynamic rewriter
- std::stringstream ss;
- ss << "_dyn_rewriter_" << drewrite_counter;
- drewrite_counter++;
- d_drewrite = std::unique_ptr<DynamicRewriter>(
- new DynamicRewriter(ss.str(), &d_fake_context));
- d_sampler.setDynamicRewriter(d_drewrite.get());
- }
}
void CandidateRewriteDatabase::initialize(ExtendedRewriter* er,
TypeNode tn,
d_tds = nullptr;
d_ext_rewrite = er;
d_sampler.initialize(tn, vars, nsamples, unique_type_ids);
+ d_crewrite_filter.initialize(&d_sampler, nullptr, false);
}
void CandidateRewriteDatabase::initializeSygus(QuantifiersEngine* qe,
d_tds = d_qe->getTermDatabaseSygus();
d_ext_rewrite = d_tds->getExtRewriter();
d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType);
+ d_crewrite_filter.initialize(&d_sampler, d_tds, true);
}
bool CandidateRewriteDatabase::addTerm(Node sol,
if (eq_sol != sol)
{
is_unique_term = false;
- // if eq_sol is null, then we have an uninteresting candidate rewrite,
- // e.g. one that is alpha-equivalent to another.
- if (!eq_sol.isNull())
+ // should we filter the pair?
+ if (!d_crewrite_filter.filterPair(sol, eq_sol))
{
// get the actual term
Node solb = sol;
if (!is_unique_term)
{
// register this as a relevant pair (helps filtering)
- d_sampler.registerRelevantPair(sol, eq_sol);
+ d_crewrite_filter.registerRelevantPair(sol, eq_sol);
// The analog of terms sol and eq_sol are equivalent under
// sample points but do not rewrite to the same term. Hence,
// this indicates a candidate rewrite.
#include <memory>
#include <unordered_set>
#include <vector>
+#include "theory/quantifiers/candidate_rewrite_filter.h"
#include "theory/quantifiers/sygus_sampler.h"
namespace CVC4 {
* This is used for the sygusRewSynth() option to synthesize new candidate
* rewrite rules.
*/
- SygusSamplerExt d_sampler;
- /** a (dummy) user context, used for d_drewrite */
- context::UserContext d_fake_context;
- /** dynamic rewriter class */
- std::unique_ptr<DynamicRewriter> d_drewrite;
+ SygusSampler d_sampler;
+ /** candidate rewrite filter */
+ CandidateRewriteFilter d_crewrite_filter;
/**
* Cache of skolems for each free variable that appears in a synthesis check
* (for --sygus-rr-synth-check).
--- /dev/null
+/********************* */
+/*! \file candidate_rewrite_filter.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 techniques for candidate rewrite rule filtering, which
+ ** filters the output of --sygus-rr-synth. The classes in this file implement
+ ** filtering based on congruence, variable ordering, and matching.
+ **/
+
+#include "theory/quantifiers/candidate_rewrite_filter.h"
+
+#include "options/base_options.h"
+#include "options/quantifiers_options.h"
+#include "printer/printer.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+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
+ {
+ 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)
+{
+ 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;
+
+CandidateRewriteFilter::CandidateRewriteFilter()
+ : d_ss(nullptr),
+ d_tds(nullptr),
+ d_use_sygus_type(false),
+ d_drewrite(nullptr),
+ d_ssenm(*this)
+{
+}
+
+void CandidateRewriteFilter::initialize(SygusSampler* ss,
+ TermDbSygus* tds,
+ bool useSygusType)
+{
+ d_ss = ss;
+ d_use_sygus_type = false;
+ d_tds = tds;
+ // initialize members of this class
+ d_match_trie.clear();
+ d_pairs.clear();
+ if (options::sygusRewSynthFilterCong())
+ {
+ // initialize the dynamic rewriter
+ std::stringstream ss;
+ ss << "_dyn_rewriter_" << drewrite_counter;
+ drewrite_counter++;
+ d_drewrite = std::unique_ptr<DynamicRewriter>(
+ new DynamicRewriter(ss.str(), &d_fake_context));
+ }
+}
+
+bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
+{
+ Node bn = n;
+ Node beq_n = eq_n;
+ if (d_use_sygus_type)
+ {
+ bn = d_tds->sygusToBuiltin(n);
+ beq_n = d_tds->sygusToBuiltin(eq_n);
+ }
+ Trace("cr-filter") << "crewriteFilter : " << bn << "..." << beq_n
+ << std::endl;
+ // whether we will keep this pair
+ bool keep = true;
+
+ // ----- check ordering redundancy
+ if (options::sygusRewSynthFilterOrder())
+ {
+ bool nor = d_ss->isOrdered(bn);
+ bool eqor = d_ss->isOrdered(beq_n);
+ Trace("cr-filter-debug") << "Ordered? : " << nor << " " << eqor
+ << std::endl;
+ if (eqor || nor)
+ {
+ // if only one is ordered, then we require that the ordered one's
+ // variables cannot be a strict subset of the variables of the other.
+ if (!eqor)
+ {
+ if (d_ss->containsFreeVariables(beq_n, bn, true))
+ {
+ keep = false;
+ }
+ else
+ {
+ // if the previous value stored was unordered, but n is
+ // ordered, we prefer n. Thus, we force its addition to the
+ // sampler database.
+ d_ss->registerTerm(n, true);
+ }
+ }
+ else if (!nor)
+ {
+ keep = !d_ss->containsFreeVariables(bn, beq_n, true);
+ }
+ }
+ else
+ {
+ keep = false;
+ }
+ if (!keep)
+ {
+ Trace("cr-filter") << "...redundant (unordered)" << std::endl;
+ }
+ }
+
+ // ----- check rewriting redundancy
+ if (keep && d_drewrite != nullptr)
+ {
+ Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl;
+ if (d_drewrite->areEqual(bn, beq_n))
+ {
+ // must be unique according to the dynamic rewriter
+ Trace("cr-filter") << "...redundant (rewritable)" << std::endl;
+ keep = false;
+ }
+ }
+
+ if (options::sygusRewSynthFilterMatch())
+ {
+ // ----- check matchable
+ // check whether the pair is matchable with a previous one
+ d_curr_pair_rhs = beq_n;
+ Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n
+ << "]..." << std::endl;
+ if (!d_match_trie.getMatches(bn, &d_ssenm))
+ {
+ keep = false;
+ Trace("cr-filter") << "...redundant (matchable)" << std::endl;
+ // regardless, would help to remember it
+ registerRelevantPair(n, eq_n);
+ }
+ }
+
+ if (keep)
+ {
+ return false;
+ }
+ if (Trace.isOn("sygus-rr-filter"))
+ {
+ Printer* p = Printer::getPrinter(options::outputLanguage());
+ std::stringstream ss;
+ ss << "(redundant-rewrite ";
+ p->toStreamSygus(ss, n);
+ ss << " ";
+ p->toStreamSygus(ss, eq_n);
+ ss << ")";
+ Trace("sygus-rr-filter") << ss.str() << std::endl;
+ }
+ return true;
+}
+
+void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n)
+{
+ Node bn = n;
+ Node beq_n = eq_n;
+ if (d_use_sygus_type)
+ {
+ bn = d_tds->sygusToBuiltin(n);
+ beq_n = d_tds->sygusToBuiltin(eq_n);
+ }
+ // ----- check rewriting redundancy
+ if (d_drewrite != nullptr)
+ {
+ Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl;
+ Assert(!d_drewrite->areEqual(bn, beq_n));
+ d_drewrite->addRewrite(bn, beq_n);
+ }
+ if (options::sygusRewSynthFilterMatch())
+ {
+ // add to match information
+ for (unsigned r = 0; r < 2; r++)
+ {
+ Node t = r == 0 ? bn : beq_n;
+ Node to = r == 0 ? beq_n : bn;
+ // insert in match trie if first time
+ if (d_pairs.find(t) == d_pairs.end())
+ {
+ Trace("crf-match") << "CRF add term : " << t << std::endl;
+ d_match_trie.addTerm(t);
+ }
+ d_pairs[t].insert(to);
+ }
+ }
+}
+
+bool CandidateRewriteFilter::notify(Node s,
+ Node n,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs)
+{
+ Assert(!d_curr_pair_rhs.isNull());
+ std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it =
+ d_pairs.find(n);
+ if (Trace.isOn("crf-match"))
+ {
+ Trace("crf-match") << " " << s << " matches " << n
+ << " under:" << std::endl;
+ for (unsigned i = 0, size = vars.size(); i < size; i++)
+ {
+ Trace("crf-match") << " " << vars[i] << " -> " << subs[i] << std::endl;
+ // TODO (#1923) ensure that we use an internal representation to
+ // ensure polymorphism is handled correctly
+ Assert(vars[i].getType().isComparableTo(subs[i].getType()));
+ }
+ }
+ Assert(it != d_pairs.end());
+ for (const Node& nr : it->second)
+ {
+ Node nrs =
+ nr.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+ bool areEqual = (nrs == d_curr_pair_rhs);
+ if (!areEqual && d_drewrite != nullptr)
+ {
+ // if dynamic rewriter is available, consult it
+ areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs);
+ }
+ if (areEqual)
+ {
+ Trace("crf-match") << "*** Match, current pair: " << std::endl;
+ Trace("crf-match") << " (" << s << ", " << d_curr_pair_rhs << ")"
+ << std::endl;
+ Trace("crf-match") << "is an instance of previous pair:" << std::endl;
+ Trace("crf-match") << " (" << n << ", " << nr << ")" << std::endl;
+ return false;
+ }
+ }
+ return true;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file candidate_rewrite_filter.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 techniques for candidate rewrite rule filtering, which
+ ** filters the output of --sygus-rr-synth. The classes in this file implement
+ ** filtering based on congruence, variable ordering, and matching.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
+#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
+
+#include <map>
+#include "theory/quantifiers/dynamic_rewrite.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+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<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
+ * rewrite rules, including:
+ * (1) filtering based on variable ordering,
+ * (2) filtering based on congruence,
+ * (3) filtering based on matching.
+ * For details, see Reynolds et al "Rewrites for SMT Solvers using Syntax-Guided
+ * Enumeration", SMT 2018.
+ *
+ * In the following, we assume that the registerRelevantPair method of this
+ * class been called for some pairs of terms. For each such call to
+ * registerRelevantPair( t, s ), we say that (t,s) and (s,t) are "relevant
+ * pairs". A relevant pair ( t, s ) typically corresponds to a (candidate)
+ * rewrite t = s.
+ */
+class CandidateRewriteFilter
+{
+ public:
+ CandidateRewriteFilter();
+
+ /** initialize
+ *
+ * Initializes this class, ss is the sygus sampler that this class is
+ * filtering rewrite rule pairs for, and tds is a point to the sygus term
+ * database utility class.
+ *
+ * If useSygusType is false, this means that the terms in filterPair and
+ * registerRelevantPair calls should be interpreted as themselves. Otherwise,
+ * if useSygusType is true, these terms should be interpreted as their
+ * analog according to the deep embedding.
+ */
+ void initialize(SygusSampler* ss, TermDbSygus* tds, bool useSygusType);
+ /** filter pair
+ *
+ * This method returns true if the pair (n, eq_n) should be filtered. If it
+ * is not filtered, then the caller may choose to call
+ * registerRelevantPair(n, eq_n) below, although it may not, say if it finds
+ * another reason to discard the pair.
+ *
+ * If this method returns false, then for all previous relevant pairs
+ * ( a, eq_a ), we have that n = eq_n is not an instance of a = eq_a
+ * modulo symmetry of equality, nor is n = eq_n derivable from the set of
+ * all previous relevant pairs. The latter is determined by the d_drewrite
+ * utility. For example:
+ * [1] ( t+0, t ) and ( x+0, x )
+ * will not both be relevant pairs of this function since t+0=t is
+ * an instance of x+0=x.
+ * [2] ( s, t ) and ( s+0, t+0 )
+ * will not both be relevant pairs of this function since s+0=t+0 is
+ * derivable from s=t.
+ * These two criteria may be combined, for example:
+ * [3] ( t+0, s ) is not a relevant pair if both ( x+0, x+s ) and ( t+s, s )
+ * are relevant pairs, since t+0 is an instance of x+0 where
+ * { x |-> t }, and x+s { x |-> t } = s is derivable, via the third pair
+ * above (t+s = s).
+ */
+ bool filterPair(Node n, Node eq_n);
+ /** register relevant pair
+ *
+ * This should be called after filterPair( n, eq_n ) returns false.
+ * This registers ( n, eq_n ) as a relevant pair with this class.
+ */
+ void registerRelevantPair(Node n, Node eq_n);
+
+ private:
+ /** pointer to the sygus sampler that this class is filtering rewrites for */
+ SygusSampler* d_ss;
+ /** pointer to the sygus term database, used if d_use_sygus_type is true */
+ TermDbSygus* d_tds;
+ /** whether we are registering sygus terms with this class */
+ bool d_use_sygus_type;
+
+ //----------------------------congruence filtering
+ /** a (dummy) user context, used for d_drewrite */
+ context::UserContext d_fake_context;
+ /** dynamic rewriter class */
+ std::unique_ptr<DynamicRewriter> d_drewrite;
+ //----------------------------end congruence filtering
+
+ //----------------------------match filtering
+ /**
+ * Stores all relevant pairs returned by this sampler (see registerTerm). In
+ * detail, if (t,s) is a relevant pair, then t in d_pairs[s].
+ */
+ std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs;
+ /** Match trie storing all terms in the domain of d_pairs. */
+ MatchTrie d_match_trie;
+ /** Notify class */
+ class CandidateRewriteFilterNotifyMatch : public NotifyMatch
+ {
+ CandidateRewriteFilter& d_sse;
+
+ public:
+ CandidateRewriteFilterNotifyMatch(CandidateRewriteFilter& sse) : d_sse(sse)
+ {
+ }
+ /** notify match */
+ bool notify(Node n,
+ Node s,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs) override
+ {
+ return d_sse.notify(n, s, vars, subs);
+ }
+ };
+ /** Notify object used for reporting matches from d_match_trie */
+ CandidateRewriteFilterNotifyMatch d_ssenm;
+ /**
+ * Stores the current right hand side of a pair we are considering.
+ *
+ * In more detail, in registerTerm, we are interested in whether a pair (s,t)
+ * is a relevant pair. We do this by:
+ * (1) Setting the node d_curr_pair_rhs to t,
+ * (2) Using d_match_trie, compute all terms s1...sn that match s.
+ * For each si, where s = si * sigma for some substitution sigma, we check
+ * whether t = ti * sigma for some previously relevant pair (si,ti), in
+ * which case (s,t) is an instance of (si,ti).
+ */
+ Node d_curr_pair_rhs;
+ /**
+ * Called by the above class during d_match_trie.getMatches( s ), when we
+ * find that si = s * sigma, where si is a term that is stored in
+ * d_match_trie.
+ *
+ * This function returns false if ( s, d_curr_pair_rhs ) is an instance of
+ * previously relevant pair.
+ */
+ bool notify(Node s, Node n, std::vector<Node>& vars, std::vector<Node>& subs);
+ //----------------------------end match filtering
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
}
}
-SygusSamplerExt::SygusSamplerExt() : d_drewrite(nullptr), d_ssenm(*this) {}
-
-void SygusSamplerExt::initializeSygus(TermDbSygus* tds,
- Node f,
- unsigned nsamples,
- bool useSygusType)
-{
- SygusSampler::initializeSygus(tds, f, nsamples, useSygusType);
- d_pairs.clear();
- d_match_trie.clear();
-}
-
-void SygusSamplerExt::setDynamicRewriter(DynamicRewriter* dr)
-{
- d_drewrite = dr;
-}
-
-Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
-{
- Node eq_n = SygusSampler::registerTerm(n, forceKeep);
- if (eq_n == n)
- {
- // this is a unique term
- return n;
- }
- Node bn = n;
- Node beq_n = eq_n;
- if (d_use_sygus_type)
- {
- bn = d_tds->sygusToBuiltin(n);
- beq_n = d_tds->sygusToBuiltin(eq_n);
- }
- Trace("sygus-synth-rr") << "sygusSampleExt : " << bn << "..." << beq_n
- << std::endl;
- // whether we will keep this pair
- bool keep = true;
-
- // ----- check ordering redundancy
- if (options::sygusRewSynthFilterOrder())
- {
- bool nor = isOrdered(bn);
- bool eqor = isOrdered(beq_n);
- Trace("sygus-synth-rr-debug") << "Ordered? : " << nor << " " << eqor
- << std::endl;
- if (eqor || nor)
- {
- // if only one is ordered, then we require that the ordered one's
- // variables cannot be a strict subset of the variables of the other.
- if (!eqor)
- {
- if (containsFreeVariables(beq_n, bn, true))
- {
- keep = false;
- }
- else
- {
- // if the previous value stored was unordered, but n is
- // ordered, we prefer n. Thus, we force its addition to the
- // sampler database.
- SygusSampler::registerTerm(n, true);
- }
- }
- else if (!nor)
- {
- keep = !containsFreeVariables(bn, beq_n, true);
- }
- }
- else
- {
- keep = false;
- }
- if (!keep)
- {
- Trace("sygus-synth-rr") << "...redundant (unordered)" << std::endl;
- }
- }
-
- // ----- check rewriting redundancy
- if (keep && d_drewrite != nullptr)
- {
- Trace("sygus-synth-rr-debug") << "Check equal rewrite pair..." << std::endl;
- if (d_drewrite->areEqual(bn, beq_n))
- {
- // must be unique according to the dynamic rewriter
- Trace("sygus-synth-rr") << "...redundant (rewritable)" << std::endl;
- keep = false;
- }
- }
-
- if (options::sygusRewSynthFilterMatch())
- {
- // ----- check matchable
- // check whether the pair is matchable with a previous one
- d_curr_pair_rhs = beq_n;
- Trace("sse-match") << "SSE check matches : " << bn << " [rhs = " << beq_n
- << "]..." << std::endl;
- if (!d_match_trie.getMatches(bn, &d_ssenm))
- {
- keep = false;
- Trace("sygus-synth-rr") << "...redundant (matchable)" << std::endl;
- // regardless, would help to remember it
- registerRelevantPair(n, eq_n);
- }
- }
-
- if (keep)
- {
- return eq_n;
- }
- if (Trace.isOn("sygus-rr-filter"))
- {
- Printer* p = Printer::getPrinter(options::outputLanguage());
- std::stringstream ss;
- ss << "(redundant-rewrite ";
- p->toStreamSygus(ss, n);
- ss << " ";
- p->toStreamSygus(ss, eq_n);
- ss << ")";
- Trace("sygus-rr-filter") << ss.str() << std::endl;
- }
- return Node::null();
-}
-
-void SygusSamplerExt::registerRelevantPair(Node n, Node eq_n)
-{
- Node bn = n;
- Node beq_n = eq_n;
- if (d_use_sygus_type)
- {
- bn = d_tds->sygusToBuiltin(n);
- beq_n = d_tds->sygusToBuiltin(eq_n);
- }
- // ----- check rewriting redundancy
- if (d_drewrite != nullptr)
- {
- Trace("sygus-synth-rr-debug") << "Add rewrite pair..." << std::endl;
- Assert(!d_drewrite->areEqual(bn, beq_n));
- d_drewrite->addRewrite(bn, beq_n);
- }
- if (options::sygusRewSynthFilterMatch())
- {
- // add to match information
- for (unsigned r = 0; r < 2; r++)
- {
- Node t = r == 0 ? bn : beq_n;
- Node to = r == 0 ? beq_n : bn;
- // insert in match trie if first time
- if (d_pairs.find(t) == d_pairs.end())
- {
- Trace("sse-match") << "SSE add term : " << t << std::endl;
- d_match_trie.addTerm(t);
- }
- d_pairs[t].insert(to);
- }
- }
-}
-
-bool SygusSamplerExt::notify(Node s,
- Node n,
- std::vector<Node>& vars,
- std::vector<Node>& subs)
-{
- Assert(!d_curr_pair_rhs.isNull());
- std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it =
- d_pairs.find(n);
- if (Trace.isOn("sse-match"))
- {
- Trace("sse-match") << " " << s << " matches " << n
- << " under:" << std::endl;
- for (unsigned i = 0, size = vars.size(); i < size; i++)
- {
- Trace("sse-match") << " " << vars[i] << " -> " << subs[i] << std::endl;
- // TODO (#1923) ensure that we use an internal representation to
- // ensure polymorphism is handled correctly
- Assert(vars[i].getType().isComparableTo(subs[i].getType()));
- }
- }
- Assert(it != d_pairs.end());
- for (const Node& nr : it->second)
- {
- Node nrs =
- nr.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
- bool areEqual = (nrs == d_curr_pair_rhs);
- if (!areEqual && d_drewrite != nullptr)
- {
- // if dynamic rewriter is available, consult it
- areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs);
- }
- if (areEqual)
- {
- Trace("sse-match") << "*** Match, current pair: " << std::endl;
- Trace("sse-match") << " (" << s << ", " << d_curr_pair_rhs << ")"
- << std::endl;
- Trace("sse-match") << "is an instance of previous pair:" << std::endl;
- Trace("sse-match") << " (" << n << ", " << nr << ")" << std::endl;
- return false;
- }
- }
- return true;
-}
-
-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("sse-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("sse-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("sse-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("sse-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("sse-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
- {
- vars.push_back(var);
- subs.push_back(cn);
- smap[var] = cn;
- visit_bound_var[index] = true;
- }
- if (recurse)
- {
- Trace("sse-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)
-{
- 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();
-}
-
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
#include <map>
#include "theory/evaluator.h"
-#include "theory/quantifiers/dynamic_rewrite.h"
#include "theory/quantifiers/lazy_trie.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_enumeration.h"
namespace theory {
namespace quantifiers {
-
/** SygusSampler
*
* This class can be used to test whether two expressions are equivalent
*/
int getDiffSamplePointIndex(Node a, Node b);
- protected:
+ //--------------------------queries about terms
/** is contiguous
*
* This returns whether n's free variables (terms occurring in the range of
* occur in the range d_type_vars.
*/
bool containsFreeVariables(Node a, Node b, bool strict = false);
+ //--------------------------end queries about terms
protected:
/** sygus term database of d_qe */
void registerSygusType(TypeNode tn);
};
-/** 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 from S that are matchable with t.
- */
-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;
-};
-
-/** Version of the above class with some additional features */
-class SygusSamplerExt : public SygusSampler
-{
- public:
- SygusSamplerExt();
- /** initialize */
- void initializeSygus(TermDbSygus* tds,
- Node f,
- unsigned nsamples,
- bool useSygusType) override;
- /** set dynamic rewriter
- *
- * This tells this class to use the dynamic rewriter object dr. This utility
- * is used to query whether pairs of terms are already entailed to be
- * equal based on previous rewrite rules.
- */
- void setDynamicRewriter(DynamicRewriter* dr);
-
- /** register term n with this sampler database
- *
- * For each call to registerTerm( t, ... ) that returns s, we say that
- * (t,s) and (s,t) are "relevant pairs".
- *
- * This returns either null, or a term ret with the same guarantees as
- * SygusSampler::registerTerm with the additional guarantee
- * that for all previous relevant pairs ( n', nret' ),
- * we have that n = ret is not an instance of n' = ret'
- * modulo symmetry of equality, nor is n = ret derivable from the set of
- * all previous relevant pairs. The latter is determined by the d_drewrite
- * utility. For example:
- * [1] ( t+0, t ) and ( x+0, x )
- * will not both be relevant pairs of this function since t+0=t is
- * an instance of x+0=x.
- * [2] ( s, t ) and ( s+0, t+0 )
- * will not both be relevant pairs of this function since s+0=t+0 is
- * derivable from s=t.
- * These two criteria may be combined, for example:
- * [3] ( t+0, s ) is not a relevant pair if both ( x+0, x+s ) and ( t+s, s )
- * are relevant pairs, since t+0 is an instance of x+0 where
- * { x |-> t }, and x+s { x |-> t } = s is derivable, via the third pair
- * above (t+s = s).
- *
- * If this function returns null, then n is equivalent to a previously
- * registered term ret, and the equality ( n, ret ) is either an instance
- * of a previous relevant pair ( n', ret' ), or n = ret is derivable
- * from the set of all previous relevant pairs based on the
- * d_drewrite utility, or is an instance of a previous pair
- */
- Node registerTerm(Node n, bool forceKeep = false) override;
- /** register relevant pair
- *
- * This should be called after registerTerm( n ) returns eq_n.
- * This registers ( n, eq_n ) as a relevant pair with this class.
- */
- void registerRelevantPair(Node n, Node eq_n);
-
- private:
- /** pointer to the dynamic rewriter class */
- DynamicRewriter* d_drewrite;
-
- //----------------------------match filtering
- /**
- * Stores all relevant pairs returned by this sampler (see registerTerm). In
- * detail, if (t,s) is a relevant pair, then t in d_pairs[s].
- */
- std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs;
- /** Match trie storing all terms in the domain of d_pairs. */
- MatchTrie d_match_trie;
- /** Notify class */
- class SygusSamplerExtNotifyMatch : public NotifyMatch
- {
- SygusSamplerExt& d_sse;
-
- public:
- SygusSamplerExtNotifyMatch(SygusSamplerExt& sse) : d_sse(sse) {}
- /** notify match */
- bool notify(Node n,
- Node s,
- std::vector<Node>& vars,
- std::vector<Node>& subs) override
- {
- return d_sse.notify(n, s, vars, subs);
- }
- };
- /** Notify object used for reporting matches from d_match_trie */
- SygusSamplerExtNotifyMatch d_ssenm;
- /**
- * Stores the current right hand side of a pair we are considering.
- *
- * In more detail, in registerTerm, we are interested in whether a pair (s,t)
- * is a relevant pair. We do this by:
- * (1) Setting the node d_curr_pair_rhs to t,
- * (2) Using d_match_trie, compute all terms s1...sn that match s.
- * For each si, where s = si * sigma for some substitution sigma, we check
- * whether t = ti * sigma for some previously relevant pair (si,ti), in
- * which case (s,t) is an instance of (si,ti).
- */
- Node d_curr_pair_rhs;
- /**
- * Called by the above class during d_match_trie.getMatches( s ), when we
- * find that si = s * sigma, where si is a term that is stored in
- * d_match_trie.
- *
- * This function returns false if ( s, d_curr_pair_rhs ) is an instance of
- * previously relevant pair.
- */
- bool notify(Node s, Node n, std::vector<Node>& vars, std::vector<Node>& subs);
- //----------------------------end match filtering
-};
-
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
projects / cvc5.git / commitdiff