diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 113 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 23 |
2 files changed, 117 insertions, 19 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 1adc3123e..8df43087f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -487,6 +487,37 @@ bool CegGrammarConstructor::isHandledType(TypeNode t) return true; } +Node CegGrammarConstructor::createLambdaWithZeroArg( + Kind k, TypeNode bArgType, std::shared_ptr<SygusPrintCallback> spc) +{ + NodeManager* nm = NodeManager::currentNM(); + std::vector<Node> opLArgs; + std::vector<Expr> opLArgsExpr; + // get the builtin type + opLArgs.push_back(nm->mkBoundVar(bArgType)); + opLArgsExpr.push_back(opLArgs.back().toExpr()); + // build zarg + Node zarg; + Assert(bArgType.isReal() || bArgType.isBitVector()); + if (bArgType.isReal()) + { + zarg = nm->mkConst(Rational(0)); + } + else + { + unsigned size = bArgType.getBitVectorSize(); + zarg = bv::utils::mkZero(size); + } + Node body = nm->mkNode(k, zarg, opLArgs.back()); + // use a print callback since we do not want to print the lambda + spc = std::make_shared<printer::SygusExprPrintCallback>(body.toExpr(), + opLArgsExpr); + // create operator + Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), body); + Trace("sygus-grammar-def") << "\t...building lambda op " << op << "\n"; + return op; +} + void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, @@ -543,7 +574,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::const_iterator itc; // maps types to the index of its "any term" grammar construction - std::map<TypeNode, unsigned> typeToGAnyTerm; + std::map<TypeNode, std::pair<unsigned, bool>> typeToGAnyTerm; options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode(); for (unsigned i = 0, size = types.size(); i < size; ++i) { @@ -589,7 +620,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // we construct the grammar for the Boolean type last. for (int i = (types.size() - 2); i >= 0; --i) { - Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl; + Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " + << unres_types[i] << std::endl; TypeNode unres_t = unres_types[i]; options::SygusGrammarConsMode tsgcm = sgcm; if (tsgcm == options::SygusGrammarConsMode::ANY_TERM @@ -606,12 +638,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { // 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); + // set tracking information for later addition at boolean type. + std::pair<unsigned, bool> p(sdts.size() - 1, false); + typeToGAnyTerm[types[i]] = p; } } Trace("sygus-grammar-def") @@ -916,7 +950,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargsIte.push_back(unres_t); sdts[i].addConstructor(k, cargsIte); } - std::map<TypeNode, unsigned>::iterator itgat; + std::map<TypeNode, std::pair<unsigned, bool>>::iterator itgat; // initialize the datatypes (except for the last one, reserved for Bool) for (unsigned i = 0, size = types.size() - 1; i < size; ++i) { @@ -933,9 +967,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // no any term datatype, we are done continue; } + unsigned iat = itgat->second.first; 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 @@ -1132,6 +1167,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // This ensures that ( c1*x + c2*y >= 0 ) has the same weight as // e.g. ( x >= 0 ) or ( y >= 0 ). sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc, 0); + // mark that predicates should be of the form (= pol 0) and (<= pol 0) + itgat->second.second = true; } else { @@ -1193,34 +1230,76 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( continue; } unsigned iuse = i; - // use the any-term type if it exists + bool zarg = false; + // use the any-term type if it exists and a zero argument if it is a + // polynomial grammar itgat = typeToGAnyTerm.find(types[i]); if (itgat != typeToGAnyTerm.end()) { - iuse = itgat->second; + iuse = itgat->second.first; + zarg = itgat->second.second; + Trace("sygus-grammar-def") + << "...unres type " << unres_types[i] << " became " + << (!zarg ? "polynomial " : "") << "unres anyterm type " + << unres_types[iuse] << "\n"; } Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl; //add equality per type Kind k = EQUAL; Trace("sygus-grammar-def") << "...add for " << k << std::endl; std::stringstream ss; - ss << kindToString(k) << "_" << types[i]; - std::vector<TypeNode> cargsBinary; - cargsBinary.push_back(unres_types[iuse]); - cargsBinary.push_back(unres_types[iuse]); - sdtBool.addConstructor(nm->operatorOf(k), ss.str(), cargsBinary); + std::vector<TypeNode> cargs; + cargs.push_back(unres_types[iuse]); + // if polynomial grammar, generate (= anyterm 0) and (<= anyterm 0) as the + // predicates + if (zarg) + { + std::shared_ptr<SygusPrintCallback> spc; + Node op = createLambdaWithZeroArg(k, types[i], spc); + ss << "eq_" << types[i]; + sdtBool.addConstructor(op, ss.str(), cargs); + } + else + { + ss << kindToString(k) << "_" << types[i]; + cargs.push_back(unres_types[iuse]); + sdtBool.addConstructor(nm->operatorOf(k), ss.str(), cargs); + cargs.pop_back(); + } // type specific predicates + std::shared_ptr<SygusPrintCallback> spc; + std::stringstream ssop; if (types[i].isReal()) { Kind kind = LEQ; - Trace("sygus-grammar-def") << "...add for " << kind << std::endl; - sdtBool.addConstructor(kind, cargsBinary); + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + if (zarg) + { + Node op = createLambdaWithZeroArg(kind, types[i], spc); + ssop << "leq_" << types[i]; + sdtBool.addConstructor(op, ssop.str(), cargs); + } + else + { + cargs.push_back(unres_types[iuse]); + sdtBool.addConstructor(kind, cargs); + } } else if (types[i].isBitVector()) { Kind kind = BITVECTOR_ULT; - Trace("sygus-grammar-def") << "...add for " << kind << std::endl; - sdtBool.addConstructor(kind, cargsBinary); + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + if (zarg) + { + Node op = createLambdaWithZeroArg(kind, types[i], spc); + ssop << "leq_" << types[i]; + sdtBool.addConstructor(op, ssop.str(), cargs); + } + else + { + cargs.push_back(unres_types[iuse]); + sdtBool.addConstructor(kind, cargs); + } } else if (types[i].isDatatype()) { @@ -1254,6 +1333,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } // add Boolean connectives, if not in a degenerate case of (recursively) // having only constant constructors + Trace("sygus-grammar-def") + << "...add Boolean connectives for unres type " << unres_bt << std::endl; if (sdtBool.d_sdt.getNumConstructors() > consts.size()) { for (unsigned i = 0; i < 4; i++) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 1abe8bf5f..b0c575809 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -100,7 +100,7 @@ public: * - term_irrelevant: a set of terms that should not be included in the * grammar. * - include_cons: a set of operators such that if this set is not empty, - * its elements that are in the default grammar (and only them) + * its elements that are in the default grammar (and only them) * will be included. */ static TypeNode mkSygusDefaultType( @@ -248,8 +248,25 @@ public: std::set<Type>& unres); // helper function for mkSygusTemplateType - static TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, - const std::string& fun, unsigned& tcount ); + static TypeNode mkSygusTemplateTypeRec(Node templ, + Node templ_arg, + TypeNode templ_arg_sygus_type, + Node bvl, + const std::string& fun, + unsigned& tcount); + + /** + * Given a kind k, create a lambda operator with the given builtin input type + * and an extra zero argument of that same type. For example, for k = LEQ and + * bArgType = Int, the operator will be lambda x : Int. x + 0. Currently the + * supported input types are Real (thus also Int) and BitVector. + * + * This method also creates a print callback for the operator, saved via the + * argument spc, if the caller wishes to not print the lambda. + */ + static Node createLambdaWithZeroArg(Kind k, + TypeNode bArgType, + std::shared_ptr<SygusPrintCallback> spc); //---------------- end grammar construction }; |