diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-21 16:33:17 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-21 16:33:17 -0500 |
commit | 4e56fd1578c51544d879cf84a4ea48c5f09a1d97 (patch) | |
tree | f31f109299c382f6dffe14682d2130041d39c094 /src | |
parent | d5e51b2f33773837768a5d89f9be2928f1551d27 (diff) |
Infrastructure to mark unused sygus strategies (#1950)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.h | 26 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.h | 7 |
4 files changed, 56 insertions, 17 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index be8d6c5ca..a96505ce4 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -44,8 +44,9 @@ void SygusUnifRl::initializeCandidate( { restrictions.d_iteReturnBoolConst = true; } + // register the strategy + registerStrategy(f, enums, restrictions.d_unused_strategies); 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()) { @@ -386,7 +387,10 @@ std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c) return it->second; } -void SygusUnifRl::registerStrategy(Node f, std::vector<Node>& enums) +void SygusUnifRl::registerStrategy( + Node f, + std::vector<Node>& enums, + std::map<Node, std::unordered_set<unsigned>>& unused_strats) { if (Trace.isOn("sygus-unif-rl-strat")) { @@ -397,7 +401,7 @@ void SygusUnifRl::registerStrategy(Node f, std::vector<Node>& enums) Trace("sygus-unif-rl-strat") << "Register..." << std::endl; Node e = d_strategy[f].getRootEnumerator(); std::map<Node, std::map<NodeRole, bool>> visited; - registerStrategyNode(f, e, role_equal, visited, enums); + registerStrategyNode(f, e, role_equal, visited, enums, unused_strats); } void SygusUnifRl::registerStrategyNode( @@ -405,7 +409,8 @@ void SygusUnifRl::registerStrategyNode( Node e, NodeRole nrole, std::map<Node, std::map<NodeRole, bool>>& visited, - std::vector<Node>& enums) + std::vector<Node>& enums, + std::map<Node, std::unordered_set<unsigned>>& unused_strats) { Trace("sygus-unif-rl-strat") << " register node " << e << std::endl; if (visited[e].find(nrole) != visited[e].end()) @@ -421,9 +426,10 @@ void SygusUnifRl::registerStrategyNode( EnumTypeInfoStrat* etis = snode.d_strats[j]; StrategyType strat = etis->d_this; // is this a simple recursive ITE strategy? + bool success = false; if (strat == strat_ITE && nrole == role_equal) { - bool success = true; + success = true; for (unsigned c = 1; c <= 2; c++) { std::pair<Node, NodeRole> child = etis->d_cenum[c]; @@ -446,6 +452,10 @@ void SygusUnifRl::registerStrategyNode( enums.push_back(e); } } + if (!success) + { + unused_strats[e].insert(j); + } // TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum) } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 8a5230d15..072766b21 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -297,21 +297,29 @@ class SygusUnifRl : public SygusUnif * * Initialize the above data for the relevant enumerators in the strategy tree * of candidate variable f. For each strategy point e which there is a - * decision tree strategy, we add e to enums. + * decision tree strategy, we add e to enums. For each strategy with index + * i in an strategy point e, if we are not using the strategy, we add i to + * unused_strats[e]. This map is later passed to + * SygusUnifStrategy::staticLearnRedundantOps. */ - void registerStrategy(Node f, std::vector<Node>& enums); + void registerStrategy( + Node f, + std::vector<Node>& enums, + std::map<Node, std::unordered_set<unsigned>>& unused_strats); /** 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. If e has a decision tree - * strategy, it is added to enums. + * indicates the nodes we have already visited. The arguments enums and + * unused_strats are modified as described above. */ - void registerStrategyNode(Node f, - Node e, - NodeRole nrole, - std::map<Node, std::map<NodeRole, bool>>& visited, - std::vector<Node>& enums); + void registerStrategyNode( + Node f, + Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool>>& visited, + std::vector<Node>& enums, + std::map<Node, std::unordered_set<unsigned>>& unused_strats); /** register conditional enumerator * * Registers that cond is a conditional enumerator for building a (recursive) diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 2f3d5b874..e236613c0 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -785,15 +785,29 @@ void SygusUnifStrategy::staticLearnRedundantOps( TypeNode etn = e.getType(); EnumTypeInfo& tinfo = getEnumTypeInfo(etn); StrategyNode& snode = tinfo.getStrategyNode(nrole); + // the constructors of the current strategy point we need std::map<unsigned, bool> needs_cons_curr; - // constructors that correspond to strategies are not needed - // the intuition is that the strategy itself is responsible for constructing - // all terms that use the given constructor + // get the unused strategies + std::map<Node, std::unordered_set<unsigned>>::iterator itus = + restrictions.d_unused_strategies.find(e); + std::unordered_set<unsigned> unused_strats; + if (itus != restrictions.d_unused_strategies.end()) + { + unused_strats.insert(itus->second.begin(), itus->second.end()); + } for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) { + // if we are not using this strategy, there is nothing to do + if (unused_strats.find(j) != unused_strats.end()) + { + continue; + } EnumTypeInfoStrat* etis = snode.d_strats[j]; unsigned cindex = static_cast<unsigned>(Datatype::indexOf(etis->d_cons.toExpr())); + // constructors that correspond to strategies are not needed + // the intuition is that the strategy itself is responsible for constructing + // all terms that use the given constructor Trace("sygus-strat-slearn") << "...by strategy, can exclude operator " << etis->d_cons << std::endl; needs_cons_curr[cindex] = false; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 0c7f207be..cbce5e70c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -256,6 +256,13 @@ struct StrategyRestrictions * the condition values of ITEs to be restricted to atoms */ bool d_iteCondOnlyAtoms; + /** + * A list of unused strategies. This maps strategy points to the indices + * in StrategyNode::d_strats that are not used by the caller of + * staticLearnRedundantOps, and hence should not be taken into account + * when doing redundant operator learning. + */ + std::map<Node, std::unordered_set<unsigned>> d_unused_strategies; }; /** |