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
+option sygusSampleGrammar --sygus-sample-grammar bool :default true
+ when applicable, use grammar for choosing sample points
# CEGQI applied to general quantified formulas
option cbqi --cbqi bool :read-write :default false
#include "theory/quantifiers/sygus_sampler.h"
+#include "options/quantifiers_options.h"
#include "util/bitvector.h"
#include "util/random.h"
d_var_index[sv] = d_type_vars[svt].size();
d_type_vars[svt].push_back(sv);
}
+ d_rvalue_cindices.clear();
+ d_rvalue_null_cindices.clear();
+ d_var_sygus_types.clear();
initializeSamples(nsamples);
}
d_type_vars[svt].push_back(sv);
}
}
+ d_rvalue_cindices.clear();
+ d_rvalue_null_cindices.clear();
+ d_var_sygus_types.clear();
+ registerSygusType(d_ftn);
initializeSamples(nsamples);
}
Trace("sygus-sample") << " var #" << types.size() << " : " << v << " : "
<< vt << std::endl;
}
+ std::map<unsigned, std::map<Node, std::vector<TypeNode> >::iterator> sts;
+ if (options::sygusSampleGrammar())
+ {
+ for (unsigned j = 0, size = types.size(); j < size; j++)
+ {
+ sts[j] = d_var_sygus_types.find(d_vars[j]);
+ }
+ }
+
+ unsigned nduplicates = 0;
for (unsigned i = 0; i < nsamples; i++)
{
std::vector<Node> sample_pt;
- Trace("sygus-sample") << "Sample point #" << i << " : ";
for (unsigned j = 0, size = types.size(); j < size; j++)
{
- Node r = getRandomValue(types[j]);
+ Node v = d_vars[j];
+ Node r;
+ if (options::sygusSampleGrammar())
+ {
+ // choose a random start sygus type, if possible
+ if (sts[j] != d_var_sygus_types.end())
+ {
+ unsigned ntypes = sts[j]->second.size();
+ Assert(ntypes > 0);
+ unsigned index = Random::getRandom().pick(0, ntypes - 1);
+ if (index < ntypes)
+ {
+ // currently hard coded to 0.0, 0.5
+ r = getSygusRandomValue(sts[j]->second[index], 0.0, 0.5);
+ }
+ }
+ }
if (r.isNull())
{
- Trace("sygus-sample") << "INVALID";
- d_is_valid = false;
+ r = getRandomValue(types[j]);
+ if (r.isNull())
+ {
+ d_is_valid = false;
+ }
}
- Trace("sygus-sample") << r << " ";
sample_pt.push_back(r);
}
- Trace("sygus-sample") << std::endl;
- d_samples.push_back(sample_pt);
+ if (d_samples_trie.add(sample_pt))
+ {
+ if (Trace.isOn("sygus-sample"))
+ {
+ Trace("sygus-sample") << "Sample point #" << i << " : ";
+ for (const Node& r : sample_pt)
+ {
+ Trace("sygus-sample") << r << " ";
+ }
+ Trace("sygus-sample") << std::endl;
+ }
+ d_samples.push_back(sample_pt);
+ }
+ else
+ {
+ i--;
+ nduplicates++;
+ if (nduplicates == nsamples * 10)
+ {
+ Trace("sygus-sample")
+ << "...WARNING: excessive duplicates, cut off sampling at " << i
+ << "/" << nsamples << " points." << std::endl;
+ break;
+ }
+ }
}
d_trie.clear();
}
+bool SygusSampler::PtTrie::add(std::vector<Node>& pt)
+{
+ PtTrie* curr = this;
+ for (unsigned i = 0, size = pt.size(); i < size; i++)
+ {
+ curr = &(curr->d_children[pt[i]]);
+ }
+ bool retVal = curr->d_children.empty();
+ curr = &(curr->d_children[Node::null()]);
+ return retVal;
+}
+
Node SygusSampler::registerTerm(Node n, bool forceKeep)
{
if (d_is_valid)
return Node::null();
}
+Node SygusSampler::getSygusRandomValue(TypeNode tn,
+ double rchance,
+ double rinc,
+ unsigned depth)
+{
+ Assert(tn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+ Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end());
+ Trace("sygus-sample-grammar") << "Sygus random value " << tn
+ << ", depth = " << depth
+ << ", rchance = " << rchance << std::endl;
+ // check if we terminate on this call
+ // we refuse to enumerate terms of 10+ depth as a hard limit
+ bool terminate = Random::getRandom().pickWithProb(rchance) || depth >= 10;
+ // if we terminate, only nullary constructors can be chosen
+ std::vector<unsigned>& cindices =
+ terminate ? d_rvalue_null_cindices[tn] : d_rvalue_cindices[tn];
+ unsigned ncons = cindices.size();
+ // select a random constructor, or random value when index=ncons.
+ unsigned index = Random::getRandom().pick(0, ncons);
+ Trace("sygus-sample-grammar") << "Random index 0..." << ncons
+ << " was : " << index << std::endl;
+ if (index < ncons)
+ {
+ Trace("sygus-sample-grammar") << "Recurse constructor index #" << index
+ << std::endl;
+ unsigned cindex = cindices[index];
+ Assert(cindex < dt.getNumConstructors());
+ const DatatypeConstructor& dtc = dt[cindex];
+ // more likely to terminate in recursive calls
+ double rchance_new = rchance + (1.0 - rchance) * rinc;
+ std::map<int, Node> pre;
+ bool success = true;
+ // generate random values for all arguments
+ for (unsigned i = 0, nargs = dtc.getNumArgs(); i < nargs; i++)
+ {
+ TypeNode tnc = d_tds->getArgType(dtc, i);
+ Node c = getSygusRandomValue(tnc, rchance_new, rinc, depth + 1);
+ if (c.isNull())
+ {
+ success = false;
+ Trace("sygus-sample-grammar") << "...fail." << std::endl;
+ break;
+ }
+ Trace("sygus-sample-grammar") << " child #" << i << " : " << c
+ << std::endl;
+ pre[i] = c;
+ }
+ if (success)
+ {
+ Trace("sygus-sample-grammar") << "mkGeneric" << std::endl;
+ Node ret = d_tds->mkGeneric(dt, cindex, pre);
+ Trace("sygus-sample-grammar") << "...returned " << ret << std::endl;
+ ret = Rewriter::rewrite(ret);
+ Trace("sygus-sample-grammar") << "...after rewrite " << ret << std::endl;
+ Assert(ret.isConst());
+ return ret;
+ }
+ }
+ Trace("sygus-sample-grammar") << "...resort to random value" << std::endl;
+ // if we did not generate based on the grammar, pick a random value
+ return getRandomValue(TypeNode::fromType(dt.getSygusType()));
+}
+
+// recursion depth bounded by number of types in grammar (small)
+void SygusSampler::registerSygusType(TypeNode tn)
+{
+ if (d_rvalue_cindices.find(tn) == d_rvalue_cindices.end())
+ {
+ d_rvalue_cindices[tn].clear();
+ Assert(tn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ const DatatypeConstructor& dtc = dt[i];
+ Node sop = Node::fromExpr(dtc.getSygusOp());
+ bool isVar = std::find(d_vars.begin(), d_vars.end(), sop) != d_vars.end();
+ if (isVar)
+ {
+ // if it is a variable, add it to the list of sygus types for that var
+ d_var_sygus_types[sop].push_back(tn);
+ }
+ else
+ {
+ // otherwise, it is a constructor for sygus random value
+ d_rvalue_cindices[tn].push_back(i);
+ if (dtc.getNumArgs() == 0)
+ {
+ d_rvalue_null_cindices[tn].push_back(i);
+ }
+ }
+ // recurse on all subfields
+ for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
+ {
+ TypeNode tnc = d_tds->getArgType(dtc, j);
+ registerSygusType(tnc);
+ }
+ }
+ }
+}
+
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
TermDbSygus* d_tds;
/** samples */
std::vector<std::vector<Node> > d_samples;
+ /** data structure to check duplication of sample points */
+ class PtTrie
+ {
+ public:
+ /** add pt to this trie, returns true if pt is not a duplicate. */
+ bool add(std::vector<Node>& pt);
+
+ private:
+ /** the children of this node */
+ std::map<Node, PtTrie> d_children;
+ };
+ /** 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). */
* length, currently by a repeated coin flip.
* Real : returns the division of two random integers, where the denominator
* is omitted if it is zero.
- *
- * TODO (#1549): improve this function. Can use the grammar to generate
- * interesting sample points.
*/
Node getRandomValue(TypeNode tn);
+ /** get sygus random value
+ *
+ * Returns a random value based on the sygus type tn. The return value is
+ * a constant in the analog type of tn. This function chooses either to
+ * return a random value, or otherwise will construct a constant based on
+ * a random constructor of tn whose builtin operator is not a variable.
+ *
+ * rchance: the chance that the call to this function will be forbidden
+ * from making recursive calls and instead must return a value based on
+ * a nullary constructor of tn or based on getRandomValue above.
+ * rinc: the percentage to increment rchance on recursive calls.
+ *
+ * For example, consider the grammar:
+ * A -> x | y | 0 | 1 | +( A, A ) | ite( B, A, A )
+ * B -> A = A
+ * If we call this function on A and rchance is 0.0, there are five evenly
+ * chosen possibilities, either we return a random value via getRandomValue
+ * above, or we choose one of the four non-variable constructors of A.
+ * Say we choose ite, then we recursively call this function for
+ * B, A, and A, which return constants c1, c2, and c3. Then, this function
+ * returns the rewritten form of ite( c1, c2, c3 ).
+ * If on the other hand, rchance was 0.5 and rand() < 0.5. Then, we force
+ * this call to terminate by either selecting a random value via
+ * getRandomValue, 0 or 1.
+ */
+ Node getSygusRandomValue(TypeNode tn,
+ double rchance,
+ double rinc,
+ unsigned depth = 0);
+ /** map from sygus types to non-variable constructors */
+ std::map<TypeNode, std::vector<unsigned> > d_rvalue_cindices;
+ /** map from sygus types to non-variable nullary constructors */
+ std::map<TypeNode, std::vector<unsigned> > d_rvalue_null_cindices;
+ /** map from variables to sygus types that include them */
+ std::map<Node, std::vector<TypeNode> > d_var_sygus_types;
+ /** register sygus type, intializes the above two data structures */
+ void registerSygusType(TypeNode tn);
};
} /* CVC4::theory::quantifiers namespace */
return ret;
}
+Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
+{
+ std::map<TypeNode, int> var_count;
+ return mkGeneric(dt, c, var_count, pre);
+}
+
Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
Assert( n.getType()==tn );
Assert( tn.isDatatype() );
SygusExplain* getExplain() { return d_syexp.get(); }
/** get the extended rewrite utility */
ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
+ //-----------------------------conversion from sygus to builtin
+ /** get free variable
+ *
+ * This class caches a list of free variables for each type, which are
+ * used, for instance, for constructing canonical forms of terms with free
+ * variables. This function returns the i^th free variable for type tn.
+ * If useSygusType is true, then this function returns a variable of the
+ * analog type for sygus type tn (see d_fv for details).
+ */
+ TNode getFreeVar(TypeNode tn, int i, bool useSygusType = false);
+ /** get free variable and increment
+ *
+ * This function returns the next free variable for type tn, and increments
+ * the counter in var_count for that type.
+ */
+ TNode getFreeVarInc(TypeNode tn,
+ std::map<TypeNode, int>& var_count,
+ bool useSygusType = false);
+ /** returns true if n is a cached free variable (in d_fv). */
+ bool isFreeVar(Node n) { return d_fv_stype.find(n) != d_fv_stype.end(); }
+ /** returns the index of n in the free variable cache (d_fv). */
+ int getVarNum(Node n) { return d_fv_num[n]; }
+ /** returns true if n has a cached free variable (in d_fv). */
+ bool hasFreeVar(Node n);
+ /** make generic
+ *
+ * This function returns a builtin term f( t1, ..., tn ) where f is the
+ * builtin op of the sygus datatype constructor specified by arguments
+ * dt and c. The mapping pre maps child indices to the term for that index
+ * in the term we are constructing. That is, for each i = 1,...,n:
+ * If i is in the domain of pre, then ti = pre[i].
+ * If i is not in the domain of pre, then ti = d_fv[1][ var_count[Ti ] ],
+ * and var_count[Ti] is incremented.
+ */
+ Node mkGeneric(const Datatype& dt,
+ int c,
+ std::map<TypeNode, int>& var_count,
+ std::map<int, Node>& pre);
+ /** same as above, but with empty var_count */
+ Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre);
+ /** sygus to builtin
+ *
+ * Given a sygus datatype term n of type tn, this function returns its analog,
+ * that is, the term that n encodes.
+ */
+ Node sygusToBuiltin(Node n, TypeNode tn);
+ /** same as above, but without tn */
+ Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
+ //-----------------------------end conversion from sygus to builtin
+
private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
*/
std::map<Node, Node> d_enum_to_active_guard;
+ //-----------------------------conversion from sygus to builtin
+ /** cache for sygusToBuiltin */
+ std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
+ /** a cache of fresh variables for each type
+ *
+ * We store two versions of this list:
+ * index 0: mapping from builtin types to fresh variables of that type,
+ * index 1: mapping from sygus types to fresh varaibles of the type they
+ * encode.
+ */
+ std::map<TypeNode, std::vector<Node> > d_fv[2];
+ /** Maps free variables to the domain type they are associated with in d_fv */
+ std::map<Node, TypeNode> d_fv_stype;
+ /** Maps free variables to their index in d_fv. */
+ std::map<Node, int> d_fv_num;
+ /** recursive helper for hasFreeVar, visited stores nodes we have visited. */
+ bool hasFreeVar(Node n, std::map<Node, bool>& visited);
+ //-----------------------------end conversion from sygus to builtin
+
// TODO :issue #1235 : below here needs refactor
public:
Node d_true;
Node d_false;
- private:
- std::map< TypeNode, std::vector< Node > > d_fv[2];
- std::map< Node, TypeNode > d_fv_stype;
- std::map< Node, int > d_fv_num;
- bool hasFreeVar( Node n, std::map< Node, bool >& visited );
-public:
- TNode getFreeVar( TypeNode tn, int i, bool useSygusType = false );
- TNode getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusType = false );
- bool isFreeVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); }
- int getVarNum( Node n ) { return d_fv_num[n]; }
- bool hasFreeVar( Node n );
private:
void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
// normalized map
std::map<TypeNode, std::map<Node, Node> > d_normalized;
- std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
// grammar information
// root -> type -> _
std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
TypeNode getSygusTypeForVar( Node v );
- Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
- Node sygusToBuiltin( Node n, TypeNode tn );
- Node sygusToBuiltin( Node n ) { return sygusToBuiltin( n, n.getType() ); }
Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args );
Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
Node getNormalized(TypeNode t, Node prog);
projects / cvc5.git / commitdiff