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.

1 files changed, 18 insertions, 5 deletions

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