From 656db44c77c6728ab72f84fb286cca7906bb4366 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Tue, 9 Nov 2021 08:34:31 -0800
Subject: [PATCH] Make secant points user context dependent (#7567)

This PR fixes an issue where the secant points associated with certain transcendental lemmas were not properly cleared when leaving a user context.
Closes #4694.
---
 .../nl/transcendental/transcendental_solver.cpp    |  9 ++++++++-
 .../nl/transcendental/transcendental_state.cpp     | 14 +++++++++-----
 .../arith/nl/transcendental/transcendental_state.h |  2 +-
 3 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 5b6db69b8..9e204f582 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -182,7 +182,14 @@ void TranscendentalSolver::processSideEffect(const NlLemma& se)
     Node tf = std::get<0>(sp);
     unsigned d = std::get<1>(sp);
     Node c = std::get<2>(sp);
-    d_tstate.d_secant_points[tf][d].push_back(c);
+    // we have a CDList within the maps, creating it requires some care
+    auto& secant_points = d_tstate.d_secant_points[tf];
+    auto it = secant_points.find(d);
+    if (it == secant_points.end())
+    {
+      it = secant_points.emplace(d, d_tstate.d_env.getUserContext()).first;
+    }
+    it->second.push_back(c);
   }
 }
 
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 19a334729..2fcbcdb38 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -178,7 +178,7 @@ void TranscendentalState::ensureCongruence(TNode a,
     if (mvaa != mvaaa)
     {
       std::vector<Node> exp;
-      for (unsigned j = 0, size = a.getNumChildren(); j < size; j++)
+      for (uint64_t j = 0, size = a.getNumChildren(); j < size; j++)
       {
         exp.push_back(a[j].eqNode(aa[j]));
       }
@@ -234,16 +234,20 @@ std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e,
                                                                   TNode center,
                                                                   unsigned d)
 {
+  auto spit = d_secant_points[e].find(d);
+  if (spit == d_secant_points[e].end())
+  {
+    spit = d_secant_points[e].emplace(d, d_env.getUserContext()).first;
+  }
   // bounds are the minimum and maximum previous secant points
   // should not repeat secant points: secant lemmas should suffice to
   // rule out previous assignment
-  Assert(std::find(
-             d_secant_points[e][d].begin(), d_secant_points[e][d].end(), center)
-         == d_secant_points[e][d].end());
+  Assert(std::find(spit->second.begin(), spit->second.end(), center)
+         == spit->second.end());
   // Insert into the (temporary) vector. We do not update this vector
   // until we are sure this secant plane lemma has been processed. We do
   // this by mapping the lemma to a side effect below.
-  std::vector<Node> spoints = d_secant_points[e][d];
+  std::vector<Node> spoints{spit->second.begin(), spit->second.end()};
   spoints.push_back(center);
 
   // sort
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 65215c83c..77fcf57fb 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -246,7 +246,7 @@ struct TranscendentalState
    * each transcendental function application. We store this set for each
    * Taylor degree.
    */
-  std::unordered_map<Node, std::map<unsigned, std::vector<Node>>>
+  std::unordered_map<Node, std::map<uint64_t, context::CDList<Node>>>
       d_secant_points;
 
   /** PI
-- 
2.30.2