From 6a24e015ca539d80317276761a42f0117dd43575 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 15 Nov 2019 22:52:58 -0600 Subject: [PATCH] Use standard interface for sygus default grammar construction (#3466) --- src/expr/sygus_datatype.cpp | 25 +- src/expr/sygus_datatype.h | 23 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 496 ++++++++---------- .../quantifiers/sygus/sygus_grammar_cons.h | 39 +- .../quantifiers/sygus/sygus_grammar_norm.cpp | 15 +- 5 files changed, 292 insertions(+), 306 deletions(-) diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index be2b04402..d8ee2e1ea 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -26,9 +26,9 @@ std::string SygusDatatype::getName() const { return d_dt.getName(); } void SygusDatatype::addConstructor(Node op, const std::string& name, + const std::vector& consTypes, std::shared_ptr spc, - int weight, - const std::vector& consTypes) + int weight) { d_ops.push_back(op); d_cons_names.push_back(std::string(name)); @@ -50,14 +50,26 @@ void SygusDatatype::addAnyConstantConstructor(TypeNode tn) std::vector builtinArg; builtinArg.push_back(tn); addConstructor( - av, cname, printer::SygusEmptyPrintCallback::getEmptyPC(), 0, builtinArg); + av, cname, builtinArg, printer::SygusEmptyPrintCallback::getEmptyPC(), 0); +} +void SygusDatatype::addConstructor(Kind k, + const std::vector& consTypes, + std::shared_ptr spc, + int weight) +{ + NodeManager* nm = NodeManager::currentNM(); + addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight); } +size_t SygusDatatype::getNumConstructors() const { return d_ops.size(); } + void SygusDatatype::initializeDatatype(TypeNode sygusType, Node sygusVars, bool allowConst, bool allowAll) { + // should not have initialized (set sygus) yet + Assert(!d_dt.isSygus()); /* Use the sygus type to not lose reference to the original types (Bool, * Int, etc) */ d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll); @@ -76,6 +88,11 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType, Trace("sygus-type-cons") << "...built datatype " << d_dt << " "; } -const Datatype& SygusDatatype::getDatatype() const { return d_dt; } +const Datatype& SygusDatatype::getDatatype() const +{ + // should have initialized by this point + Assert(d_dt.isSygus()); + return d_dt; +} } // namespace CVC4 diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index d7b18644a..132406c69 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -61,18 +61,35 @@ class SygusDatatype * weight: the weight of this constructor, * consTypes: the argument types of the constructor (typically other sygus * datatype types). + * + * It should be the case that consTypes are sygus datatype types (possibly + * unresolved) that encode the arguments of the builtin operator. That is, + * if op is the builtin PLUS operator, then consTypes could contain 2+ + * sygus datatype types that encode integer. */ void addConstructor(Node op, const std::string& name, - std::shared_ptr spc, - int weight, - const std::vector& consTypes); + const std::vector& consTypes, + std::shared_ptr spc = nullptr, + int weight = -1); + /** + * Add constructor that encodes an application of builtin kind k. Like above, + * the arguments consTypes should correspond to sygus datatypes that encode + * the types of the arguments of the kind. + */ + void addConstructor(Kind k, + const std::vector& consTypes, + std::shared_ptr spc = nullptr, + int weight = -1); /** * This adds a constructor that corresponds to the any constant constructor * for the given (builtin) type tn. */ void addAnyConstantConstructor(TypeNode tn); + /** Get the number of constructors added to this class so far */ + size_t getNumConstructors() const; + /** builds a datatype with the information in the type object * * sygusType: the builtin type that this datatype encodes, diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index b8bf6c865..d00df38c5 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -48,8 +48,7 @@ bool CegGrammarConstructor::hasSyntaxRestrictions(Node q) if (!gv.isNull()) { TypeNode tn = gv.getType(); - if (tn.isDatatype() - && static_cast(tn.toType()).getDatatype().isSygus()) + if (tn.isDatatype() && tn.getDatatype().isSygus()) { return true; } @@ -260,7 +259,7 @@ Node CegGrammarConstructor::process(Node q, } tds->registerSygusType(tn); Assert(tn.isDatatype()); - const Datatype& dt = static_cast(tn.toType()).getDatatype(); + const Datatype& dt = tn.getDatatype(); Assert(dt.isSygus()); if( !dt.getSygusAllowAll() ){ d_is_syntax_restricted = true; @@ -433,21 +432,16 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor( for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args; ++j) { - collectSygusGrammarTypesFor( - TypeNode::fromType(static_cast(dt[i][j].getType()) - .getRangeType()), - types); + TypeNode tn = TypeNode::fromType(dt[i][j].getRangeType()); + collectSygusGrammarTypesFor(tn, types); } } } else if (range.isArray()) { - ArrayType arrayType = static_cast(range.toType()); // add index and constituent type - collectSygusGrammarTypesFor( - TypeNode::fromType(arrayType.getIndexType()), types); - collectSygusGrammarTypesFor( - TypeNode::fromType(arrayType.getConstituentType()), types); + collectSygusGrammarTypesFor(range.getArrayIndexType(), types); + collectSygusGrammarTypesFor(range.getArrayConstituentType(), types); } else if (range.isString() ) { @@ -487,11 +481,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Node bvl, const std::string& fun, std::map>& extra_cons, - std::map>& exc_cons, + std::map>& + exclude_cons, const std::map>& - inc_cons, + include_cons, std::unordered_set& term_irrelevant, - std::vector& datatypes, + std::vector& sdts, std::set& unres) { NodeManager* nm = NodeManager::currentNM(); @@ -515,19 +510,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } } } - // operators for each constructor in type - std::vector> ops; - // names for the operators - std::vector> cnames; - // argument types of operators - std::vector>> cargs; - // set of callbacks for each constructor - std::vector>> pcs; - // weights for each constructor - std::vector> weights; // index of top datatype, i.e. the datatype for the range type int startIndex = -1; - std::map< Type, Type > sygus_to_builtin; + std::map sygus_to_builtin; std::vector types; // collect connected types for each of the variables @@ -542,32 +527,39 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::stringstream ssb; ssb << fun << "_Bool"; std::string dbname = ssb.str(); - Type unres_bt = mkUnresolvedType(ssb.str(), unres).toType(); + TypeNode unres_bt = mkUnresolvedType(ssb.str(), unres); // create placeholders for collected types - std::vector< Type > unres_types; - std::map< TypeNode, Type > type_to_unres; + std::vector unres_types; + std::map type_to_unres; + std::map>::const_iterator + itc; for (unsigned i = 0, size = types.size(); i < size; ++i) { std::stringstream ss; ss << fun << "_" << types[i]; std::string dname = ss.str(); - datatypes.push_back(Datatype(dname)); - ops.push_back(std::vector< Expr >()); - cnames.push_back(std::vector()); - cargs.push_back(std::vector>()); - pcs.push_back(std::vector>()); - weights.push_back(std::vector()); + sdts.push_back(SygusDatatypeGenerator(dname)); + itc = exclude_cons.find(types[i]); + if (itc != exclude_cons.end()) + { + sdts.back().d_exclude_cons = itc->second; + } + itc = include_cons.find(types[i]); + if (itc != include_cons.end()) + { + sdts.back().d_include_cons = itc->second; + } //make unresolved type - Type unres_t = mkUnresolvedType(dname, unres).toType(); + TypeNode unres_t = mkUnresolvedType(dname, unres); unres_types.push_back(unres_t); type_to_unres[types[i]] = unres_t; - sygus_to_builtin[unres_t] = types[i].toType(); + sygus_to_builtin[unres_t] = types[i]; } for (unsigned i = 0, size = types.size(); i < size; ++i) { Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl; - Type unres_t = unres_types[i]; + TypeNode unres_t = unres_types[i]; //add variables for (const Node& sv : sygus_vars) { @@ -578,18 +570,15 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( ss << sv; Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; - ops[i].push_back(sv.toExpr()); - cnames[i].push_back(ss.str()); - cargs[i].push_back(std::vector()); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + std::vector cargsEmpty; + sdts[i].addConstructor(sv, ss.str(), cargsEmpty); } else if (svt.isFunction() && svt.getRangeType() == types[i]) { // We add an APPLY_UF for all function whose return type is this type // whose argument types are the other sygus types we are constructing. std::vector argTypes = svt.getArgTypes(); - std::vector stypes; + std::vector stypes; for (unsigned k = 0, ntypes = argTypes.size(); k < ntypes; k++) { unsigned index = @@ -599,11 +588,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } std::stringstream ss; ss << "apply_" << sv; - ops[i].push_back(sv.toExpr()); - cnames[i].push_back(ss.str()); - cargs[i].push_back(stypes); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + sdts[i].addConstructor(sv, ss.str(), stypes); } } //add constants @@ -628,23 +613,17 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::stringstream ss; ss << consts[j]; Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl; - ops[i].push_back( consts[j].toExpr() ); - cnames[i].push_back(ss.str()); - cargs[i].push_back(std::vector()); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + std::vector cargsEmpty; + sdts[i].addConstructor(consts[j], ss.str(), cargsEmpty); } // ITE Kind k = ITE; Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames[i].push_back(kindToString(k)); - cargs[i].push_back(std::vector()); - cargs[i].back().push_back(unres_bt); - cargs[i].back().push_back(unres_t); - cargs[i].back().push_back(unres_t); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + std::vector cargsIte; + cargsIte.push_back(unres_bt); + cargsIte.push_back(unres_t); + cargsIte.push_back(unres_t); + sdts[i].addConstructor(k, cargsIte); if (types[i].isReal()) { @@ -653,13 +632,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( for (const Kind k : kinds) { Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames[i].push_back(kindToString(k)); - cargs[i].push_back(std::vector()); - cargs[i].back().push_back(unres_t); - cargs[i].back().push_back(unres_t); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + std::vector cargsOp; + cargsOp.push_back(unres_t); + cargsOp.push_back(unres_t); + sdts[i].addConstructor(k, cargsOp); } if (!types[i].isInteger()) { @@ -670,61 +646,42 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( ss << fun << "_PosInt"; std::string pos_int_name = ss.str(); // make unresolved type - Type unres_pos_int_t = mkUnresolvedType(pos_int_name, unres).toType(); - // make data type - datatypes.push_back(Datatype(pos_int_name)); - /* add placeholders */ - std::vector ops_pos_int; - std::vector cnames_pos_int; - std::vector> cargs_pos_int; + TypeNode unres_pos_int_t = mkUnresolvedType(pos_int_name, unres); + // make data type for positive constant integers + sdts.push_back(SygusDatatypeGenerator(pos_int_name)); /* Add operator 1 */ Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n"; - ops_pos_int.push_back(nm->mkConst(Rational(1)).toExpr()); - ss.str(""); - ss << "1"; - cnames_pos_int.push_back(ss.str()); - cargs_pos_int.push_back(std::vector()); + std::vector cargsEmpty; + sdts.back().addConstructor(nm->mkConst(Rational(1)), "1", cargsEmpty); /* Add operator PLUS */ Kind k = PLUS; Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n"; - ops_pos_int.push_back(nm->operatorOf(k).toExpr()); - cnames_pos_int.push_back(kindToString(k)); - cargs_pos_int.push_back(std::vector()); - cargs_pos_int.back().push_back(unres_pos_int_t); - cargs_pos_int.back().push_back(unres_pos_int_t); - datatypes.back().setSygus(types[i].toType(), bvl.toExpr(), true, true); - for (unsigned j = 0, size_j = ops_pos_int.size(); j < size_j; ++j) - { - datatypes.back().addSygusConstructor( - ops_pos_int[j], cnames_pos_int[j], cargs_pos_int[j]); - } + std::vector cargsPlus; + cargsPlus.push_back(unres_pos_int_t); + cargsPlus.push_back(unres_pos_int_t); + sdts.back().addConstructor(k, cargsPlus); + sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true); Trace("sygus-grammar-def") - << " ...built datatype " << datatypes.back() << " "; + << " ...built datatype " << sdts.back().d_sdt.getDatatype() << " "; /* Adding division at root */ k = DIVISION; Trace("sygus-grammar-def") << "\t...add for " << k << std::endl; - ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames[i].push_back(kindToString(k)); - cargs[i].push_back(std::vector()); - cargs[i].back().push_back(unres_t); - cargs[i].back().push_back(unres_pos_int_t); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + std::vector cargsDiv; + cargsDiv.push_back(unres_t); + cargsDiv.push_back(unres_pos_int_t); + sdts[i].addConstructor(k, cargsDiv); } } else if (types[i].isBitVector()) { // unary apps std::vector un_kinds = {BITVECTOR_NOT, BITVECTOR_NEG}; + std::vector cargsUnary; + cargsUnary.push_back(unres_t); for (const Kind k : un_kinds) { Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames[i].push_back(kindToString(k)); - cargs[i].push_back(std::vector()); - cargs[i].back().push_back(unres_t); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + sdts[i].addConstructor(k, cargsUnary); } // binary apps std::vector bin_kinds = {BITVECTOR_AND, @@ -740,28 +697,22 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( BITVECTOR_SHL, BITVECTOR_LSHR, BITVECTOR_ASHR}; + std::vector cargsBinary; + cargsBinary.push_back(unres_t); + cargsBinary.push_back(unres_t); for (const Kind k : bin_kinds) { Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames[i].push_back(kindToString(k)); - cargs[i].push_back(std::vector()); - cargs[i].back().push_back(unres_t); - cargs[i].back().push_back(unres_t); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + sdts[i].addConstructor(k, cargsBinary); } } else if (types[i].isString()) { // concatenation - ops[i].push_back(nm->operatorOf(STRING_CONCAT).toExpr()); - cnames[i].push_back(kindToString(STRING_CONCAT)); - cargs[i].push_back(std::vector()); - cargs[i].back().push_back(unres_t); - cargs[i].back().push_back(unres_t); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + std::vector cargsBinary; + cargsBinary.push_back(unres_t); + cargsBinary.push_back(unres_t); + sdts[i].addConstructor(STRING_CONCAT, cargsBinary); // length TypeNode intType = nm->integerType(); Assert(std::find(types.begin(), types.end(), intType) != types.end()); @@ -770,63 +721,46 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::find(types.begin(), types.end(), intType)); - ops[i_intType].push_back(nm->operatorOf(STRING_LENGTH).toExpr()); - cnames[i_intType].push_back(kindToString(STRING_LENGTH)); - cargs[i_intType].push_back(std::vector()); - cargs[i_intType].back().push_back(unres_t); - pcs[i_intType].push_back(nullptr); - weights[i_intType].push_back(-1); + std::vector cargsLen; + cargsLen.push_back(unres_t); + sdts[i_intType].addConstructor(STRING_LENGTH, cargsLen); } else if (types[i].isArray()) { - ArrayType arrayType = static_cast(types[i].toType()); - Trace("sygus-grammar-def") - << "...building for array type " << arrayType << "\n"; Trace("sygus-grammar-def") - << "......finding unres type for index type " - << arrayType.getIndexType() << " with typenode " - << TypeNode::fromType(arrayType.getIndexType()) << "\n"; + << "...building for array type " << types[i] << "\n"; + Trace("sygus-grammar-def") << "......finding unres type for index type " + << types[i].getArrayIndexType() << "\n"; // retrieve index and constituent unresolved types - Assert(std::find(types.begin(), - types.end(), - TypeNode::fromType(arrayType.getIndexType())) + Assert(std::find(types.begin(), types.end(), types[i].getArrayIndexType()) != types.end()); unsigned i_indexType = std::distance( types.begin(), - std::find(types.begin(), - types.end(), - TypeNode::fromType(arrayType.getIndexType()))); - Type unres_indexType = unres_types[i_indexType]; - Assert(std::find(types.begin(), - types.end(), - TypeNode::fromType(arrayType.getConstituentType())) + std::find(types.begin(), types.end(), types[i].getArrayIndexType())); + TypeNode unres_indexType = unres_types[i_indexType]; + Assert(std::find( + types.begin(), types.end(), types[i].getArrayConstituentType()) != types.end()); unsigned i_constituentType = std::distance( types.begin(), - std::find(types.begin(), - types.end(), - TypeNode::fromType(arrayType.getConstituentType()))); - Type unres_constituentType = unres_types[i_constituentType]; + std::find( + types.begin(), types.end(), types[i].getArrayConstituentType())); + TypeNode unres_constituentType = unres_types[i_constituentType]; // add (store ArrayType IndexType ConstituentType) Trace("sygus-grammar-def") << "...add for STORE\n"; - ops[i].push_back(nm->operatorOf(STORE).toExpr()); - cnames[i].push_back(kindToString(STORE)); - cargs[i].push_back(std::vector()); - cargs[i].back().push_back(unres_t); - cargs[i].back().push_back(unres_indexType); - cargs[i].back().push_back(unres_constituentType); - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + + std::vector cargsStore; + cargsStore.push_back(unres_t); + cargsStore.push_back(unres_indexType); + cargsStore.push_back(unres_constituentType); + sdts[i].addConstructor(STORE, cargsStore); // add to constituent type : (select ArrayType IndexType) Trace("sygus-grammar-def") << "...add select for constituent type" << unres_constituentType << "\n"; - ops[i_constituentType].push_back(nm->operatorOf(SELECT).toExpr()); - cnames[i_constituentType].push_back(kindToString(SELECT)); - cargs[i_constituentType].push_back(std::vector()); - cargs[i_constituentType].back().push_back(unres_t); - cargs[i_constituentType].back().push_back(unres_indexType); - pcs[i_constituentType].push_back(nullptr); - weights[i_constituentType].push_back(-1); + std::vector cargsSelect; + cargsSelect.push_back(unres_t); + cargsSelect.push_back(unres_indexType); + sdts[i_constituentType].addConstructor(SELECT, cargsSelect); } else if (types[i].isDatatype()) { @@ -835,42 +769,36 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) { Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl; - Expr cop = dt[k].getConstructor(); + Node cop = Node::fromExpr(dt[k].getConstructor()); if (dt[k].getNumArgs() == 0) { // Nullary constructors are interpreted as terms, not operators. // Thus, we apply them to no arguments here. - cop = nm->mkNode(APPLY_CONSTRUCTOR, Node::fromExpr(cop)).toExpr(); + cop = nm->mkNode(APPLY_CONSTRUCTOR, cop); } - ops[i].push_back(cop); - cnames[i].push_back(dt[k].getName()); - cargs[i].push_back(std::vector()); + std::vector cargsCons; Trace("sygus-grammar-def") << "...add for selectors" << std::endl; for (unsigned j = 0, size_j = dt[k].getNumArgs(); j < size_j; ++j) { Trace("sygus-grammar-def") << "...for " << dt[k][j].getName() << std::endl; - TypeNode crange = TypeNode::fromType( - static_cast(dt[k][j].getType()).getRangeType()); + TypeNode crange = TypeNode::fromType(dt[k][j].getRangeType()); Assert(type_to_unres.find(crange) != type_to_unres.end()); - cargs[i].back().push_back(type_to_unres[crange]); + cargsCons.push_back(type_to_unres[crange]); // add to the selector type the selector operator Assert(std::find(types.begin(), types.end(), crange) != types.end()); unsigned i_selType = std::distance( types.begin(), std::find(types.begin(), types.end(), crange)); - TypeNode arg_type = TypeNode::fromType( - static_cast(dt[k][j].getType()).getDomain()); - ops[i_selType].push_back(dt[k][j].getSelector()); - cnames[i_selType].push_back(dt[k][j].getName()); - cargs[i_selType].push_back(std::vector()); + TypeNode arg_type = TypeNode::fromType(dt[k][j].getType()); + arg_type = arg_type.getSelectorDomainType(); Assert(type_to_unres.find(arg_type) != type_to_unres.end()); - cargs[i_selType].back().push_back(type_to_unres[arg_type]); - pcs[i_selType].push_back(nullptr); - weights[i_selType].push_back(-1); + std::vector cargsSel; + cargsSel.push_back(type_to_unres[arg_type]); + Node sel = Node::fromExpr(dt[k][j].getSelector()); + sdts[i_selType].addConstructor(sel, dt[k][j].getName(), cargsSel); } - pcs[i].push_back(nullptr); - weights[i].push_back(-1); + sdts[i].addConstructor(cop, dt[k].getName(), cargsCons); } } else if (types[i].isSort() || types[i].isFunction()) @@ -887,40 +815,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // make datatypes for (unsigned i = 0, size = types.size(); i < size; ++i) { - Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl; - datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true ); - std::map>::iterator - itexc = exc_cons.find(types[i]); - std::map>::const_iterator itinc = - inc_cons.find(types[i]); - for (unsigned j = 0, size = ops[i].size(); j < size; ++j) - { - // add the constructor if it is not excluded, - // and it is in inc_cons, in case it is not empty - Node opn = Node::fromExpr(ops[i][j]); - Trace("sygus-grammar-def") - << "...considering " << opn.toString() << " of kind " << opn.getKind() - << " and of type " << opn.getType() << " and of kind of type " - << opn.getType().getKind() << " of metakind " << opn.getMetaKind() - << std::endl; - if (itexc == exc_cons.end() - || std::find(itexc->second.begin(), itexc->second.end(), opn) - == itexc->second.end()) - { - Trace("sygus-grammar-def") << "......not excluded " << std::endl; - if ((opn.isVar()) || (opn.getType().getKind() != kind::TYPE_CONSTANT) - || (itinc == inc_cons.end()) - || (std::find(itinc->second.begin(), itinc->second.end(), opn) - != itinc->second.end())) - { - Trace("sygus-grammar-def") << "......included " << std::endl; - datatypes[i].addSygusConstructor( - ops[i][j], cnames[i][j], cargs[i][j], pcs[i][j], weights[i][j]); - } - } - } - Trace("sygus-grammar-def") << "...built datatype " << datatypes[i] << " "; + sdts[i].d_sdt.initializeDatatype(types[i], bvl, true, true); + Trace("sygus-grammar-def") + << "...built datatype " << sdts[i].d_sdt.getDatatype() << " "; //set start index if applicable if( types[i]==range ){ startIndex = i; @@ -929,13 +826,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( //------ make Boolean type TypeNode btype = nm->booleanType(); - datatypes.push_back(Datatype(dbname)); - ops.push_back(std::vector()); - cnames.push_back(std::vector()); - cargs.push_back(std::vector>()); - pcs.push_back(std::vector>()); - weights.push_back(std::vector()); - Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; + sdts.push_back(SygusDatatypeGenerator(dbname)); + SygusDatatypeGenerator& sdtBool = sdts.back(); + Trace("sygus-grammar-def") << "Make grammar for " << btype << std::endl; //add variables for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i) { @@ -943,12 +836,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::stringstream ss; ss << sygus_vars[i]; Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; - ops.back().push_back( sygus_vars[i].toExpr() ); - cnames.back().push_back(ss.str()); - cargs.back().push_back(std::vector()); - pcs.back().push_back(nullptr); + std::vector cargsEmpty; // make boolean variables weight as non-nullary constructors - weights.back().push_back(1); + sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, nullptr, 1); } } // add constants @@ -960,11 +850,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( ss << consts[i]; Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl; - ops.back().push_back(consts[i].toExpr()); - cnames.back().push_back(ss.str()); - cargs.back().push_back(std::vector()); - pcs.back().push_back(nullptr); - weights.back().push_back(-1); + std::vector cargsEmpty; + sdtBool.addConstructor(consts[i], ss.str(), cargsEmpty); } // add predicates for types for (unsigned i = 0, size = types.size(); i < size; ++i) @@ -977,60 +864,43 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( //add equality per type Kind k = EQUAL; Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(nm->operatorOf(k).toExpr()); std::stringstream ss; ss << kindToString(k) << "_" << types[i]; - cnames.back().push_back(ss.str()); - cargs.back().push_back(std::vector()); - cargs.back().back().push_back(unres_types[i]); - cargs.back().back().push_back(unres_types[i]); - pcs.back().push_back(nullptr); - weights.back().push_back(-1); + std::vector cargsBinary; + cargsBinary.push_back(unres_types[i]); + cargsBinary.push_back(unres_types[i]); + sdtBool.addConstructor(nm->operatorOf(k), ss.str(), cargsBinary); // type specific predicates if (types[i].isReal()) { Kind k = LEQ; Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.back().push_back(kindToString(k)); - cargs.back().push_back(std::vector()); - cargs.back().back().push_back(unres_types[i]); - cargs.back().back().push_back(unres_types[i]); - pcs.back().push_back(nullptr); - weights.back().push_back(-1); + sdtBool.addConstructor(k, cargsBinary); } else if (types[i].isBitVector()) { Kind k = BITVECTOR_ULT; Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.back().push_back(kindToString(k)); - cargs.back().push_back(std::vector()); - cargs.back().back().push_back(unres_types[i]); - cargs.back().back().push_back(unres_types[i]); - pcs.back().push_back(nullptr); - weights.back().push_back(-1); + sdtBool.addConstructor(k, cargsBinary); } else if (types[i].isDatatype()) { //add for testers Trace("sygus-grammar-def") << "...add for testers" << std::endl; const Datatype& dt = types[i].getDatatype(); + std::vector cargsTester; + cargsTester.push_back(unres_types[i]); for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) { Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl; - ops.back().push_back(dt[k].getTester()); - cnames.back().push_back(dt[k].getTesterName()); - cargs.back().push_back(std::vector()); - cargs.back().back().push_back(unres_types[i]); - pcs.back().push_back(nullptr); - weights.back().push_back(-1); + sdtBool.addConstructor( + dt[k].getTester(), dt[k].getTesterName(), cargsTester); } } } // add Boolean connectives, if not in a degenerate case of (recursively) // having only constant constructors - if (ops.back().size() > consts.size()) + if (sdtBool.d_sdt.getNumConstructors() > consts.size()) { for (unsigned i = 0; i < 4; i++) { @@ -1043,42 +913,31 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( continue; } Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.back().push_back(kindToString(k)); - cargs.back().push_back(std::vector()); - cargs.back().back().push_back(unres_bt); + std::vector cargs; + cargs.push_back(unres_bt); if (k != NOT) { - cargs.back().back().push_back(unres_bt); + cargs.push_back(unres_bt); if (k == ITE) { - cargs.back().back().push_back(unres_bt); + cargs.push_back(unres_bt); } } - pcs.back().push_back(nullptr); - weights.back().push_back(-1); + sdtBool.addConstructor(k, cargs); } } if( range==btype ){ - startIndex = datatypes.size()-1; - } - Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl; - datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true ); - for (unsigned i = 0, size = ops.back().size(); i < size; ++i) - { - datatypes.back().addSygusConstructor(ops.back()[i], - cnames.back()[i], - cargs.back()[i], - pcs.back()[i], - weights.back()[i]); + startIndex = sdts.size() - 1; } - Trace("sygus-grammar-def") << "...built datatype " << datatypes.back() << " "; + sdtBool.d_sdt.initializeDatatype(btype, bvl, true, true); + Trace("sygus-grammar-def") + << "...built datatype for Bool " << sdtBool.d_sdt.getDatatype() << " "; Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl; // make first datatype be the top level datatype if( startIndex>0 ){ - Datatype tmp_dt = datatypes[0]; - datatypes[0] = datatypes[startIndex]; - datatypes[startIndex] = tmp_dt; + SygusDatatypeGenerator tmp_dt = sdts[0]; + sdts[0] = sdts[startIndex]; + sdts[startIndex] = tmp_dt; } } @@ -1102,7 +961,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl; } std::set unres; - std::vector< CVC4::Datatype > datatypes; + std::vector sdts; mkSygusDefaultGrammar(range, bvl, fun, @@ -1110,8 +969,14 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( exclude_cons, include_cons, term_irrelevant, - datatypes, + sdts, unres); + // extract the datatypes from the sygus datatype generator objects + std::vector datatypes; + for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) + { + datatypes.push_back(sdts[i].d_sdt.getDatatype()); + } Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; Assert(!datatypes.empty()); std::vector types = @@ -1130,13 +995,13 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a }else{ tcount++; std::set unres; - std::vector< CVC4::Datatype > datatypes; + std::vector sdts; std::stringstream ssd; ssd << fun << "_templ_" << tcount; std::string dbname = ssd.str(); - datatypes.push_back(Datatype(dbname)); + sdts.push_back(SygusDatatype(dbname)); Node op; - std::vector< Type > argTypes; + std::vector argTypes; if( templ.getNumChildren()==0 ){ // TODO : can short circuit to this case when !TermUtil::containsTerm( templ, templ_arg ) op = templ; @@ -1147,15 +1012,20 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a for( unsigned i=0; i datatypes; + for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) + { + datatypes.push_back(sdts[i].getDatatype()); + } std::vector types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes( datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); @@ -1191,6 +1061,52 @@ Node CegGrammarConstructor::getSygusVarList(Node f) return sfvl; } +CegGrammarConstructor::SygusDatatypeGenerator::SygusDatatypeGenerator( + const std::string& name) + : d_sdt(name) +{ +} +void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor( + Node op, + const std::string& name, + const std::vector& consTypes, + std::shared_ptr spc, + int weight) +{ + if (shouldInclude(op)) + { + d_sdt.addConstructor(op, name, consTypes, spc, weight); + } +} +void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor( + Kind k, + const std::vector& consTypes, + std::shared_ptr spc, + int weight) +{ + NodeManager* nm = NodeManager::currentNM(); + addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight); +} +bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const +{ + if (d_exclude_cons.find(op) != d_exclude_cons.end()) + { + return false; + } + if (!d_include_cons.empty()) + { + // special case, variables and terms of certain types are always included + if (!op.isVar() && op.getType().getKind() == TYPE_CONSTANT) + { + if (d_include_cons.find(op) == d_include_cons.end()) + { + return false; + } + } + } + return true; +} + }/* namespace CVC4::theory::quantifiers */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 85efddada..00e9d45fb 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -23,6 +23,7 @@ #include "expr/attribute.h" #include "expr/node.h" +#include "expr/sygus_datatype.h" namespace CVC4 { namespace theory { @@ -186,6 +187,42 @@ public: Node n, std::map>& consts); //---------------- grammar construction + /** A class for generating sygus datatypes */ + class SygusDatatypeGenerator + { + public: + SygusDatatypeGenerator(const std::string& name); + ~SygusDatatypeGenerator() {} + /** + * Possibly add a constructor to d_sdt, based on the criteria mentioned + * in this class below. For details see expr/sygus_datatype.h. + */ + void addConstructor(Node op, + const std::string& name, + const std::vector& consTypes, + std::shared_ptr spc = nullptr, + int weight = -1); + /** + * Possibly add a constructor to d_sdt, based on the criteria mentioned + * in this class below. + */ + void addConstructor(Kind k, + const std::vector& consTypes, + std::shared_ptr spc = nullptr, + int weight = -1); + /** Should we include constructor with operator op? */ + bool shouldInclude(Node op) const; + /** The constructors that should be excluded. */ + std::unordered_set d_exclude_cons; + /** + * If this set is non-empty, then only include variables and constructors + * from it. + */ + std::unordered_set d_include_cons; + /** The sygus datatype we are generating. */ + SygusDatatype d_sdt; + }; + // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) static TypeNode mkUnresolvedType(const std::string& name, std::set& unres); // collect the list of types that depend on type range @@ -207,7 +244,7 @@ public: const std::map>& include_cons, std::unordered_set& term_irrelevant, - std::vector& datatypes, + std::vector& sdts, std::set& unres); // helper function for mkSygusTemplateType diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 68445fca0..40046ef15 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -222,9 +222,9 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm, << "\n\tExpanded one: " << exp_sop_n << "\n\n"; d_sdt.addConstructor(exp_sop_n, cons.getName(), + consTypes, cons.getSygusPrintCallback(), - cons.getWeight(), - consTypes); + cons.getWeight()); } void SygusGrammarNorm::TypeObject::initializeDatatype( @@ -342,17 +342,16 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, ctypes.push_back(t); to.d_sdt.addConstructor(iden_op, "id", + ctypes, printer::SygusEmptyPrintCallback::getEmptyPC(), - 0, - ctypes); + 0); Trace("sygus-grammar-normalize-chain") << "\tAdding " << t << " to " << to.d_unres_tn << "\n"; /* adds to Root: "type + Root" */ std::vector ctypesp; ctypesp.push_back(t); ctypesp.push_back(to.d_unres_tn); - to.d_sdt.addConstructor( - nm->operatorOf(PLUS), kindToString(PLUS), nullptr, -1, ctypesp); + to.d_sdt.addConstructor(nm->operatorOf(PLUS), kindToString(PLUS), ctypesp); Trace("sygus-grammar-normalize-chain") << "\tAdding PLUS to " << to.d_unres_tn << " with arg types " << to.d_unres_tn << " and " << t << "\n"; @@ -385,9 +384,9 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, ctypes.push_back(sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos)); to.d_sdt.addConstructor(iden_op, "id_next", + ctypes, printer::SygusEmptyPrintCallback::getEmptyPC(), - 0, - ctypes); + 0); } std::map SygusGrammarNorm::d_tn_to_id = {}; -- 2.30.2