type = "bool"
default = "false"
read_only = true
- help = "use sygus to enumerate and verify correctness of rewrite rules via sampling"
+ help = "use sygus to enumerate and verify correctness of rewrite rules"
[[option]]
name = "sygusRewSynth"
long = "sygus-rr-synth"
type = "bool"
default = "false"
- help = "use sygus to enumerate candidate rewrite rules via sampling"
+ help = "use sygus to enumerate candidate rewrite rules"
[[option]]
name = "sygusRewSynthFilterOrder"
long = "sygus-expr-miner-check-timeout=N"
type = "unsigned long"
help = "timeout (in milliseconds) for satisfiability checks in expression miners"
+
+[[option]]
+ name = "sygusRewSynthRec"
+ category = "regular"
+ long = "sygus-rr-synth-rec"
+ type = "bool"
+ default = "false"
+ help = "synthesize rewrite rules over all sygus grammar types recursively"
[[option]]
name = "sygusQueryGen"
}
bool CandidateRewriteDatabase::addTerm(Node sol,
+ bool rec,
std::ostream& out,
bool& rew_print)
{
+ // have we added this term before?
+ std::unordered_map<Node, bool, NodeHashFunction>::iterator itac =
+ d_add_term_cache.find(sol);
+ if (itac != d_add_term_cache.end())
+ {
+ return itac->second;
+ }
+
+ if (rec)
+ {
+ // if recursive, we first add all subterms
+ for (const Node& solc : sol)
+ {
+ // whether a candidate rewrite is printed for any subterm is irrelevant
+ bool rew_printc = false;
+ addTerm(solc, rec, out, rew_printc);
+ }
+ }
+ // register the term
bool is_unique_term = true;
Node eq_sol = d_sampler->registerTerm(sol);
// eq_sol is a candidate solution that is equivalent to sol
// it discards it as a redundant candidate rewrite rule before
// checking its correctness.
}
+ d_add_term_cache[sol] = is_unique_term;
return is_unique_term;
}
-bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
+bool CandidateRewriteDatabase::addTerm(Node sol, bool rec, std::ostream& out)
{
bool rew_print = false;
- return addTerm(sol, out, rew_print);
+ return addTerm(sol, rec, out, rew_print);
+}
+bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
+{
+ return addTerm(sol, false, out);
}
void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; }
Trace("synth-rr-dbg") << "...finish." << std::endl;
}
Trace("synth-rr-dbg") << "Add term " << nr << " for " << tn << std::endl;
- return itc->second.addTerm(nr, out);
+ return itc->second.addTerm(nr, false, out);
}
} /* CVC4::theory::quantifiers namespace */
* cause a candidate-rewrite to be printed on the output stream out.
* We return true if the term sol is distinct (up to equivalence) with
* all previous terms added to this class. The argument rew_print is set to
- * true if this class printed a rewrite.
+ * true if this class printed a rewrite involving sol.
+ *
+ * If the flag rec is true, then we also recursively add all subterms of sol
+ * to this class as well.
*/
- bool addTerm(Node sol, std::ostream& out, bool& rew_print);
+ bool addTerm(Node sol, bool rec, std::ostream& out, bool& rew_print);
+ bool addTerm(Node sol, bool rec, std::ostream& out);
bool addTerm(Node sol, std::ostream& out) override;
/** sets whether this class should output candidate rewrites it finds */
void setSilent(bool flag);
bool d_using_sygus;
/** 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).
+ */
+ std::map<Node, Node> d_fv_to_skolem;
+ /** the cache for results of addTerm */
+ std::unordered_map<Node, bool, NodeHashFunction> d_add_term_cache;
/** if true, we silence the output of candidate rewrites */
bool d_silent;
};
* This registers term n with this class. We generate the candidate rewrite
* database of the appropriate type (if not allocated already), and register
* n with this database. This may result in "candidate-rewrite" being
- * printed on the output stream out.
+ * printed on the output stream out. We return true if the term sol is
+ * distinct (up to equivalence) with all previous terms added to this class.
*/
bool addTerm(Node n, std::ostream& out);
// ----- check rewriting redundancy
if (keep && options::sygusRewSynthFilterCong())
{
+ // When using sygus types, this filtering applies to the builtin versions
+ // of n and eq_n. This means that we may filter out a rewrite rule for one
+ // sygus type based on another, e.g. we won't report x=x+0 for both A and B
+ // in:
+ // A -> x | 0 | A+A
+ // B -> x | 0 | B+B
Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl;
if (d_drewrite->areEqual(bn, beq_n))
{
Node bni = d_drewrite->toInternal(bn);
if (!bni.isNull())
{
- if (!d_match_trie.getMatches(bni, &d_ssenm))
+ // as with congruence filtering, we cache based on the builtin type
+ TypeNode tn = bn.getType();
+ if (!d_match_trie[tn].getMatches(bni, &d_ssenm))
{
keep = false;
Trace("cr-filter") << "...redundant (matchable)" << std::endl;
}
if (options::sygusRewSynthFilterMatch())
{
+ // cache based on the builtin type
+ TypeNode tn = bn.getType();
// add to match information
for (unsigned r = 0; r < 2; r++)
{
Node ti = d_drewrite->toInternal(t);
if (!ti.isNull())
{
- d_match_trie.addTerm(ti);
+ d_match_trie[tn].addTerm(ti);
}
}
d_pairs[t].insert(to);
* 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.
+ /**
+ * For each (builtin) type, a match trie storing all terms in the domain of
+ * d_pairs.
*
* Notice that we store d_drewrite->toInternal(t) instead of t, for each
* term t, so that polymorphism is handled properly. In particular, this
* prevents matches between terms select( x, y ) and select( z, y ) where
* the type of x and z are different.
*/
- MatchTrie d_match_trie;
+ std::map<TypeNode, MatchTrie> d_match_trie;
/** Notify class */
class CandidateRewriteFilterNotifyMatch : public NotifyMatch
{
#include "theory/quantifiers/expr_miner_manager.h"
#include "theory/quantifiers_engine.h"
+#include "options/quantifiers_options.h"
+
namespace CVC4 {
namespace theory {
namespace quantifiers {
bool ret = true;
if (d_doRewSynth)
{
- ret = d_crd.addTerm(sol, out, rew_print);
+ ret = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print);
}
// a unique term, let's try the query generator
d_tds = nullptr;
d_use_sygus_type = false;
d_is_valid = true;
- d_tn = tn;
d_ftn = TypeNode::null();
d_type_vars.clear();
d_vars.clear();
Assert(d_ftn.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype();
Assert(dt.isSygus());
- d_tn = TypeNode::fromType(dt.getSygusType());
Trace("sygus-sample") << "Register sampler for " << f << std::endl;
Node SygusSampler::registerTerm(Node n, bool forceKeep)
{
- if (d_is_valid)
+ if (!d_is_valid)
{
- Node bn = n;
- // if this is a sygus type, get its builtin analog
- if (d_use_sygus_type)
- {
- Assert(!d_ftn.isNull());
- bn = d_tds->sygusToBuiltin(n);
- Assert(d_builtin_to_sygus.find(bn) == d_builtin_to_sygus.end()
- || d_builtin_to_sygus[bn] == n);
- d_builtin_to_sygus[bn] = n;
- }
- Assert(bn.getType() == d_tn);
- Node res = d_trie.add(bn, this, 0, d_samples.size(), forceKeep);
- if (d_use_sygus_type)
- {
- Assert(d_builtin_to_sygus.find(res) != d_builtin_to_sygus.end());
- res = res != bn ? d_builtin_to_sygus[res] : n;
- }
- return res;
+ // do nothing
+ return n;
+ }
+ Node bn = n;
+ TypeNode tn = n.getType();
+ // If we are using sygus types, get the builtin analog of n.
+ if (d_use_sygus_type)
+ {
+ bn = d_tds->sygusToBuiltin(n);
+ d_builtin_to_sygus[tn][bn] = n;
+ }
+ // cache based on the (original) type of n
+ Node res = d_trie[tn].add(bn, this, 0, d_samples.size(), forceKeep);
+ // If we are using sygus types, map back to an original.
+ // Notice that d_builtin_to_sygus is not necessarily bijective.
+ if (d_use_sygus_type)
+ {
+ std::map<Node, Node>& bts = d_builtin_to_sygus[tn];
+ Assert(bts.find(res) != bts.end());
+ res = res != bn ? bts[res] : n;
}
- return n;
+ return res;
}
bool SygusSampler::isContiguous(Node n)
};
/** a trie for samples */
PtTrie d_samples_trie;
- /** type of nodes we will be registering with this class */
- TypeNode d_tn;
/** the sygus type for this sampler (if applicable). */
TypeNode d_ftn;
- /** whether we are registering terms of type d_ftn */
+ /** whether we are registering terms of sygus types with this sampler */
bool d_use_sygus_type;
- /** map from builtin terms to the sygus term they correspond to */
- std::map<Node, Node> d_builtin_to_sygus;
+ /**
+ * For each (sygus) type, a map from builtin terms to the sygus term they
+ * correspond to.
+ */
+ std::map<TypeNode, std::map<Node, Node> > d_builtin_to_sygus;
/** all variables we are sampling values for */
std::vector<Node> d_vars;
/** type variables
* that type.
*/
std::map<TypeNode, std::vector<Node> > d_type_consts;
- /** the lazy trie */
- LazyTrie d_trie;
+ /** a lazy trie for each type
+ *
+ * This stores the evaluation of all terms registered to this class.
+ *
+ * Notice if we are registering sygus terms with this class, then terms
+ * are grouped into this trie according to their sygus type, and not their
+ * builtin type. For example, for grammar:
+ * A -> x | B+1
+ * B -> x | 0 | 1 | B+B
+ * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class,
+ * then x+0 is registered to d_trie[B] and x is registered to d_trie[A],
+ * and no rewrite rule is reported. The reason for this is that otherwise
+ * we would end up reporting many useless rewrites since the same builtin
+ * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()).
+ */
+ std::map<TypeNode, LazyTrie> d_trie;
/** is this sampler valid?
*
* A sampler can be invalid if sample points cannot be generated for a type
projects / cvc5.git / commitdiff