From: Haniel Barbosa Date: Sun, 3 Dec 2017 19:18:42 +0000 (-0600) Subject: Normalize grammars - 2 (#1420) X-Git-Tag: cvc5-1.0.0~5432 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=612e4e2a58e3bd47708b7e6f8771b539ee1383bf;p=cvc5.git Normalize grammars - 2 (#1420) This is another step towards addressing #1304 and #1344. This pull request: - Refactors SygusGrammarNorm - Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used. - Performs a "chain transformation" in the application of the PLUS operator in integer grammars - Removes redundant expansions of definitions from TermDbSygus - Adds a default empty print callback to SygusEmptyPrintCallback This lays the basis for more general linearizations. --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 4a7a9e8a7..f997a8923 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -272,8 +272,8 @@ option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false aggressively minimize sygus grammars option sygusAddConstGrammar --sygus-add-const-grammar bool :default true statically add constants appearing in conjecture to grammars -option sygusNormalizeGrammar --sygus-norm-grammar bool :default false - statically normalize sygus grammars based on flattening +option sygusGrammarNorm --sygus-grammar-norm bool :default false + statically normalize sygus grammars based on flattening (linearization) option sygusTemplEmbedGrammar --sygus-templ-embed-grammar bool :default false embed sygus templates into grammars diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp index c5287e469..77f68e097 100644 --- a/src/printer/sygus_print_callback.cpp +++ b/src/printer/sygus_print_callback.cpp @@ -208,5 +208,7 @@ void SygusEmptyPrintCallback::toStreamSygus(const Printer* p, } } +std::shared_ptr SygusEmptyPrintCallback::d_empty_pc = nullptr; + } /* CVC4::printer namespace */ } /* CVC4 namespace */ diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h index 84da0f86c..e0c220e00 100644 --- a/src/printer/sygus_print_callback.h +++ b/src/printer/sygus_print_callback.h @@ -154,6 +154,19 @@ class CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback virtual void toStreamSygus(const Printer* p, std::ostream& out, Expr e) const override; + /* Retrieves empty callback pointer */ + static inline std::shared_ptr getEmptyPC() + { + if (!d_empty_pc) + { + d_empty_pc = std::make_shared(); + } + return d_empty_pc; + } + + private: + /* empty callback object */ + static std::shared_ptr d_empty_pc; }; } /* CVC4::printer namespace */ diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp index 05aa599b1..ee1b50842 100644 --- a/src/theory/quantifiers/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus_grammar_cons.cpp @@ -119,11 +119,8 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, v.getType(), sfvl, ss.str(), extra_cons, term_irrelevant); } // normalize type - if (options::sygusNormalizeGrammar()) - { - SygusGrammarNorm sygus_norm(d_qe, d_parent); - tn = sygus_norm.normalizeSygusType(tn, sfvl); - } + SygusGrammarNorm sygus_norm(d_qe); + tn = sygus_norm.normalizeSygusType(tn, sfvl); // check if there is a template std::map< Node, Node >::iterator itt = templates.find( sf ); if( itt!=templates.end() ){ diff --git a/src/theory/quantifiers/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus_grammar_norm.cpp index 9037566b7..67c40d6aa 100644 --- a/src/theory/quantifiers/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus_grammar_norm.cpp @@ -17,162 +17,435 @@ #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 // 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 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()); + 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(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& tos, - std::map& tn_to_unres, - std::map& visited) +void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, + TypeObject& to, + const Datatype& dt, + std::vector& op_pos) { - if (visited.find(tn) != visited.end()) + NodeManager* nm = NodeManager::currentNM(); + std::vector 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 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 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()); + 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()); + 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(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(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()); + 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& tos, - std::map& tn_to_unres, - Node sygus_vars) +std::map 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& op_pos) { - const Datatype& dt = - static_cast(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 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(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& op_pos) { - /* Make int_type and zero */ - NodeManager* nm = NodeManager::currentNM(); - /* Accumulates all typing information for normalization and reconstruction */ - std::vector tos; - /* Allows retrieving respective unresolved types for the sygus types of the - * original type nodes */ - std::map tn_to_unres; - std::map 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(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()); - 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(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 dts; - std::set 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(tn.toType()).getDatatype(); + std::vector 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 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 diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus_grammar_norm.h index 15b4502d3..38e3f168e 100644 --- a/src/theory/quantifiers/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus_grammar_norm.h @@ -14,137 +14,407 @@ **/ #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 d_ops; - /* Names for each constructor. */ - std::vector d_cons_names; - /* Print callbacks for each constructor */ - std::vector> d_pcb; - /* List of argument types for each constructor */ - std::vector> 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 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 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 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 d_ops; + /* Names for each constructor. */ + std::vector d_cons_names; + /* Print callbacks for each constructor */ + std::vector> d_pc; + /* Weights for each constructor */ + std::vector d_weight; + /* List of argument types for each constructor */ + std::vector> 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& 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 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& 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 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> 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> 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 d_dt_all; + /* Types to be resolved */ + std::set d_unres_t_all; + /* Associates type nodes with OpPosTries */ + std::map d_tries; + /* Map of type nodes into their identity operators (\lambda x. x) */ + static std::map 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& tos, - std::map& 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& 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& tos, - std::map& tn_to_unres, - std::map& visited); -}; + Transf* inferTransf(TypeNode tn, + const Datatype& dt, + const std::vector& op_pos); +}; /* class SygusGrammarNorm */ } // namespace quantifiers } // namespace theory diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index 8625d9089..295d7fb52 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -237,8 +237,6 @@ Node TermDbSygus::getGenericBase( TypeNode tn, const Datatype& dt, int c ) { Trace("sygus-db-debug") << "Sygus DB : Generic is " << g << std::endl; Node gr = Rewriter::rewrite( g ); Trace("sygus-db-debug") << "Sygus DB : Generic rewritten is " << gr << std::endl; - gr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( gr.toExpr() ) ); - Trace("sygus-db-debug") << "Sygus DB : Generic base " << dt[c].getName() << " : " << gr << std::endl; d_generic_base[tn][c] = gr; return gr; }else{ @@ -411,8 +409,7 @@ Node TermDbSygus::getNormalized(TypeNode t, Node prog) { std::map< Node, Node >::iterator itn = d_normalized[t].find( prog ); if( itn==d_normalized[t].end() ){ - Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) ); - progr = Rewriter::rewrite( progr ); + Node progr = Rewriter::rewrite( prog ); Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl; d_normalized[t][prog] = progr; return progr;