Fix pruning of covering intervals in proofs (#8084)

We need to mirror the pruning of intervals in the coverings solver in the corresponding proof. To match the proof nodes with the coverings-internal intervals, we use ids, where non-interval nodes have the id zero. In this process, we had three separate issues that never showed up because we don't have a proof checker for CAD proofs:

we did not check for zeros, pruning all non-interval nodes
we ran the pruning on the direct children of a CAD_RECURSIVE proof step, which are SCOPE nodes that don't have ids
iterating over and then removing children was done by a custom but faulty reimplementation of std::remove_if
Thus, we now

never prune zero nodes,
prune based on the (single) child node, if we are checking a SCOPE node, and
simply use std::remove_if.

diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp
index e397ea353e7e91aba1d7452b7f71f6342c936491..996a6051316212c5141362ba042a8b7aa2a0023b 100644 (file)
--- a/src/proof/lazy_tree_proof_generator.cpp
+++ b/src/proof/lazy_tree_proof_generator.cpp
@@ -17,6 +17,7 @@
 
 #include <iostream>
 
+#include "base/output.h"
 #include "expr/node.h"
 #include "proof/proof_generator.h"
 #include "proof/proof_node.h"
@@ -32,14 +33,19 @@ LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm,
 }
 void LazyTreeProofGenerator::openChild()
 {
+  Trace("proof-ltpg") << "openChild() start" << std::endl << *this << std::endl;
   detail::TreeProofNode& pn = getCurrent();
   pn.d_children.emplace_back();
   d_stack.emplace_back(&pn.d_children.back());
+  Trace("proof-ltpg") << "openChild() end" << std::endl << *this << std::endl;
 }
 void LazyTreeProofGenerator::closeChild()
 {
+  Trace("proof-ltpg") << "closeChild() start" << std::endl
+                      << *this << std::endl;
   Assert(getCurrent().d_rule != PfRule::UNKNOWN);
   d_stack.pop_back();
+  Trace("proof-ltpg") << "closeChild() end" << std::endl << *this << std::endl;
 }
 detail::TreeProofNode& LazyTreeProofGenerator::getCurrent()
 {
@@ -122,7 +128,7 @@ void LazyTreeProofGenerator::print(std::ostream& os,
                                    const std::string& prefix,
                                    const detail::TreeProofNode& pn) const
 {
-  os << prefix << pn.d_rule << ": ";
+  os << prefix << pn.d_rule << " [" << pn.d_objectId << "]: ";
   container_to_stream(os, pn.d_premise);
   os << " ==> " << pn.d_proven << std::endl;
   if (!pn.d_args.empty())

diff --git a/src/proof/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h
index 314685843817e73ff20c8ddfa9d48e7ebd7f2f3b..1863c739fd50d4f72aa41aeef021c6ec44e5c5b9 100644 (file)
--- a/src/proof/lazy_tree_proof_generator.h
+++ b/src/proof/lazy_tree_proof_generator.h
@@ -167,7 +167,7 @@ class LazyTreeProofGenerator : public ProofGenerator
    * generated and then later pruned, for example to produce smaller conflicts.
    * The predicate is given as a Callable f that is called for every child with
    * the id of the child and the child itself.
-   * f should return true if the child should be kept, fals if the child should
+   * f should return false if the child should be kept, true if the child should
    * be removed.
    * @param f a Callable bool(std::size_t, const detail::TreeProofNode&)
    */
@@ -175,20 +175,10 @@ class LazyTreeProofGenerator : public ProofGenerator
   void pruneChildren(F&& f)
   {
     auto& children = getCurrent().d_children;
-    std::size_t cur = 0;
-    std::size_t pos = 0;
-    for (std::size_t size = children.size(); cur < size; ++cur)
-    {
-      if (f(children[pos]))
-      {
-        if (cur != pos)
-        {
-          children[pos] = std::move(children[cur]);
-        }
-        ++pos;
-      }
-    }
-    children.resize(pos);
+
+    auto it =
+        std::remove_if(children.begin(), children.end(), std::forward<F>(f));
+    children.erase(it, children.end());
   }
 
  private:

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index b5984a0a01dc55049a4519fbb45258e81e24be6b..9891447295bfd6968de6611fc685ad5ffefa042c 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -726,10 +726,11 @@ void CDCAC::pruneRedundantIntervals(std::vector<CACInterval>& intervals)
   if (isProofEnabled())
   {
     d_proof->pruneChildren([&intervals](std::size_t id) {
+      if (id == 0) return false;
       return std::find_if(intervals.begin(),
                           intervals.end(),
                           [id](const CACInterval& i) { return i.d_id == id; })
-             != intervals.end();
+             == intervals.end();
     });
   }
 }

diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp
index 429287681306f2acaf0575e2f29d99884abb6614..f5723a63463e137c5ce27bed7301fbbe92f8cc36 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac_utils.cpp
+++ b/src/theory/arith/nl/cad/cdcac_utils.cpp
@@ -175,6 +175,15 @@ void cleanIntervals(std::vector<CACInterval>& intervals)
   // Simplifies removal of redundancies later on.
   if (intervals.size() < 2) return;
 
+  if (Trace.isOn("cdcac"))
+  {
+    Trace("cdcac") << "Before pruning:" << std::endl;
+    for (const auto& i : intervals)
+    {
+      Trace("cdcac") << "\t[" << i.d_id << "] " << i.d_interval << std::endl;
+    }
+  }
+
   // Sort intervals.
   std::sort(intervals.begin(),
             intervals.end(),
@@ -215,6 +224,14 @@ void cleanIntervals(std::vector<CACInterval>& intervals)
       intervals.pop_back();
     }
   }
+  if (Trace.isOn("cdcac"))
+  {
+    Trace("cdcac") << "After pruning:" << std::endl;
+    for (const auto& i : intervals)
+    {
+      Trace("cdcac") << "\t[" << i.d_id << "] " << i.d_interval << std::endl;
+    }
+  }
 }
 
 void removeRedundantIntervals(std::vector<CACInterval>& intervals)

diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index fcc07cbf06bdd6245c6ad8eebe9c95681ed472b7..1e3c522025525357143c2e0f809faff21ea824b9 100644 (file)
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -225,7 +225,7 @@ std::vector<Node> CADProofGenerator::constructCell(Node var,
       if (ids.second <= roots.size())
       {
         // Interval has upper bound that is not inf
-        res.emplace_back(mkIRP(var, Kind::LT, d_zero, ids.first, poly, vm));
+        res.emplace_back(mkIRP(var, Kind::LT, d_zero, ids.second, poly, vm));
       }
     }
   }

diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 2f05ff11bf981b27f27164f7a4f655f2aca61045..521d5aa45ceb28c069a743dcc010d2a187e730fd 100644 (file)
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -78,8 +78,15 @@ class CADProofGenerator
   template <typename F>
   void pruneChildren(F&& f)
   {
-    d_current->pruneChildren(
-        [&f](const detail::TreeProofNode& tpn) { return f(tpn.d_objectId); });
+    d_current->pruneChildren([&f](const detail::TreeProofNode& tpn) {
+      // The direct children of recursive rules are scopes, but the ids are
+      // attached to their children
+      if (tpn.d_rule == PfRule::SCOPE && tpn.d_children.size() == 1)
+      {
+        return f(tpn.d_children[0].d_objectId);
+      }
+      return f(tpn.d_objectId);
+    });
   }
 
   /**

diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp
index 75425eba494594cdc997de29d5b36b21480ec4d3..aef2189bad7db27ef52b86fcd6d9e3e8fd6fd218 100644 (file)
--- a/test/unit/theory/theory_arith_cad_white.cpp
+++ b/test/unit/theory/theory_arith_cad_white.cpp
@@ -22,6 +22,10 @@
 #include <vector>
 
 #include "test_smt.h"
+#include "options/options_handler.h"
+#include "options/proof_options.h"
+#include "options/smt_options.h"
+#include "smt/proof_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/cad/lazard_evaluation.h"
 #include "theory/arith/nl/cad/projections.h"
@@ -55,9 +59,24 @@ class TestTheoryWhiteArithCAD : public TestSmt
     nodeManager = d_nodeManager;
   }
 
-  Node dummy(int i) const
+  void TearDown() override
   {
-    return d_nodeManager->mkConst(CONST_RATIONAL, Rational(i));
+    d_dummyCache.clear();
+    TestSmt::TearDown();
+  }
+
+  Node dummy(int i)
+  {
+    auto it = d_dummyCache.find(i);
+    if (it == d_dummyCache.end())
+    {
+      it = d_dummyCache
+               .emplace(i,
+                        d_nodeManager->mkBoundVar("c" + std::to_string(i),
+                                                  d_nodeManager->booleanType()))
+               .first;
+    }
+    return it->second;
   }
 
   Theory::Effort d_level = Theory::EFFORT_FULL;
@@ -65,6 +84,7 @@ class TestTheoryWhiteArithCAD : public TestSmt
   std::unique_ptr<TypeNode> d_intType;
   const Rational d_zero = 0;
   const Rational d_one = 1;
+  std::map<int, Node> d_dummyCache;
 };
 
 poly::AlgebraicNumber get_ran(std::initializer_list<long> init,
@@ -279,6 +299,8 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2)
   EXPECT_TRUE(!cover.empty());
   auto nodes = cad::collectConstraints(cover);
   std::vector<Node> ref{dummy(1), dummy(2), dummy(3), dummy(4), dummy(5)};
+  std::sort(nodes.begin(), nodes.end());
+  std::sort(ref.begin(), ref.end());
   EXPECT_EQ(nodes, ref);
 }
 
@@ -359,6 +381,49 @@ void test_delta(const std::vector<Node>& a)
   }
 }
 
+TEST_F(TestTheoryWhiteArithCAD, test_cdcac_proof_1)
+{
+  Options opts;
+  // enable proofs
+  opts.smt.proofMode = options::ProofMode::FULL;
+  opts.smt.produceProofs = true;
+  Env env(NodeManager::currentNM(), &opts);
+  opts.handler().setDefaultDagThresh("--dag-thresh", 0);
+  smt::PfManager pfm(env);
+  EXPECT_TRUE(env.isTheoryProofProducing());
+  // register checkers that we need
+  builtin::BuiltinProofRuleChecker btchecker(env);
+  btchecker.registerTo(env.getProofNodeManager()->getChecker());
+  cad::CADProofRuleChecker checker;
+  checker.registerTo(env.getProofNodeManager()->getChecker());
+  // do the coverings problem
+  cad::CDCAC cac(env, {});
+  EXPECT_TRUE(cac.getProof() != nullptr);
+  cac.startNewProof();
+  poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
+  poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
+
+  cac.getConstraints().addConstraint(
+      4 * y - x * x + 4, poly::SignCondition::LT, dummy(1));
+  cac.getConstraints().addConstraint(
+      3 * y - 5 + (x - 2) * (x - 2), poly::SignCondition::GT, dummy(2));
+  cac.getConstraints().addConstraint(
+      4 * y - x - 2, poly::SignCondition::GT, dummy(3));
+  cac.getConstraints().addConstraint(
+      x + 1, poly::SignCondition::GT, dummy(4));
+  cac.getConstraints().addConstraint(
+      x - 2, poly::SignCondition::LT, dummy(5));
+
+  cac.computeVariableOrdering();
+
+  auto cover = cac.getUnsatCover();
+  EXPECT_FALSE(cover.empty());
+  
+  std::vector<Node> mis{dummy(1), dummy(3), dummy(4), dummy(5)};
+  LazyTreeProofGenerator* pg = dynamic_cast<LazyTreeProofGenerator*>(cac.closeProof(mis));
+  EXPECT_TRUE(pg != nullptr);
+}
+
 TEST_F(TestTheoryWhiteArithCAD, test_delta_one)
 {
   std::vector<Node> a;