From: Gereon Kremer Date: Wed, 23 Feb 2022 15:18:07 +0000 (+0100) Subject: Fix pruning of covering intervals in proofs (#8084) X-Git-Tag: cvc5-1.0.0~402 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c23b18236556dc5ed5101cdc588c1c942ae4ed3;p=cvc5.git 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 e397ea353..996a60513 100644 --- a/src/proof/lazy_tree_proof_generator.cpp +++ b/src/proof/lazy_tree_proof_generator.cpp @@ -17,6 +17,7 @@ #include +#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 314685843..1863c739f 100644 --- 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)); + 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 b5984a0a0..989144729 100644 --- 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& 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 429287681..f5723a634 100644 --- 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& 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& 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& intervals) diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index fcc07cbf0..1e3c52202 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -225,7 +225,7 @@ std::vector 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 2f05ff11b..521d5aa45 100644 --- 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 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 75425eba4..aef2189ba 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -22,6 +22,10 @@ #include #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 d_intType; const Rational d_zero = 0; const Rational d_one = 1; + std::map d_dummyCache; }; poly::AlgebraicNumber get_ran(std::initializer_list init, @@ -279,6 +299,8 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2) EXPECT_TRUE(!cover.empty()); auto nodes = cad::collectConstraints(cover); std::vector 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& 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 mis{dummy(1), dummy(3), dummy(4), dummy(5)}; + LazyTreeProofGenerator* pg = dynamic_cast(cac.closeProof(mis)); + EXPECT_TRUE(pg != nullptr); +} + TEST_F(TestTheoryWhiteArithCAD, test_delta_one) { std::vector a;