From f29ced85757a85b6bd72b741d6ac7ff45ba29619 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 10 May 2018 15:57:54 -0500 Subject: [PATCH] Static learn redundant operators in CegisUnif (#1899) --- src/theory/quantifiers/sygus/cegis_unif.cpp | 68 +++++++++++++++++-- src/theory/quantifiers/sygus/cegis_unif.h | 7 +- src/theory/quantifiers/sygus/sygus_pbe.cpp | 40 +++++++---- src/theory/quantifiers/sygus/sygus_pbe.h | 43 +++++++----- src/theory/quantifiers/sygus/sygus_unif.cpp | 5 +- src/theory/quantifiers/sygus/sygus_unif.h | 7 +- .../quantifiers/sygus/sygus_unif_io.cpp | 6 +- src/theory/quantifiers/sygus/sygus_unif_io.h | 28 ++++---- .../quantifiers/sygus/sygus_unif_rl.cpp | 41 ++++++++--- src/theory/quantifiers/sygus/sygus_unif_rl.h | 27 ++++++-- .../quantifiers/sygus/sygus_unif_strat.cpp | 9 ++- .../quantifiers/sygus/sygus_unif_strat.h | 6 +- 12 files changed, 205 insertions(+), 82 deletions(-) diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index a5ab27bf3..2456839e7 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -40,7 +40,8 @@ bool CegisUnif::initialize(Node n, { Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; // Init UNIF util - d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas); + std::map> strategy_lemmas; + d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, strategy_lemmas); Trace("cegis-unif") << "Initializing enums for pure Cegis case\n"; std::vector unif_candidates; // Initialize enumerators for non-unif functions-to-synhesize @@ -64,7 +65,7 @@ bool CegisUnif::initialize(Node n, d_enum_to_active_guard[e] = g; } // initialize the enumeration manager - d_u_enum_manager.initialize(unif_candidates); + d_u_enum_manager.initialize(unif_candidates, strategy_lemmas); return true; } @@ -175,13 +176,14 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, std::vector& lems) { // Notify lemma to unification utility and get its purified form - std::map > eval_pts; + std::map> eval_pts; Node plem = d_sygus_unif.addRefLemma(lem, eval_pts); d_refinement_lemmas.push_back(plem); Trace("cegis-unif") << "* Refinement lemma:\n" << plem << "\n"; // Notify the enumeration manager if there are new evaluation points - for (const std::pair >& ep : eval_pts) + for (const std::pair>& ep : eval_pts) { + Trace("cegis-unif") << "** Registering new point:\n" << plem << "\n"; d_u_enum_manager.registerEvalPts(ep.second, ep.first); } // Make the refinement lemma and add it to lems. This lemma is guarded by the @@ -208,7 +210,9 @@ CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe, d_tds = d_qe->getTermDatabaseSygus(); } -void CegisUnifEnumManager::initialize(const std::vector& cs) +void CegisUnifEnumManager::initialize( + const std::vector& cs, + const std::map>& strategy_lemmas) { Assert(!d_initialized); d_initialized = true; @@ -216,12 +220,51 @@ void CegisUnifEnumManager::initialize(const std::vector& cs) { return; } + // process strategy lemmas + std::map>> tn_strategy_lemmas; + for (const std::pair>& p : strategy_lemmas) + { + if (Trace.isOn("cegis-unif-enum-debug")) + { + Trace("cegis-unif-enum-debug") << "...lemmas of strategy pt " << p.first + << ":\n"; + for (const Node& lem : p.second) + { + Trace("cegis-unif-enum-debug") << "\t" << lem << "\n"; + } + } + TypeNode tn = p.first.getType(); + Assert(tn_strategy_lemmas.find(tn) == tn_strategy_lemmas.end()); + tn_strategy_lemmas[tn].first = p.first; + tn_strategy_lemmas[tn].second = p.second; + } + // initialize type information for candidates + NodeManager* nm = NodeManager::currentNM(); for (const Node& c : cs) { + Trace("cegis-unif-enum-debug") << "...adding candidate " << c << "\n"; // currently, we allocate the same enumerators for candidates of the same // type TypeNode tn = c.getType(); d_ce_info[tn].d_candidates.push_back(c); + // retrieve symmetry breaking lemma template for type if not already init + if (!d_ce_info[tn].d_sbt_lemma.isNull()) + { + continue; + } + std::map>>::iterator it = + tn_strategy_lemmas.find(tn); + if (it == tn_strategy_lemmas.end()) + { + continue; + } + // collect lemmas for removing redundant ops for this candidate's type + d_ce_info[tn].d_sbt_lemma = nm->mkNode(AND, it->second.second); + Trace("cegis-unif-enum-debug") + << "...adding lemma template to remove redundant operators for " << c + << " and its type " << tn << " --> " << d_ce_info[tn].d_sbt_lemma + << "\n"; + d_ce_info[tn].d_sbt_arg = it->second.first; } // initialize the current literal incrementNumEnumerators(); @@ -299,6 +342,17 @@ void CegisUnifEnumManager::incrementNumEnumerators() { TypeNode ct = ci.first; Node eu = nm->mkSkolem("eu", ct); + // instantiate template for removing redundant operators + if (!ci.second.d_sbt_lemma.isNull()) + { + Node templ = ci.second.d_sbt_lemma; + TNode templ_var = ci.second.d_sbt_arg; + Node sym_break_red_ops = templ.substitute(templ_var, eu); + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, remove redundant ops of " << eu << " : " + << sym_break_red_ops << "\n"; + d_qe->getOutputChannel().lemma(sym_break_red_ops); + } if (!ci.second.d_enums.empty()) { Node eu_prev = ci.second.d_enums.back(); @@ -368,8 +422,8 @@ void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct, disj.push_back(ei.eqNode(itc->second.d_enums[i])); } Node lem = NodeManager::currentNM()->mkNode(OR, disj); - Trace("cegis-unif-enum-lemma") - << "CegisUnifEnum::lemma, domain:" << lem << "\n"; + Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, domain:" << lem + << "\n"; d_qe->getOutputChannel().lemma(lem); } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ed38c9268..dd98b20ba 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -54,7 +54,8 @@ class CegisUnifEnumManager * Each candidate c in cs should be such that we are using a * synthesis-by-unification approach for c. */ - void initialize(const std::vector& cs); + void initialize(const std::vector& cs, + const std::map>& strategy_lemmas); /** register evaluation point for candidate * * This notifies this class that eis is a set of heads of evaluation points @@ -100,6 +101,10 @@ class CegisUnifEnumManager std::vector d_enums; /** the set of evaluation points of this type */ std::vector d_eval_points; + /** symmetry breaking lemma template for this type */ + Node d_sbt_lemma; + /** argument (to be instantiated) of symmetry breaking lemma template */ + Node d_sbt_arg; }; /** map types to the above info */ std::map d_ce_info; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index cae2a432d..7faeb0252 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -113,30 +113,38 @@ bool CegConjecturePbe::initialize(Node n, std::vector& lemmas) { Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; - - for( unsigned i=0; i visited; - collectExamples( n, visited, true, true ); - - for( unsigned i=0; i visited; + collectExamples(n, visited, true, true); + + for (unsigned i = 0; i < candidates.size(); i++) + { Node v = candidates[i]; Trace("sygus-pbe") << " examples for " << v << " : "; - if( d_examples_invalid.find( v )!=d_examples_invalid.end() ){ + if (d_examples_invalid.find(v) != d_examples_invalid.end()) + { Trace("sygus-pbe") << "INVALID" << std::endl; - }else{ + } + else + { Trace("sygus-pbe") << std::endl; - for( unsigned j=0; j " << d_examples_out[v][j]; } Trace("sygus-pbe") << std::endl; @@ -168,8 +176,14 @@ bool CegConjecturePbe::initialize(Node n, << std::endl; std::vector singleton_c; singleton_c.push_back(c); + std::map> strategy_lemmas; d_sygus_unif[c].initialize( - d_qe, singleton_c, d_candidate_to_enum[c], lemmas); + d_qe, singleton_c, d_candidate_to_enum[c], strategy_lemmas); + // collect lemmas from all strategies + for (const std::pair>& p : strategy_lemmas) + { + lemmas.insert(lemmas.end(), p.second.begin(), p.second.end()); + } Assert(!d_candidate_to_enum[c].empty()); Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size() << " enumerators for " << c << "..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 235fbe3dd..fbf89fee9 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -189,7 +189,7 @@ class CegConjecturePbe : public SygusModule private: /** sygus term database of d_qe */ - quantifiers::TermDbSygus * d_tds; + quantifiers::TermDbSygus* d_tds; /** true and false nodes */ Node d_true; Node d_false; @@ -200,7 +200,7 @@ class CegConjecturePbe : public SygusModule * In other words, all occurrences of f are guarded by equalities that * constraint its arguments to constants. */ - std::map< Node, bool > d_examples_invalid; + std::map d_examples_invalid; /** for each candidate variable (function-to-synthesize), whether the * conjecture is purely PBE for that variable. * An example of a conjecture for which d_examples_invalid is false but @@ -213,7 +213,7 @@ class CegConjecturePbe : public SygusModule * However, the domain of f in both cases is finite, which can be used for * search space pruning. */ - std::map< Node, bool > d_examples_out_invalid; + std::map d_examples_out_invalid; /** * Map from candidates to sygus unif utility. This class implements * the core algorithm (e.g. decision tree learning) that this module relies @@ -231,19 +231,22 @@ class CegConjecturePbe : public SygusModule std::map d_enum_to_active_guard; /** for each candidate variable (function-to-synthesize), input of I/O * examples */ - std::map< Node, std::vector< std::vector< Node > > > d_examples; + std::map > > d_examples; /** for each candidate variable (function-to-synthesize), output of I/O * examples */ - std::map< Node, std::vector< Node > > d_examples_out; + std::map > d_examples_out; /** the list of example terms * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 ) */ - std::map< Node, std::vector< Node > > d_examples_term; + std::map > d_examples_term; /** collect the PBE examples in n * This is called on the input conjecture, and will populate the above vectors. * hasPol/pol denote the polarity of n in the conjecture. */ - void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol ); + void collectExamples(Node n, + std::map& visited, + bool hasPol, + bool pol); //--------------------------------- PBE search values /** @@ -254,7 +257,8 @@ class CegConjecturePbe : public SygusModule * term x+y is indexed by 1,4 * term 0 is indexed by 0,0. */ - class PbeTrie { + class PbeTrie + { public: PbeTrie() {} ~PbeTrie() {} @@ -271,13 +275,21 @@ class CegConjecturePbe : public SygusModule * index : the index of the example we are processing, * ntotal : the total of the examples for enumerator e. */ - Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe, - unsigned index, unsigned ntotal); + Node addPbeExample(TypeNode etn, + Node e, + Node b, + CegConjecturePbe* cpbe, + unsigned index, + unsigned ntotal); private: /** Helper function for above, called when we get the current example ex. */ - Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector& ex, - CegConjecturePbe* cpbe, unsigned index, + Node addPbeExampleEval(TypeNode etn, + Node e, + Node b, + std::vector& ex, + CegConjecturePbe* cpbe, + unsigned index, unsigned ntotal); }; /** trie of candidate solutions tried @@ -288,11 +300,10 @@ class CegConjecturePbe : public SygusModule */ std::map > d_pbe_trie; //--------------------------------- end PBE search values - }; -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ #endif diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 23b04aa4d..5cf96e513 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -27,12 +27,11 @@ namespace theory { namespace quantifiers { SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {} - SygusUnif::~SygusUnif() {} void SygusUnif::initialize(QuantifiersEngine* qe, const std::vector& funs, std::vector& enums, - std::vector& lemmas) + std::map>& strategy_lemmas) { Assert(d_candidates.empty()); d_qe = qe; @@ -98,7 +97,7 @@ Node SygusUnif::constructBestConditional(const std::vector& conds) Node SygusUnif::constructBestStringToConcat( const std::vector& strs, const std::map& total_inc, - const std::map >& incr) + const std::map>& incr) { Assert(!strs.empty()); std::vector strs_tmp = strs; diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index e55f7e6ff..fe80a3d44 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -55,15 +55,16 @@ class SygusUnif * the grammar of f and adds them to enums. These enumerators are those that * should be later given to calls to notifyEnumeration below. * - * This also may result in lemmas being added to lemmas, + * This also may result in lemmas being added to strategy_lemmas, * which 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). + * strategy is ITE_strat). The lemmas are associated with a strategy point of + * the respective function-to-synthesize. */ virtual void initialize(QuantifiersEngine* qe, const std::vector& funs, std::vector& enums, - std::vector& lemmas); + std::map>& strategy_lemmas); /** * Notify that the value v has been enumerated for enumerator e. This call diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 8f2038d31..60a3d70d8 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -469,16 +469,16 @@ SygusUnifIo::~SygusUnifIo() {} void SygusUnifIo::initialize(QuantifiersEngine* qe, const std::vector& funs, std::vector& enums, - std::vector& lemmas) + std::map>& strategy_lemmas) { Assert(funs.size() == 1); d_examples.clear(); d_examples_out.clear(); d_ecache.clear(); d_candidate = funs[0]; - SygusUnif::initialize(qe, funs, enums, lemmas); + SygusUnif::initialize(qe, funs, enums, strategy_lemmas); // learn redundant operators based on the strategy - d_strategy[d_candidate].staticLearnRedundantOps(lemmas); + d_strategy[d_candidate].staticLearnRedundantOps(strategy_lemmas); } void SygusUnifIo::addExample(const std::vector& input, Node output) diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index b0d6ce3ce..359aa4443 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -37,7 +37,7 @@ class UnifContextIo : public UnifContext public: UnifContextIo(); /** get current role */ - virtual NodeRole getCurrentRole() override; + NodeRole getCurrentRole() override; /** * This intiializes this context based on information in sui regarding the @@ -122,7 +122,7 @@ class UnifContextIo : public UnifContext * This is the current set of enumerator/node role pairs we are currently * visiting. This set is cleared when the context is updated. */ - std::map > d_visit_role; + std::map> d_visit_role; /** unif context enumerator information */ class UEnumInfo @@ -142,7 +142,7 @@ class UnifContextIo : public UnifContext * resulting in 2 and 4, are equal to the output value for the respective * pairs. */ - std::map > d_look_ahead_sols; + std::map> d_look_ahead_sols; }; /** map from enumerators to the above info class */ std::map d_uinfo; @@ -214,7 +214,7 @@ class SubsumeTrie */ void getLeaves(const std::vector& vals, bool pol, - std::map >& v); + std::map>& v); /** is this trie empty? */ bool isEmpty() { return d_term.isNull() && d_children.empty(); } /** clear this trie */ @@ -242,7 +242,7 @@ class SubsumeTrie /** helper function for above functions */ void getLeavesInternal(const std::vector& vals, bool pol, - std::map >& v, + std::map>& v, unsigned index, int status); }; @@ -276,17 +276,15 @@ class SygusUnifIo : public SygusUnif * The vector funs should be of length one, since I/O specifications across * multiple functions can be separated. */ - virtual void initialize(QuantifiersEngine* qe, - const std::vector& funs, - std::vector& enums, - std::vector& lemmas) override; + void initialize(QuantifiersEngine* qe, + const std::vector& funs, + std::vector& enums, + std::map>& strategy_lemmas) override; /** Notify enumeration */ - virtual void notifyEnumeration(Node e, - Node v, - std::vector& lemmas) override; + void notifyEnumeration(Node e, Node v, std::vector& lemmas) override; /** Construct solution */ - virtual bool constructSolution(std::vector& sols) override; + bool constructSolution(std::vector& sols) override; /** add example * @@ -314,7 +312,7 @@ class SygusUnifIo : public SygusUnif Node d_true; Node d_false; /** input of I/O examples */ - std::vector > d_examples; + std::vector> d_examples; /** output of I/O examples */ std::vector d_examples_out; @@ -347,7 +345,7 @@ class SygusUnifIo : public SygusUnif * This either stores the values of f( I ) for inputs * or the value of f( I ) = O if d_role==enum_io */ - std::vector > d_enum_vals_res; + std::vector> d_enum_vals_res; /** * The set of values in d_enum_vals that have been "subsumed" by others * (see SubsumeTrie for explanation of subsumed). diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index a2299f834..427d413c8 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -28,16 +28,17 @@ SygusUnifRl::~SygusUnifRl() {} void SygusUnifRl::initialize(QuantifiersEngine* qe, const std::vector& funs, std::vector& enums, - std::vector& lemmas) + std::map>& strategy_lemmas) { // initialize std::vector all_enums; - SygusUnif::initialize(qe, funs, all_enums, lemmas); + SygusUnif::initialize(qe, funs, 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. for (const Node& f : funs) { - registerStrategy(f); + d_strategy[f].staticLearnRedundantOps(strategy_lemmas); + registerStrategy(f, strategy_lemmas); } enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end()); // Copy candidates and check whether CegisUnif for any of them @@ -363,7 +364,8 @@ std::vector SygusUnifRl::getEvalPointHeads(Node c) return it->second; } -void SygusUnifRl::registerStrategy(Node f) +void SygusUnifRl::registerStrategy( + Node f, std::map>& strategy_lemmas) { if (Trace.isOn("sygus-unif-rl-strat")) { @@ -374,14 +376,15 @@ void SygusUnifRl::registerStrategy(Node f) Trace("sygus-unif-rl-strat") << "Register..." << std::endl; Node e = d_strategy[f].getRootEnumerator(); std::map> visited; - registerStrategyNode(f, e, role_equal, visited); + registerStrategyNode(f, e, role_equal, visited, strategy_lemmas); } void SygusUnifRl::registerStrategyNode( Node f, Node e, NodeRole nrole, - std::map>& visited) + std::map>& visited, + std::map>& strategy_lemmas) { Trace("sygus-unif-rl-strat") << " register node " << e << std::endl; if (visited[e].find(nrole) != visited[e].end()) @@ -417,17 +420,19 @@ void SygusUnifRl::registerStrategyNode( << " ...detected recursive ITE strategy, condition enumerator : " << cond << std::endl; // indicate that we will be enumerating values for cond - registerConditionalEnumerator(f, e, cond, j); + registerConditionalEnumerator(f, e, cond, j, strategy_lemmas); } } // TODO: recurse? for (std::pair& cec : etis->d_cenum) } } -void SygusUnifRl::registerConditionalEnumerator(Node f, - Node e, - Node cond, - unsigned strategy_index) +void SygusUnifRl::registerConditionalEnumerator( + Node f, + Node e, + Node cond, + unsigned strategy_index, + std::map>& strategy_lemmas) { // we will do unification for this candidate d_unif_candidates.insert(f); @@ -440,6 +445,20 @@ void SygusUnifRl::registerConditionalEnumerator(Node f, // register the conditional enumerator d_tds->registerEnumerator(cond, f, d_parent, true); d_cenum_to_stratpt[cond].clear(); + // register lemmas to remove redundant operators from condition enumeration + std::map>::iterator it = + strategy_lemmas.find(cond); + if (it != strategy_lemmas.end()) + { + for (const Node& lemma : it->second) + { + Trace("cegis-unif-enum-debug") + << "* Registering lemma to remove redundand operators for " << cond + << " --> " << lemma << "\n"; + d_qe->getOutputChannel().lemma(lemma); + } + strategy_lemmas.erase(cond); + } } // register that this strategy node has a decision tree construction d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index); diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 58cf9011e..941bb5763 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -53,7 +53,7 @@ class SygusUnifRl : public SygusUnif void initialize(QuantifiersEngine* qe, const std::vector& funs, std::vector& enums, - std::vector& lemmas) override; + std::map>& strategy_lemmas) override; /** Notify enumeration */ void notifyEnumeration(Node e, Node v, std::vector& lemmas) override; /** Construct solution */ @@ -261,27 +261,40 @@ class SygusUnifRl : public SygusUnif * * Initialize the above data for the relevant enumerators in the strategy tree * of candidate variable f. + * + * Lemmas to remove redundant operators from enumerators of specific strategy + * points, if any, are retrived from strategy_lemmas. */ - void registerStrategy(Node f); + void registerStrategy(Node f, + std::map>& strategy_lemmas); /** register strategy node * * Called while traversing the strategy tree of f. The arguments e and nrole * indicate the current node in the tree we are traversing, and visited * indicates the nodes we have already visited. + * + * Lemmas to remove redundant operators from enumerators of specific strategy + * points, if any, are retrived from strategy_lemmas. */ void registerStrategyNode(Node f, Node e, NodeRole nrole, - std::map>& visited); + std::map>& visited, + std::map>& strategy_lemmas); /** register conditional enumerator * * Registers that cond is a conditional enumerator for building a (recursive) * decision tree at strategy node e within the strategy tree of f. + * + * Lemmas to remove redundant operators from enumerators of specific strategy + * points, if any, are retrived from strategy_lemmas. */ - void registerConditionalEnumerator(Node f, - Node e, - Node cond, - unsigned strategy_index); + void registerConditionalEnumerator( + Node f, + Node e, + Node cond, + unsigned strategy_index, + std::map>& strategy_lemmas); }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index d3a5d6c23..a3158fbe8 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -680,7 +680,8 @@ bool SygusUnifStrategy::inferTemplate( return true; } -void SygusUnifStrategy::staticLearnRedundantOps(std::vector& lemmas) +void SygusUnifStrategy::staticLearnRedundantOps( + std::map>& strategy_lemmas) { for (unsigned i = 0; i < d_esym_list.size(); i++) { @@ -716,6 +717,7 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector& lemmas) Node em = nce.first; const Datatype& dt = static_cast(em.getType().toType()).getDatatype(); + std::vector lemmas; for (std::pair& nc : nce.second) { Assert(nc.first < dt.getNumConstructors()); @@ -723,6 +725,7 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector& lemmas) { Node tst = datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate(); + if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end()) { Trace("sygus-unif") << "...can exclude based on : " << tst @@ -731,6 +734,10 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector& lemmas) } } } + if (!lemmas.empty()) + { + strategy_lemmas[em] = lemmas; + } } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 8f9adefb9..a24e323e8 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -274,13 +274,15 @@ class SygusUnifStrategy * * This learns static lemmas for pruning enumerative space based on the * strategy for the function-to-synthesize of this class, and stores these - * into lemmas. + * into strategy_lemmas. * * 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). */ - void staticLearnRedundantOps(std::vector& lemmas); + void staticLearnRedundantOps( + std::map>& strategy_lemmas); + /** debug print this strategy on Trace c */ void debugPrint(const char* c); -- 2.30.2