From 2ac3d0bf2c00edbbd04033815f10ba0207010f77 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 May 2018 20:27:32 -0500 Subject: [PATCH] Repair constants using symbolic constructors (#1960) --- src/options/quantifiers_options.toml | 2 +- src/theory/datatypes/datatypes_sygus.cpp | 102 +++++++++-- .../quantifiers/cegqi/ceg_instantiator.h | 5 - .../sygus/ce_guided_conjecture.cpp | 22 --- src/theory/quantifiers/sygus/cegis.cpp | 69 ++++++- src/theory/quantifiers/sygus/cegis.h | 12 +- .../quantifiers/sygus/sygus_grammar_norm.cpp | 28 +++ .../quantifiers/sygus/sygus_grammar_norm.h | 6 + .../quantifiers/sygus/sygus_repair_const.cpp | 115 ++++++++---- .../quantifiers/sygus/sygus_repair_const.h | 42 +++-- .../quantifiers/sygus/term_database_sygus.cpp | 171 +++++++++++++++--- .../quantifiers/sygus/term_database_sygus.h | 54 +++++- test/regress/Makefile.tests | 2 - test/regress/regress0/expect/scrub.07.sy | 7 - .../regress0/expect/scrub.07.sy.expect | 5 - test/regress/regress2/sygus/ex23.sy | 4 +- 16 files changed, 503 insertions(+), 143 deletions(-) delete mode 100644 test/regress/regress0/expect/scrub.07.sy delete mode 100644 test/regress/regress0/expect/scrub.07.sy.expect diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 107f3896f..4a7004821 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -989,7 +989,7 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-repair-const" type = "bool" - default = "true" + default = "false" help = "use approach to repair constants in sygus candidate solutions" [[option]] diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 15c071431..d4a21ea2f 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -408,6 +408,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned //symmetry breaking Kind nk = d_tds->getConsNumKind( tn, tindex ); if( options::sygusSymBreak() ){ + NodeManager* nm = NodeManager::currentNM(); // if less than the maximum depth we consider if( depth<2 ){ //get children @@ -480,13 +481,37 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned if( nk==STRING_STRREPL ){ deq_child[0].push_back( 0 );deq_child[1].push_back( 1 ); } + // this code adds simple symmetry breaking predicates of the form + // d.i != d.j, for example if we are considering an ITE constructor, + // we enforce that d.1 != d.2 since otherwise the ITE can be + // simplified. for( unsigned i=0; igetAnyConstantConsNum(tnc); + if (anyc_cons_num_c != -1) + { + const Datatype& cdt = + static_cast(tnc.toType()).getDatatype(); + Node guard_val = nm->mkNode( + APPLY_CONSTRUCTOR, + Node::fromExpr(cdt[anyc_cons_num_c].getConstructor())); + Node exp = d_tds->getExplain()->getExplanationForEquality( + children[c1], guard_val); + sym_lem_deq = nm->mkNode(OR, exp, sym_lem_deq); } + sbp_conj.push_back(sym_lem_deq); } } @@ -520,12 +545,19 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned // if not already solved if( children_solved.find( j )==children_solved.end() ){ TypeNode tnc = nc.getType(); + int anyc_cons_num = d_tds->getAnyConstantConsNum(tnc); const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype(); for( unsigned k=0; kgetConsNumKind(tnc, k); bool red = false; // check if the argument is redundant - if (nck != UNDEFINED_KIND) + if (static_cast(k) == anyc_cons_num) + { + // check if the any constant constructor is redundant at + // this argument position + // TODO + } + else if (nck != UNDEFINED_KIND) { Trace("sygus-sb-simple-debug") << " argument " << j << " " << k << " is : " << nck @@ -558,6 +590,42 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned }else{ // defined function? } + // explicitly handle "any constant" constructors + // if this type admits any constant, then at least one of my children + // must not be the "any constant" constructor + unsigned dt_index_nargs = dt[tindex].getNumArgs(); + int tn_ac = d_tds->getAnyConstantConsNum(tn); + if (tn_ac != -1 && dt_index_nargs > 0) + { + std::vector exp_all_anyc; + bool success = true; + for (unsigned j = 0; j < dt_index_nargs; j++) + { + TypeNode ctn = TypeNode::fromType(dt[tindex].getArgType(j)); + int ctn_ac = d_tds->getAnyConstantConsNum(ctn); + if (ctn_ac == -1) + { + success = false; + break; + } + Node nc = children[j]; + TypeNode tnc = nc.getType(); + const Datatype& cdt = + static_cast(tnc.toType()).getDatatype(); + exp_all_anyc.push_back( + DatatypesRewriter::mkTester(nc, ctn_ac, cdt)); + } + if (success) + { + Node expaan = exp_all_anyc.size() == 1 + ? exp_all_anyc[0] + : nm->mkNode(AND, exp_all_anyc); + expaan = expaan.negate(); + Trace("sygus-sb-simple-debug") + << "Ensure not all any constant: " << expaan << std::endl; + sbp_conj.push_back(expaan); + } + } }else if( depth==2 ){ if( nk!=UNDEFINED_KIND ){ // commutative operators @@ -845,12 +913,17 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, st void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, Node a, std::vector< Node >& lemmas ) { Assert( t.getType()==tn ); Assert( !a.isNull() ); + Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d + << " " << a << std::endl; std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = d_cache[a].d_sb_lemmas.find( tn ); if( its != d_cache[a].d_sb_lemmas.end() ){ TNode x = getFreeVar( tn ); //get symmetry breaking lemmas for this term unsigned csz = getSearchSizeForAnchor( a ); int max_sz = ((int)csz) - ((int)d); + Trace("sygus-sb-debug2") + << "add lemmas up to size " << max_sz << ", which is (search_size) " + << csz << " - (depth) " << d << std::endl; for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){ if( (int)it->first<=max_sz ){ for( unsigned k=0; ksecond.size(); k++ ){ @@ -860,6 +933,7 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No } } } + Trace("sygus-sb-debug2") << "...finished." << std::endl; } void SygusSymBreakNew::addSymBreakLemma(Node lem, @@ -1047,16 +1121,22 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { { for (const Node& a : anchors) { - std::vector sbl; - d_tds->getSymBreakLemmas(a, sbl); - for (const Node& lem : sbl) + // is this a registered enumerator? + if (d_register_st.find(a) != d_register_st.end()) { - TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); - unsigned sz = d_tds->getSizeForSymBreakLemma(lem); - registerSymBreakLemma(tn, lem, sz, a, lemmas); + // symmetry breaking lemmas should only be for enumerators + Assert(d_register_st[a]); + std::vector sbl; + d_tds->getSymBreakLemmas(a, sbl); + for (const Node& lem : sbl) + { + TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); + unsigned sz = d_tds->getSizeForSymBreakLemma(lem); + registerSymBreakLemma(tn, lem, sz, a, lemmas); + } + d_tds->clearSymBreakLemmas(a); } } - d_tds->clearSymBreakLemmas(); if (!lemmas.empty()) { return; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index b1da66d18..e7deb6a1a 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -23,11 +23,6 @@ namespace CVC4 { namespace theory { - -namespace arith { - class TheoryArith; -} - namespace quantifiers { class CegqiOutput { diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 6f5709fc2..f66a97ce8 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -258,28 +258,6 @@ void CegConjecture::doCheck(std::vector& lems) std::vector candidate_values; bool constructed_cand = false; - if (options::sygusRepairConst()) - { - // have we tried to repair the previous solution? - // if not, call the repair constant utility - unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size(); - if (d_repair_index < ninst) - { - std::vector fail_cvs; - for (const Node& cprog : d_candidates) - { - Assert(d_repair_index < d_cinfo[cprog].d_inst.size()); - fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]); - } - d_repair_index++; - if (d_sygus_rconst->repairSolution( - d_candidates, fail_cvs, candidate_values)) - { - constructed_cand = true; - } - } - } - // get the model value of the relevant terms from the master module std::vector enum_values; getModelValues(terms, enum_values); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index fc41c7561..92ed41f3d 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -29,7 +29,7 @@ namespace theory { namespace quantifiers { Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) - : SygusModule(qe, p), d_eval_unfold(nullptr) + : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false) { if (options::sygusEvalUnfold()) { @@ -66,10 +66,27 @@ bool Cegis::processInitialize(Node n, const std::vector& candidates, std::vector& lemmas) { + Trace("cegis") << "Initialize cegis..." << std::endl; // initialize an enumerator for each candidate for (unsigned i = 0; i < candidates.size(); i++) { - d_tds->registerEnumerator(candidates[i], candidates[i], d_parent); + Trace("cegis") << "...register enumerator " << candidates[i]; + bool do_repair_const = false; + if (options::sygusRepairConst()) + { + TypeNode ctn = candidates[i].getType(); + d_tds->registerSygusType(ctn); + if (d_tds->hasSubtermSymbolicCons(ctn)) + { + do_repair_const = true; + // remember that we are doing grammar-based repair + d_using_gr_repair = true; + Trace("cegis") << " (using repair)"; + } + } + Trace("cegis") << std::endl; + d_tds->registerEnumerator( + candidates[i], candidates[i], d_parent, false, do_repair_const); } return true; } @@ -156,6 +173,46 @@ bool Cegis::constructCandidates(const std::vector& enums, Trace("cegis") << ss.str() << std::endl; } } + // if we are using grammar-based repair + if (d_using_gr_repair) + { + SygusRepairConst* src = d_parent->getRepairConst(); + Assert(src != nullptr); + // check if any enum_values have symbolic terms that must be repaired + bool mustRepair = false; + for (const Node& c : enum_values) + { + if (SygusRepairConst::mustRepair(c)) + { + mustRepair = true; + break; + } + } + Trace("cegis") << "...must repair is: " << mustRepair << std::endl; + // if the solution contains a subterm that must be repaired + if (mustRepair) + { + std::vector fail_cvs = enum_values; + Assert(candidates.size() == fail_cvs.size()); + if (src->repairSolution(candidates, fail_cvs, candidate_values)) + { + return true; + } + // repair solution didn't work, exclude this solution + std::vector exp; + for (unsigned i = 0, size = enums.size(); i < size; i++) + { + d_tds->getExplain()->getExplanationForEquality( + enums[i], enum_values[i], exp); + } + Assert(!exp.empty()); + Node expn = + exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp); + lems.push_back(expn.negate()); + return false; + } + } + // evaluate on refinement lemmas bool addedEvalLemmas = addEvalLemmas(enums, enum_values); @@ -197,14 +254,6 @@ bool Cegis::processConstructCandidates(const std::vector& enums, candidate_values.end(), enum_values.begin(), enum_values.end()); return true; } - SygusRepairConst* src = d_parent->getRepairConst(); - if (src != nullptr) - { - // it may be repairable - std::vector fail_cvs = enum_values; - Assert(candidates.size() == fail_cvs.size()); - return src->repairSolution(candidates, fail_cvs, candidate_values); - } return false; } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 70f3ce8b6..ca27a2281 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -79,7 +79,7 @@ class Cegis : public SygusModule virtual bool processInitialize(Node n, const std::vector& candidates, std::vector& lemmas); - /** do cegis-implementation-specific construct candidate + /** do cegis-implementation-specific post-processing for construct candidate * * satisfiedRl is whether all refinement lemmas are satisfied under the * substitution { enums -> enum_values }. @@ -164,6 +164,16 @@ class Cegis : public SygusModule * added as refinement lemmas. */ std::unordered_set d_cegis_sample_refine; + + //---------------------------------for sygus repair + /** are we using grammar-based repair? + * + * This flag is set ot true if at least one of the enumerators allocated + * by this class has been configured to allow model values with symbolic + * constructors, such as the "any constant" constructor. + */ + bool d_using_gr_repair; + //---------------------------------end for sygus repair }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 73311b0bd..a468e1383 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -20,6 +20,7 @@ #include "printer/sygus_print_callback.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -104,6 +105,33 @@ 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 empty_arg_types; + // we add this constructor first since we use left associative chains + // and our symmetry breaking should group any constants together + // beneath the same application + d_dt.addSygusConstructor(av.toExpr(), cname, empty_arg_types); + } + } for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i) { d_dt.addSygusConstructor(d_ops[i].toExpr(), diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index f72a83e5a..47cc19377 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -36,6 +36,12 @@ namespace quantifiers { class SygusGrammarNorm; +/** Attribute true for variables that represent any constant */ +struct SygusAnyConstAttributeId +{ +}; +typedef expr::Attribute SygusAnyConstAttribute; + /** Operator position trie class * * This data structure stores an unresolved type corresponding to the diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index f9208599f..77930fb42 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -20,6 +20,7 @@ #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; @@ -83,7 +84,8 @@ void SygusRepairConst::registerSygusType(TypeNode tn, bool SygusRepairConst::repairSolution(const std::vector& candidates, const std::vector& candidate_values, - std::vector& repair_cv) + std::vector& repair_cv, + bool useConstantsAsHoles) { Assert(candidates.size() == candidate_values.size()); @@ -106,7 +108,6 @@ bool SygusRepairConst::repairSolution(const std::vector& candidates, Trace("sygus-repair-const") << "Getting candidate skeletons : " << std::endl; } - NodeManager* nm = NodeManager::currentNM(); std::vector candidate_skeletons; std::map free_var_count; std::vector sk_vars; @@ -114,7 +115,8 @@ bool SygusRepairConst::repairSolution(const std::vector& candidates, for (unsigned i = 0, size = candidates.size(); i < size; i++) { Node cv = candidate_values[i]; - Node skeleton = getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs); + Node skeleton = + getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles); if (Trace.isOn("sygus-repair-const")) { Printer* p = Printer::getPrinter(options::outputLanguage()); @@ -143,6 +145,7 @@ bool SygusRepairConst::repairSolution(const std::vector& candidates, return false; } + NodeManager* nm = NodeManager::currentNM(); Trace("sygus-repair-const") << "Get first-order query..." << std::endl; Node fo_body = getFoQuery(candidates, candidate_skeletons, sk_vars); @@ -215,6 +218,7 @@ bool SygusRepairConst::repairSolution(const std::vector& candidates, std::vector sk_sygus_m; for (const Node& v : sk_vars) { + Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end()); Node fov = d_sk_to_fo[v]; Node fov_m = Node::fromExpr(repcChecker.getValue(fov.toExpr())); Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl; @@ -251,7 +255,35 @@ bool SygusRepairConst::repairSolution(const std::vector& candidates, return false; } -bool SygusRepairConst::isRepairableConstant(Node n) +bool SygusRepairConst::mustRepair(Node n) +{ + std::unordered_set visited; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + Assert(cur.getKind() == APPLY_CONSTRUCTOR); + if (isRepairable(cur, false)) + { + return true; + } + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + + return false; +} + +bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles) { if (n.getKind() != APPLY_CONSTRUCTOR) { @@ -261,17 +293,24 @@ bool SygusRepairConst::isRepairableConstant(Node n) Assert(tn.isDatatype()); const Datatype& dt = static_cast(tn.toType()).getDatatype(); Assert(dt.isSygus()); - if (dt.getSygusAllowConst()) + Node op = n.getOperator(); + unsigned cindex = Datatype::indexOf(op.toExpr()); + if (dt[cindex].getNumArgs() > 0) { - Node op = n.getOperator(); - unsigned cindex = Datatype::indexOf(op.toExpr()); - if (dt[cindex].getNumArgs() == 0) + return false; + } + Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp()); + if (sygusOp.getAttribute(SygusAnyConstAttribute())) + { + // if it represents "any constant" then it is repairable + return true; + } + if (useConstantsAsHoles && dt.getSygusAllowConst()) + { + if (sygusOp.isConst()) { - Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp()); - if (sygusOp.isConst()) - { - return true; - } + // if a constant, it is repairable + return true; } } return false; @@ -280,9 +319,10 @@ bool SygusRepairConst::isRepairableConstant(Node n) Node SygusRepairConst::getSkeleton(Node n, std::map& free_var_count, std::vector& sk_vars, - std::map& sk_vars_to_subs) + std::map& sk_vars_to_subs, + bool useConstantsAsHoles) { - if (isRepairableConstant(n)) + if (isRepairable(n, useConstantsAsHoles)) { Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count); sk_vars.push_back(sk_var); @@ -325,8 +365,8 @@ Node SygusRepairConst::getSkeleton(Node n, for (const Node& cn : cur) { Node child; - // if it is a constant over a type that allows all constants - if (isRepairableConstant(cn)) + // if it is repairable + if (isRepairable(cn, useConstantsAsHoles)) { // replace it by the next free variable child = d_tds->getFreeVarInc(cn.getType(), free_var_count); @@ -375,6 +415,19 @@ Node SygusRepairConst::getFoQuery(const std::vector& candidates, Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl; + for (const Node& v : sk_vars) + { + std::map::iterator itf = d_sk_to_fo.find(v); + if (itf == d_sk_to_fo.end()) + { + TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType()); + Node sk_fov = nm->mkSkolem("k", builtinType); + d_sk_to_fo[v] = sk_fov; + d_fo_to_sk[sk_fov] = v; + Trace("sygus-repair-const-debug") + << "Map " << v << " -> " << sk_fov << std::endl; + } + } // now, we must replace all terms of the form eval( z_i, t1...tn ) with // a fresh first-order variable w_i, where z_i is a variable introduced in // the skeleton inference step (z_i is a variable in sk_vars). @@ -398,19 +451,8 @@ Node SygusRepairConst::getFoQuery(const std::vector& candidates, if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end()) { std::map::iterator itf = d_sk_to_fo.find(v); - if (itf == d_sk_to_fo.end()) - { - Node sk_fov = nm->mkSkolem("k", cur.getType()); - d_sk_to_fo[v] = sk_fov; - d_fo_to_sk[sk_fov] = v; - visited[cur] = sk_fov; - Trace("sygus-repair-const-debug") - << "Map " << v << " -> " << sk_fov << std::endl; - } - else - { - visited[cur] = itf->second; - } + Assert(itf != d_sk_to_fo.end()); + visited[cur] = itf->second; } } if (visited[cur].isNull()) @@ -515,15 +557,20 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic, if (it == visited.end()) { visited.insert(cur); - if (restrictLA && cur.getKind() == NONLINEAR_MULT) + Kind ck = cur.getKind(); + if (restrictLA && (ck == NONLINEAR_MULT || ck == DIVISION)) { - for (const Node& ccur : cur) + for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++) { + Node ccur = cur[j]; std::map::iterator itf = d_fo_to_sk.find(ccur); if (itf != d_fo_to_sk.end()) { - exvar = itf->second; - return true; + if (ck == NONLINEAR_MULT || (ck == DIVISION && j == 1)) + { + exvar = itf->second; + return true; + } } } return false; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index b2a0d888d..ba1295988 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -33,9 +33,9 @@ class CegConjecture; * This module is used to repair portions of candidate solutions. In particular, * given a synthesis conjecture: * exists f. forall x. P( f, x ) - * and a candidate solution f = \x. t[x,c] where c are constants, this function - * checks whether there exists a term of the form \x. t[x,c'] for some constants - * c' such that: + * and a candidate solution f = \x. t[x,r] where r are repairable terms, this + * function checks whether there exists a term of the form \x. t[x,c'] for some + * constants c' such that: * forall x. P( (\x. t[x,c']), x ) [***] * is satisfiable, where notice that the above formula after beta-reduction may * be one in pure first-order logic in a decidable theory (say linear @@ -68,10 +68,22 @@ class SygusRepairConst * is a solution for the synthesis conjecture associated with this class. * Moreover, it is the case that * repair_cv[j] != candidate_values[j], for at least one j. + * We always consider applications of the "any constant" constructors in + * candidate_values to be repairable. In addition, if the flag + * useConstantsAsHoles is true, we consider all constants whose (sygus) type + * admit alls constants to be repairable. */ bool repairSolution(const std::vector& candidates, const std::vector& candidate_values, - std::vector& repair_cv); + std::vector& repair_cv, + bool useConstantsAsHoles = false); + /** must repair? + * + * This returns true if n must be repaired for it to be a valid solution. + * This corresponds to whether n contains a subterm that is a symbolic + * constructor like the "any constant" constructor. + */ + static bool mustRepair(Node n); private: /** reference to quantifier engine */ @@ -100,26 +112,30 @@ class SygusRepairConst * already registered types. */ void registerSygusType(TypeNode tn, std::map& tprocessed); - /** - * Returns true if n is a term of a sygus datatype type that allows all - * constants, and n encodes a constant. The term n must have a sygus datatype - * type. + /** is repairable? + * + * This returns true if n can be repaired by this class. In particular, we + * return true if n is an "any constant" constructor, or it is a constructor + * for a constant in a type that allows all constants and useConstantsAsHoles + * is true. */ - bool isRepairableConstant(Node n); + static bool isRepairable(Node n, bool useConstantsAsHoles); /** get skeleton * - * Returns a skeleton for n, where the subterms of n that are repairable - * constants are replaced by free variables. Since we are interested in + * Returns a skeleton for sygus datatype value n, where the subterms of n that + * are repairable are replaced by free variables. Since we are interested in * returning canonical skeletons, the free variables we use in this * replacement are taken from TermDbSygus, where we track indices * in free_var_count. Variables we introduce in this way are added to sk_vars. * The mapping sk_vars_to_subs contains entries v -> c, where v is a - * variable in sk_vars, and c is the term in n that it replaced. + * variable in sk_vars, and c is the term in n that it replaced. The flag + * useConstantsAsHoles affects which terms we consider to be repairable. */ Node getSkeleton(Node n, std::map& free_var_count, std::vector& sk_vars, - std::map& sk_vars_to_subs); + std::map& sk_vars_to_subs, + bool useConstantsAsHoles); /** get first-order query * * This function returns a formula that is equivalent to the negation of the diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 37a8ae382..126f01136 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -18,14 +18,12 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -using namespace std; using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory::inst; namespace CVC4 { namespace theory { @@ -184,6 +182,12 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map& pre) return mkGeneric(dt, c, var_count, pre); } +Node TermDbSygus::mkGeneric(const Datatype& dt, int c) +{ + std::map pre; + return mkGeneric(dt, c, pre); +} + struct SygusToBuiltinAttributeId { }; @@ -191,32 +195,48 @@ typedef expr::Attribute SygusToBuiltinAttribute; Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { + std::map var_count; + return sygusToBuiltin(n, tn, var_count); +} + +Node TermDbSygus::sygusToBuiltin(Node n, + TypeNode tn, + std::map& var_count) +{ Assert( n.getType()==tn ); Assert( tn.isDatatype() ); // has it already been computed? - if (n.hasAttribute(SygusToBuiltinAttribute())) + if (var_count.empty() && n.hasAttribute(SygusToBuiltinAttribute())) { return n.getAttribute(SygusToBuiltinAttribute()); } - Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; const Datatype& dt = static_cast(tn.toType()).getDatatype(); if (n.getKind() == APPLY_CONSTRUCTOR) { + bool var_count_empty = var_count.empty(); unsigned i = Datatype::indexOf(n.getOperator().toExpr()); Assert(n.getNumChildren() == dt[i].getNumArgs()); - std::map var_count; std::map pre; for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) { - pre[j] = sygusToBuiltin(n[j], getArgType(dt[i], j)); + // if the child is a symbolic constructor, do not include it + if (!isSymbolicConsApp(n[j])) + { + pre[j] = sygusToBuiltin( + n[j], TypeNode::fromType(dt[i].getArgType(j)), var_count); + } } Node ret = mkGeneric(dt, i, var_count, pre); Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl; - n.setAttribute(SygusToBuiltinAttribute(), ret); + // cache if we had a fresh variable count + if (var_count_empty) + { + n.setAttribute(SygusToBuiltinAttribute(), ret); + } return ret; } if (n.hasAttribute(SygusPrintProxyAttribute())) @@ -691,7 +711,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { { for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) { - registerSygusType(getArgType(dt[i], j)); + TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j)); + registerSygusType(ctn); + // carry type attributes + if (d_has_subterm_sym_cons.find(ctn) + != d_has_subterm_sym_cons.end()) + { + d_has_subterm_sym_cons[tn] = true; + } } } //iterate over constructors @@ -725,6 +752,12 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { << std::endl; } } + // symbolic constructors + if (n.getAttribute(SygusAnyConstAttribute())) + { + d_sym_cons_any_constant[tn] = i; + d_has_subterm_sym_cons[tn] = true; + } // TODO (as part of #1170): we still do not properly catch type // errors in sygus grammars for arguments of builtin operators. // The challenge is that we easily ask for expected argument types of @@ -736,13 +769,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { // ensure that terms that this constructor encodes are // of the type specified in the datatype. This will fail if // e.g. bitvector-and is a constructor of an integer grammar. - std::map pre; - Node g = mkGeneric(dt, i, pre); + Node g = mkGeneric(dt, i); TypeNode gtn = g.getType(); CVC4_CHECK(gtn.isSubtypeOf(btn)) << "Sygus datatype " << dt.getName() << " encodes terms that are not of type " << btn << std::endl; } + // compute min type depth information + computeMinTypeDepthInternal(tn, tn, 0); } } } @@ -751,7 +785,8 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { void TermDbSygus::registerEnumerator(Node e, Node f, CegConjecture* conj, - bool mkActiveGuard) + bool mkActiveGuard, + bool useSymbolicCons) { if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) { @@ -760,21 +795,81 @@ void TermDbSygus::registerEnumerator(Node e, } Trace("sygus-db") << "Register enumerator : " << e << std::endl; // register its type - registerSygusType(e.getType()); + TypeNode et = e.getType(); + registerSygusType(et); d_enum_to_conjecture[e] = conj; d_enum_to_synth_fun[e] = f; + NodeManager* nm = NodeManager::currentNM(); if( mkActiveGuard ){ // make the guard - Node eg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "eG", NodeManager::currentNM()->booleanType() ) ); + Node eg = Rewriter::rewrite(nm->mkSkolem("eG", nm->booleanType())); eg = d_quantEngine->getValuation().ensureLiteral( eg ); AlwaysAssert( !eg.isNull() ); d_quantEngine->getOutputChannel().requirePhase( eg, true ); //add immediate lemma - Node lem = NodeManager::currentNM()->mkNode( OR, eg, eg.negate() ); + Node lem = nm->mkNode(OR, eg, eg.negate()); Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl; d_quantEngine->getOutputChannel().lemma( lem ); d_enum_to_active_guard[e] = eg; } + + // depending on if we are using symbolic constructors, introduce symmetry + // breaking lemma templates for each relevant subtype of the grammar + std::map >::iterator it = + d_min_type_depth.find(et); + Assert(it != d_min_type_depth.end()); + // for each type of subterm of this enumerator + for (const std::pair& st : it->second) + { + std::vector rm_indices; + TypeNode stn = st.first; + Assert(stn.isDatatype()); + const Datatype& dt = static_cast(stn.toType()).getDatatype(); + std::map::iterator itsa = + d_sym_cons_any_constant.find(stn); + if (itsa != d_sym_cons_any_constant.end()) + { + if (!useSymbolicCons) + { + // do not use the symbolic constructor + rm_indices.push_back(itsa->second); + } + else + { + // can remove all other concrete constant constructors + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + if (i != itsa->second) + { + Node c_op = getConsNumConst(stn, i); + if (!c_op.isNull()) + { + rm_indices.push_back(i); + } + } + } + } + } + for (unsigned& rindex : rm_indices) + { + // make the apply-constructor corresponding to an application of the + // "any constant" constructor + Node exc_val = nm->mkNode(APPLY_CONSTRUCTOR, + Node::fromExpr(dt[rindex].getConstructor())); + // should not include the constuctor in any subterm + Node x = getFreeVar(stn, 0); + Trace("sygus-db") << "Construct symmetry breaking lemma from " << x + << " == " << exc_val << std::endl; + Node lem = getExplain()->getExplanationForEquality(x, exc_val); + lem = lem.negate(); + Trace("cegqi-lemma") + << "Cegqi::Lemma : exclude symbolic cons lemma (template) : " << lem + << std::endl; + // the size of the subterm we are blocking is the weight of the + // constructor (usually zero) + registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight()); + } + } } bool TermDbSygus::isEnumerator(Node e) const @@ -870,14 +965,10 @@ unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const return it->second; } -void TermDbSygus::clearSymBreakLemmas() -{ - d_enum_to_sb_lemmas.clear(); - d_sb_lemma_to_type.clear(); - d_sb_lemma_to_size.clear(); -} +void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); } -bool TermDbSygus::isRegistered( TypeNode tn ) { +bool TermDbSygus::isRegistered(TypeNode tn) const +{ return d_register.find( tn )!=d_register.end(); } @@ -904,7 +995,6 @@ void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, un unsigned TermDbSygus::getMinTypeDepth( TypeNode root_tn, TypeNode tn ){ std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn ); if( it==d_min_type_depth[root_tn].end() ){ - computeMinTypeDepthInternal( root_tn, root_tn, 0 ); Assert( d_min_type_depth[root_tn].find( tn )!=d_min_type_depth[root_tn].end() ); return d_min_type_depth[root_tn][tn]; }else{ @@ -1107,6 +1197,38 @@ bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeCons } } +int TermDbSygus::getAnyConstantConsNum(TypeNode tn) const +{ + Assert(isRegistered(tn)); + std::map::const_iterator itt = + d_sym_cons_any_constant.find(tn); + if (itt != d_sym_cons_any_constant.end()) + { + return static_cast(itt->second); + } + return -1; +} + +bool TermDbSygus::hasSubtermSymbolicCons(TypeNode tn) const +{ + return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end(); +} + +bool TermDbSygus::isSymbolicConsApp(Node n) const +{ + if (n.getKind() != APPLY_CONSTRUCTOR) + { + return false; + } + TypeNode tn = n.getType(); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Assert(dt.isSygus()); + unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); + Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp()); + // it is symbolic if it represents "any constant" + return sygusOp.getAttribute(SygusAnyConstAttribute()); +} + Node TermDbSygus::minimizeBuiltinTerm( Node n ) { if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) && ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){ @@ -1338,8 +1460,7 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod cc.insert( cc.end(), args.begin(), args.end() ); pre[j] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc ); } - std::map< TypeNode, int > var_count; - Node ret = mkGeneric( dt, i, var_count, pre ); + Node ret = mkGeneric(dt, i, pre); // if it is a variable, apply the substitution if( ret.getKind()==kind::BOUND_VARIABLE ){ Assert( ret.hasAttribute(SygusVarNumAttribute()) ); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 9f370cd15..139e00794 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -63,7 +63,9 @@ class TermDbSygus { * conj : the conjecture that the enumeration of e is for. * f : the synth-fun that the enumeration of e is for. * mkActiveGuard : whether we want to make an active guard for e - * (see d_enum_to_active_guard). + * (see d_enum_to_active_guard), + * useSymbolicCons : whether we want model values for e to include symbolic + * constructors like the "any constant" variable. * * Notice that enumerator e may not be one-to-one with f in * synthesis-through-unification approaches (e.g. decision tree construction @@ -72,7 +74,8 @@ class TermDbSygus { void registerEnumerator(Node e, Node f, CegConjecture* conj, - bool mkActiveGuard = false); + bool mkActiveGuard = false, + bool useSymbolicCons = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ @@ -109,8 +112,8 @@ class TermDbSygus { TypeNode getTypeForSymBreakLemma(Node lem) const; /** Get the minimum size of terms symmetry breaking lemma lem applies to */ unsigned getSizeForSymBreakLemma(Node lem) const; - /** Clear information about symmetry breaking lemmas */ - void clearSymBreakLemmas(); + /** Clear information about symmetry breaking lemmas for enumerator e */ + void clearSymBreakLemmas(Node e); //------------------------------end enumerators //-----------------------------conversion from sygus to builtin @@ -161,12 +164,19 @@ class TermDbSygus { std::map& pre); /** same as above, but with empty var_count */ Node mkGeneric(const Datatype& dt, int c, std::map& pre); + /** same as above, but with empty pre */ + Node mkGeneric(const Datatype& dt, int c); /** sygus to builtin * * Given a sygus datatype term n of type tn, this function returns its analog, * that is, the term that n encodes. + * + * Notice that each occurrence of a symbolic constructor application is + * replaced by a unique variable. To track counters for introducing unique + * variables, we use the var_count map. */ Node sygusToBuiltin(Node n, TypeNode tn); + Node sygusToBuiltin(Node n, TypeNode tn, std::map& var_count); /** same as above, but without tn */ Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); } /** evaluate builtin @@ -265,7 +275,8 @@ class TermDbSygus { Node d_true; Node d_false; -private: + private: + /** computes the map d_min_type_depth */ void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ); bool involvesDivByZero( Node n, std::map< Node, bool >& visited ); @@ -282,6 +293,14 @@ private: std::map > d_semantic_skolem; // grammar information // root -> type -> _ + /** + * For each sygus type t1, this maps datatype types t2 to the smallest size of + * a term of type t1 that includes t2 as a subterm. For example, for grammar: + * A -> B+B | 0 | B-D + * B -> C+C + * ... + * we have that d_min_type_depth[A] = { A -> 0, B -> 1, C -> 2, D -> 1 }. + */ std::map > d_min_type_depth; // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > > // d_consider_const; @@ -290,9 +309,20 @@ private: std::map > d_min_cons_term_size; /** a cache for getSelectorWeight */ std::map > d_sel_weight; + /** + * For each sygus type, the index of the "any constant" constructor, if it + * has one. + */ + std::map d_sym_cons_any_constant; + /** + * Whether any subterm of this type contains a symbolic constructor. This + * corresponds to whether sygus repair techniques will ever have any effect + * for this type. + */ + std::map d_has_subterm_sym_cons; public: // general sygus utilities - bool isRegistered( TypeNode tn ); + bool isRegistered(TypeNode tn) const; // get the minimum depth of type in its parent grammar unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn ); // get the minimum size for a constructor term @@ -319,6 +349,18 @@ private: int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn ); /** is type match */ bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ); + /** + * Get the index of the "any constant" constructor of type tn if it has one, + * or returns -1 otherwise. + */ + int getAnyConstantConsNum(TypeNode tn) const; + /** has subterm symbolic constructor + * + * Returns true if any subterm of type tn can be a symbolic constructor. + */ + bool hasSubtermSymbolicCons(TypeNode tn) const; + /** return whether n is an application of a symbolic constructor */ + bool isSymbolicConsApp(Node n) const; TypeNode getSygusTypeForVar( Node v ); Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ); diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index ed2390fe5..4324171a8 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -406,7 +406,6 @@ REG0_TESTS = \ regress0/expect/scrub.03.smt2 \ regress0/expect/scrub.04.smt2 \ regress0/expect/scrub.06.cvc \ - regress0/expect/scrub.07.sy \ regress0/expect/scrub.08.sy \ regress0/expect/scrub.09.p \ regress0/flet.smt \ @@ -1974,7 +1973,6 @@ TESTS_EXPECT = \ regress0/decision/wchains010ue.smt.expect \ regress0/expect/scrub.01.smt.expect \ regress0/expect/scrub.03.smt2.expect \ - regress0/expect/scrub.07.sy.expect \ regress0/quantifiers/bug291.smt2.expect \ regress0/uflia/check02.smt2.expect \ regress0/uflia/check03.smt2.expect \ diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy deleted file mode 100644 index 79b917c7a..000000000 --- a/test/regress/regress0/expect/scrub.07.sy +++ /dev/null @@ -1,7 +0,0 @@ -; COMMAND-LINE: --cegqi-si=all --sygus-out=status -(set-logic LIA) -(declare-var n Int) - -(synth-fun f ((n Int)) Int) -(constraint (= (/ n n) 1)) -(check-synth) diff --git a/test/regress/regress0/expect/scrub.07.sy.expect b/test/regress/regress0/expect/scrub.07.sy.expect deleted file mode 100644 index 4c5aa1491..000000000 --- a/test/regress/regress0/expect/scrub.07.sy.expect +++ /dev/null @@ -1,5 +0,0 @@ -% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. -% EXPECT: The fact in question: TERM -% EXPECT: ") -% EXIT: 1 diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy index 61b08a838..c19b2ff42 100644 --- a/test/regress/regress2/sygus/ex23.sy +++ b/test/regress/regress2/sygus/ex23.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --sygus-repair-const (set-logic LIA) (synth-inv inv-f ((y Int) (z Int) (c Int))) @@ -20,4 +20,6 @@ (inv-constraint inv-f pre-f trans-f post-f) +; needs --sygus-repair-const, since easy solution involves the constant 4608 + (check-synth) -- 2.30.2