mode for using samples in the counterexample-guided inductive synthesis loop
# internal uses of sygus
-option sygusRewSynth --sygus-rr-synth bool :default false
+option sygusRew --sygus-rr bool :default false
+ use sygus to enumerate and verify correctness of rewrite rules via sampling
+option sygusRewSynth --sygus-rr-synth bool :read-write :default false
use sygus to enumerate candidate rewrite rules via sampling
-option sygusRewVerify --sygus-rr-verify bool :default false
+option sygusRewVerify --sygus-rr-verify bool :read-write :default false
use sygus to verify the correctness of rewrite rules via sampling
option sygusSamples --sygus-samples=N int :read-write :default 100 :read-write
number of points to consider when doing sygus rewriter sample testing
if( !options::instNoEntail.wasSetByUser() ){
options::instNoEntail.set( false );
}
- if (options::sygusRewSynth())
+ if (options::sygusRew())
+ {
+ options::sygusRewSynth.set(true);
+ options::sygusRewVerify.set(true);
+ }
+ if (options::sygusRewSynth() || options::sygusRewVerify())
{
// rewrite rule synthesis implies that sygus stream must be true
options::sygusStream.set(true);
std::ostream* out = nodeManagerOptions.getOut();
(*out) << "(unsound-rewrite " << prev_bv << " " << bv << ")"
<< std::endl;
+ // debugging information
+ if (Trace.isOn("sygus-rr-debug"))
+ {
+ int pt_index = its->second.getDiffSamplePointIndex(bv, prev_bv);
+ if (pt_index >= 0)
+ {
+ Trace("sygus-rr-debug")
+ << "; both ext-rewrite to : " << bvr << std::endl;
+ Trace("sygus-rr-debug")
+ << "; but are not equivalent for : " << std::endl;
+ std::vector<Node> vars;
+ std::vector<Node> pt;
+ its->second.getSamplePoint(pt_index, vars, pt);
+ Assert(vars.size() == pt.size());
+ for (unsigned i = 0, size = pt.size(); i < size; i++)
+ {
+ Trace("sygus-rr-debug")
+ << "; " << vars[i] << " -> " << pt[i] << std::endl;
+ }
+ Node bv_e = its->second.evaluate(bv, pt_index);
+ Node pbv_e = its->second.evaluate(prev_bv, pt_index);
+ Assert(bv_e != pbv_e);
+ Trace("sygus-rr-debug") << "; where they evaluate to " << pbv_e
+ << " and " << bv_e << std::endl;
+ }
+ else
+ {
+ Assert(false);
+ }
+ }
}
}
}
if (status != 0 && options::sygusRewSynth())
{
TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
- std::map<Node, SygusSampler>::iterator its = d_sampler.find(prog);
+ std::map<Node, SygusSamplerExt>::iterator its = d_sampler.find(prog);
if (its == d_sampler.end())
{
d_sampler[prog].initializeSygus(
// eq_sol is a candidate solution that is equivalent to sol
if (eq_sol != solb)
{
- // one of eq_sol or solb must be ordered
- bool eqor = its->second.isOrdered(eq_sol);
- bool sor = its->second.isOrdered(solb);
- bool outputRewrite = false;
- if (eqor || sor)
+ // Terms solb and eq_sol are equivalent under sample points but do
+ // not rewrite to the same term. Hence, this indicates a candidate
+ // rewrite.
+ out << "(candidate-rewrite " << solb << " " << eq_sol << ")"
+ << std::endl;
+ // debugging information
+ if (Trace.isOn("sygus-rr-debug"))
{
- outputRewrite = true;
- // if only one is ordered, then the ordered one must contain the
- // free variables of the other
- if (!eqor)
- {
- outputRewrite = its->second.containsFreeVariables(solb, eq_sol);
- }
- else if (!sor)
- {
- outputRewrite = its->second.containsFreeVariables(eq_sol, solb);
- }
- }
-
- if (outputRewrite)
- {
- // Terms solb and eq_sol are equivalent under sample points but do
- // not rewrite to the same term. Hence, this indicates a candidate
- // rewrite.
- out << "(candidate-rewrite " << solb << " " << eq_sol << ")"
- << std::endl;
- // if the previous value stored was unordered, but this is
- // ordered, we prefer this one. Thus, we force its addition to the
- // sampler database.
- if (!eqor)
- {
- its->second.registerTerm(solb, true);
- }
- }
- else
- {
- Trace("sygus-synth-rr")
- << "Alpha equivalent candidate rewrite : " << eq_sol << " "
- << solb << std::endl;
+ ExtendedRewriter* er = sygusDb->getExtRewriter();
+ Node solbr = er->extendedRewrite(solb);
+ Node eq_solr = er->extendedRewrite(eq_sol);
+ Trace("sygus-rr-debug")
+ << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
+ Trace("sygus-rr-debug")
+ << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
}
}
}
Trace("cegis-sample-debug") << "...false for point #" << i << std::endl;
// mark this as a CEGIS point (no longer sampled)
d_cegis_sample_refine.insert(i);
+ std::vector<Node> vars;
std::vector<Node> pt;
- d_cegis_sampler.getSamplePoint(i, pt);
+ d_cegis_sampler.getSamplePoint(i, vars, pt);
Assert(d_base_vars.size() == pt.size());
Node rlem = d_base_body.substitute(
d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end());
* This is used for the sygusRewSynth() option to synthesize new candidate
* rewrite rules.
*/
- std::map<Node, SygusSampler> d_sampler;
+ std::map<Node, SygusSamplerExt> d_sampler;
/** sampler object for the option cegisSample()
*
* This samples points of the type of the inner variables of the synthesis
d_is_valid = true;
d_tn = tn;
d_ftn = TypeNode::null();
+ d_type_vars.clear();
+ d_vars.clear();
+ d_rvalue_cindices.clear();
+ d_rvalue_null_cindices.clear();
+ d_var_sygus_types.clear();
d_vars.insert(d_vars.end(), vars.begin(), vars.end());
- for (const Node& sv : vars)
+ std::map<TypeNode, unsigned> type_to_type_id;
+ unsigned type_id_counter = 0;
+ for (const Node& sv : d_vars)
{
TypeNode svt = sv.getType();
- d_var_index[sv] = d_type_vars[svt].size();
- d_type_vars[svt].push_back(sv);
+ unsigned tnid;
+ std::map<TypeNode, unsigned>::iterator itt = type_to_type_id.find(svt);
+ if (itt == type_to_type_id.end())
+ {
+ type_to_type_id[svt] = type_id_counter;
+ type_id_counter++;
+ }
+ else
+ {
+ tnid = itt->second;
+ }
+ Trace("sygus-sample-debug")
+ << "Type id for " << sv << " is " << tnid << std::endl;
+ d_var_index[sv] = d_type_vars[tnid].size();
+ d_type_vars[tnid].push_back(sv);
}
- d_rvalue_cindices.clear();
- d_rvalue_null_cindices.clear();
- d_var_sygus_types.clear();
initializeSamples(nsamples);
}
Trace("sygus-sample") << "Register sampler for " << f << std::endl;
+ d_vars.clear();
+ d_type_vars.clear();
d_var_index.clear();
d_type_vars.clear();
+ d_rvalue_cindices.clear();
+ d_rvalue_null_cindices.clear();
+ d_var_sygus_types.clear();
// get the sygus variable list
Node var_list = Node::fromExpr(dt.getSygusVarList());
if (!var_list.isNull())
{
for (const Node& sv : var_list)
{
- TypeNode svt = sv.getType();
- d_var_index[sv] = d_type_vars[svt].size();
d_vars.push_back(sv);
- d_type_vars[svt].push_back(sv);
}
}
- d_rvalue_cindices.clear();
- d_rvalue_null_cindices.clear();
- d_var_sygus_types.clear();
+ // register sygus type
registerSygusType(d_ftn);
+ // Variables are associated with type ids based on the set of sygus types they
+ // appear in.
+ std::map<Node, unsigned> var_to_type_id;
+ unsigned type_id_counter = 0;
+ for (const Node& sv : d_vars)
+ {
+ TypeNode svt = sv.getType();
+ // is it equivalent to a previous variable?
+ for (const std::pair<Node, unsigned>& v : var_to_type_id)
+ {
+ Node svc = v.first;
+ if (svc.getType() == svt)
+ {
+ if (d_var_sygus_types[sv].size() == d_var_sygus_types[svc].size())
+ {
+ bool success = true;
+ for (unsigned t = 0, size = d_var_sygus_types[sv].size(); t < size;
+ t++)
+ {
+ if (d_var_sygus_types[sv][t] != d_var_sygus_types[svc][t])
+ {
+ success = false;
+ break;
+ }
+ }
+ if (success)
+ {
+ var_to_type_id[sv] = var_to_type_id[svc];
+ }
+ }
+ }
+ }
+ if (var_to_type_id.find(sv) == var_to_type_id.end())
+ {
+ var_to_type_id[sv] = type_id_counter;
+ type_id_counter++;
+ }
+ unsigned tnid = var_to_type_id[sv];
+ Trace("sygus-sample-debug")
+ << "Type id for " << sv << " is " << tnid << std::endl;
+ d_var_index[sv] = d_type_vars[tnid].size();
+ d_type_vars[tnid].push_back(sv);
+ }
+
initializeSamples(nsamples);
}
std::vector<Node> fvs;
computeFreeVariables(n, fvs);
// compute contiguous condition
- for (const std::pair<const TypeNode, std::vector<Node> >& p : d_type_vars)
+ for (const std::pair<const unsigned, std::vector<Node> >& p : d_type_vars)
{
bool foundNotFv = false;
for (const Node& v : p.second)
bool SygusSampler::isOrdered(Node n)
{
// compute free variables in n for each type
- std::map<TypeNode, std::vector<Node> > fvs;
+ std::map<unsigned, std::vector<Node> > fvs;
std::unordered_set<TNode, TNodeHashFunction> visited;
std::unordered_set<TNode, TNodeHashFunction>::iterator it;
std::map<Node, unsigned>::iterator itv = d_var_index.find(cur);
if (itv != d_var_index.end())
{
- TypeNode tn = cur.getType();
+ unsigned tnid = d_type_ids[cur];
// if this variable is out of order
- if (itv->second != fvs[tn].size())
+ if (itv->second != fvs[tnid].size())
{
return false;
}
- fvs[tn].push_back(cur);
+ fvs[tnid].push_back(cur);
}
}
for (unsigned j = 0, nchildren = cur.getNumChildren(); j < nchildren; j++)
return true;
}
-void SygusSampler::getSamplePoint(unsigned index, std::vector<Node>& pt)
+void SygusSampler::getSamplePoint(unsigned index,
+ std::vector<Node>& vars,
+ std::vector<Node>& pt)
{
Assert(index < d_samples.size());
+ vars.insert(vars.end(), d_vars.begin(), d_vars.end());
std::vector<Node>& spt = d_samples[index];
pt.insert(pt.end(), spt.begin(), spt.end());
}
return ev;
}
+int SygusSampler::getDiffSamplePointIndex(Node a, Node b)
+{
+ for (unsigned i = 0, nsamp = d_samples.size(); i < nsamp; i++)
+ {
+ Node ae = evaluate(a, i);
+ Node be = evaluate(b, i);
+ if (ae != be)
+ {
+ return i;
+ }
+ }
+ return -1;
+}
+
Node SygusSampler::getRandomValue(TypeNode tn)
{
NodeManager* nm = NodeManager::currentNM();
}
}
+Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
+{
+ Node eq_n = SygusSampler::registerTerm(n, forceKeep);
+ if (eq_n == n)
+ {
+ return n;
+ }
+ // one of eq_n or n must be ordered
+ bool eqor = isOrdered(eq_n);
+ bool nor = isOrdered(n);
+ bool isUnique = false;
+ if (eqor || nor)
+ {
+ isUnique = true;
+ // if only one is ordered, then the ordered one must contain the
+ // free variables of the other
+ if (!eqor)
+ {
+ isUnique = containsFreeVariables(n, eq_n);
+ }
+ else if (!nor)
+ {
+ isUnique = containsFreeVariables(eq_n, n);
+ }
+ }
+
+ if (isUnique)
+ {
+ // if the previous value stored was unordered, but this is
+ // ordered, we prefer this one. Thus, we force its addition to the
+ // sampler database.
+ if (!eqor)
+ {
+ registerTerm(n, true);
+ }
+ return eq_n;
+ }
+ else
+ {
+ Trace("sygus-synth-rr") << "Alpha equivalent candidate rewrite : " << eq_n
+ << " " << n << std::endl;
+ }
+ return n;
+}
+
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
* forceKeep is whether we wish to force that n is chosen as a representative
* value in the trie.
*/
- Node registerTerm(Node n, bool forceKeep = false);
+ virtual Node registerTerm(Node n, bool forceKeep = false);
+ /** get number of sample points */
+ unsigned getNumSamplePoints() const { return d_samples.size(); }
+ /** get sample point
+ *
+ * Appends sample point #index to the vector pt, d_vars to vars.
+ */
+ void getSamplePoint(unsigned index,
+ std::vector<Node>& vars,
+ std::vector<Node>& pt);
+ /** evaluate n on sample point index */
+ Node evaluate(Node n, unsigned index);
+ /**
+ * Returns the index of a sample point such that the evaluation of a and b
+ * diverge, or -1 if no such sample point exists.
+ */
+ int getDiffSamplePointIndex(Node a, Node b);
+
+ protected:
/** is contiguous
*
* This returns whether n's free variables (terms occurring in the range of
* d_type_vars) are a prefix of the list of variables in d_type_vars for each
- * type. For instance, if d_type_vars[Int] = { x, y }, then 0, x, x+y, y+x are
- * contiguous but y is not. This is useful for excluding terms from
- * consideration that are alpha-equivalent to others.
+ * type id. For instance, if d_type_vars[id] = { x, y } for some id, then
+ * 0, x, x+y, y+x are contiguous but y is not. This is useful for excluding
+ * terms from consideration that are alpha-equivalent to others.
*/
bool isContiguous(Node n);
/** is ordered
*
* This returns whether n's free variables are in order with respect to
* variables in d_type_vars for each type. For instance, if
- * d_type_vars[Int] = { x, y }, then 0, x, x+y are ordered but y and y+x
- * are not.
+ * d_type_vars[id] = { x, y } for some id, then 0, x, x+y are ordered but
+ * y and y+x are not.
*/
bool isOrdered(Node n);
/** contains free variables
* are those that occur in the range d_type_vars.
*/
bool containsFreeVariables(Node a, Node b);
- /** get number of sample points */
- unsigned getNumSamplePoints() const { return d_samples.size(); }
- /** get sample point
- *
- * Appends sample point #index to the vector pt.
- */
- void getSamplePoint(unsigned index, std::vector<Node>& pt);
- /** evaluate n on sample point index */
- Node evaluate(Node n, unsigned index);
-
private:
/** sygus term database of d_qe */
TermDbSygus* d_tds;
TypeNode d_tn;
/** the sygus type for this sampler (if applicable). */
TypeNode d_ftn;
- /** all variables */
+ /** all variables we are sampling values for */
std::vector<Node> d_vars;
/** type variables
*
- * For each type, a list of variables in the grammar we are considering, for
- * that type. These typically correspond to the arguments of the
+ * We group variables according to "type ids". Two variables have the same
+ * type id if they have indistinguishable status according to this sampler.
+ * This is a finer-grained grouping than types. For example, two variables
+ * of the same type may have different type ids if they occur as constructors
+ * of a different set of sygus types in the grammar we are considering.
+ * For instance, we assign x and y different type ids in this grammar:
+ * A -> B + C
+ * B -> x | 0 | 1
+ * C -> y
+ * Type ids are computed for each variable in d_vars during initialize(...).
+ *
+ * For each type id, a list of variables in the grammar we are considering,
+ * for that type. These typically correspond to the arguments of the
* function-to-synthesize whose grammar we are considering.
*/
- std::map<TypeNode, std::vector<Node> > d_type_vars;
+ std::map<unsigned, std::vector<Node> > d_type_vars;
/**
* A map all variables in the grammar we are considering to their index in
* d_type_vars.
*/
std::map<Node, unsigned> d_var_index;
+ /** Map from variables to the id (the domain of d_type_vars). */
+ std::map<Node, unsigned> d_type_ids;
/** constants
*
* For each type, a list of constants in the grammar we are considering, for
void registerSygusType(TypeNode tn);
};
+/** Version of the above class with some additional features */
+class SygusSamplerExt : public SygusSampler
+{
+ public:
+ /** register term n with this sampler database
+ *
+ * This returns a term ret with the same guarantees as
+ * SygusSampler::registerTerm, with the additional guarantee
+ * that for all ret' returned by a previous call to registerTerm( n' ),
+ * we have that ret = n is not alpha-equivalent to ret' = n,
+ * modulo symmetry of equality. For example,
+ * (t+0), t and (s+0), s
+ * will not be input/output pairs of this function.
+ */
+ virtual Node registerTerm(Node n, bool forceKeep = false) override;
+};
+
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
projects / cvc5.git / commitdiff