diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 65 |
1 files changed, 35 insertions, 30 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index f4cdc22c5..8a415cc10 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -106,36 +106,6 @@ void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm, sygus_norm->d_sygus_vars.toExpr(), dt.getSygusAllowConst(), dt.getSygusAllowAll()); - if (dt.getSygusAllowConst()) - { - TypeNode sygus_type = TypeNode::fromType(dt.getSygusType()); - // must be handled by counterexample-guided instantiation - // don't do it for Boolean (not worth the trouble, since it has only - // minimal gain (1 any constant vs 2 constructors for true/false), and - // we need to do a lot of special symmetry breaking, e.g. for ensuring - // any constant constructors are not the 1st children of ITEs. - if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED - && !sygus_type.isBoolean()) - { - Trace("sygus-grammar-normalize") << "...add any constant constructor.\n"; - // add an "any constant" proxy variable - Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type); - // mark that it represents any constant - SygusAnyConstAttribute saca; - av.setAttribute(saca, true); - std::stringstream ss; - ss << d_unres_tn << "_any_constant"; - std::string cname(ss.str()); - std::vector<Type> builtin_arg; - builtin_arg.push_back(dt.getSygusType()); - // we add this constructor first since we use left associative chains - // and our symmetry breaking should group any constants together - // beneath the same application - // we set its weight to zero since it should be considered at the - // same level as constants. - d_dt.addSygusConstructor(av.toExpr(), cname, builtin_arg, nullptr, 0); - } - } for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i) { d_dt.addSygusConstructor(d_ops[i].toExpr(), @@ -462,6 +432,41 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, Assert(op_pos[i] < dt.getNumConstructors()); to.addConsInfo(this, dt[op_pos[i]]); } + if (dt.getSygusAllowConst()) + { + TypeNode sygus_type = TypeNode::fromType(dt.getSygusType()); + // must be handled by counterexample-guided instantiation + // don't do it for Boolean (not worth the trouble, since it has only + // minimal gain (1 any constant vs 2 constructors for true/false), and + // we need to do a lot of special symmetry breaking, e.g. for ensuring + // any constant constructors are not the 1st children of ITEs. + if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED + && !sygus_type.isBoolean()) + { + Trace("sygus-grammar-normalize") << "...add any constant constructor.\n"; + // add an "any constant" proxy variable + Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type); + // mark that it represents any constant + SygusAnyConstAttribute saca; + av.setAttribute(saca, true); + std::stringstream ss; + ss << to.d_unres_tn << "_any_constant"; + std::string cname(ss.str()); + std::vector<Type> builtin_arg; + builtin_arg.push_back(dt.getSygusType()); + // we add this constructor first since we use left associative chains + // and our symmetry breaking should group any constants together + // beneath the same application + // we set its weight to zero since it should be considered at the + // same level as constants. + to.d_ops.insert(to.d_ops.begin(), av.toExpr()); + to.d_cons_names.insert(to.d_cons_names.begin(), cname); + to.d_cons_args_t.insert(to.d_cons_args_t.begin(), builtin_arg); + to.d_pc.insert(to.d_pc.begin(), + printer::SygusEmptyPrintCallback::getEmptyPC()); + to.d_weight.insert(to.d_weight.begin(), 0); + } + } /* Build normalize datatype */ if (Trace.isOn("sygus-grammar-normalize")) { |