From: Andrew Reynolds Date: Wed, 4 Dec 2019 23:18:06 +0000 (-0600) Subject: New grammar construction modes for SyGuS (#3486) X-Git-Tag: cvc5-1.0.0~3799 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd66d825a0e05b46690b0bb914da3b0aa2045654;p=cvc5.git New grammar construction modes for SyGuS (#3486) --- diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index d4194d456..faf358573 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -569,6 +569,29 @@ auto (default) \n\ \n\ "; +const std::string OptionsHandler::s_sygusGrammarConsHelp = + "\ +Modes for default SyGuS grammars, supported by --sygus-grammar-cons:\n\ +\n\ +simple (default) \n\ ++ Use simple grammar construction (no symbolic terms or constants).\n\ +\n\ +any-const \n\ ++ Use symoblic constant constructors.\n\ +\n\ +any-term \n\ ++ When applicable, use constructors corresponding to any symbolic term.\n\ +This option enables a sum-of-monomials grammar for arithmetic. For all\n\ +other types, it enables symbolic constant constructors.\n\ +\n\ +any-term-concise \n\ ++ When applicable, use constructors corresponding to any symbolic term,\n\ +favoring conciseness over generality. This option is equivalent to any-term\n\ +but enables a polynomial grammar for arithmetic when not in a combined\n\ +theory.\n\ +\n\ +"; + const std::string OptionsHandler::s_macrosQuantHelp = "\ Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ \n\ @@ -1085,6 +1108,38 @@ OptionsHandler::stringToSygusActiveGenMode(std::string option, + optarg + "'. Try --sygus-inv-templ help."); } } +theory::quantifiers::SygusGrammarConsMode +OptionsHandler::stringToSygusGrammarConsMode(std::string option, + std::string optarg) +{ + if (optarg == "simple") + { + return theory::quantifiers::SYGUS_GCONS_SIMPLE; + } + else if (optarg == "any-const") + { + return theory::quantifiers::SYGUS_GCONS_ANY_CONST; + } + else if (optarg == "any-term") + { + return theory::quantifiers::SYGUS_GCONS_ANY_TERM; + } + else if (optarg == "any-term-concise") + { + return theory::quantifiers::SYGUS_GCONS_ANY_TERM_CONCISE; + } + else if (optarg == "help") + { + puts(s_sygusGrammarConsHelp.c_str()); + exit(1); + } + else + { + throw OptionException( + std::string("unknown option for --sygus-grammar-cons: `") + optarg + + "'. Try --sygus-grammar-cons help."); + } +} theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode( std::string option, std::string optarg) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 84b7002e3..eae61c5b2 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -122,6 +122,8 @@ public: std::string option, std::string optarg); theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode( std::string option, std::string optarg); + theory::quantifiers::SygusGrammarConsMode stringToSygusGrammarConsMode( + std::string option, std::string optarg); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode( std::string option, std::string optarg); theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode( @@ -275,6 +277,7 @@ public: static const std::string s_sygusFilterSolHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_sygusActiveGenHelp; + static const std::string s_sygusGrammarConsHelp; static const std::string s_termDbModeHelp; static const std::string s_theoryOfModeHelp; static const std::string s_triggerSelModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 049cdef1c..9ff2ac196 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -292,6 +292,29 @@ enum SygusFilterSolMode SYGUS_FILTER_SOL_WEAK, }; +enum SygusGrammarConsMode +{ + /** + * Use simple default SyGuS grammar construction (no symbolic terms or + * constants). + */ + SYGUS_GCONS_SIMPLE, + /** Use "any constant" constructors in default SyGuS grammar construction. */ + SYGUS_GCONS_ANY_CONST, + /** + * When applicable, use constructors that encode any term using "any constant" + * constructors. This construction uses sum-of-monomials for arithmetic + * grammars. + */ + SYGUS_GCONS_ANY_TERM, + /** + * When applicable, use constructors that encode any term using "any constant" + * constructors in a way that prefers conciseness over generality. This + * construction uses polynomials for arithmetic grammars. + */ + SYGUS_GCONS_ANY_TERM_CONCISE, +}; + enum MacrosQuantMode { /** infer all definitions */ MACROS_QUANT_MODE_ALL, diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 019b052bc..171af1e47 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1076,6 +1076,16 @@ header = "options/quantifiers_options.h" read_only = true help = "embed sygus templates into grammars" +[[option]] + name = "sygusGrammarConsMode" + category = "regular" + long = "sygus-grammar-cons=MODE" + type = "CVC4::theory::quantifiers::SygusGrammarConsMode" + default = "CVC4::theory::quantifiers::SYGUS_GCONS_SIMPLE" + handler = "stringToSygusGrammarConsMode" + includes = ["options/quantifiers_modes.h"] + help = "mode for SyGuS grammar construction" + [[option]] name = "sygusInvTemplMode" category = "regular" diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index 5bf0ca036..43d23b523 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -125,8 +125,14 @@ Node mkSygusTerm(const Datatype& dt, Assert(i < dt.getNumConstructors()); Assert(dt.isSygus()); Assert(!dt[i].getSygusOp().isNull()); - std::vector schildren; Node op = Node::fromExpr(dt[i].getSygusOp()); + return mkSygusTerm(op, children, doBetaReduction); +} + +Node mkSygusTerm(Node op, + const std::vector& children, + bool doBetaReduction) +{ Trace("dt-sygus-util") << "Operator is " << op << std::endl; if (children.empty()) { @@ -140,6 +146,7 @@ Node mkSygusTerm(const Datatype& dt, Assert(children.size() == 1); return children[0]; } + std::vector schildren; // get the kind of the operator Kind ok = op.getKind(); if (ok != BUILTIN) diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index 2ac288c4c..5f74a4bee 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -147,6 +147,13 @@ Node mkSygusTerm(const Datatype& dt, unsigned i, const std::vector& children, bool doBetaReduction = true); +/** + * Same as above, but we already have the sygus operator op. The above method + * is syntax sugar for calling this method on dt[i].getSygusOp(). + */ +Node mkSygusTerm(Node op, + const std::vector& children, + bool doBetaReduction = true); /** * n is a builtin term that is an application of operator op. * diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index c806bb1e7..7a9a9ca21 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -77,8 +77,11 @@ bool Cegis::processInitialize(Node conj, for (unsigned i = 0; i < csize; i++) { Trace("cegis") << "...register enumerator " << candidates[i]; + // We use symbolic constants if we are doing repair constants or if the + // grammar construction was not simple. bool useSymCons = false; - if (options::sygusRepairConst()) + if (options::sygusRepairConst() + || options::sygusGrammarConsMode() != SYGUS_GCONS_SIMPLE) { TypeNode ctn = candidates[i].getType(); d_tds->registerSygusType(ctn); diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index b1baed9cb..cf1993efb 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -189,8 +189,13 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, TypeNode ntn = n.getType(); if (!ntn.isDatatype()) { - // sygus datatype fields that are not sygus datatypes are treated as - // abstractions only, hence we disregard this field + // SyGuS datatype fields that are not sygus datatypes are treated as + // abstractions only, hence we disregard this field. It is important + // that users of this method pay special attention to any constants, + // otherwise the explanation n.eqNode(vn) is necessary here. For example, + // any lemma schema that blocks the current value of an enumerator should + // not make any assumptions about the value of the arguments of its any + // constant constructors, since their explanation is not included here. return; } Assert(vn.getKind() == APPLY_CONSTRUCTOR); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index d00df38c5..5e4513ff3 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,6 +20,7 @@ #include "options/quantifiers_options.h" #include "printer/sygus_print_callback.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/synth_conjecture.h" @@ -515,10 +516,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::map sygus_to_builtin; std::vector types; - // collect connected types for each of the variables + // Collect connected types for each of the variables. for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i) { - collectSygusGrammarTypesFor(sygus_vars[i].getType(), types); + TypeNode tni = sygus_vars[i].getType(); + collectSygusGrammarTypesFor(tni, types); } // collect connected types to range collectSygusGrammarTypesFor(range, types); @@ -534,6 +536,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::map type_to_unres; std::map>::const_iterator itc; + // maps types to the index of its "any term" grammar construction + std::map typeToGAnyTerm; + SygusGrammarConsMode sgcm = options::sygusGrammarConsMode(); for (unsigned i = 0, size = types.size(); i < size; ++i) { std::stringstream ss; @@ -556,10 +561,40 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( type_to_unres[types[i]] = unres_t; sygus_to_builtin[unres_t] = types[i]; } - for (unsigned i = 0, size = types.size(); i < size; ++i) + // We ensure an ordering on types such that parametric types are processed + // before their consitituents. Since parametric types were added before their + // arguments in collectSygusGrammarTypesFor above, we will construct the + // sygus grammars by iterating on types in reverse order. This ensures + // that we know all constructors coming from other types (e.g. select(A,i)) + // by the time we process the type. + for (int i = (types.size() - 1); i >= 0; --i) { Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl; TypeNode unres_t = unres_types[i]; + SygusGrammarConsMode tsgcm = sgcm; + if (tsgcm == SYGUS_GCONS_ANY_TERM || tsgcm == SYGUS_GCONS_ANY_TERM_CONCISE) + { + // If the type does not support any term, we do any constant instead. + // We also fall back on any constant construction if the type has no + // constructors at this point (e.g. it simply encodes all constants). + if (!types[i].isReal()) + { + tsgcm = SYGUS_GCONS_ANY_CONST; + } + else + { + // Add a placeholder for the "any term" version of this datatype, to be + // constructed later. + typeToGAnyTerm[types[i]] = sdts.size(); + std::stringstream ssat; + ssat << sdts[i].d_sdt.getName() << "_any_term"; + sdts.push_back(SygusDatatypeGenerator(ssat.str())); + TypeNode unresAnyTerm = mkUnresolvedType(ssat.str(), unres); + unres_types.push_back(unresAnyTerm); + } + } + Trace("sygus-grammar-def") + << "Grammar constructor mode for this type is " << tsgcm << std::endl; //add variables for (const Node& sv : sygus_vars) { @@ -592,29 +627,44 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } } //add constants - std::vector< Node > consts; - mkSygusConstantsForType( types[i], consts ); - std::map>::iterator - itec = extra_cons.find(types[i]); - if( itec!=extra_cons.end() ){ - for (std::unordered_set::iterator set_it = - itec->second.begin(); - set_it != itec->second.end(); - ++set_it) + std::vector consts; + mkSygusConstantsForType(types[i], consts); + if (tsgcm == SYGUS_GCONS_ANY_CONST) + { + // Use the any constant constructor. Notice that for types that don't + // have constants (e.g. uninterpreted or function types), we don't add + // this constructor. + if (!consts.empty()) { - if (std::find(consts.begin(), consts.end(), *set_it) == consts.end()) - { - consts.push_back(*set_it); - } + sdts[i].d_sdt.addAnyConstantConstructor(types[i]); } } - for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j) + else { - std::stringstream ss; - ss << consts[j]; - Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl; - std::vector cargsEmpty; - sdts[i].addConstructor(consts[j], ss.str(), cargsEmpty); + std::map>::iterator + itec = extra_cons.find(types[i]); + if (itec != extra_cons.end()) + { + for (std::unordered_set::iterator set_it = + itec->second.begin(); + set_it != itec->second.end(); + ++set_it) + { + if (std::find(consts.begin(), consts.end(), *set_it) == consts.end()) + { + consts.push_back(*set_it); + } + } + } + for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j) + { + std::stringstream ss; + ss << consts[j]; + Trace("sygus-grammar-def") + << "...add for constant " << ss.str() << std::endl; + std::vector cargsEmpty; + sdts[i].addConstructor(consts[j], ss.str(), cargsEmpty); + } } // ITE Kind k = ITE; @@ -641,12 +691,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << " ...create auxiliary Positive Integers grammar\n"; - /* Creating type for positive integers */ + // Creating type for positive integers. Notice we can't use the any + // constant constructor here, since it admits zero. std::stringstream ss; ss << fun << "_PosInt"; std::string pos_int_name = ss.str(); // make unresolved type - TypeNode unres_pos_int_t = mkUnresolvedType(pos_int_name, unres); + TypeNode unresPosInt = mkUnresolvedType(pos_int_name, unres); + unres_types.push_back(unresPosInt); // make data type for positive constant integers sdts.push_back(SygusDatatypeGenerator(pos_int_name)); /* Add operator 1 */ @@ -657,8 +709,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Kind k = PLUS; Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n"; std::vector cargsPlus; - cargsPlus.push_back(unres_pos_int_t); - cargsPlus.push_back(unres_pos_int_t); + cargsPlus.push_back(unresPosInt); + cargsPlus.push_back(unresPosInt); sdts.back().addConstructor(k, cargsPlus); sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true); Trace("sygus-grammar-def") @@ -668,7 +720,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "\t...add for " << k << std::endl; std::vector cargsDiv; cargsDiv.push_back(unres_t); - cargsDiv.push_back(unres_pos_int_t); + cargsDiv.push_back(unresPosInt); sdts[i].addConstructor(k, cargsDiv); } } @@ -812,7 +864,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( << types[i] << std::endl; } } - // make datatypes + std::map::iterator itgat; + // initialize the datatypes for (unsigned i = 0, size = types.size(); i < size; ++i) { sdts[i].d_sdt.initializeDatatype(types[i], bvl, true, true); @@ -822,8 +875,227 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( if( types[i]==range ){ startIndex = i; } - } + itgat = typeToGAnyTerm.find(types[i]); + if (itgat == typeToGAnyTerm.end()) + { + // no any term datatype, we are done + continue; + } + Trace("sygus-grammar-def") + << "Build any-term datatype for " << types[i] << "..." << std::endl; + unsigned iat = itgat->second; + // for now, only real has any term construction + Assert(types[i].isReal()); + // We have initialized the given type sdts[i], which should now contain + // a constructor for each relevant arithmetic term/variable. We now + // construct a sygus datatype of one of the following two forms. + // + // (1) The "sum of monomials" grammar: + // I -> C*x1 | ... | C*xn | C | I + I | ite( B, I, I ) + // C -> any_constant + // where x1, ..., xn are the arithmetic terms/variables (non-arithmetic + // builtin operators) terms we have considered thus far. + // + // (2) The "polynomial" grammar: + // I -> C*x1 + ... + C*xn + C | ite( B, I, I ) + // C -> any_constant + // + // The advantage of the first is that it allows for sums of terms + // constructible from other theories that share sorts with arithmetic, e.g. + // c1*str.len(x) + c2*str.len(y) + // The advantage of the second is that there are fewer constructors, and + // hence may be more efficient. + // Before proceeding, we build the any constant datatype + Trace("sygus-grammar-def") + << "Build any-constant datatype for " << types[i] << std::endl; + std::stringstream ss; + ss << fun << "_AnyConst"; + // Make sygus datatype for any constant. + TypeNode unresAnyConst = mkUnresolvedType(ss.str(), unres); + unres_types.push_back(unresAnyConst); + sdts.push_back(SygusDatatypeGenerator(ss.str())); + sdts.back().d_sdt.addAnyConstantConstructor(types[i]); + sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true); + + // Now get the reference to the sygus datatype at position i (important that + // this comes after the modification to sdts above, which may modify + // the references). + const SygusDatatype& sdti = sdts[i].d_sdt; + // whether we will use the polynomial grammar + bool polynomialGrammar = sgcm == SYGUS_GCONS_ANY_TERM_CONCISE; + // A set of constructor indices that will be used in the overall sum we + // are constructing; indices of constructors corresponding to builtin + // arithmetic operators will be excluded from this set. + std::set useConstructor; + Trace("sygus-grammar-def") + << "Look at operators, num = " << sdti.getNumConstructors() << "..." + << std::endl; + for (unsigned k = 0, ncons = sdti.getNumConstructors(); k < ncons; k++) + { + const SygusDatatypeConstructor& sdc = sdti.getConstructor(k); + Node sop = sdc.d_op; + bool isBuiltinArithOp = (sop.getKind() == CONST_RATIONAL); + bool hasExternalType = false; + for (unsigned j = 0, nargs = sdc.d_argTypes.size(); j < nargs; j++) + { + // Since we are accessing the fields of the sygus datatype, this + // already corresponds to the correct sygus datatype type. + TypeNode atype = sdc.d_argTypes[j]; + if (atype == unres_types[i]) + { + // It is recursive, thus is (likely) a builtin arithmetic operator + // as constructed above. It may also be an operator from another + // theory that has both an arithmetic return type and an arithmetic + // argument (e.g. str.indexof). In either case, we ignore it for the + // sake of well-foundedness. + isBuiltinArithOp = true; + break; + } + else if (atype != unres_bt) + { + // It is an external type. This is the case of an operator of another + // theory whose return type is arithmetic, e.g. select. + hasExternalType = true; + } + } + if (!isBuiltinArithOp) + { + useConstructor.insert(k); + if (hasExternalType) + { + // If we have an external term in the sum, e.g. select(A,i), we + // cannot use a fixed polynomial template. As mentioned above, we + // cannot use a polynomial grammar when external terms (those built + // from the symbols of other theories) are involved. + Trace("sygus-grammar-def") + << "Cannot use polynomial grammar due to " << sop << std::endl; + polynomialGrammar = false; + } + } + } + Trace("sygus-grammar-def") + << "Done look at operators, num = " << sdti.getNumConstructors() + << "..." << std::endl; + // we have now decided whether we will use sum-of-monomials or polynomial + // Now, extract the terms and set up the polynomial + std::vector sumChildren; + std::vector cargsAnyTerm; + std::vector lambdaVars; + for (unsigned k = 0, ncons = sdti.getNumConstructors(); k < ncons; k++) + { + Trace("sygus-grammar-def") << "Process #" << k << std::endl; + if (useConstructor.find(k) == useConstructor.end()) + { + Trace("sygus-grammar-def") << "Skip variable #" << k << std::endl; + // builtin operator, as computed above, we skip + continue; + } + const SygusDatatypeConstructor& sdc = sdti.getConstructor(k); + Node sop = sdc.d_op; + Trace("sygus-grammar-def") + << "Monomial variable: #" << k << ": " << sop << std::endl; + unsigned nargs = sdc.d_argTypes.size(); + std::vector opCArgs; + std::vector opLArgs; + if (nargs > 0) + { + // Take its arguments. For example, if we are building a polynomial + // over str.len(s), then our any term constructor would include an + // argument of string type, e.g.: + // (lambda s : String, c1, c2 : Int. c1*len(s) + c2) + for (unsigned j = 0; j < nargs; j++) + { + // this is already corresponds to the correct sygus datatype type + TypeNode atype = sdc.d_argTypes[j]; + opCArgs.push_back(atype); + // get the builtin type + TypeNode btype = sygus_to_builtin[atype]; + opLArgs.push_back(nm->mkBoundVar(btype)); + } + // Do beta reduction on the operator so that its arguments match the + // fresh variables of the lambda (op) we are constructing below. + sop = datatypes::utils::mkSygusTerm(sop, opLArgs); + sop = Rewriter::rewrite(sop); + } + opCArgs.push_back(unresAnyConst); + Node coeff = nm->mkBoundVar(types[i]); + opLArgs.push_back(coeff); + Node monomial = nm->mkNode(MULT, coeff, sop); + if (polynomialGrammar) + { + // add the monomial c*t to the sum + sumChildren.push_back(monomial); + lambdaVars.insert(lambdaVars.end(), opLArgs.begin(), opLArgs.end()); + cargsAnyTerm.insert(cargsAnyTerm.end(), opCArgs.begin(), opCArgs.end()); + } + else + { + Node op = + nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), monomial); + // use a print callback since we do not want to print the lambda + std::shared_ptr spc; + std::vector opLArgsExpr; + for (unsigned i = 0, nvars = opLArgs.size(); i < nvars; i++) + { + opLArgsExpr.push_back(opLArgs[i].toExpr()); + } + spc = std::make_shared( + monomial.toExpr(), opLArgsExpr); + // add it as a constructor + std::stringstream ssop; + ssop << "monomial_" << sdc.d_name; + sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, spc); + } + } + if (polynomialGrammar) + { + // add the constant + Node coeff = nm->mkBoundVar(types[i]); + lambdaVars.push_back(coeff); + cargsAnyTerm.push_back(unresAnyConst); + // make the sygus operator lambda X. c1*t1 + ... + cn*tn + c + Assert(sumChildren.size() > 1); + Node ops = nm->mkNode(PLUS, sumChildren); + Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops); + std::shared_ptr spc; + std::vector lambdaVarsExpr; + for (unsigned i = 0, nvars = lambdaVars.size(); i < nvars; i++) + { + lambdaVarsExpr.push_back(lambdaVars[i].toExpr()); + } + spc = std::make_shared(ops.toExpr(), + lambdaVarsExpr); + Trace("sygus-grammar-def") << "any term operator is " << op << std::endl; + // make the any term datatype, add to back + // do not consider the exclusion criteria of the generator + sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc); + } + else + { + // add the any constant constructor as a separate constructor + sdts[iat].d_sdt.addAnyConstantConstructor(types[i]); + // add plus + std::vector cargsPlus; + cargsPlus.push_back(unres_types[iat]); + cargsPlus.push_back(unres_types[iat]); + sdts[iat].d_sdt.addConstructor(PLUS, cargsPlus); + } + // add the ITE, regardless of sum-of-monomials vs polynomial + std::vector cargsIte; + cargsIte.push_back(unres_bt); + cargsIte.push_back(unres_types[iat]); + cargsIte.push_back(unres_types[iat]); + sdts[iat].d_sdt.addConstructor(ITE, cargsIte); + sdts[iat].d_sdt.initializeDatatype(types[i], bvl, true, true); + Trace("sygus-grammar-def") + << "...built datatype " << sdts[iat].d_sdt.getDatatype() << std::endl; + // if the type is range, use it as the default type + if (types[i] == range) + { + startIndex = iat; + } + } //------ make Boolean type TypeNode btype = nm->booleanType(); sdts.push_back(SygusDatatypeGenerator(dbname)); @@ -860,6 +1132,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { continue; } + unsigned iuse = i; + // use the any-term type if it exists + itgat = typeToGAnyTerm.find(types[i]); + if (itgat != typeToGAnyTerm.end()) + { + iuse = itgat->second; + } Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl; //add equality per type Kind k = EQUAL; @@ -867,8 +1146,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::stringstream ss; ss << kindToString(k) << "_" << types[i]; std::vector cargsBinary; - cargsBinary.push_back(unres_types[i]); - cargsBinary.push_back(unres_types[i]); + cargsBinary.push_back(unres_types[iuse]); + cargsBinary.push_back(unres_types[iuse]); sdtBool.addConstructor(nm->operatorOf(k), ss.str(), cargsBinary); // type specific predicates if (types[i].isReal()) @@ -889,7 +1168,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for testers" << std::endl; const Datatype& dt = types[i].getDatatype(); std::vector cargsTester; - cargsTester.push_back(unres_types[i]); + cargsTester.push_back(unres_types[iuse]); for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) { Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cf06d2e90..7d3fb2d5c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1713,6 +1713,7 @@ set(regress_1_tests regress1/sygus/icfp_14_12_diff_types.sy regress1/sygus/icfp_28_10.sy regress1/sygus/icfp_easy-ite.sy + regress1/sygus/int-any-const.sy regress1/sygus/inv-example.sy regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy @@ -1750,6 +1751,7 @@ set(regress_1_tests regress1/sygus/process-10-vars.sy regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 + regress1/sygus/real-any-const.sy regress1/sygus/real-grammar.sy regress1/sygus/rec-fun-swap.sy regress1/sygus/rec-fun-sygus.sy @@ -1760,6 +1762,7 @@ set(regress_1_tests regress1/sygus/repair-const-rl.sy regress1/sygus/simple-regexp.sy regress1/sygus/stopwatch-bt.sy + regress1/sygus/strings-any-term1.sy regress1/sygus/strings-no-syntax.sy regress1/sygus/strings-concat-3-args.sy regress1/sygus/strings-double-rec.sy @@ -1924,6 +1927,7 @@ set(regress_3_tests regress3/pp-regfile.smtv1.smt2 regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2 regress3/sixfuncs.sy + regress3/strings-any-term.sy regress3/strings/extf_d_perf.smt2 ) diff --git a/test/regress/regress1/sygus/int-any-const.sy b/test/regress/regress1/sygus/int-any-const.sy new file mode 100644 index 000000000..b5de57533 --- /dev/null +++ b/test/regress/regress1/sygus/int-any-const.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise + +(set-logic LIA) +(synth-fun f ((x Int) (y Int)) Int) +(constraint (= (f 1 7) 15)) +(constraint (= (f 0 27) 27)) +(constraint (= (f 2 27) 43)) +; this example does not fit the polynomial solution to the above example, thus, we expect to construct an ITE +(constraint (= (f 3 27) 43)) +(check-synth) diff --git a/test/regress/regress1/sygus/real-any-const.sy b/test/regress/regress1/sygus/real-any-const.sy new file mode 100644 index 000000000..2b59b7301 --- /dev/null +++ b/test/regress/regress1/sygus/real-any-const.sy @@ -0,0 +1,9 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise + +(set-logic LRA) +(synth-fun f ((x Real) (y Real)) Real) +(constraint (= (f 1.5 7.5) 59.7)) +(constraint (= (f 0.5 27.5) 174.9)) +(constraint (= (f 0.8 20.0) 131.04)) +(check-synth) diff --git a/test/regress/regress1/sygus/strings-any-term1.sy b/test/regress/regress1/sygus/strings-any-term1.sy new file mode 100644 index 000000000..3d8fd7530 --- /dev/null +++ b/test/regress/regress1/sygus/strings-any-term1.sy @@ -0,0 +1,10 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term +(set-logic ALL) +(synth-fun f ((x String) (y String)) Int) +(declare-var x String) +(constraint (= (f "A" "BC") 11)) +(constraint (= (f "BB" "CC") 18)) +(constraint (= (f "BCB" "") 25)) +(constraint (= (f "BCBD" "") 32)) +(check-synth) diff --git a/test/regress/regress3/strings-any-term.sy b/test/regress/regress3/strings-any-term.sy new file mode 100644 index 000000000..88b30b208 --- /dev/null +++ b/test/regress/regress3/strings-any-term.sy @@ -0,0 +1,10 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none +(set-logic ALL) +(synth-fun f ((x String) (y String)) Int) +(declare-var x String) +(constraint (= (f "A" "BC") 207)) +(constraint (= (f "BB" "CC") 214)) +(constraint (= (f "BCB" "") 21)) +(constraint (= (f "BCBD" "") 28)) +(check-synth)