Infrastructure to mark unused sygus strategies (#1950)

6 files changed, 206 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;
 };
 
 /**
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)