From 4e56fd1578c51544d879cf84a4ea48c5f09a1d97 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 May 2018 16:33:17 -0500 Subject: [PATCH] Infrastructure to mark unused sygus strategies (#1950) --- .../quantifiers/sygus/sygus_unif_rl.cpp | 20 ++- src/theory/quantifiers/sygus/sygus_unif_rl.h | 26 +-- .../quantifiers/sygus/sygus_unif_strat.cpp | 20 ++- .../quantifiers/sygus/sygus_unif_strat.h | 7 + test/regress/Makefile.tests | 1 + test/regress/regress1/sygus/planning-unif.sy | 149 ++++++++++++++++++ 6 files changed, 206 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress1/sygus/planning-unif.sy 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 SygusUnifRl::getEvalPointHeads(Node c) return it->second; } -void SygusUnifRl::registerStrategy(Node f, std::vector& enums) +void SygusUnifRl::registerStrategy( + Node f, + std::vector& enums, + std::map>& unused_strats) { if (Trace.isOn("sygus-unif-rl-strat")) { @@ -397,7 +401,7 @@ void SygusUnifRl::registerStrategy(Node f, std::vector& enums) Trace("sygus-unif-rl-strat") << "Register..." << std::endl; Node e = d_strategy[f].getRootEnumerator(); std::map> 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>& visited, - std::vector& enums) + std::vector& enums, + std::map>& 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 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& 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& enums); + void registerStrategy( + Node f, + std::vector& enums, + std::map>& 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>& visited, - std::vector& enums); + void registerStrategyNode( + Node f, + Node e, + NodeRole nrole, + std::map>& visited, + std::vector& enums, + std::map>& 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 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>::iterator itus = + restrictions.d_unused_strategies.find(e); + std::unordered_set 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(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> d_unused_strategies; }; /** diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index ca22aba5f..72bf64ac8 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1502,6 +1502,7 @@ REG1_TESTS = \ regress1/sygus/no-flat-simp.sy \ regress1/sygus/no-mention.sy \ regress1/sygus/pbe_multi.sy \ + regress1/sygus/planning-unif.sy \ regress1/sygus/process-10-vars.sy \ regress1/sygus/qe.sy \ regress1/sygus/real-grammar.sy \ diff --git a/test/regress/regress1/sygus/planning-unif.sy b/test/regress/regress1/sygus/planning-unif.sy new file mode 100644 index 000000000..39c89dc53 --- /dev/null +++ b/test/regress/regress1/sygus/planning-unif.sy @@ -0,0 +1,149 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-unif --sygus-out=status +(set-logic LIA) + +(define-fun get-y ((currPoint Int)) Int +(ite (< currPoint 10) 0 (ite (< currPoint 20) 1 (ite (< currPoint 30) 2 (ite (< currPoint 40) 3 (ite (< currPoint 50) 4 (ite (< currPoint 60) 5 (ite (< currPoint 70) 6 (ite (< currPoint 80) 7 (ite (< currPoint 90) 8 9)))))))))) + +(define-fun get-x ((currPoint Int)) Int + (- currPoint (* (get-y currPoint) 10))) +(define-fun interpret-move (( currPoint Int ) ( move Int)) Int +(ite (= move 0) currPoint +(ite (= move 1) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) +(ite (= move 2) (ite (or (< (+ (get-x currPoint) 1) 0) (>= (+ (get-x currPoint) 1) 10)) currPoint (+ currPoint 1)) +(ite (= move 3) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) +(ite (= move 4) (ite (or (< (+ (get-x currPoint) -1) 0) (>= (+ (get-x currPoint) -1) 10)) currPoint (+ currPoint -1)) +currPoint)))))) + +(define-fun interpret-move-obstacle-0 (( currPoint Int ) ( move Int)) Int +(ite (= move 0) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) +(ite (= move 1) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) +currPoint))) + +(define-fun interpret-move-obstacle-1 (( currPoint Int ) ( move Int)) Int +(ite (= move 0) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) +(ite (= move 1) currPoint +(ite (= move 2) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) +currPoint)))) + +(define-fun allowable-move-obstacle-0 (( start Int ) ( end Int)) Bool + (or (= (interpret-move-obstacle-0 start 0) end) + (or (= (interpret-move-obstacle-0 start 1) end) false))) + +(define-fun allowable-move-obstacle-1 (( start Int ) ( end Int)) Bool + (or (= (interpret-move-obstacle-1 start 0) end) + (or (= (interpret-move-obstacle-1 start 1) end) + (or (= (interpret-move-obstacle-1 start 2) end) false)))) + +(define-fun get-move-obstacle-0 (( start Int ) ( end Int)) Int + (ite (= (interpret-move-obstacle-0 start 0) end) 0 + (ite (= (interpret-move-obstacle-0 start 1) end) 1 -1))) + +(define-fun get-move-obstacle-1 (( start Int ) ( end Int)) Int + (ite (= (interpret-move-obstacle-1 start 0) end) 0 + (ite (= (interpret-move-obstacle-1 start 1) end) 1 + (ite (= (interpret-move-obstacle-1 start 2) end) 2 -1)))) + +(define-fun no-overlap-one-move-combination-2-2 ((p0 Int) (p1 Int) (p2 Int) (p3 Int)) Bool + (and (not (= p0 p2)) (and (not (= p0 p3)) (and (not (= p1 p2)) (and (not (= p1 p3)) true))))) + +(define-fun no-overlaps-0 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool + (= 1 + (ite (= move 0) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) + (ite (= move 1) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) + (ite (= move 2) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) + (ite (= move 3) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) + (ite (= move 4) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) 0))))))) + +(define-fun no-overlaps-1 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool + (= 1 + (ite (= move 0) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) + (ite (= move 1) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) + (ite (= move 2) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) + (ite (= move 3) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) + (ite (= move 4) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) 0))))))) + +(define-fun no-overlaps-one-step-helper ((currPoint Int) (move Int) (o0-t Int) (o0move Int) (o1-t Int) (o1move Int)) Bool + (and (no-overlaps-0 currPoint move o0-t o0move) (and (no-overlaps-1 currPoint move o1-t o1move) true))) + +(define-fun no-overlaps-one-step ((currPoint Int) (move Int) (o0-0 Int) (o0-1 Int) (o1-0 Int) (o1-1 Int)) Bool + (no-overlaps-one-step-helper currPoint move o0-0 (get-move-obstacle-0 o0-0 o0-1) o1-0 (get-move-obstacle-1 o1-0 o1-1))) + + + +(declare-var o0-1 Int) +(declare-var o0-2 Int) +(declare-var o0-3 Int) +(declare-var o1-1 Int) +(declare-var o1-2 Int) +(declare-var o1-3 Int) + +(synth-fun move ((currPoint Int) (o0 Int) (o1 Int)) Int + ((Start Int ( + MoveId + (ite StartBool Start Start))) + (MoveId Int (0 + 1 + 2 + 3 + 4 + )) + (CondInt Int ( + (get-y currPoint) ;y coord + (get-x currPoint) ;x coord + (get-y o0) + (get-x o0) + (get-y o1) + (get-x o1) + (+ CondInt CondInt) + (- CondInt CondInt) + -1 + 0 + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + )) + (StartBool Bool ((and StartBool StartBool) + (or StartBool StartBool) + (not StartBool) + (<= CondInt CondInt) + (= CondInt CondInt) + (>= CondInt CondInt))))) + + (constraint (or + (and + (= (interpret-move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2)) 30) + (and (no-overlaps-one-step 0 (move 0 99 98) 99 o0-1 98 o1-1) (and (no-overlaps-one-step (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1) o0-1 o0-2 o1-1 o1-2) (and (no-overlaps-one-step (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2) o0-2 o0-3 o1-2 o1-3) true)))) + (not (and (allowable-move-obstacle-0 99 o0-1) (and (allowable-move-obstacle-0 o0-1 o0-2) (and (allowable-move-obstacle-0 o0-2 o0-3) (and (allowable-move-obstacle-1 98 o1-1) (and (allowable-move-obstacle-1 o1-1 o1-2) (and (allowable-move-obstacle-1 o1-2 o1-3) true))))))))) +(check-synth) -- 2.30.2