From 6e3f8936d74ec2d2ed99b68cd77df771607c527f Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 17 May 2018 14:47:30 -0500 Subject: [PATCH] Option to force return values of Bool functions to be constant in CegisUnif (#1930) --- src/options/quantifiers_options.toml | 8 ++ src/theory/quantifiers/sygus/cegis_unif.cpp | 23 +---- .../quantifiers/sygus/sygus_grammar_cons.cpp | 31 ++++--- .../quantifiers/sygus/sygus_unif_rl.cpp | 8 +- .../quantifiers/sygus/sygus_unif_strat.cpp | 85 ++++++++++++++++--- .../quantifiers/sygus/sygus_unif_strat.h | 36 +++++++- 6 files changed, 147 insertions(+), 44 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 691b2fef4..d784447c6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -967,6 +967,14 @@ header = "options/quantifiers_options.h" default = "false" help = "Unification-based function synthesis" +[[option]] + name = "sygusBoolIteReturnConst" + category = "regular" + long = "sygus-bool-ite-return-const" + type = "bool" + default = "false" + help = "Only use Boolean constants for return values in unification-based function synthesis" + [[option]] name = "sygusQePreproc" category = "regular" diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 9ae598f83..692055b87 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -37,7 +37,6 @@ bool CegisUnif::processInitialize(Node n, const std::vector& candidates, std::vector& lemmas) { - Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; // list of strategy points for unification candidates std::vector unif_candidate_pts; // map from strategy points to their conditions @@ -453,24 +452,10 @@ void CegisUnifEnumManager::incrementNumEnumerators() << " to strategy point " << ci.second.d_pt << "\n"; d_tds->registerEnumerator(e, ci.second.d_pt, d_parent); - // if the sygus datatype is interpreted as an infinite type - // (this should be the case for almost all examples) - TypeNode et = e.getType(); - if (!et.isInterpretedFinite()) - { - // it is disequal from all previous ones - for (const Node& ei : ci.second.d_enums[index]) - { - if (ei == e) - { - continue; - } - Node deq = e.eqNode(ei).negate(); - Trace("cegis-unif-enum-lemma") - << "CegisUnifEnum::lemma, enum deq:" << deq << "\n"; - d_qe->getOutputChannel().lemma(deq); - } - } + // TODO symmetry breaking for making + // e distinct from ei : (ci.second.d_enums[index] \ {e}) + // if its respective type has had at least + // ci.second.d_enums[index].size() distinct values enumerated } } // register the evaluation points at the new value diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index f331d8fc6..412d1b211 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -619,18 +619,18 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs.push_back( std::vector< CVC4::Type >() ); } } - //add constants if no variables and no connected types - if( ops.back().empty() && types.empty() ){ - std::vector< Node > consts; - mkSygusConstantsForType( btype, consts ); - for( unsigned j=0; j() ); - } + //add constants + std::vector consts; + mkSygusConstantsForType(btype, consts); + for (unsigned j = 0; j < consts.size(); j++) + { + std::stringstream ss; + ss << consts[j]; + Trace("sygus-grammar-def") << "...add for constant " << ss.str() + << std::endl; + ops.back().push_back(consts[j].toExpr()); + cnames.push_back(ss.str()); + cargs.push_back(std::vector()); } //add operators for (unsigned i = 0; i < 4; i++) @@ -638,6 +638,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( CVC4::Kind k = i == 0 ? kind::NOT : (i == 1 ? kind::AND : (i == 2 ? kind::OR : kind::ITE)); + // TODO #1935 ITEs are added to Boolean grammars so that we can infer + // unification strategies. We can do away with this if we can infer + // unification strategies from and/or/not + if (k == ITE && !options::sygusUnif()) + { + continue; + } Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); cnames.push_back(kind::kindToString(k)); diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 3fbb4b2b7..be8d6c5ca 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_unif_rl.h" #include "options/base_options.h" +#include "options/quantifiers_options.h" #include "printer/printer.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -38,7 +39,12 @@ void SygusUnifRl::initializeCandidate( SygusUnif::initializeCandidate(qe, f, all_enums, strategy_lemmas); // based on the strategy inferred for each function, determine if we are // using a unification strategy that is compatible our approach. - d_strategy[f].staticLearnRedundantOps(strategy_lemmas); + StrategyRestrictions restrictions; + if (options::sygusBoolIteReturnConst()) + { + restrictions.d_iteReturnBoolConst = true; + } + d_strategy[f].staticLearnRedundantOps(strategy_lemmas, restrictions); registerStrategy(f, enums); // Copy candidates and check whether CegisUnif for any of them if (d_unif_candidates.find(f) != d_unif_candidates.end()) diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 855922fc5..0ecf01b74 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -682,6 +682,14 @@ bool SygusUnifStrategy::inferTemplate( void SygusUnifStrategy::staticLearnRedundantOps( std::map>& strategy_lemmas) +{ + StrategyRestrictions restrictions; + staticLearnRedundantOps(strategy_lemmas, restrictions); +} + +void SygusUnifStrategy::staticLearnRedundantOps( + std::map>& strategy_lemmas, + StrategyRestrictions& restrictions) { for (unsigned i = 0; i < d_esym_list.size(); i++) { @@ -710,7 +718,8 @@ void SygusUnifStrategy::staticLearnRedundantOps( debugPrint("sygus-unif"); std::map > visited; std::map > needs_cons; - staticLearnRedundantOps(getRootEnumerator(), role_equal, visited, needs_cons); + staticLearnRedundantOps( + getRootEnumerator(), role_equal, visited, needs_cons, restrictions); // now, check the needs_cons map for (std::pair >& nce : needs_cons) { @@ -753,8 +762,9 @@ void SygusUnifStrategy::debugPrint(const char* c) void SygusUnifStrategy::staticLearnRedundantOps( Node e, NodeRole nrole, - std::map >& visited, - std::map >& needs_cons) + std::map>& visited, + std::map>& needs_cons, + StrategyRestrictions& restrictions) { if (visited[e].find(nrole) != visited[e].end()) { @@ -778,26 +788,81 @@ void SygusUnifStrategy::staticLearnRedundantOps( for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) { EnumTypeInfoStrat* etis = snode.d_strats[j]; - int cindex = Datatype::indexOf(etis->d_cons.toExpr()); - Assert(cindex != -1); - Trace("sygus-strat-slearn") - << "...by strategy, can exclude operator " << etis->d_cons << std::endl; - needs_cons_curr[static_cast(cindex)] = false; + unsigned cindex = + static_cast(Datatype::indexOf(etis->d_cons.toExpr())); + Trace("sygus-strat-slearn") << "...by strategy, can exclude operator " + << etis->d_cons << std::endl; + needs_cons_curr[cindex] = false; + // try to eliminate from etn's datatype all operators except TRUE/FALSE if + // arguments of ITE are the same BOOL type + if (restrictions.d_iteReturnBoolConst) + { + const Datatype& dt = + static_cast(etn.toType()).getDatatype(); + Node op = Node::fromExpr(dt[cindex].getSygusOp()); + TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType()); + if (op.getKind() == kind::BUILTIN + && NodeManager::operatorToKind(op) == ITE + && sygus_tn.isBoolean() + && (TypeNode::fromType(dt[cindex].getArgType(1)) + == TypeNode::fromType(dt[cindex].getArgType(2)))) + { + unsigned ncons = dt.getNumConstructors(), indexT = ncons, + indexF = ncons; + for (unsigned k = 0; k < ncons; ++k) + { + Node op_arg = Node::fromExpr(dt[k].getSygusOp()); + if (dt[k].getNumArgs() > 0 || !op_arg.isConst()) + { + continue; + } + if (op_arg.getConst()) + { + indexT = k; + } + else + { + indexF = k; + } + } + if (indexT < ncons && indexF < ncons) + { + Trace("sygus-strat-slearn") + << "...for ite boolean arg, can exclude all operators but T/F\n"; + for (unsigned k = 0; k < ncons; ++k) + { + needs_cons_curr[k] = false; + } + needs_cons_curr[indexT] = true; + needs_cons_curr[indexF] = true; + } + } + } for (std::pair& cec : etis->d_cenum) { - staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons); + staticLearnRedundantOps( + cec.first, cec.second, visited, needs_cons, restrictions); } } // get the current datatype const Datatype& dt = static_cast(etn.toType()).getDatatype(); // do not use recursive Boolean connectives for conditions of ITEs - if (nrole == role_ite_condition) + if (nrole == role_ite_condition && restrictions.d_iteCondOnlyAtoms) { + TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType()); for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) { Node op = Node::fromExpr(dt[j].getSygusOp()); Trace("sygus-strat-slearn") << "...for ite condition, look at operator : " << op << std::endl; + if (op.isConst() && dt[j].getNumArgs() == 0) + { + Trace("sygus-strat-slearn") + << "...for ite condition, can exclude Boolean constant " << op + << std::endl; + needs_cons_curr[j] = false; + continue; + } if (op.getKind() == kind::BUILTIN) { Kind k = NodeManager::operatorToKind(op); diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index a24e323e8..43919d68e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -237,6 +237,27 @@ class EnumTypeInfoStrat bool isValid(UnifContext& x); }; +/** + * flags for extra restrictions to be inferred during redundant operators + * learning + */ +struct StrategyRestrictions +{ + StrategyRestrictions() : d_iteReturnBoolConst(false), d_iteCondOnlyAtoms(true) + { + } + /** + * if this flag is true then staticLearnRedundantOps will also try to make + * the return value of boolean ITEs to be restricted to constants + */ + bool d_iteReturnBoolConst; + /** + * if this flag is true then staticLearnRedundantOps will also try to make + * the condition values of ITEs to be restricted to atoms + */ + bool d_iteCondOnlyAtoms; +}; + /** * Stores strategy and enumeration information for a function-to-synthesize. * @@ -279,6 +300,16 @@ class SygusUnifStrategy * These may correspond to static symmetry breaking predicates (for example, * those that exclude ITE from enumerators whose role is enum_io when the * strategy is ITE_strat). + * + * then the module may also try to apply the given pruning restrictions (see + * StrategyRestrictions for more details) + */ + void staticLearnRedundantOps( + std::map>& strategy_lemmas, + StrategyRestrictions& restrictions); + /** + * creates the default restrictions when they are not given and calls the + * above function */ void staticLearnRedundantOps( std::map>& strategy_lemmas); @@ -353,8 +384,9 @@ class SygusUnifStrategy void staticLearnRedundantOps( Node e, NodeRole nrole, - std::map >& visited, - std::map >& needs_cons); + std::map>& visited, + std::map>& needs_cons, + StrategyRestrictions& restrictions); /** finish initialization of the strategy tree * * (e, nrole) specify the strategy node in the graph we are currently -- 2.30.2