From 05d11815c049d1145884d510196e4e16a88931a0 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Fri, 4 Mar 2022 17:33:47 -0600 Subject: [PATCH] Fix bag.map upwards inferences (#8232) --- src/expr/skolem_manager.cpp | 1 + src/expr/skolem_manager.h | 6 +++++ src/theory/bags/bag_solver.cpp | 31 +++++++++++++++---------- src/theory/bags/bag_solver.h | 16 +++++++++---- src/theory/bags/infer_info.cpp | 8 +++---- src/theory/bags/inference_generator.cpp | 15 ++++++------ src/theory/bags/inference_generator.h | 6 ++--- src/theory/bags/solver_state.cpp | 8 +++---- src/theory/inference_id.cpp | 3 ++- src/theory/inference_id.h | 3 ++- 10 files changed, 61 insertions(+), 36 deletions(-) diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 4bda69bcb..ba1f0b0ea 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -86,6 +86,7 @@ const char* toString(SkolemFunId id) case SkolemFunId::BAGS_FOLD_ELEMENTS: return "BAGS_FOLD_ELEMENTS"; case SkolemFunId::BAGS_FOLD_UNION_DISJOINT: return "BAGS_FOLD_UNION_DISJOINT"; case SkolemFunId::BAGS_MAP_PREIMAGE: return "BAGS_MAP_PREIMAGE"; + case SkolemFunId::BAGS_MAP_PREIMAGE_INDEX: return "BAGS_MAP_PREIMAGE_INDEX"; case SkolemFunId::BAGS_MAP_SUM: return "BAGS_MAP_SUM"; case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED"; default: return "?"; diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 2c696d23f..733fbabdc 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -147,6 +147,12 @@ enum class SkolemFunId * where uf: Int -> E is a skolem function, and E is the type of elements of A */ BAGS_MAP_PREIMAGE, + /** + * A skolem variable for the index that is unique per terms + * (map f A), y, preImageSize, y, e which might be an element in A. + * (see the documentation for BAGS_MAP_PREIMAGE) + */ + BAGS_MAP_PREIMAGE_INDEX, /** An uninterpreted function for bag.map operator: * If the preimage of {y} in A is {uf(1), ..., uf(n)} (see BAGS_MAP_PREIMAGE}, * then the multiplicity of an element y in a bag (map f A) is sum(n), diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index dbd2bbc29..219e3187d 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -261,24 +261,31 @@ void BagSolver::checkMap(Node n) for (const Node& z : downwards) { Node y = d_state.getRepresentative(z); - if (d_mapCache.count(n) && d_mapCache[n].get()->contains(y)) + if (!d_mapCache.count(n)) { - continue; + std::shared_ptr>> nMap = + std::make_shared>>( + userContext()); + d_mapCache[n] = nMap; } - auto [downInference, uf, preImageSize] = d_ig.mapDownwards(n, y); - d_im.lemmaTheoryInference(&downInference); - for (const Node& x : upwards) + if (!d_mapCache[n].get()->count(y)) { - InferInfo upInference = d_ig.mapUpwards(n, uf, preImageSize, y, x); - d_im.lemmaTheoryInference(&upInference); + auto [downInference, uf, preImageSize] = d_ig.mapDown(n, y); + d_im.lemmaTheoryInference(&downInference); + std::pair yPair = std::make_pair(uf, preImageSize); + d_mapCache[n].get()->insert(y, yPair); } - if (!d_mapCache.count(n)) + + context::CDHashMap>::iterator it = + d_mapCache[n].get()->find(y); + + auto [uf, preImageSize] = it->second; + + for (const Node& x : upwards) { - std::shared_ptr > set = - std::make_shared >(userContext()); - d_mapCache.insert(n, set); + InferInfo upInference = d_ig.mapUp(n, uf, preImageSize, y, x); + d_im.lemmaTheoryInference(&upInference); } - d_mapCache[n].get()->insert(y); } } diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index eb578aafd..e5dba3896 100644 --- a/src/theory/bags/bag_solver.h +++ b/src/theory/bags/bag_solver.h @@ -110,11 +110,19 @@ class BagSolver : protected EnvObj /** Reference to the term registry of theory of bags */ TermRegistry& d_termReg; - /** a cache that stores bags of kind BAG_MAP and those element representatives - * which we generated their inferences. + /** + * a map where the keys are nodes of the form (bag.map f A) + * where f is a function (-> E T), A a bag of type (Bag E), + * and values are maps where keys are elements y's of (bag.map f A) + * and values are pairs such that + * uf is an uninterpreted function Int -> E represents the and + * preImageSize is the cardinality of the distinct elements in A that are + * mapped to each y + * */ - using BagElementsMap = - context::CDHashMap > >; + using BagElementsMap = context::CDHashMap< + Node, + std::shared_ptr > > >; BagElementsMap d_mapCache; /** Commonly used constants */ diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp index 9080f29e9..187cbff99 100644 --- a/src/theory/bags/infer_info.cpp +++ b/src/theory/bags/infer_info.cpp @@ -67,13 +67,13 @@ bool InferInfo::isFact() const std::ostream& operator<<(std::ostream& out, const InferInfo& ii) { - out << "(infer :id " << ii.getId() << std::endl; - out << ":conclusion " << ii.d_conclusion << std::endl; + out << "(infer ;id " << std::endl << ii.getId() << std::endl; + out << ";conclusion " << std::endl << ii.d_conclusion << std::endl; if (!ii.d_premises.empty()) { - out << " :premise (" << ii.d_premises << ")" << std::endl; + out << " ;premise" << std::endl << ii.d_premises << std::endl; } - out << ":skolems " << ii.d_skolems << std::endl; + out << ";skolems " << ii.d_skolems << std::endl; out << ")"; return out; } diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index aa5bf74d8..b87296f32 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -393,15 +393,14 @@ Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag) return count; } -std::tuple InferenceGenerator::mapDownwards(Node n, - Node e) +std::tuple InferenceGenerator::mapDown(Node n, Node e) { Assert(n.getKind() == BAG_MAP && n[1].getType().isBag()); Assert(n[0].getType().isFunction() && n[0].getType().getArgTypes().size() == 1); Assert(e.getType() == n[0].getType().getRangeType()); - InferInfo inferInfo(d_im, InferenceId::BAGS_MAP); + InferInfo inferInfo(d_im, InferenceId::BAGS_MAP_DOWN); Node f = n[0]; Node A = n[1]; @@ -488,19 +487,19 @@ std::tuple InferenceGenerator::mapDownwards(Node n, std::map m; m[e] = conclusion; - Trace("bags::InferenceGenerator::mapDownwards") + Trace("bags::InferenceGenerator::mapDown") << "conclusion: " << inferInfo.d_conclusion << std::endl; return std::tuple(inferInfo, uf, preImageSize); } -InferInfo InferenceGenerator::mapUpwards( +InferInfo InferenceGenerator::mapUp( Node n, Node uf, Node preImageSize, Node y, Node x) { Assert(n.getKind() == BAG_MAP && n[1].getType().isBag()); Assert(n[0].getType().isFunction() && n[0].getType().getArgTypes().size() == 1); - InferInfo inferInfo(d_im, InferenceId::BAGS_MAP); + InferInfo inferInfo(d_im, InferenceId::BAGS_MAP_UP); Node f = n[0]; Node A = n[1]; @@ -508,7 +507,9 @@ InferInfo InferenceGenerator::mapUpwards( Node xInA = d_nm->mkNode(GEQ, countA, d_one); Node notEqual = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, f, x), y).negate(); - Node k = d_sm->mkDummySkolem("k", d_nm->integerType()); + Node k = d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_PREIMAGE_INDEX, + d_nm->integerType(), + {n, uf, preImageSize, y, x}); Node inRange = d_nm->mkNode( AND, d_nm->mkNode(GEQ, k, d_one), d_nm->mkNode(LEQ, k, preImageSize)); Node equal = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, uf, k), x); diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index ed6122356..ed6f856e2 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -239,7 +239,7 @@ class InferenceGenerator * preimage of e, * and skolem is a fresh variable equals (bag.map f A)) */ - std::tuple mapDownwards(Node n, Node e); + std::tuple mapDown(Node n, Node e); /** * @param n is (bag.map f A) where f is a function (-> E T), A a bag of type @@ -251,7 +251,7 @@ class InferenceGenerator * @param e is an element of type E * @return an inference that represents the following implication * (=> - * (>= (bag.count x A) 1) + * (bag.member x A) * (or * (not (= (f x) y) * (and @@ -260,7 +260,7 @@ class InferenceGenerator * (= (uf skolem) x))))) * where skolem is a fresh variable */ - InferInfo mapUpwards(Node n, Node uf, Node preImageSize, Node y, Node x); + InferInfo mapUp(Node n, Node uf, Node preImageSize, Node y, Node x); /** * @param n is (bag.filter p A) where p is a function (-> E Bool), diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 575dcf577..604c05cb4 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -135,7 +135,7 @@ std::vector SolverState::collectBagsAndCountTerms() while (!repIt.isFinished()) { Node eqc = (*repIt); - Trace("bags-eqc") << "Eqc [ " << eqc << " ] = { "; + Trace("bags-eqc") << "(eqc " << eqc << std::endl << ""; if (eqc.getType().isBag()) { @@ -173,11 +173,11 @@ std::vector SolverState::collectBagsAndCountTerms() } ++it; } - Trace("bags-eqc") << " } " << std::endl; + Trace("bags-eqc") << std::endl << " ) " << std::endl; ++repIt; } - Trace("bags-eqc") << "bag representatives: " << d_bags << endl; + Trace("bags-eqc") << "(bagRepresentatives " << d_bags << ")" << std::endl; return lemmas; } @@ -189,7 +189,7 @@ void SolverState::collectDisequalBagTerms() Node n = (*it); if (n.getKind() == EQUAL && n[0].getType().isBag()) { - Trace("bags-eqc") << "Disequal terms: " << n << std::endl; + Trace("bags-eqc") << "(disequalTerms " << n << " )" << std::endl; d_deq.insert(n); } ++it; diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index b5980d781..20d758b21 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -129,7 +129,8 @@ const char* toString(InferenceId i) return "BAGS_DIFFERENCE_SUBTRACT"; case InferenceId::BAGS_DIFFERENCE_REMOVE: return "BAGS_DIFFERENCE_REMOVE"; case InferenceId::BAGS_DUPLICATE_REMOVAL: return "BAGS_DUPLICATE_REMOVAL"; - case InferenceId::BAGS_MAP: return "BAGS_MAP"; + case InferenceId::BAGS_MAP_DOWN: return "BAGS_MAP_DOWN"; + case InferenceId::BAGS_MAP_UP: return "BAGS_MAP_UP"; case InferenceId::BAGS_FILTER_DOWN: return "BAGS_FILTER_DOWN"; case InferenceId::BAGS_FILTER_UP: return "BAGS_FILTER_UP"; case InferenceId::BAGS_FOLD: return "BAGS_FOLD"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 4734e0d60..f5699540c 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -195,7 +195,8 @@ enum class InferenceId BAGS_DIFFERENCE_SUBTRACT, BAGS_DIFFERENCE_REMOVE, BAGS_DUPLICATE_REMOVAL, - BAGS_MAP, + BAGS_MAP_DOWN, + BAGS_MAP_UP, BAGS_FILTER_DOWN, BAGS_FILTER_UP, BAGS_FOLD, -- 2.30.2