Fix out-of-sync pruning in CDCAC proofs (#7470)

This PR resolves a subtle issue with CDCAC proofs.
The CDCAC proof is maintained as a tree where (mostly) every node corresponds to an (infeasible) interval generated within the CDCAC method. We prune these intervals regularly to get rid of redundant intervals, which also sorts intervals. The pruning however relied on a stable ordering of both intervals and child nodes within the proof tree, as there was no easy way to map nodes back to intervals.
This PR adds an objectId field to the proof tree nodes and assigns ids to the CDCAC intervals. This allows for a robust mapping between the two, even if the interval list is reordered.

Fixes cvc5/cvc5-projects#313.

9 files changed, 119 insertions, 59 deletions

diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp
index 225a6c75c..e397ea353 100644
--- a/src/proof/lazy_tree_proof_generator.cpp
+++ b/src/proof/lazy_tree_proof_generator.cpp
@@ -46,12 +46,14 @@ detail::TreeProofNode& LazyTreeProofGenerator::getCurrent()
   Assert(!d_stack.empty()) << "Proof construction has already been finished.";
   return *d_stack.back();
 }
-void LazyTreeProofGenerator::setCurrent(PfRule rule,
+void LazyTreeProofGenerator::setCurrent(size_t objectId,
+                                        PfRule rule,
                                         const std::vector<Node>& premise,
                                         std::vector<Node> args,
                                         Node proven)
 {
   detail::TreeProofNode& pn = getCurrent();
+  pn.d_objectId = objectId;
   pn.d_rule = rule;
   pn.d_premise = premise;
   pn.d_args = args;
diff --git a/src/proof/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h
index ff5d0ad2e..314685843 100644
--- a/src/proof/lazy_tree_proof_generator.h
+++ b/src/proof/lazy_tree_proof_generator.h
@@ -31,9 +31,13 @@ namespace detail {
  * A node directly represents a ProofNode that is eventually constructed from
  * it. The Nodes of the additional field d_premise are added to d_children as
  * new assumptions via ASSUME.
+ * The object id can be used to store an arbitrary id to identify tree nodes
+ * and map them back to some other type, for example during pruning.
  */
 struct TreeProofNode
 {
+  /** Storage for some custom object identifier, used for pruning */
+  size_t d_objectId;
   /** The proof rule */
   PfRule d_rule = PfRule::UNKNOWN;
   /** Assumptions used as premise for this proof step */
@@ -145,7 +149,8 @@ class LazyTreeProofGenerator : public ProofGenerator
    */
   detail::TreeProofNode& getCurrent();
   /** Set the current node / proof step */
-  void setCurrent(PfRule rule,
+  void setCurrent(size_t objectId,
+                  PfRule rule,
                   const std::vector<Node>& premise,
                   std::vector<Node> args,
                   Node proven);
@@ -174,7 +179,7 @@ class LazyTreeProofGenerator : public ProofGenerator
     std::size_t pos = 0;
     for (std::size_t size = children.size(); cur < size; ++cur)
     {
-      if (f(cur, children[pos]))
+      if (f(children[pos]))
       {
         if (cur != pos)
         {
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index d259bc096..4a2709cf8 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -55,6 +55,7 @@ void CDCAC::reset()
 {
   d_constraints.reset();
   d_assignment.clear();
+  d_nextIntervalId = 1;
 }
 
 void CDCAC::computeVariableOrdering()
@@ -150,7 +151,7 @@ std::vector<CACInterval> CDCAC::getUnsatIntervals(std::size_t cur_variable)
       m.pushDownPolys(d, d_variableOrdering[cur_variable]);
       if (!is_minus_infinity(get_lower(i))) l = m;
       if (!is_plus_infinity(get_upper(i))) u = m;
-      res.emplace_back(CACInterval{i, l, u, m, d, {n}});
+      res.emplace_back(CACInterval{d_nextIntervalId++, i, l, u, m, d, {n}});
       if (isProofEnabled())
       {
         d_proof->addDirect(
@@ -160,7 +161,8 @@ std::vector<CACInterval> CDCAC::getUnsatIntervals(std::size_t cur_variable)
             d_assignment,
             sc,
             i,
-            n);
+            n,
+            res.back().d_id);
       }
     }
   }
@@ -293,18 +295,21 @@ PolyVector requiredCoefficientsLazardModified(
 
 PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p)
 {
-  if (Trace.isOn("cdcac"))
+  if (Trace.isOn("cdcac::projection"))
   {
-    Trace("cdcac") << "Poly: " << p << " over " << d_assignment << std::endl;
-    Trace("cdcac") << "Lazard:   "
-                   << requiredCoefficientsLazard(p, d_assignment) << std::endl;
-    Trace("cdcac") << "LMod: "
-                   << requiredCoefficientsLazardModified(
-                          p, d_assignment, d_constraints.varMapper())
-                   << std::endl;
-    Trace("cdcac") << "Original: "
-                   << requiredCoefficientsOriginal(p, d_assignment)
-                   << std::endl;
+    Trace("cdcac::projection")
+        << "Poly: " << p << " over " << d_assignment << std::endl;
+    Trace("cdcac::projection")
+        << "Lazard:   " << requiredCoefficientsLazard(p, d_assignment)
+        << std::endl;
+    Trace("cdcac::projection")
+        << "LMod: "
+        << requiredCoefficientsLazardModified(
+               p, d_assignment, d_constraints.varMapper())
+        << std::endl;
+    Trace("cdcac::projection")
+        << "Original: " << requiredCoefficientsOriginal(p, d_assignment)
+        << std::endl;
   }
   switch (options().arith.nlCadProjection)
   {
@@ -346,15 +351,16 @@ PolyVector CDCAC::constructCharacterization(std::vector<CACInterval>& intervals)
     }
     for (const auto& p : i.d_mainPolys)
     {
-      Trace("cdcac") << "Discriminant of " << p << " -> " << discriminant(p)
-                     << std::endl;
+      Trace("cdcac::projection")
+          << "Discriminant of " << p << " -> " << discriminant(p) << std::endl;
       // Add all discriminants
       res.add(discriminant(p));
 
       for (const auto& q : requiredCoefficients(p))
       {
         // Add all required coefficients
-        Trace("cdcac") << "Coeff of " << p << " -> " << q << std::endl;
+        Trace("cdcac::projection")
+            << "Coeff of " << p << " -> " << q << std::endl;
         res.add(q);
       }
       for (const auto& q : i.d_lowerPolys)
@@ -362,8 +368,8 @@ PolyVector CDCAC::constructCharacterization(std::vector<CACInterval>& intervals)
         if (p == q) continue;
         // Check whether p(s \times a) = 0 for some a <= l
         if (!hasRootBelow(q, get_lower(i.d_interval))) continue;
-        Trace("cdcac") << "Resultant of " << p << " and " << q << " -> "
-                       << resultant(p, q) << std::endl;
+        Trace("cdcac::projection") << "Resultant of " << p << " and " << q
+                                   << " -> " << resultant(p, q) << std::endl;
         res.add(resultant(p, q));
       }
       for (const auto& q : i.d_upperPolys)
@@ -371,8 +377,8 @@ PolyVector CDCAC::constructCharacterization(std::vector<CACInterval>& intervals)
         if (p == q) continue;
         // Check whether p(s \times a) = 0 for some a >= u
         if (!hasRootAbove(q, get_upper(i.d_interval))) continue;
-        Trace("cdcac") << "Resultant of " << p << " and " << q << " -> "
-                       << resultant(p, q) << std::endl;
+        Trace("cdcac::projection") << "Resultant of " << p << " and " << q
+                                   << " -> " << resultant(p, q) << std::endl;
         res.add(resultant(p, q));
       }
     }
@@ -385,8 +391,8 @@ PolyVector CDCAC::constructCharacterization(std::vector<CACInterval>& intervals)
     {
       for (const auto& q : intervals[i + 1].d_lowerPolys)
       {
-        Trace("cdcac") << "Resultant of " << p << " and " << q << " -> "
-                       << resultant(p, q) << std::endl;
+        Trace("cdcac::projection") << "Resultant of " << p << " and " << q
+                                   << " -> " << resultant(p, q) << std::endl;
         res.add(resultant(p, q));
       }
     }
@@ -477,25 +483,31 @@ CACInterval CDCAC::intervalFromCharacterization(
   if (lower == upper)
   {
     // construct a point interval
-    return CACInterval{
-        poly::Interval(lower, false, upper, false), l, u, m, d, {}};
+    return CACInterval{d_nextIntervalId++,
+                       poly::Interval(lower, false, upper, false),
+                       l,
+                       u,
+                       m,
+                       d,
+                       {}};
   }
   else
   {
     // construct an open interval
     Assert(lower < upper);
-    return CACInterval{
-        poly::Interval(lower, true, upper, true), l, u, m, d, {}};
+    return CACInterval{d_nextIntervalId++,
+                       poly::Interval(lower, true, upper, true),
+                       l,
+                       u,
+                       m,
+                       d,
+                       {}};
   }
 }
 
-std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
-                                              bool returnFirstInterval)
+std::vector<CACInterval> CDCAC::getUnsatCoverImpl(std::size_t curVariable,
+                                                  bool returnFirstInterval)
 {
-  if (isProofEnabled())
-  {
-    d_proof->startRecursive();
-  }
   Trace("cdcac") << "Looking for unsat cover for "
                  << d_variableOrdering[curVariable] << std::endl;
   std::vector<CACInterval> intervals = getUnsatIntervals(curVariable);
@@ -537,9 +549,10 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
     if (isProofEnabled())
     {
       d_proof->startScope();
+      d_proof->startRecursive();
     }
     // Recurse to next variable
-    auto cov = getUnsatCover(curVariable + 1);
+    auto cov = getUnsatCoverImpl(curVariable + 1);
     if (cov.empty())
     {
       // Found SAT!
@@ -558,6 +571,7 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
     intervals.emplace_back(newInterval);
     if (isProofEnabled())
     {
+      d_proof->endRecursive(newInterval.d_id);
       auto cell = d_proof->constructCell(
           d_constraints.varMapper()(d_variableOrdering[curVariable]),
           newInterval,
@@ -596,11 +610,21 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
       Trace("cdcac") << "-> " << i.d_interval << std::endl;
     }
   }
+  return intervals;
+}
+
+std::vector<CACInterval> CDCAC::getUnsatCover(bool returnFirstInterval)
+{
+  if (isProofEnabled())
+  {
+    d_proof->startRecursive();
+  }
+  auto res = getUnsatCoverImpl(0, returnFirstInterval);
   if (isProofEnabled())
   {
-    d_proof->endRecursive();
+    d_proof->endRecursive(0);
   }
-  return intervals;
+  return res;
 }
 
 void CDCAC::startNewProof()
@@ -639,7 +663,8 @@ CACInterval CDCAC::buildIntegralityInterval(std::size_t cur_variable,
   poly::Integer below = poly::floor(value);
   poly::Integer above = poly::ceil(value);
   // construct var \in (below, above)
-  return CACInterval{poly::Interval(below, above),
+  return CACInterval{d_nextIntervalId++,
+                     poly::Interval(below, above),
                      {var - below},
                      {var - above},
                      {var - below, var - above},
@@ -669,10 +694,11 @@ void CDCAC::pruneRedundantIntervals(std::vector<CACInterval>& intervals)
 {
   if (isProofEnabled())
   {
-    std::vector<CACInterval> allIntervals = intervals;
     cleanIntervals(intervals);
-    d_proof->pruneChildren([&allIntervals, &intervals](std::size_t i) {
-      return std::find(intervals.begin(), intervals.end(), allIntervals[i])
+    d_proof->pruneChildren([&intervals](std::size_t id) {
+      return std::find_if(intervals.begin(),
+                          intervals.end(),
+                          [id](const CACInterval& i) { return i.d_id == id; })
              != intervals.end();
     });
   }
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index be72e4063..04b5cab24 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -123,6 +123,18 @@ class CDCAC : protected EnvObj
                                            const poly::Value& sample);
 
   /**
+   * Internal implementation of getUnsatCover().
+   * @param curVariable The id of the variable (within d_variableOrdering) to
+   * be considered. This argument is used to manage the recursion internally and
+   * should always be zero if called externally.
+   * @param returnFirstInterval If true, the function returns after the first
+   * interval obtained from a recursive call. The result is not (necessarily) an
+   * unsat cover, but merely a list of infeasible intervals.
+   */
+  std::vector<CACInterval> getUnsatCoverImpl(std::size_t curVariable = 0,
+                                             bool returnFirstInterval = false);
+
+  /**
    * Main method that checks for the satisfiability of the constraints.
    * Recursively explores possible assignments and excludes regions based on the
    * coverings. Returns either a covering for the lowest dimension or an empty
@@ -130,15 +142,13 @@ class CDCAC : protected EnvObj
    * be obtained from d_assignment. If the covering is not empty, the result is
    * UNSAT and an infeasible subset can be extracted from the returned covering.
    * Implements Algorithm 2.
-   * @param curVariable The id of the variable (within d_variableOrdering) to
-   * be considered. This argument is used to manage the recursion internally and
-   * should always be zero if called externally.
+   * This method itself only takes care of the outermost proof scope and calls
+   * out to getUnsatCoverImpl() with curVariable set to zero.
    * @param returnFirstInterval If true, the function returns after the first
    * interval obtained from a recursive call. The result is not (necessarily) an
    * unsat cover, but merely a list of infeasible intervals.
    */
-  std::vector<CACInterval> getUnsatCover(std::size_t curVariable = 0,
-                                         bool returnFirstInterval = false);
+  std::vector<CACInterval> getUnsatCover(bool returnFirstInterval = false);
 
   void startNewProof();
   /**
@@ -205,6 +215,9 @@ class CDCAC : protected EnvObj
 
   /** The proof generator */
   std::unique_ptr<CADProofGenerator> d_proof;
+
+  /** The next interval id */
+  size_t d_nextIntervalId = 1;
 };
 
 }  // namespace cad
diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h
index 8fde21fde..9eb761ae3 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.h
+++ b/src/theory/arith/nl/cad/cdcac_utils.h
@@ -38,6 +38,7 @@ namespace cad {
  * https://arxiv.org/pdf/2003.05633.pdf.
  *
  * It consists of
+ * - the interval id, used to map the interval to its (partial) proof,
  * - the actual interval, either an open or a point interal,
  * - the characterizing polynomials of the lower and upper bound,
  * - the characterizing polynomials in the main variable,
@@ -46,6 +47,8 @@ namespace cad {
  */
 struct CACInterval
 {
+  /** Id of this interval to couple it to the proof */
+  size_t d_id;
   /** The actual interval. */
   poly::Interval d_interval;
   /** The polynomials characterizing the lower bound. */
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index a74913d99..b56c2755a 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -102,9 +102,10 @@ void CADProofGenerator::startNewProof()
   d_current = d_proofs.allocateProof();
 }
 void CADProofGenerator::startRecursive() { d_current->openChild(); }
-void CADProofGenerator::endRecursive()
+void CADProofGenerator::endRecursive(size_t intervalId)
 {
-  d_current->setCurrent(PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false);
+  d_current->setCurrent(
+      intervalId, PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false);
   d_current->closeChild();
 }
 void CADProofGenerator::startScope()
@@ -114,7 +115,7 @@ void CADProofGenerator::startScope()
 }
 void CADProofGenerator::endScope(const std::vector<Node>& args)
 {
-  d_current->setCurrent(PfRule::SCOPE, {}, args, d_false);
+  d_current->setCurrent(0, PfRule::SCOPE, {}, args, d_false);
   d_current->closeChild();
 }
 
@@ -129,15 +130,19 @@ void CADProofGenerator::addDirect(Node var,
                                   const poly::Assignment& a,
                                   poly::SignCondition& sc,
                                   const poly::Interval& interval,
-                                  Node constraint)
+                                  Node constraint,
+                                  size_t intervalId)
 {
   if (is_minus_infinity(get_lower(interval))
       && is_plus_infinity(get_upper(interval)))
   {
     // "Full conflict", constraint excludes (-inf,inf)
     d_current->openChild();
-    d_current->setCurrent(
-        PfRule::ARITH_NL_CAD_DIRECT, {constraint}, {d_false}, d_false);
+    d_current->setCurrent(intervalId,
+                          PfRule::ARITH_NL_CAD_DIRECT,
+                          {constraint},
+                          {d_false},
+                          d_false);
     d_current->closeChild();
     return;
   }
@@ -173,8 +178,11 @@ void CADProofGenerator::addDirect(Node var,
   // Add to proof manager
   startScope();
   d_current->openChild();
-  d_current->setCurrent(
-      PfRule::ARITH_NL_CAD_DIRECT, {constraint}, {d_false}, d_false);
+  d_current->setCurrent(intervalId,
+                        PfRule::ARITH_NL_CAD_DIRECT,
+                        {constraint},
+                        {d_false},
+                        d_false);
   d_current->closeChild();
   endScope(res);
 }
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 613db7565..2f05ff11b 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -62,7 +62,7 @@ class CADProofGenerator
   /** Start a new recursive call */
   void startRecursive();
   /** Finish the current recursive call */
-  void endRecursive();
+  void endRecursive(size_t intervalId);
   /** Start a new scope, corresponding to a guess in CDCAC */
   void startScope();
   /** Finish a scope and add the (generalized) sample that was refuted */
@@ -79,7 +79,7 @@ class CADProofGenerator
   void pruneChildren(F&& f)
   {
     d_current->pruneChildren(
-        [&f](std::size_t i, const detail::TreeProofNode& tpn) { return f(i); });
+        [&f](const detail::TreeProofNode& tpn) { return f(tpn.d_objectId); });
   }
 
   /**
@@ -102,7 +102,8 @@ class CADProofGenerator
                  const poly::Assignment& a,
                  poly::SignCondition& sc,
                  const poly::Interval& interval,
-                 Node constraint);
+                 Node constraint,
+                 size_t intervalId);
 
   /**
    * Constructs the (generalized) interval that is to be excluded from a
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 132cb9795..6b1749305 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -118,7 +118,7 @@ void CadSolver::checkPartial()
     Trace("nl-cad") << "No constraints. Return." << std::endl;
     return;
   }
-  auto covering = d_CAC.getUnsatCover(0, true);
+  auto covering = d_CAC.getUnsatCover(true);
   if (covering.empty())
   {
     d_foundSatisfiability = true;
diff --git a/test/regress/regress1/nl/factor_agg_s.smt2 b/test/regress/regress1/nl/factor_agg_s.smt2
index fd12d4515..fc2e7a789 100644
--- a/test/regress/regress1/nl/factor_agg_s.smt2
+++ b/test/regress/regress1/nl/factor_agg_s.smt2
@@ -3,6 +3,8 @@
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)
+(set-option :check-proofs true)
+(set-option :proof-check eager)
 (declare-fun skoX () Real)
 (declare-fun skoY () Real)
 (declare-fun skoZ () Real)