From f17e2555ee0a43e41e23f793c991e6e0b20cf148 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 22 Mar 2022 20:11:06 -0500 Subject: [PATCH] Fix cvc5-projects issue 497 (#8331) Fixes cvc5/cvc5-projects#497 --- src/theory/bags/card_solver.cpp | 13 ++++---- src/theory/bags/card_solver.h | 1 - src/theory/bags/infer_info.cpp | 30 +++++++++++++------ src/theory/bags/infer_info.h | 4 +++ src/theory/bags/inference_generator.cpp | 13 ++++---- src/theory/bags/inference_generator.h | 2 +- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress1/bags/proj-issue497.smt2 | 6 ++++ 8 files changed, 46 insertions(+), 24 deletions(-) create mode 100644 test/regress/cli/regress1/bags/proj-issue497.smt2 diff --git a/src/theory/bags/card_solver.cpp b/src/theory/bags/card_solver.cpp index 146149e3b..6ec9b7a26 100644 --- a/src/theory/bags/card_solver.cpp +++ b/src/theory/bags/card_solver.cpp @@ -65,7 +65,8 @@ std::set CardSolver::getChildren(Node bag) void CardSolver::checkCardinalityGraph() { - for (const auto& pair : d_state.getCardinalityTerms()) + const std::map& cardinalityTerms = d_state.getCardinalityTerms(); + for (const auto& pair : cardinalityTerms) { Trace("bags-card") << "CardSolver::checkCardinalityGraph cardTerm: " << pair << std::endl; @@ -96,14 +97,16 @@ void CardSolver::checkCardinalityGraph() case BAG_DIFFERENCE_REMOVE: checkDifferenceRemove(pair, n); break; default: break; } + if (d_im.hasSentLemma()) + { + // exit with each new pending lemma + return; + } it++; } // if the bag is a leaf in the graph, then we reduce its cardinality checkLeafBag(pair, bag); - } - - for (const auto& pair : d_state.getCardinalityTerms()) - { + // cardinality term is non-negative InferInfo i = d_ig.nonNegativeCardinality(pair.second); d_im.lemmaTheoryInference(&i); } diff --git a/src/theory/bags/card_solver.h b/src/theory/bags/card_solver.h index 5af0bc701..9e08fcb62 100644 --- a/src/theory/bags/card_solver.h +++ b/src/theory/bags/card_solver.h @@ -133,7 +133,6 @@ class CardSolver : protected EnvObj * This map needs to cleared before each full effort check. */ std::map>> d_cardGraph; - /** Commonly used constants */ Node d_true; Node d_false; diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp index aa949ebc8..6b222cd36 100644 --- a/src/theory/bags/infer_info.cpp +++ b/src/theory/bags/infer_info.cpp @@ -14,8 +14,9 @@ */ #include "theory/bags/infer_info.h" -#include "theory/inference_manager_buffered.h" + #include "theory/bags/inference_manager.h" +#include "theory/inference_manager_buffered.h" namespace cvc5 { namespace theory { @@ -28,20 +29,31 @@ InferInfo::InferInfo(InferenceManagerBuffered* im, InferenceId id) TrustNode InferInfo::processLemma(LemmaProperty& p) { - NodeManager* nm = NodeManager::currentNM(); - Node pnode = nm->mkAnd(d_premises); - Node lemma = nm->mkNode(kind::IMPLIES, pnode, d_conclusion); + Node lemma = getLemma(); + + Trace("bags::InferInfo::process") << (*this) << std::endl; + d_im->addPendingLemma(lemma, getId()); + return TrustNode::mkTrustLemma(lemma, nullptr); +} +Node InferInfo::getLemma() const +{ + NodeManager* nm = NodeManager::currentNM(); + std::vector nodes; + Node premises = nm->mkAnd(d_premises); + Node lemma = nm->mkNode(kind::IMPLIES, premises, d_conclusion); + nodes.push_back(lemma); // send lemmas corresponding to the skolems introduced for (const auto& pair : d_skolems) { Node n = pair.first.eqNode(pair.second); - d_im->addPendingLemma(n, InferenceId::BAGS_SKOLEM); + nodes.push_back(n); } - - Trace("bags::InferInfo::process") << (*this) << std::endl; - d_im->addPendingLemma(lemma, getId()); - return TrustNode::mkTrustLemma(lemma, nullptr); + if (nodes.size() == 1) + { + return lemma; + } + return nm->mkNode(kind::AND, nodes); } bool InferInfo::isTrivial() const diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h index bebeaa077..d896844f6 100644 --- a/src/theory/bags/infer_info.h +++ b/src/theory/bags/infer_info.h @@ -72,6 +72,10 @@ class InferInfo : public TheoryInference * engine with no new external premises (d_noExplain). */ bool isFact() const; + /** + * @return the lemma for this InferInfo. + */ + Node getLemma() const; }; /** diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 63a90cf18..140b6d0b8 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -61,7 +61,7 @@ void InferenceGenerator::registerCardinalityTerm(Node n) Assert(n.getKind() == BAG_CARD); Node bag = d_state->getRepresentative(n[0]); Node cardTerm = d_nm->mkNode(BAG_CARD, bag); - Node skolem = registerAndAssertSkolemLemma(cardTerm, "bag.card"); + Node skolem = registerAndAssertSkolemLemma(cardTerm, "bagCard"); d_state->registerCardinalityTerm(cardTerm, skolem); Node premise = n[0].eqNode(bag); Node conclusion = skolem.eqNode(n); @@ -338,7 +338,7 @@ InferInfo InferenceGenerator::cardEmpty(const std::pair& pair, InferInfo inferInfo(d_im, InferenceId::BAGS_CARD_EMPTY); Node premise = pair.first[0].eqNode(n); Node conclusion = pair.second.eqNode(d_zero); - inferInfo.d_conclusion = premise.notNode().orNode(conclusion); + inferInfo.d_conclusion = premise.eqNode(conclusion); return inferInfo; } @@ -373,8 +373,7 @@ InferInfo InferenceGenerator::cardUnionDisjoint(Node premise, Node unionDisjoints = child; Node card = d_nm->mkNode(BAG_CARD, child); std::vector lemmas; - registerCardinalityTerm(card); - Node sum = d_state->getCardinalitySkolem(card); + Node sum = registerAndAssertSkolemLemma(card, "bagCard"); ++it; while (it != children.end()) { @@ -383,14 +382,12 @@ InferInfo InferenceGenerator::cardUnionDisjoint(Node premise, unionDisjoints = d_nm->mkNode(kind::BAG_UNION_DISJOINT, unionDisjoints, child); card = d_nm->mkNode(BAG_CARD, child); - registerCardinalityTerm(card); - Node skolem = d_state->getCardinalitySkolem(card); + Node skolem = registerAndAssertSkolemLemma(card, "bagCard"); sum = d_nm->mkNode(ADD, sum, skolem); ++it; } Node parentCard = d_nm->mkNode(BAG_CARD, parent); - registerCardinalityTerm(parentCard); - Node parentSkolem = d_state->getCardinalitySkolem(parentCard); + Node parentSkolem = registerAndAssertSkolemLemma(parentCard, "bagCard"); Node bags = parent.eqNode(unionDisjoints); lemmas.push_back(bags); diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index ef8939b64..8d67ea4f4 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -195,7 +195,7 @@ class InferenceGenerator * @param cardTerm a term of the form (bag.card A) where A has type (Bag E) * @param n is (as bag.empty (Bag E)) * @return an inference that represents the following implication - * (=> (= A (as bag.empty (Bag E))) + * (= (= A (as bag.empty (Bag E))) * (= (bag.card A) 0)) */ InferInfo cardEmpty(const std::pair& pair, Node n); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 0c2b4e146..d263fe10d 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1770,6 +1770,7 @@ set(regress_1_tests regress1/bags/product1.smt2 regress1/bags/product2.smt2 regress1/bags/product3.smt2 + regress1/bags/proj-issue497.smt2 regress1/bags/subbag1.smt2 regress1/bags/subbag2.smt2 regress1/bags/union_disjoint.smt2 diff --git a/test/regress/cli/regress1/bags/proj-issue497.smt2 b/test/regress/cli/regress1/bags/proj-issue497.smt2 new file mode 100644 index 000000000..40950eab5 --- /dev/null +++ b/test/regress/cli/regress1/bags/proj-issue497.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :fmf-bound true) +(declare-const x (Bag Bool)) +(declare-const x5 (Bag Bool)) +(check-sat-assuming ((= 0 (bag.card (bag.inter_min x5 (bag.inter_min x5 x)))))) -- 2.30.2