From: Gereon Kremer Date: Tue, 9 Nov 2021 16:34:31 +0000 (-0800) Subject: Make secant points user context dependent (#7567) X-Git-Tag: cvc5-1.0.0~851 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=656db44c77c6728ab72f84fb286cca7906bb4366;p=cvc5.git 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 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 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 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 spoints = d_secant_points[e][d]; + std::vector 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>> + std::unordered_map>> d_secant_points; /** PI