}
}else{
// no arguments to synthesis functions
+ d_var_list[tn].clear();
}
// register connected types
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
}
}
+/** A trie indexed by types that assigns unique identifiers to nodes. */
+class TypeNodeIdTrie
+{
+ public:
+ /** children of this node */
+ std::map<TypeNode, TypeNodeIdTrie> d_children;
+ /** the data stored at this node */
+ std::vector<Node> d_data;
+ /** add v to this trie, indexed by types */
+ void add(Node v, std::vector<TypeNode>& types)
+ {
+ TypeNodeIdTrie* tnt = this;
+ for (unsigned i = 0, size = types.size(); i < size; i++)
+ {
+ tnt = &tnt->d_children[types[i]];
+ }
+ tnt->d_data.push_back(v);
+ }
+ /**
+ * Assign each node in this trie an identifier such that
+ * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values.
+ */
+ void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount)
+ {
+ if (!d_data.empty())
+ {
+ for (const Node& v : d_data)
+ {
+ assign[v] = idCount;
+ }
+ idCount++;
+ }
+ for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children)
+ {
+ c.second.assignIds(assign, idCount);
+ }
+ }
+};
+
void TermDbSygus::registerEnumerator(Node e,
Node f,
SynthConjecture* conj,
bool mkActiveGuard,
- bool useSymbolicCons)
+ bool useSymbolicCons,
+ bool isVarAgnostic)
{
if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
{
NodeManager* nm = NodeManager::currentNM();
if( mkActiveGuard ){
// make the guard
- Node eg = Rewriter::rewrite(nm->mkSkolem("eG", nm->booleanType()));
- eg = d_quantEngine->getValuation().ensureLiteral( eg );
- AlwaysAssert( !eg.isNull() );
- d_quantEngine->getOutputChannel().requirePhase( eg, true );
- //add immediate lemma
- Node lem = nm->mkNode(OR, eg, eg.negate());
- Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl;
- d_quantEngine->getOutputChannel().lemma( lem );
- d_enum_to_active_guard[e] = eg;
+ d_enum_to_active_guard[e] = nm->mkSkolem("eG", nm->booleanType());
}
Trace("sygus-db") << " registering symmetry breaking clauses..."
// breaking lemma templates for each relevant subtype of the grammar
std::vector<TypeNode> sf_types;
getSubfieldTypes(et, sf_types);
+ // maps variables to the list of subfield types they occur in
+ std::map<Node, std::vector<TypeNode> > type_occurs;
+ std::map<TypeNode, std::vector<Node> >::iterator itv = d_var_list.find(et);
+ Assert(itv != d_var_list.end());
+ for (const Node& v : itv->second)
+ {
+ type_occurs[v].clear();
+ }
// for each type of subfield type of this enumerator
for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
{
std::vector<unsigned> rm_indices;
TypeNode stn = sf_types[i];
Assert(stn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(stn.toType()).getDatatype();
- std::map<TypeNode, unsigned>::iterator itsa =
- d_sym_cons_any_constant.find(stn);
- if (itsa != d_sym_cons_any_constant.end())
+ const Datatype& dt = stn.getDatatype();
+ int anyC = getAnyConstantConsNum(stn);
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
- if (!useSymbolicCons)
+ Expr sop = dt[i].getSygusOp();
+ Assert(!sop.isNull());
+ bool isAnyC = static_cast<int>(i) == anyC;
+ Node sopn = Node::fromExpr(sop);
+ if (type_occurs.find(sopn) != type_occurs.end())
+ {
+ // if it is a variable, store that it occurs in stn
+ type_occurs[sopn].push_back(stn);
+ }
+ else if (isAnyC && !useSymbolicCons)
{
+ // if we are not using the any constant constructor
// do not use the symbolic constructor
- rm_indices.push_back(itsa->second);
+ rm_indices.push_back(i);
}
- else
+ else if (anyC != -1 && !isAnyC && useSymbolicCons)
{
- // can remove all other concrete constant constructors
- for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ // if we are using the any constant constructor, do not use any
+ // concrete constant
+ Node c_op = getConsNumConst(stn, i);
+ if (!c_op.isNull())
{
- if (i != itsa->second)
- {
- Node c_op = getConsNumConst(stn, i);
- if (!c_op.isNull())
- {
- rm_indices.push_back(i);
- }
- }
+ rm_indices.push_back(i);
}
}
}
}
}
Trace("sygus-db") << " ...finished" << std::endl;
+
+ d_enum_var_agnostic[e] = isVarAgnostic;
+ if (isVarAgnostic)
+ {
+ // if not done so already, compute type class identifiers for each variable
+ if (d_var_subclass_id.find(et) == d_var_subclass_id.end())
+ {
+ d_var_subclass_id[et].clear();
+ TypeNodeIdTrie tnit;
+ for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
+ {
+ tnit.add(to.first, to.second);
+ }
+ // 0 is reserved for "no type class id"
+ unsigned typeIdCount = 1;
+ tnit.assignIds(d_var_subclass_id[et], typeIdCount);
+ // assign the list and reverse map to index
+ for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
+ {
+ Node v = to.first;
+ unsigned sc = d_var_subclass_id[et][v];
+ Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
+ d_var_subclass_list_index[et][v] = d_var_subclass_list[et][sc].size();
+ d_var_subclass_list[et][sc].push_back(v);
+ }
+ }
+ }
}
bool TermDbSygus::isEnumerator(Node e) const
return false;
}
+bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const
+{
+ std::map<Node, bool>::const_iterator itus = d_enum_var_agnostic.find(e);
+ if (itus != d_enum_var_agnostic.end())
+ {
+ return itus->second;
+ }
+ return false;
+}
+
void TermDbSygus::getEnumerators(std::vector<Node>& mts)
{
for (std::map<Node, SynthConjecture*>::iterator itm =
return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end();
}
+unsigned TermDbSygus::getSubclassForVar(TypeNode tn, Node n) const
+{
+ std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itc =
+ d_var_subclass_id.find(tn);
+ if (itc == d_var_subclass_id.end())
+ {
+ Assert(false);
+ return 0;
+ }
+ std::map<Node, unsigned>::const_iterator itcc = itc->second.find(n);
+ if (itcc == itc->second.end())
+ {
+ Assert(false);
+ return 0;
+ }
+ return itcc->second;
+}
+
+unsigned TermDbSygus::getNumSubclassVars(TypeNode tn, unsigned sc) const
+{
+ std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
+ itv = d_var_subclass_list.find(tn);
+ if (itv == d_var_subclass_list.end())
+ {
+ Assert(false);
+ return 0;
+ }
+ std::map<unsigned, std::vector<Node> >::const_iterator itvv =
+ itv->second.find(sc);
+ if (itvv == itv->second.end())
+ {
+ Assert(false);
+ return 0;
+ }
+ return itvv->second.size();
+}
+Node TermDbSygus::getVarSubclassIndex(TypeNode tn,
+ unsigned sc,
+ unsigned i) const
+{
+ std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
+ itv = d_var_subclass_list.find(tn);
+ if (itv == d_var_subclass_list.end())
+ {
+ Assert(false);
+ return Node::null();
+ }
+ std::map<unsigned, std::vector<Node> >::const_iterator itvv =
+ itv->second.find(sc);
+ if (itvv == itv->second.end() || i >= itvv->second.size())
+ {
+ Assert(false);
+ return Node::null();
+ }
+ return itvv->second[i];
+}
+
+bool TermDbSygus::getIndexInSubclassForVar(TypeNode tn,
+ Node v,
+ unsigned& index) const
+{
+ std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itv =
+ d_var_subclass_list_index.find(tn);
+ if (itv == d_var_subclass_list_index.end())
+ {
+ return false;
+ }
+ std::map<Node, unsigned>::const_iterator itvv = itv->second.find(v);
+ if (itvv == itv->second.end())
+ {
+ return false;
+ }
+ index = itvv->second;
+ return true;
+}
+
bool TermDbSygus::isSymbolicConsApp(Node n) const
{
if (n.getKind() != APPLY_CONSTRUCTOR)
* (see d_enum_to_active_guard),
* useSymbolicCons : whether we want model values for e to include symbolic
* constructors like the "any constant" variable.
+ * isVarAgnostic : if this flag is true, the enumerator will only generate
+ * values whose variables are in canonical order (for example, only x1-x2
+ * and not x2-x1 will be generated, assuming x1 and x2 are in the same
+ * "subclass", see getSubclassForVar).
*
* Notice that enumerator e may not be one-to-one with f in
* synthesis-through-unification approaches (e.g. decision tree construction
Node f,
SynthConjecture* conj,
bool mkActiveGuard = false,
- bool useSymbolicCons = false);
+ bool useSymbolicCons = false,
+ bool isVarAgnostic = false);
/** is e an enumerator registered with this class? */
bool isEnumerator(Node e) const;
/** return the conjecture e is associated with */
Node getActiveGuardForEnumerator(Node e) const;
/** are we using symbolic constructors for enumerator e? */
bool usingSymbolicConsForEnumerator(Node e) const;
+ /** is this enumerator agnostic to variables? */
+ bool isVariableAgnosticEnumerator(Node e) const;
/** get all registered enumerators */
void getEnumerators(std::vector<Node>& mts);
/** Register symmetry breaking lemma
std::map<Node, TypeNode> d_sb_lemma_to_type;
/** mapping from symmetry breaking lemmas to size */
std::map<Node, unsigned> d_sb_lemma_to_size;
+ /** enumerators to whether they are variable agnostic */
+ std::map<Node, bool> d_enum_var_agnostic;
//------------------------------end enumerators
//-----------------------------conversion from sygus to builtin
* for this type.
*/
std::map<TypeNode, bool> d_has_subterm_sym_cons;
+ /**
+ * Map from sygus types and bound variables to their type subclass id. Note
+ * type class identifiers are computed for each type of registered sygus
+ * enumerators, but not all sygus types. For details, see getSubclassIdForVar.
+ */
+ std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_id;
+ /** the list of variables with given subclass */
+ std::map<TypeNode, std::map<unsigned, std::vector<Node> > >
+ d_var_subclass_list;
+ /** the index of each variable in the above list */
+ std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_list_index;
public: // general sygus utilities
bool isRegistered(TypeNode tn) const;
* Returns true if any subterm of type tn can be a symbolic constructor.
*/
bool hasSubtermSymbolicCons(TypeNode tn) const;
+ //--------------------------------- variable subclasses
+ /** Get subclass id for variable
+ *
+ * This returns the "subclass" identifier for variable v in sygus
+ * type tn. A subclass identifier groups variables based on the sygus
+ * types they occur in:
+ * A -> A + B | C + C | x | y | z | w | u
+ * B -> y | z
+ * C -> u
+ * The variables in this grammar can be grouped according to the sygus types
+ * they appear in:
+ * { x,w } occur in A
+ * { y,z } occur in A,B
+ * { u } occurs in A,C
+ * We say that e.g. x, w are in the same subclass.
+ *
+ * If this method returns 0, then v is not a variable in sygus type tn.
+ * Otherwise, this method returns a positive value n, such that
+ * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
+ * same subclass.
+ *
+ * The type tn should be the type of an enumerator registered to this
+ * database, where notice that we do not compute this information for the
+ * subfield types of the enumerator.
+ */
+ unsigned getSubclassForVar(TypeNode tn, Node v) const;
+ /**
+ * Get the number of variable in the subclass with identifier sc for type tn.
+ */
+ unsigned getNumSubclassVars(TypeNode tn, unsigned sc) const;
+ /** Get the i^th variable in the subclass with identifier sc for type tn */
+ Node getVarSubclassIndex(TypeNode tn, unsigned sc, unsigned i) const;
+ /**
+ * Get the a variable's index in its subclass list. This method returns true
+ * iff variable v has been assigned a subclass in tn. It updates index to
+ * be v's index iff the method returns true.
+ */
+ bool getIndexInSubclassForVar(TypeNode tn, Node v, unsigned& index) const;
+ //--------------------------------- end variable subclasses
/** return whether n is an application of a symbolic constructor */
bool isSymbolicConsApp(Node n) const;
/** can construct kind
projects / cvc5.git / commitdiff