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.

diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 5b6db69b84c9851d15ba89f2d51246c4ec005b74..9e204f582ac654eb18382926934f8710c2c99d27 100644 (file)
--- 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 19a3347298688015b5d9ffcac251eda332c73ad5..2fcbcdb384f022e7ad888bb6dcd47b241ac8e2c1 100644 (file)
--- 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 65215c83caff21c1a804b9b8b394302009e1880f..77fcf57fbdddd30c8fa4e660e31830760ff70f3c 100644 (file)
--- 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