typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node>
SygusToBuiltinVarAttribute;
+// A variant of the above attribute for cases where we introduce a fresh
+// variable. This is to support sygusToBuiltin on non-constant sygus terms,
+// where sygus variables should be mapped to canonical builtin variables.
+// It is important to cache this so that sygusToBuiltin is deterministic.
+struct BuiltinVarToSygusAttributeId
+{
+};
+typedef expr::Attribute<BuiltinVarToSygusAttributeId, Node>
+ BuiltinVarToSygusAttribute;
+
Node sygusToBuiltin(Node n, bool isExternal)
{
std::unordered_map<TNode, Node, TNodeHashFunction> visited;
SygusToBuiltinVarAttribute stbv;
cur.setAttribute(stbv, var);
visited[cur] = var;
+ // create backwards mapping
+ BuiltinVarToSygusAttribute bvtsa;
+ var.setAttribute(bvtsa, cur);
}
}
else
return visited[n];
}
+Node builtinVarToSygus(Node v)
+{
+ BuiltinVarToSygusAttribute bvtsa;
+ if (v.hasAttribute(bvtsa))
+ {
+ return v.getAttribute(bvtsa);
+ }
+ return Node::null();
+}
+
void getFreeSymbolsSygusType(TypeNode sdt,
std::unordered_set<Node, NodeHashFunction>& syms)
{
#include "theory/quantifiers/sygus/sygus_enumerator.h"
+#include "expr/node_algorithm.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "theory/datatypes/theory_datatypes_utils.h"
SygusEnumerator::SygusEnumerator(TermDbSygus* tds,
SynthConjecture* p,
- SygusStatistics& s)
- : d_tds(tds), d_parent(p), d_stats(s), d_tlEnum(nullptr), d_abortSize(-1)
+ SygusStatistics& s,
+ bool enumShapes)
+ : d_tds(tds),
+ d_parent(p),
+ d_stats(s),
+ d_enumShapes(enumShapes),
+ d_tlEnum(nullptr),
+ d_abortSize(-1)
{
}
return ret;
}
+bool SygusEnumerator::isEnumShapes() const { return d_enumShapes; }
+
SygusEnumerator::TermCache::TermCache()
: d_tds(nullptr),
d_eec(nullptr),
SygusEnumerator::TermEnumMaster::TermEnumMaster()
: TermEnum(),
+ d_enumShapes(false),
+ d_enumShapesInit(false),
d_isIncrementing(false),
d_currTermSet(false),
d_consClassNum(0),
TypeNode tn)
{
Trace("sygus-enum-debug") << "master(" << tn << "): init...\n";
+ d_tds = se->d_tds;
d_se = se;
d_tn = tn;
d_consClassNum = 0;
d_currChildSize = 0;
d_ccCons.clear();
+ d_enumShapes = se->isEnumShapes();
+ d_enumShapesInit = false;
d_isIncrementing = false;
d_currTermSet = false;
bool ret = increment();
}
children.push_back(cc);
}
+ if (d_enumShapes)
+ {
+ // ensure all variables are unique
+ childrenToShape(children);
+ }
d_currTerm = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
return d_currTerm;
}
unsigned ncc = tc.getLastConstructorClassIndexForWeight(d_currSize);
Trace("sygus-enum-debug2") << "Last constructor class " << d_currSize << ": "
<< ncc << std::endl;
+ // If we are enumerating shapes, the first enumerated term is a free variable.
+ if (d_enumShapes && !d_enumShapesInit)
+ {
+ Node fv = d_tds->getFreeVar(d_tn, 0);
+ d_enumShapesInit = true;
+ d_currTermSet = true;
+ d_currTerm = fv;
+ // must add to term cache
+ tc.addTerm(fv);
+ return true;
+ }
// have we initialized the current constructor class?
while (d_ccCons.empty() && d_consClassNum < ncc)
return true;
}
+void SygusEnumerator::TermEnumMaster::childrenToShape(
+ std::vector<Node>& children)
+{
+ if (children.size() <= 2)
+ {
+ // don't need to convert constants and unary applications
+ return;
+ }
+ std::map<TypeNode, int> vcounter;
+ // Buffered child, so that we only compute vcounter if there are more than
+ // one children with free variables, since otherwise there is no change.
+ // For example, if we are given { C, (+ x1 x2), 1 }, we buffer child (+ x1 x2)
+ // noting that it has free variables. We proceed with processing the remaining
+ // children, and note that no other child contains free variables, and hence
+ // no change is necessary (since by construction, all children have the
+ // property of having unique variable subterms). On the other hand if the
+ // last child above was x1, then this would trigger us to convert (+ x1 x2)
+ // while computing vcounter, and subsequently update x1 to x3 to obtain
+ // { C, (+ x1 x2), x3 }.
+ // Have we set the buffer child index
+ bool bufferChildSet = false;
+ // Have we processed the buffer child index
+ bool bufferChildProcessed = false;
+ // The buffer child index
+ size_t bufferChild = 0;
+ for (size_t i = 1, nchildren = children.size(); i < nchildren; i++)
+ {
+ if (!expr::hasBoundVar(children[i]))
+ {
+ // don't need to care about expressions with no bound variables
+ continue;
+ }
+ else if (!bufferChildSet)
+ {
+ bufferChild = i;
+ bufferChildSet = true;
+ continue;
+ }
+ else if (!bufferChildProcessed)
+ {
+ // process the buffer child
+ children[bufferChild] = convertShape(children[bufferChild], vcounter);
+ bufferChildProcessed = true;
+ }
+ children[i] = convertShape(children[i], vcounter);
+ }
+}
+
+Node SygusEnumerator::TermEnumMaster::convertShape(
+ Node n, std::map<TypeNode, int>& vcounter)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ if (cur.isVar())
+ {
+ // do the conversion
+ visited[cur] = d_tds->getFreeVarInc(cur.getType(), vcounter);
+ }
+ else if (!expr::hasBoundVar(cur))
+ {
+ // no bound variables, no change
+ visited[cur] = cur;
+ }
+ else
+ {
+ visited[cur] = Node::null();
+ visit.push_back(cur);
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ }
+ else if (it->second.isNull())
+ {
+ Node ret = cur;
+ bool childChanged = false;
+ std::vector<Node> children;
+ if (cur.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ children.push_back(cur.getOperator());
+ }
+ for (const Node& cn : cur)
+ {
+ it = visited.find(cn);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ childChanged = childChanged || cn != it->second;
+ children.push_back(it->second);
+ }
+ if (childChanged)
+ {
+ ret = nm->mkNode(cur.getKind(), children);
+ }
+ visited[cur] = ret;
+ }
+ } while (!visit.empty());
+ Assert(visited.find(n) != visited.end());
+ Assert(!visited.find(n)->second.isNull());
+ return visited[n];
+}
+
SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn)
: TermEnum(), d_te(tn), d_currNumConsts(0), d_nextIndexEnd(0)
{
* builtin terms (TermDb::sygusToBuiltin) can be shown to be equivalent via
* rewriting. It enumerates terms in order of sygus term size
* (TermDb::getSygusTermSize).
+ *
+ * It also can be configured to enumerates sygus terms with free variables,
+ * (as opposed to variables bound in the formal arguments list of the
+ * function-to-synthesize), where each free variable appears in exactly one
+ * subterm. For grammar:
+ * S -> 0 | 1 | x | S+S
+ * this enumerator will generate the stream:
+ * z1, C_0, C_1, C_x, C_+(z1, z2), C_+(z1, C_1), C_+(C_1, C_1) ...
+ * and so on, where z1 and z2 are variables of sygus datatype type S. We call
+ * these "shapes". This feature can be enabled by setting enumShapes to true
+ * in the constructor below.
*/
class SygusEnumerator : public EnumValGenerator
{
public:
- SygusEnumerator(TermDbSygus* tds, SynthConjecture* p, SygusStatistics& s);
+ SygusEnumerator(TermDbSygus* tds,
+ SynthConjecture* p,
+ SygusStatistics& s,
+ bool enumShapes = false);
~SygusEnumerator() {}
/** initialize this class with enumerator e */
void initialize(Node e) override;
bool increment() override;
/** Get the next concrete value generated by this class. */
Node getCurrent() override;
+ /** Are we enumerating shapes? */
+ bool isEnumShapes() const;
private:
/** pointer to term database sygus */
SynthConjecture* d_parent;
/** reference to the statistics of parent */
SygusStatistics& d_stats;
+ /** Whether we are enumerating shapes */
+ bool d_enumShapes;
/** Term cache
*
* This stores a list of terms for a given sygus type. The key features of
bool increment() override;
private:
+ /** pointer to term database sygus */
+ TermDbSygus* d_tds;
+ /** are we enumerating shapes? */
+ bool d_enumShapes;
+ /** have we initialized the shape enumeration? */
+ bool d_enumShapesInit;
/** are we currently inside a increment() call? */
bool d_isIncrementing;
/** cache for getCurrent() */
bool initializeChild(unsigned i, unsigned sizeMin);
/** increment internal, helper for increment() */
bool incrementInternal();
+ /**
+ * The vector children is a set of terms given to
+ * NodeManager::mkNode(APPLY_CONSTRUCTOR, children)
+ * This converts children so that all sygus free variables are unique. Note
+ * that the first child is a constructor operator and should be skipped.
+ */
+ void childrenToShape(std::vector<Node>& children);
+ /**
+ * Convert n into shape based on the variable counters. For example if
+ * vcounter is { Int -> 7 }, then (+ x1 x2) is converted to (+ x7 x8) and
+ * vouncter is updated to { Int -> 9 }.
+ */
+ Node convertShape(Node n, std::map<TypeNode, int>& vcounter);
};
/** an interpreted value enumerator
*
projects / cvc5.git / commitdiff