#include "expr/datatype.h"
#include "options/quantifiers_options.h"
+#include "printer/sygus_print_callback.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/ce_guided_conjecture.h"
#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
+#include <numeric> // for std::iota
+
using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
namespace quantifiers {
-TypeObject::TypeObject(std::string type_name) : d_dt(Datatype(type_name))
+bool OpPosTrie::getOrMakeType(TypeNode tn,
+ TypeNode& unres_tn,
+ std::vector<unsigned> op_pos,
+ unsigned ind)
{
- d_tn = TypeNode::null();
- /* Create an unresolved type */
- d_unres_t = NodeManager::currentNM()
- ->mkSort(type_name, ExprManager::SORT_FLAG_PLACEHOLDER)
- .toType();
+ if (ind == op_pos.size())
+ {
+ /* Found type */
+ if (!d_unres_tn.isNull())
+ {
+ Trace("sygus-grammar-normalize-trie")
+ << "\tFound type " << d_unres_tn << "\n";
+ unres_tn = d_unres_tn;
+ return true;
+ }
+ /* Creating unresolved type */
+ std::stringstream ss;
+ ss << tn << "_";
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+ {
+ ss << "_" << std::to_string(op_pos[i]);
+ }
+ d_unres_tn = NodeManager::currentNM()->mkSort(
+ ss.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
+ Trace("sygus-grammar-normalize-trie")
+ << "\tCreating type " << d_unres_tn << "\n";
+ unres_tn = d_unres_tn;
+ return false;
+ }
+ /* Go to next node */
+ return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
}
-TypeObject::TypeObject(TypeNode src_tn, std::string type_name)
- : d_dt(Datatype(type_name))
+void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm,
+ const DatatypeConstructor& cons)
{
- d_tn = src_tn;
- d_t = src_tn.toType();
- /* Create an unresolved type */
- d_unres_t = NodeManager::currentNM()
- ->mkSort(type_name, ExprManager::SORT_FLAG_PLACEHOLDER)
- .toType();
+ Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n";
+ /* Recover the sygus operator to not lose reference to the original
+ * operator (NOT, ITE, etc) */
+ Node exp_sop_n = Node::fromExpr(
+ smt::currentSmtEngine()->expandDefinitions(cons.getSygusOp()));
+ d_ops.push_back(Rewriter::rewrite(exp_sop_n));
+ Trace("sygus-grammar-normalize-defs")
+ << "\tOriginal op: " << cons.getSygusOp()
+ << "\n\tExpanded one: " << exp_sop_n
+ << "\n\tRewritten one: " << d_ops.back() << "\n\n";
+ d_cons_names.push_back(cons.getName());
+ d_pc.push_back(cons.getSygusPrintCallback());
+ d_weight.push_back(cons.getWeight());
+ d_cons_args_t.push_back(std::vector<Type>());
+ for (const DatatypeConstructorArg& arg : cons)
+ {
+ /* Collect unresolved type nodes corresponding to the typenode of the
+ * arguments */
+ d_cons_args_t.back().push_back(
+ sygus_norm
+ ->normalizeSygusRec(TypeNode::fromType(
+ static_cast<SelectorType>(arg.getType()).getRangeType()))
+ .toType());
+ }
+}
+
+void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
+ const Datatype& dt)
+{
+ /* Use the sygus type to not lose reference to the original types (Bool,
+ * Int, etc) */
+ d_dt.setSygus(dt.getSygusType(),
+ sygus_norm->d_sygus_vars.toExpr(),
+ dt.getSygusAllowConst(),
+ dt.getSygusAllowAll());
+ for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
+ {
+ d_dt.addSygusConstructor(d_ops[i].toExpr(),
+ d_cons_names[i],
+ d_cons_args_t[i],
+ d_pc[i],
+ d_weight[i]);
+ }
+ Trace("sygus-grammar-normalize") << "...built datatype " << d_dt << " ";
+ /* Add to global accumulators */
+ sygus_norm->d_dt_all.push_back(d_dt);
+ sygus_norm->d_unres_t_all.insert(d_unres_tn.toType());
+ Trace("sygus-grammar-normalize") << "---------------------------------\n";
+}
+
+/* TODO #1304: have more operators and types. Moreover, have more general ways
+ of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
+ function should realize that it is chainable for integers */
+bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn, Node op)
+{
+ /* Checks whether operator occurs chainable for its type */
+ if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS)
+ {
+ return true;
+ }
+ return false;
}
-SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe, CegConjecture* p)
- : d_qe(qe), d_parent(p), d_tds(d_qe->getTermDatabaseSygus())
+/* TODO #1304: have more operators and types. Moreover, have more general ways
+ of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
+ function should realize that it is chainable for integers */
+bool SygusGrammarNorm::TransfChain::isId(TypeNode tn, Node op, Node n)
{
+ if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS
+ && n == TermUtil::mkTypeValue(tn, 0))
+ {
+ return true;
+ }
+ return false;
}
-/* recursion depth is limited by the height of the types, which is small */
-void SygusGrammarNorm::collectInfoFor(TypeNode tn,
- std::vector<TypeObject>& tos,
- std::map<TypeNode, Type>& tn_to_unres,
- std::map<TypeNode, bool>& visited)
+void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm,
+ TypeObject& to,
+ const Datatype& dt,
+ std::vector<unsigned>& op_pos)
{
- if (visited.find(tn) != visited.end())
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<unsigned> claimed(d_elem_pos);
+ claimed.push_back(d_chain_op_pos);
+ unsigned nb_op_pos = op_pos.size();
+ /* TODO do this properly */
+ /* Remove from op_pos the positions claimed by the transformation */
+ std::sort(op_pos.begin(), op_pos.end());
+ std::sort(claimed.begin(), claimed.end());
+ std::vector<unsigned> difference;
+ std::set_difference(op_pos.begin(),
+ op_pos.end(),
+ claimed.begin(),
+ claimed.end(),
+ std::back_inserter(difference));
+ op_pos = difference;
+ if (Trace.isOn("sygus-grammar-normalize-chain"))
+ {
+ Trace("sygus-grammar-normalize-chain")
+ << "OP at " << d_chain_op_pos << "\n"
+ << d_elem_pos.size() << " d_elem_pos: ";
+ for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i)
+ {
+ Trace("sygus-grammar-normalize-chain") << d_elem_pos[i] << " ";
+ }
+ Trace("sygus-grammar-normalize-chain")
+ << "\n"
+ << op_pos.size() << " remaining op_pos: ";
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+ {
+ Trace("sygus-grammar-normalize-chain") << op_pos[i] << " ";
+ }
+ Trace("sygus-grammar-normalize-chain") << "\n";
+ }
+ /* Build identity operator and empty callback */
+ Node iden_op =
+ SygusGrammarNorm::getIdOp(TypeNode::fromType(dt.getSygusType()));
+ /* If all operators are claimed, create a monomial */
+ if (nb_op_pos == d_elem_pos.size() + 1)
+ {
+ Trace("sygus-grammar-normalize-chain")
+ << "\tCreating id type for " << d_elem_pos.back() << "\n";
+ /* creates type for element */
+ std::vector<unsigned> tmp;
+ tmp.push_back(d_elem_pos.back());
+ Type t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp).toType();
+ /* consumes element */
+ d_elem_pos.pop_back();
+ /* adds to Root: "type" */
+ to.d_ops.push_back(iden_op);
+ to.d_cons_names.push_back("id");
+ to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
+ /* Identity operators should not increase the size of terms */
+ to.d_weight.push_back(0);
+ to.d_cons_args_t.push_back(std::vector<Type>());
+ to.d_cons_args_t.back().push_back(t);
+ Trace("sygus-grammar-normalize-chain")
+ << "\tAdding " << t << " to " << to.d_unres_tn << "\n";
+ /* adds to Root: "type + Root" */
+ to.d_ops.push_back(nm->operatorOf(PLUS));
+ to.d_cons_names.push_back(kindToString(PLUS));
+ to.d_pc.push_back(nullptr);
+ to.d_weight.push_back(-1);
+ to.d_cons_args_t.push_back(std::vector<Type>());
+ to.d_cons_args_t.back().push_back(t);
+ to.d_cons_args_t.back().push_back(to.d_unres_tn.toType());
+ Trace("sygus-grammar-normalize-chain")
+ << "\tAdding PLUS to " << to.d_unres_tn << " with arg types "
+ << to.d_unres_tn << " and " << t << "\n";
+ }
+ /* In the initial case if not all operators claimed always creates a next */
+ Assert(nb_op_pos != d_elem_pos.size() + 1 || d_elem_pos.size() > 1);
+ /* TODO #1304: consider case in which CHAIN op has different types than
+ to.d_tn */
+ /* If no more elements to chain, finish */
+ if (d_elem_pos.size() == 0)
{
return;
}
- visited[tn] = true;
- Assert(tn.isDatatype());
- /* Create new type name */
- std::stringstream ss;
- ss << tn << "_norm";
- std::string type_name = ss.str();
- /* Add to global accumulators */
- tos.push_back(TypeObject(tn, type_name));
- const Datatype& dt = static_cast<DatatypeType>(tos.back().d_t).getDatatype();
- tn_to_unres[tn] = tos.back().d_unres_t;
- /* Visit types of constructor arguments */
- for (const DatatypeConstructor& cons : dt)
+ /* Creates a type do be added to root representing next step in the chain */
+ /* Add + to elems */
+ d_elem_pos.push_back(d_chain_op_pos);
+ if (Trace.isOn("sygus-grammar-normalize-chain"))
{
- for (const DatatypeConstructorArg& arg : cons)
+ Trace("sygus-grammar-normalize-chain")
+ << "\tCreating type for next entry with sygus_ops ";
+ for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i)
{
- collectInfoFor(
- TypeNode::fromType(
- static_cast<SelectorType>(arg.getType()).getRangeType()),
- tos,
- tn_to_unres,
- visited);
+ Trace("sygus-grammar-normalize-chain")
+ << dt[d_elem_pos[i]].getSygusOp() << " ";
}
+ Trace("sygus-grammar-normalize-chain") << "\n";
}
+ /* adds to Root: (\lambda x. x ) Next */
+ to.d_ops.push_back(iden_op);
+ to.d_cons_names.push_back("id_next");
+ to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
+ to.d_weight.push_back(0);
+ to.d_cons_args_t.push_back(std::vector<Type>());
+ to.d_cons_args_t.back().push_back(
+ sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos).toType());
}
-void SygusGrammarNorm::normalizeSygusInt(unsigned ind,
- std::vector<TypeObject>& tos,
- std::map<TypeNode, Type>& tn_to_unres,
- Node sygus_vars)
+std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {};
+
+/* Traverse the constructors of dt according to the positions in op_pos. Collect
+ * those that fit the kinds established by to_collect. Remove collected operator
+ * positions from op_pos. Accumulate collected positions in collected
+ *
+ * returns true if collected anything
+ */
+SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf(
+ TypeNode tn, const Datatype& dt, const std::vector<unsigned>& op_pos)
{
- const Datatype& dt =
- static_cast<DatatypeType>(tos[ind].d_t).getDatatype();
- Trace("sygus-grammar-normalize")
- << "Normalizing integer type " << tos[ind].d_tn << " from datatype\n"
- << dt << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
+ TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
+ /* TODO #1304: step 0: look for redundant constructors to drop */
+ /* TODO #1304: step 1: look for singleton */
+ /* step 2: look for chain */
+ unsigned chain_op_pos = dt.getNumConstructors();
+ std::vector<unsigned> elem_pos;
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+ {
+ Assert(op_pos[i] < dt.getNumConstructors());
+ Expr sop = dt[op_pos[i]].getSygusOp();
+ /* Collects a chainable operator such as PLUS */
+ if (sop.getKind() == BUILTIN
+ && TransfChain::isChainable(sygus_tn, Node::fromExpr(sop)))
+ {
+ Assert(nm->operatorToKind(Node::fromExpr(sop)) == PLUS);
+ /* TODO #1304: be robust for this case */
+ /* For now only transforms applications whose arguments have the same type
+ * as the root */
+ bool same_type_plus = true;
+ for (const DatatypeConstructorArg& arg : dt[op_pos[i]])
+ {
+ if (TypeNode::fromType(
+ static_cast<SelectorType>(arg.getType()).getRangeType())
+ != tn)
+ {
+ same_type_plus = false;
+ break;
+ }
+ }
+ if (!same_type_plus)
+ {
+ Trace("sygus-grammar-normalize-infer")
+ << "\tFor OP " << PLUS << " did not collecting sop " << sop
+ << " in position " << op_pos[i] << "\n";
+ continue;
+ }
+ Assert(chain_op_pos == dt.getNumConstructors());
+ Trace("sygus-grammar-normalize-infer")
+ << "\tCollecting chainable OP " << sop << " in position " << op_pos[i]
+ << "\n";
+ chain_op_pos = op_pos[i];
+ continue;
+ }
+ /* TODO #1304: check this for each operator */
+ /* Collects elements that are not the identity (e.g. 0 is the id of PLUS) */
+ if (!TransfChain::isId(sygus_tn, nm->operatorOf(PLUS), Node::fromExpr(sop)))
+ {
+ Trace("sygus-grammar-normalize-infer")
+ << "\tCollecting for NON_ID_ELEMS the sop " << sop
+ << " in position " << op_pos[i] << "\n";
+ elem_pos.push_back(op_pos[i]);
+ }
+ }
+ /* Typenode admits a chain transformation for normalization */
+ if (chain_op_pos != dt.getNumConstructors() && !elem_pos.empty())
+ {
+ Trace("sygus-grammar-normalize-infer")
+ << "\tInfering chain transformation\n";
+ return new TransfChain(chain_op_pos, elem_pos);
+ }
+ return nullptr;
}
-TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
+TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
+ const Datatype& dt,
+ std::vector<unsigned>& op_pos)
{
- /* Make int_type and zero */
- NodeManager* nm = NodeManager::currentNM();
- /* Accumulates all typing information for normalization and reconstruction */
- std::vector<TypeObject> tos;
- /* Allows retrieving respective unresolved types for the sygus types of the
- * original type nodes */
- std::map<TypeNode, Type> tn_to_unres;
- std::map<TypeNode, bool> visited;
- collectInfoFor(tn, tos, tn_to_unres, visited);
- /* Build datatypes TODO and normalize accordingly #1304 */
- for (unsigned i = 0, size = tos.size(); i < size; ++i)
- {
- const Datatype& dt =
- static_cast<DatatypeType>(tos[i].d_t).getDatatype();
- Trace("sygus-grammar-normalize")
- << "Rebuild " << tos[i].d_tn << " from " << dt << std::endl;
- /* Collect information to rebuild constructors */
- for (const DatatypeConstructor& cons : dt)
+ /* Corresponding type node to tn with the given operator positions. To be
+ * retrieved (if cached) or defined (otherwise) */
+ TypeNode unres_tn;
+ if (Trace.isOn("sygus-grammar-normalize-trie"))
+ {
+ Trace("sygus-grammar-normalize-trie")
+ << "\tRecursing on " << tn << " with op_positions ";
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+ {
+ Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
+ }
+ Trace("sygus-grammar-normalize-trie") << "\n";
+ }
+ /* Checks if unresolved type already created (and returns) or creates it
+ * (and then proceeds to definition) */
+ std::sort(op_pos.begin(), op_pos.end());
+ if (d_tries[tn].getOrMakeType(tn, unres_tn, op_pos))
+ {
+ if (Trace.isOn("sygus-grammar-normalize-trie"))
{
- Trace("sygus-grammar-normalize")
- << "...for " << cons.getName() << std::endl;
- /* Recover the sygus operator to not lose reference to the original
- * operator (NOT, ITE, etc) */
- Node exp_sop_n = Node::fromExpr(
- smt::currentSmtEngine()->expandDefinitions(cons.getSygusOp()));
- tos[i].d_ops.push_back(Rewriter::rewrite(exp_sop_n));
- Trace("sygus-grammar-normalize")
- << "\tOriginal op: " << cons.getSygusOp()
- << "\n\tExpanded one: " << exp_sop_n
- << "\n\tRewritten one: " << tos[i].d_ops.back() << std::endl;
- tos[i].d_cons_names.push_back(cons.getName());
- tos[i].d_pcb.push_back(cons.getSygusPrintCallback());
- tos[i].d_cons_args_t.push_back(std::vector<Type>());
- for (const DatatypeConstructorArg& arg : cons)
+ Trace("sygus-grammar-normalize-trie")
+ << "\tTypenode " << tn << " has already been normalized with op_pos ";
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
{
- /* Collect unresolved types corresponding to the typenode of the
- * arguments */
- tos[i].d_cons_args_t.back().push_back(tn_to_unres[TypeNode::fromType(
- static_cast<SelectorType>(arg.getType()).getRangeType())]);
+ Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
}
+ Trace("sygus-grammar-normalize-trie") << " with tn " << unres_tn << "\n";
+ }
+ return unres_tn;
+ }
+ if (Trace.isOn("sygus-grammar-normalize-trie"))
+ {
+ Trace("sygus-grammar-normalize-trie")
+ << "\tTypenode " << tn << " not yet normalized with op_pos ";
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+ {
+ Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
}
- /* Use the sygus type to not lose reference to the original types (Bool,
- * Int, etc) */
- tos[i].d_dt.setSygus(dt.getSygusType(),
- sygus_vars.toExpr(),
- dt.getSygusAllowConst(),
- dt.getSygusAllowAll());
- for (unsigned j = 0, size_d_ops = tos[i].d_ops.size(); j < size_d_ops; ++j)
+ Trace("sygus-grammar-normalize-trie") << "\n";
+ }
+ /* Creates type object for normalization */
+ TypeObject to(tn, unres_tn);
+ /* If normalization option enabled, infer transformations to be applied in the
+ * type */
+ if (options::sygusGrammarNorm())
+ {
+ /* Determine normalization transformation based on sygus type and given
+ * operators */
+ Transf* transformation = inferTransf(tn, dt, op_pos);
+ /* If a transformation was selected, apply it */
+ if (transformation != nullptr)
{
- tos[i].d_dt.addSygusConstructor(tos[i].d_ops[j].toExpr(),
- tos[i].d_cons_names[j],
- tos[i].d_cons_args_t[j],
- tos[i].d_pcb[j]);
+ transformation->buildType(this, to, dt, op_pos);
}
- Trace("sygus-grammar-normalize")
- << "...built datatype " << tos[i].d_dt << std::endl;
}
- /* Resolve types */
- std::vector<Datatype> dts;
- std::set<Type> unres_all;
- for (TypeObject& to : tos)
+ /* Remaining operators are rebuilt as they are */
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
{
- dts.push_back(to.d_dt);
- unres_all.insert(to.d_unres_t);
+ Assert(op_pos[i] < dt.getNumConstructors());
+ to.addConsInfo(this, dt[op_pos[i]]);
+ }
+ /* Build normalize datatype */
+ if (Trace.isOn("sygus-grammar-normalize"))
+ {
+ Trace("sygus-grammar-normalize") << "\nFor positions ";
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+ {
+ Trace("sygus-grammar-normalize") << op_pos[i] << " ";
+ }
+ Trace("sygus-grammar-normalize") << " and datatype " << dt << " \n";
+ }
+ to.buildDatatype(this, dt);
+ return to.d_unres_tn;
+}
+
+TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
+{
+ /* Collect all operators for normalization */
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ std::vector<unsigned> op_pos(dt.getNumConstructors());
+ std::iota(op_pos.begin(), op_pos.end(), 0);
+ return normalizeSygusRec(tn, dt, op_pos);
+}
+
+TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
+{
+ /* Normalize all types in tn */
+ d_sygus_vars = sygus_vars;
+ normalizeSygusRec(tn);
+ /* Resolve created types */
+ Assert(!d_dt_all.empty() && !d_unres_t_all.empty());
+ if (Trace.isOn("sygus-grammar-normalize-build"))
+ {
+ Trace("sygus-grammar-normalize-build")
+ << "making mutual datatyes with datatypes \n";
+ for (unsigned i = 0, size = d_dt_all.size(); i < size; ++i)
+ {
+ Trace("sygus-grammar-normalize-build") << d_dt_all[i];
+ }
+ Trace("sygus-grammar-normalize-build") << " and unresolved types\n";
+ for (const Type& unres_t : d_unres_t_all)
+ {
+ Trace("sygus-grammar-normalize-build") << unres_t << " ";
+ }
+ Trace("sygus-grammar-normalize-build") << "\n";
}
+ Assert(d_dt_all.size() == d_unres_t_all.size());
std::vector<DatatypeType> types =
- nm->toExprManager()->mkMutualDatatypeTypes(dts, unres_all);
- Assert(types.size() == dts.size());
- /* By construction the normalized type node will be first one considered */
- return TypeNode::fromType(types[0]);
+ NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
+ d_dt_all, d_unres_t_all);
+ Assert(types.size() == d_dt_all.size());
+ /* Clear accumulators */
+ d_dt_all.clear();
+ d_unres_t_all.clear();
+ /* By construction the normalized type node will be the last one considered */
+ return TypeNode::fromType(types.back());
}
} // namespace quantifiers
**/
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_SIMP_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_SIMP_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#include "expr/node_manager_attributes.h" // for VarNameAttr
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
-class CegConjecture;
+class SygusGrammarNorm;
-/** Keeps the necessary information about a sygus type:
+/** Operator position trie class
*
- * the original typenode, from which the datatype representation can be
- * extracted
+ * This data structure stores an unresolved type corresponding to the
+ * normalization of a type. This unresolved type is indexed by the positions of
+ * the construtors of the datatype associated with the original type. The list
+ * of positions represent the operators, associated with the respective
+ * considered constructors, that were used for building the unresolved type.
*
- * the operators, names and argument types for each constructor
+ * Example:
*
- * the unresolved type used as placeholder for references of the yet to be built
- * type
+ * Let A be a type defined by the grammar "A -> x | 0 | 1 | A + A". In its
+ * datatype representation the operator for "x" is in position 0, for "0" in
+ * position "1" and so on. Consider entries (T, [op_1, ..., op_n]) -> T' to
+ * represent that a type T is normalized with operators [op_1, ..., op_n] into
+ * the type T'. For entries
*
- * a datatype to represent the structure of the typenode for the new type */
-struct TypeObject
+ * (A, [x, 0, 1, +]) -> A1
+ * (A, [x, 1, +]) -> A2
+ * (A, [1, +]) -> A3
+ * (A, [0]) -> AZ
+ * (A, [x]) -> AX
+ * (A, [1]) -> AO
+ *
+ * the OpPosTrie T we build for this type is :
+ *
+ * T[A] :
+ * T[A].d_children[0] : AX
+ * T[A].d_children[0].d_children[1] :
+ * T[A].d_children[0].d_children[1].d_children[2] :
+ * T[A].d_children[0].d_children[1].d_children[2].d_children[3] : A1
+ * T[A].d_children[0].d_children[2] :
+ * T[A].d_children[0].d_children[2].d_children[3] : A2
+ * T[A].d_children[1] : AZ
+ * T[A].d_children[2] : AO
+ * T[A].d_children[2].d_children[4] : A3
+ *
+ * Nodes store the types built for the path of positions up to that point, if
+ * any.
+ */
+class OpPosTrie
{
- /* Both constructors create an unresolved type and datatype with the given
- * name. An original typenode is optional, since normalized types can be
- * created from scratch during normalization */
- TypeObject(TypeNode src_tn, std::string type_name);
- TypeObject(std::string type_name);
- ~TypeObject() {}
-
- /* The original typenode this TypeObject is built from */
- TypeNode d_tn;
- /* The type represented by d_tn */
- Type d_t;
- /* Operators for each constructor. */
- std::vector<Node> d_ops;
- /* Names for each constructor. */
- std::vector<std::string> d_cons_names;
- /* Print callbacks for each constructor */
- std::vector<std::shared_ptr<SygusPrintCallback>> d_pcb;
- /* List of argument types for each constructor */
- std::vector<std::vector<Type>> d_cons_args_t;
- /* Unresolved type placeholder */
- Type d_unres_t;
- /* Datatype to represent type's structure */
- Datatype d_dt;
-};
-
-/** Utility for normalizing SyGuS grammars and avoid spurious enumarations
+ public:
+ /** type retrieval/addition
+ *
+ * if type indexed by the given operator positions is already in the trie then
+ * unres_t becomes the indexed type and true is returned. Otherwise a new type
+ * is created, indexed by the given positions, and assigned to unres_t, with
+ * false being returned.
+ */
+ bool getOrMakeType(TypeNode tn,
+ TypeNode& unres_tn,
+ std::vector<unsigned> op_pos,
+ unsigned ind = 0);
+ /** clear all data from this trie */
+ void clear() { d_children.clear(); }
+
+ private:
+ /** the data (only set for the final node of an inserted path) */
+ TypeNode d_unres_tn;
+ /* the children of the trie node */
+ std::map<unsigned, OpPosTrie> d_children;
+}; /* class OpPosTrie */
+
+/** Utility for normalizing SyGuS grammars to avoid spurious enumerations
*
* Uses the datatype representation of a SyGuS grammar to identify entries that
* can normalized in order to have less possible enumerations. An example is
* with integer types, e.g.:
*
- * Int -> x | y | Int + Int | Int - Int | 0 | 1 | ite( Bool, Int, Int ) |
- * c1...cn
- *
- * where c1...cn are additional constants (in the case of large constants
- * appearing in the conjecture).
+ * Int -> x | y | Int + Int | 0 | 1 | ite(Bool, Int, Int)
*
* becomes
*
- * Int -> ite( Bool, Int, Int ) | IntN
- * IntN -> IntX | Int0 - IntX
- * Int0 -> 0
- * IntX -> IntXX + IntX | IntY
- * IntXX -> x
- * IntY -> IntYY + IntY | IntC
- * IntYY -> y
- * IntC -> IntCC + IntC | IntV
- * IntCC -> 1
- * IntV -> 0 | c1...cn */
+ * Int0 -> IntZ | Int1
+ * IntZ -> 0
+ * Int1 -> IntX | IntX + Int1 | Int2
+ * IntX -> x
+ * Int2 -> IntY | IntY + Int2 | Int3
+ * IntY -> y
+ * Int3 -> IntO | IntO + Int3 | Int4
+ * IntO -> 1
+ * Int4 -> IntITE | IntITE + Int4
+ * IntITE -> ite(Bool, Int0, Int0)
+ *
+ * TODO: #1304 normalize more complex grammars
+ *
+ * This class also performs more straightforward normalizations, such as
+ * expanding definitions of functions declared with a "define-fun" command.
+ * These lighweight transformations are always applied, independently of the
+ * normalization option being enabled.
+ */
class SygusGrammarNorm
{
public:
- SygusGrammarNorm(QuantifiersEngine* qe, CegConjecture* p);
+ SygusGrammarNorm(QuantifiersEngine* qe)
+ : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus())
+ {
+ }
~SygusGrammarNorm() {}
/** creates a normalized typenode from a given one.
*
- * In a normalized typenode all of its types that can be normalized (e.g. Int)
- * are so and its other types are structurally identical to the original
- * typenode it normalizes.
+ * In a normalized typenode all typenodes it contains are normalized.
+ * Normalized typenodes can be structurally identicial to their original
+ * counterparts.
*
* sygus_vars are the input variables for the function to be synthesized,
- * which are used as input for the built datatypes. */
+ * which are used as input for the built datatypes.
+ *
+ * This is the function that will resolve all types and datatypes built during
+ * normalization. This operation can only be performed after all types
+ * contained in "tn" have been normalized, since the resolution of datatypes
+ * depends on all types involved being defined.
+ */
TypeNode normalizeSygusType(TypeNode tn, Node sygus_vars);
+ /* Retrives, or, if none, creates, stores and returns, the node for the
+ * identity operator (\lambda x. x) for the given type node */
+ static inline Node getIdOp(TypeNode tn)
+ {
+ auto it = d_tn_to_id.find(tn);
+ if (it == d_tn_to_id.end())
+ {
+ std::vector<Node> vars = {NodeManager::currentNM()->mkBoundVar(tn)};
+ Node n = NodeManager::currentNM()->mkNode(
+ kind::LAMBDA,
+ NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars),
+ vars.back());
+ d_tn_to_id[tn] = n;
+ return n;
+ }
+ return it->second;
+ }
+
private:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
- /** parent conjecture
+ /** Keeps the necessary information for bulding a normalized type:
+ *
+ * the original typenode, from which the datatype representation can be
+ * extracted
+ *
+ * the operators, names, print callbacks and list of argument types for each
+ * constructor
*
- * This contains global information about the synthesis conjecture. */
- CegConjecture* d_parent;
+ * the unresolved type node used as placeholder for references of the yet to
+ * be built normalized type
+ *
+ * a datatype to represent the structure of the type node for the normalized
+ * type
+ */
+ class TypeObject
+ {
+ public:
+ /* Stores the original type node and the unresolved placeholder. The
+ * datatype for the latter is created with the respective name. */
+ TypeObject(TypeNode src_tn, TypeNode unres_tn)
+ : d_tn(src_tn),
+ d_unres_tn(unres_tn),
+ d_dt(Datatype(unres_tn.getAttribute(expr::VarNameAttr())))
+ {
+ }
+ ~TypeObject() {}
+
+ /** adds information in "cons" (operator, name, print callback, argument
+ * types) as it is into "to"
+ *
+ * A side effect of this procedure is to expand the definitions in the sygus
+ * operator of "cons"
+ *
+ * The types of the arguments of "cons" are recursively normalized
+ */
+ void addConsInfo(SygusGrammarNorm* sygus_norm,
+ const DatatypeConstructor& cons);
+
+ /** builds a datatype with the information in the type object
+ *
+ * "dt" is the datatype of the original typenode. It is necessary for
+ * retrieving ancillary information during the datatype building, such as
+ * its sygus type (e.g. Int)
+ *
+ * The built datatype and its unresolved type are saved in the global
+ * accumulators of "sygus_norm"
+ */
+ void buildDatatype(SygusGrammarNorm* sygus_norm, const Datatype& dt);
+
+ //---------- information stored from original type node
+
+ /* The original typenode this TypeObject is built from */
+ TypeNode d_tn;
+ //---------- information to build normalized type node
+
+ /* Operators for each constructor. */
+ std::vector<Node> d_ops;
+ /* Names for each constructor. */
+ std::vector<std::string> d_cons_names;
+ /* Print callbacks for each constructor */
+ std::vector<std::shared_ptr<SygusPrintCallback>> d_pc;
+ /* Weights for each constructor */
+ std::vector<int> d_weight;
+ /* List of argument types for each constructor */
+ std::vector<std::vector<Type>> d_cons_args_t;
+ /* Unresolved type node placeholder */
+ TypeNode d_unres_tn;
+ /* Datatype to represent type's structure */
+ Datatype d_dt;
+ }; /* class TypeObject */
+
+ /** Transformation abstract class
+ *
+ * Classes extending this one will define specif transformationst for building
+ * normalized types based on applications of specific operators
+ */
+ class Transf
+ {
+ public:
+ /** abstract function for building normalized types
+ *
+ * Builds normalized types for the operators specifed by the positions in
+ * op_pos of constructors from dt. The built types are associated with the
+ * given type object and accumulated in the sygus_norm object, whose
+ * utilities for any extra necessary normalization.
+ */
+ virtual void buildType(SygusGrammarNorm* sygus_norm,
+ TypeObject& to,
+ const Datatype& dt,
+ std::vector<unsigned>& op_pos) = 0;
+ }; /* class Transf */
+
+ /** Chain transformation class
+ *
+ * Determines how to build normalized types by chaining the application of one
+ * of its operators. The resulting type should admit the same terms as the
+ * previous one modulo commutativity, associativity and identity of the
+ * neutral element.
+ *
+ * TODO: #1304:
+ * - define this transformation for more than just PLUS for Int.
+ * - improve the building such that elements that should not be entitled a
+ * "link in the chain" (such as 5 in opposition to variables and 1) do not get
+ * one
+ * - consider the case when operator is applied to different types, e.g.:
+ * A -> B + B | x; B -> 0 | 1
+ * - consider the case in which in which the operator occurs nested in an
+ * argument type of itself, e.g.:
+ * A -> (B + B) + B | x; B -> 0 | 1
+ */
+ class TransfChain : public Transf
+ {
+ public:
+ TransfChain(unsigned chain_op_pos, std::vector<unsigned> elem_pos)
+ : d_chain_op_pos(chain_op_pos), d_elem_pos(elem_pos){};
+
+ /** builds types encoding a chain in which each link contains a repetition
+ * of the application of the chain operator over a non-identity element
+ *
+ * Example: when considering, over the integers, the operator "+" and the
+ * elemenst "1", "x" and "y", the built chain is e.g.
+ *
+ * x + ... + x + y + ... + y + 1 + ...+ 1
+ *
+ * whose encoding in types would be e.g.
+ *
+ * A -> AX | AX + A | B
+ * AX -> x
+ * B -> BY | BY + B | C
+ * BY -> y
+ * C -> C1 | C1 + C
+ * C1 -> 1
+ *
+ * ++++++++
+ *
+ * The types composing links in the chain are built recursively by invoking
+ * sygus_norm, which caches results and handles the global normalization, on
+ * the operators not used in a given link, which will lead to recalling this
+ * transformation and so on until all operators originally given are
+ * considered.
+ */
+ virtual void buildType(SygusGrammarNorm* sygus_norm,
+ TypeObject& to,
+ const Datatype& dt,
+ std::vector<unsigned>& op_pos) override;
+
+ /** Whether operator is chainable for the type (e.g. PLUS for Int)
+ *
+ * Since the map this function depends on cannot be built statically, this
+ * function first build maps the first time a type is checked. As a
+ * consequence the list of chainabel operators is hardcoded in the map
+ * building.
+ *
+ * TODO: #1304: Cover more types and operators, make this robust to more
+ * complex grammars
+ */
+ static bool isChainable(TypeNode tn, Node op);
+ /* Whether n is the identity for the chain operator of the type (e.g. 1 is
+ * not the identity 0 for PLUS for Int)
+ *
+ * TODO: #1304: Cover more types, make this robust to more complex grammars
+ */
+ static bool isId(TypeNode tn, Node op, Node n);
+
+ private:
+ /* TODO #1304: this should admit more than one, as well as which elements
+ * are associated with which operator */
+ /* Position of chain operator */
+ unsigned d_chain_op_pos;
+ /* Positions (of constructors in the datatype whose type is being
+ * normalized) of elements the chain operator is applied to */
+ std::vector<unsigned> d_elem_pos;
+ /** Specifies for each type node which are its chainable operators
+ *
+ * For example, for Int the map is {OP -> [+]}
+ *
+ * TODO #1304: consider more operators
+ */
+ static std::map<TypeNode, std::vector<Kind>> d_chain_ops;
+ /** Specifies for each type node and chainable operator its identity
+ *
+ * For example, for Int and PLUS the map is {Int -> {+ -> 0}}
+ *
+ * TODO #1304: consider more operators
+ */
+ static std::map<TypeNode, std::map<Kind, Node>> d_chain_op_id;
+
+ }; /* class TransfChain */
+
+ /** reference to quantifier engine */
+ QuantifiersEngine* d_qe;
/** sygus term database associated with this utility */
TermDbSygus* d_tds;
+ /** List of variable inputs of function-to-synthesize.
+ *
+ * This information is needed in the construction of each datatype
+ * representation of type nodes contained in the type node being normalized
+ */
+ TNode d_sygus_vars;
+ /* Datatypes to be resolved */
+ std::vector<Datatype> d_dt_all;
+ /* Types to be resolved */
+ std::set<Type> d_unres_t_all;
+ /* Associates type nodes with OpPosTries */
+ std::map<TypeNode, OpPosTrie> d_tries;
+ /* Map of type nodes into their identity operators (\lambda x. x) */
+ static std::map<TypeNode, Node> d_tn_to_id;
- /** normalize integer type
+ /** recursively traverses a typenode normalizing all of its elements
*
- * TODO actually perform the normalization #1304
+ * "tn" is the typenode to be normalized
+ * "dt" is its datatype representation
+ * "op_pos" is the list of positions of construtors of dt that are being
+ * considered for the normalization
*
- * ind is the index of the analyzed typeobject in tos
+ * The result of normalizing tn with the respective constructors is cached
+ * with an OpPosTrie. New types and datatypes created during normalization are
+ * accumulated grobally to be later resolved.
*
- * New types created during normalization will be added to tos and
- * tn_to_unres
+ * The normalization occurs following some inferred transformation based on
+ * the sygus type (e.g. Int) of tn, and the operators being considered.
*
- * sygus_vars is used as above for datatype construction */
- void normalizeSygusInt(unsigned ind,
- std::vector<TypeObject>& tos,
- std::map<TypeNode, Type>& tn_to_unres,
- Node sygus_vars);
-
- /** Traverses the datatype representation of src_tn and collects the types it
- * contains
+ * Example: Let A be the type node encoding the grammar
*
- * For each new typenode a TypeObject is created, with an unresolved type and
- * a datatype to be later resolved and constructed, respectively. These are
- * accumulated in tos.
+ * Int -> x | y | Int + Int | 0 | 1 | ite(Bool, Int, Int)
*
- * tn_to_unres maps the sygus types that the typenodes stand for into
- * the unresolved type to be built for the typenodes normalizations.
+ * and assume all its datatype constructors are being used for
+ * normalization. The inferred normalization transformation will consider the
+ * non-zero elements {x, y, 1, ite(...)} and the operator {+} to build a chain
+ * of monomials, as seen above. The operator for "0" is rebuilt as is (the
+ * default behaviour of operators not selected for transformations).
+ *
+ * recursion depth is limited by the height of the types, which is small
+ */
+ TypeNode normalizeSygusRec(TypeNode tn,
+ const Datatype& dt,
+ std::vector<unsigned>& op_pos);
+
+ /** wrapper for the above function
+ *
+ * invoked when all operators of "tn" are to be considered for normalization
+ */
+ TypeNode normalizeSygusRec(TypeNode tn);
+
+ /** infers a transformation for normalizing dt when allowed to use the
+ * operators in the positions op_pos.
*
- * visited caches visited nodes
+ * TODO: #1304: Infer more complex transformations
*/
- void collectInfoFor(TypeNode src_tn,
- std::vector<TypeObject>& tos,
- std::map<TypeNode, Type>& tn_to_unres,
- std::map<TypeNode, bool>& visited);
-};
+ Transf* inferTransf(TypeNode tn,
+ const Datatype& dt,
+ const std::vector<unsigned>& op_pos);
+}; /* class SygusGrammarNorm */
} // namespace quantifiers
} // namespace theory
projects / cvc5.git / commitdiff