From: mudathirmahgoub Date: Tue, 4 Jan 2022 15:39:33 +0000 (-0600) Subject: Refactor bag solver (#7770) X-Git-Tag: cvc5-1.0.0~610 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d7417bbc2ea2b166e17afe201e7770a8aff3d36;p=cvc5.git Refactor bag solver (#7770) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index fde0088e8..1ee726047 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -555,6 +555,8 @@ libcvc5_add_sources( theory/bags/rewrites.h theory/bags/solver_state.cpp theory/bags/solver_state.h + theory/bags/strategy.cpp + theory/bags/strategy.h theory/bags/term_registry.cpp theory/bags/term_registry.h theory/bags/theory_bags.cpp diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 80ccd6707..55367bb89 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -15,6 +15,7 @@ #include "theory/bags/bag_solver.h" +#include "expr/emptybag.h" #include "theory/bags/inference_generator.h" #include "theory/bags/inference_manager.h" #include "theory/bags/normal_form.h" @@ -50,10 +51,8 @@ BagSolver::BagSolver(Env& env, BagSolver::~BagSolver() {} -void BagSolver::postCheck() +void BagSolver::checkBasicOperations() { - d_state.initialize(); - checkDisequalBagTerms(); // At this point, all bag and count representatives should be in the solver @@ -164,6 +163,39 @@ void BagSolver::checkDifferenceSubtract(const Node& n) } } +bool BagSolver::checkBagMake() +{ + bool sentLemma = false; + for (const Node& bag : d_state.getBags()) + { + TypeNode bagType = bag.getType(); + NodeManager* nm = NodeManager::currentNM(); + Node empty = nm->mkConst(EmptyBag(bagType)); + if (d_state.areEqual(empty, bag) || d_state.areDisequal(empty, bag)) + { + continue; + } + + // look for BAG_MAKE terms in the equivalent class + eq::EqClassIterator it = + eq::EqClassIterator(bag, d_state.getEqualityEngine()); + while (!it.isFinished()) + { + Node n = (*it); + if (n.getKind() == BAG_MAKE) + { + Trace("bags-check") << "splitting on node " << std::endl; + InferInfo i = d_ig.bagMake(n); + sentLemma |= d_im.lemmaTheoryInference(&i); + // it is enough to split only once per equivalent class + break; + } + it++; + } + } + return sentLemma; +} + void BagSolver::checkBagMake(const Node& n) { Assert(n.getKind() == BAG_MAKE); diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index 45a20e055..499b7998d 100644 --- a/src/theory/bags/bag_solver.h +++ b/src/theory/bags/bag_solver.h @@ -40,11 +40,29 @@ class BagSolver : protected EnvObj BagSolver(Env& env, SolverState& s, InferenceManager& im, TermRegistry& tr); ~BagSolver(); - void postCheck(); + /** + * apply inference rules for basic bag operators: + * BAG_MAKE, BAG_UNION_DISJOINT, BAG_UNION_MAX, BAG_INTER_MIN, + * BAG_DIFFERENCE_SUBTRACT, BAG_DIFFERENCE_REMOVE, BAG_DUPLICATE_REMOVAL + */ + void checkBasicOperations(); + + /** + * apply inference rules for BAG_MAKE terms. + * For each term (bag x c) that is neither equal nor disequal to the empty + * bag, we do a split using the following lemma: + * (or + * (and (< c 1) (= (bag x c) (as bag.empty (Bag E)))) + * (and (>= c 1) (not (= (bag x c) (as bag.empty (Bag E)))) + * where (Bag E) is the type of the bag term + * @return true if a new lemma was successfully sent. + */ + bool checkBagMake(); private: /** apply inference rules for empty bags */ void checkEmpty(const Node& n); + /** * apply inference rules for BAG_MAKE operator. * Example: Suppose n = (bag x c), and we have two count terms (bag.count x n) diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index a5fb206aa..f193bf73c 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -177,13 +177,12 @@ BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const // (bag.count x bag.empty) = 0 return BagsRewriteResponse(d_zero, Rewrite::COUNT_EMPTY); } - if (n[1].getKind() == BAG_MAKE && n[0] == n[1][0]) + if (n[1].getKind() == BAG_MAKE && n[0] == n[1][0] && n[1][1].isConst() + && n[1][1].getConst() > Rational(0)) { - // (bag.count x (bag x c)) = (ite (>= c 1) c 0) + // (bag.count x (bag x c)) = c, c > 0 is a constant Node c = n[1][1]; - Node geq = d_nm->mkNode(GEQ, c, d_one); - Node ite = d_nm->mkNode(ITE, geq, c, d_zero); - return BagsRewriteResponse(ite, Rewrite::COUNT_BAG_MAKE); + return BagsRewriteResponse(c, Rewrite::COUNT_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 9be0c2b93..e2b220777 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -17,6 +17,7 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" +#include "expr/emptybag.h" #include "expr/skolem_manager.h" #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" @@ -47,12 +48,32 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e) InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT); Node count = d_nm->mkNode(BAG_COUNT, e, n); - Node gte = d_nm->mkNode(GEQ, count, d_zero); inferInfo.d_conclusion = gte; return inferInfo; } +InferInfo InferenceGenerator::bagMake(Node n) +{ + Assert(n.getKind() == BAG_MAKE); + /* + * (or + * (and (< c 1) (= (bag x c) (as bag.empty (Bag E)))) + * (and (>= c 1) (not (= (bag x c) (as bag.empty (Bag E)))) + */ + Node x = n[0]; + Node c = n[1]; + InferInfo inferInfo(d_im, InferenceId::BAGS_BAG_MAKE_SPLIT); + Node empty = d_nm->mkConst(EmptyBag(n.getType())); + Node equal = d_nm->mkNode(EQUAL, n, empty); + Node geq = d_nm->mkNode(GEQ, c, d_one); + Node isEmpty = geq.notNode().andNode(equal); + Node isNotEmpty = geq.andNode(equal.notNode()); + Node orNode = isEmpty.orNode(isNotEmpty); + inferInfo.d_conclusion = orNode; + return inferInfo; +} + InferInfo InferenceGenerator::bagMake(Node n, Node e) { Assert(n.getKind() == BAG_MAKE); diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 8ed3ead38..29da01629 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -47,6 +47,15 @@ class InferenceGenerator */ InferInfo nonNegativeCount(Node n, Node e); + /** + * @param n is (bag x c) of type (Bag E) + * @return an inference that represents the following lemma: + * (or + * (and (< c 1) (= (bag x c) (as bag.empty (Bag E)))) + * (and (>= c 1) (not (= (bag x c) (as bag.empty (Bag E)))) + */ + InferInfo bagMake(Node n); + /** * @param n is (bag x c) of type (Bag E) * @param e is a node of type E diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index ad817062f..52cbb8671 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -40,19 +40,35 @@ void SolverState::registerBag(TNode n) d_bags.insert(n); } -void SolverState::registerCountTerm(TNode n) +Node SolverState::registerCountTerm(TNode n) { Assert(n.getKind() == BAG_COUNT); - Node element = n[0]; + Node element = getRepresentative(n[0]); Node bag = getRepresentative(n[1]); - d_bagElements[bag].insert(element); + Node count = d_nm->mkNode(BAG_COUNT, element, bag); + Node skolem = d_nm->getSkolemManager()->mkPurifySkolem(count, "bag.count"); + d_bagElements[bag].push_back(std::make_pair(element, skolem)); + return count.eqNode(skolem); } const std::set& SolverState::getBags() { return d_bags; } -const std::set& SolverState::getElements(Node B) +std::set SolverState::getElements(Node B) { Node bag = getRepresentative(B); + std::set elements; + std::vector> pairs = d_bagElements[bag]; + for (std::pair pair : pairs) + { + elements.insert(pair.first); + } + return elements; +} + +const std::vector>& SolverState::getElementCountPairs( + Node n) +{ + Node bag = getRepresentative(n); return d_bagElements[bag]; } @@ -65,15 +81,17 @@ void SolverState::reset() d_deq.clear(); } -void SolverState::initialize() +std::vector SolverState::initialize() { reset(); - collectBagsAndCountTerms(); collectDisequalBagTerms(); + return collectBagsAndCountTerms(); } -void SolverState::collectBagsAndCountTerms() +std::vector SolverState::collectBagsAndCountTerms() { + std::vector lemmas; + eq::EqClassesIterator repIt = eq::EqClassesIterator(d_ee); while (!repIt.isFinished()) { @@ -96,14 +114,16 @@ void SolverState::collectBagsAndCountTerms() // for terms (bag x c) we need to store x by registering the count term // (bag.count x (bag x c)) Node count = d_nm->mkNode(BAG_COUNT, n[0], n); - registerCountTerm(count); + Node lemma = registerCountTerm(count); + lemmas.push_back(lemma); Trace("SolverState::collectBagsAndCountTerms") << "registered " << count << endl; } if (k == BAG_COUNT) { // this takes care of all count terms in each equivalent class - registerCountTerm(n); + Node lemma = registerCountTerm(n); + lemmas.push_back(lemma); Trace("SolverState::collectBagsAndCountTerms") << "registered " << n << endl; } @@ -114,7 +134,7 @@ void SolverState::collectBagsAndCountTerms() } Trace("bags-eqc") << "bag representatives: " << d_bags << endl; - Trace("bags-eqc") << "bag elements: " << d_bagElements << endl; + return lemmas; } void SolverState::collectDisequalBagTerms() diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index d6f628537..64c4b1674 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -42,9 +42,10 @@ class SolverState : public TheoryState /** * @param n has the form (bag.count e A) * @pre bag A needs is already registered using registerBag(A) - * @return a unique skolem for (bag.count e A) + * @return a lemma (= skolem (bag.count eRep ARep)) where + * eRep, ARep are representatives of e, A respectively */ - void registerCountTerm(TNode n); + Node registerCountTerm(TNode n); /** get all bag terms that are representatives in the equality engine. * This function is valid after the current solver is initialized during * postCheck. See SolverState::initialize and BagSolver::postCheck @@ -58,11 +59,18 @@ class SolverState : public TheoryState * (assert (= 0 (bag.count x B))) * element x is associated with bag B, albeit x is definitely not in B. */ - const std::set& getElements(Node B); - /** initialize bag and count terms */ - void initialize(); + std::set getElements(Node B); + /** + * initialize bag and count terms + * @return a list of skolem lemmas to be asserted + * */ + std::vector initialize(); /** return disequal bag terms */ const std::set& getDisequalBagTerms(); + /** + * return a list of bag elements and their skolem counts + */ + const std::vector>& getElementCountPairs(Node n); private: /** clear all bags data structures */ @@ -70,8 +78,9 @@ class SolverState : public TheoryState /** * collect bags' representatives and all count terms. * This function is called during postCheck + * @return a list of skolem lemmas to be asserted */ - void collectBagsAndCountTerms(); + std::vector collectBagsAndCountTerms(); /** * collect disequal bag terms. This function is called during postCheck. */ @@ -83,8 +92,12 @@ class SolverState : public TheoryState NodeManager* d_nm; /** collection of bag representatives */ std::set d_bags; - /** bag -> associated elements */ - std::map> d_bagElements; + /** + * This cache maps bag representatives to pairs of elements and multiplicity + * skolems which are used for model building. + * This map is cleared and initialized at the start of each full effort check. + */ + std::map>> d_bagElements; /** Disequal bag terms */ std::set d_deq; }; /* class SolverState */ diff --git a/src/theory/bags/strategy.cpp b/src/theory/bags/strategy.cpp new file mode 100644 index 000000000..541be9ac7 --- /dev/null +++ b/src/theory/bags/strategy.cpp @@ -0,0 +1,105 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of the strategy of the theory of bags. + */ + +#include "theory/bags/strategy.h" + +namespace cvc5 { +namespace theory { +namespace bags { + +std::ostream& operator<<(std::ostream& out, InferStep s) +{ + switch (s) + { + case BREAK: out << "break"; break; + case CHECK_INIT: out << "check_init"; break; + case CHECK_BAG_MAKE: out << "check_bag_make"; break; + case CHECK_BASIC_OPERATIONS: out << "CHECK_BASIC_OPERATIONS"; break; + default: out << "?"; break; + } + return out; +} + +Strategy::Strategy() : d_strategy_init(false) {} + +Strategy::~Strategy() {} + +bool Strategy::isStrategyInit() const { return d_strategy_init; } + +bool Strategy::hasStrategyEffort(Theory::Effort e) const +{ + return d_strat_steps.find(e) != d_strat_steps.end(); +} + +std::vector >::iterator Strategy::stepBegin( + Theory::Effort e) +{ + std::map >::const_iterator it = + d_strat_steps.find(e); + Assert(it != d_strat_steps.end()); + return d_infer_steps.begin() + it->second.first; +} + +std::vector >::iterator Strategy::stepEnd( + Theory::Effort e) +{ + std::map >::const_iterator it = + d_strat_steps.find(e); + Assert(it != d_strat_steps.end()); + return d_infer_steps.begin() + it->second.second; +} + +void Strategy::addStrategyStep(InferStep s, int effort, bool addBreak) +{ + // must run check init first + Assert((s == CHECK_INIT) == d_infer_steps.empty()); + d_infer_steps.push_back(std::pair(s, effort)); + if (addBreak) + { + d_infer_steps.push_back(std::pair(BREAK, 0)); + } +} + +void Strategy::initializeStrategy() +{ + // initialize the strategy if not already done so + if (!d_strategy_init) + { + std::map step_begin; + std::map step_end; + d_strategy_init = true; + // beginning indices + step_begin[Theory::EFFORT_FULL] = 0; + // add the inference steps + addStrategyStep(CHECK_INIT); + addStrategyStep(CHECK_BAG_MAKE); + addStrategyStep(CHECK_BASIC_OPERATIONS); + step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1; + + // set the beginning/ending ranges + for (const std::pair& it_begin : step_begin) + { + Theory::Effort e = it_begin.first; + std::map::iterator it_end = step_end.find(e); + Assert(it_end != step_end.end()); + d_strat_steps[e] = + std::pair(it_begin.second, it_end->second); + } + } +} + +} // namespace bags +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/bags/strategy.h b/src/theory/bags/strategy.h new file mode 100644 index 000000000..7dc5d693c --- /dev/null +++ b/src/theory/bags/strategy.h @@ -0,0 +1,97 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Strategy of the theory of bags. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__BAGS__STRATEGY_H +#define CVC5__THEORY__BAGS__STRATEGY_H + +#include +#include + +#include "theory/theory.h" + +namespace cvc5 { +namespace theory { +namespace bags { + +/** inference steps + * + * Corresponds to a step in the overall strategy of the bags solver. For + * details on the individual steps, see documentation on the inference schemas + * within Strategy. + */ +enum InferStep +{ + // indicates that the strategy should break if lemmas or facts are added + BREAK, + // check initial + CHECK_INIT, + // check bag operator + CHECK_BAG_MAKE, + // check basic operations + CHECK_BASIC_OPERATIONS +}; +std::ostream& operator<<(std::ostream& out, InferStep i); + +/** + * The strategy of theory of bags. + * + * This stores a sequence of the above enum that indicates the calls to + * runInferStep to make on the theory of bags, given by parent. + */ +class Strategy +{ + public: + Strategy(); + ~Strategy(); + /** is this strategy initialized? */ + bool isStrategyInit() const; + /** do we have a strategy for effort e? */ + bool hasStrategyEffort(Theory::Effort e) const; + /** begin and end iterators for effort e */ + std::vector >::iterator stepBegin( + Theory::Effort e); + std::vector >::iterator stepEnd( + Theory::Effort e); + /** initialize the strategy + * + * This initializes the above information based on the options. This makes + * a series of calls to addStrategyStep above. + */ + void initializeStrategy(); + + private: + /** add strategy step + * + * This adds (s,effort) as a strategy step to the vectors d_infer_steps and + * d_infer_step_effort. This indicates that a call to runInferStep should + * be run as the next step in the strategy. If addBreak is true, we add + * a BREAK to the strategy following this step. + */ + void addStrategyStep(InferStep s, int effort = 0, bool addBreak = true); + /** is strategy initialized */ + bool d_strategy_init; + /** the strategy */ + std::vector > d_infer_steps; + /** the range (begin, end) of steps to run at given efforts */ + std::map > d_strat_steps; +}; /* class Strategy */ + +} // namespace bags +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__BAGS__STRATEGY_H */ diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 39598975b..cfd6f1178 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -159,11 +159,11 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, void TheoryBags::postCheck(Effort effort) { d_im.doPendingFacts(); - // TODO issue #78: add Assert(d_strat.isStrategyInit()); - if (!d_state.isInConflict() && !d_valuation.needCheck()) - // TODO issue #78: add && d_strat.hasStrategyEffort(e)) + Assert(d_strat.isStrategyInit()); + if (!d_state.isInConflict() && !d_valuation.needCheck() + && d_strat.hasStrategyEffort(effort)) { - Trace("bags::TheoryBags::postCheck") << "effort: " << std::endl; + Trace("bags::TheoryBags::postCheck") << "effort: " << effort << std::endl; // TODO issue #78: add ++(d_statistics.d_checkRuns); bool sentLemma = false; @@ -174,9 +174,12 @@ void TheoryBags::postCheck(Effort effort) d_im.reset(); // TODO issue #78: add ++(d_statistics.d_strategyRuns); Trace("bags-check") << " * Run strategy..." << std::endl; - // TODO issue #78: add runStrategy(e); - - d_solver.postCheck(); + std::vector lemmas = d_state.initialize(); + for (Node lemma : lemmas) + { + d_im.lemma(lemma, InferenceId::BAGS_COUNT_SKOLEM); + } + runStrategy(effort); // remember if we had pending facts or lemmas hadPending = d_im.hasPending(); @@ -192,7 +195,7 @@ void TheoryBags::postCheck(Effort effort) sentLemma = d_im.hasSentLemma(); if (Trace.isOn("bags-check")) { - // TODO: clean this Trace("bags-check") << " ...finish run strategy: "; + Trace("bags-check") << " ...finish run strategy: "; Trace("bags-check") << (hadPending ? "hadPending " : ""); Trace("bags-check") << (sentLemma ? "sentLemma " : ""); Trace("bags-check") << (d_state.isInConflict() ? "conflict " : ""); @@ -211,6 +214,66 @@ void TheoryBags::postCheck(Effort effort) Assert(!d_im.hasPendingLemma()); } +void TheoryBags::runStrategy(Theory::Effort e) +{ + std::vector>::iterator it = d_strat.stepBegin(e); + std::vector>::iterator stepEnd = + d_strat.stepEnd(e); + + Trace("bags-process") << "----check, next round---" << std::endl; + while (it != stepEnd) + { + InferStep curr = it->first; + if (curr == BREAK) + { + if (d_state.isInConflict() || d_im.hasPending()) + { + break; + } + } + else + { + if (runInferStep(curr, it->second) || d_state.isInConflict()) + { + break; + } + } + ++it; + } + Trace("bags-process") << "----finished round---" << std::endl; +} + +/** run the given inference step */ +bool TheoryBags::runInferStep(InferStep s, int effort) +{ + Trace("bags-process") << "Run " << s; + if (effort > 0) + { + Trace("bags-process") << ", effort = " << effort; + } + Trace("bags-process") << "..." << std::endl; + switch (s) + { + case CHECK_INIT: break; + case CHECK_BAG_MAKE: + { + if (d_solver.checkBagMake()) + { + return true; + } + break; + } + case CHECK_BASIC_OPERATIONS: d_solver.checkBasicOperations(); break; + default: Unreachable(); break; + } + Trace("bags-process") << "Done " << s + << ", addedFact = " << d_im.hasPendingFact() + << ", addedLemma = " << d_im.hasPendingLemma() + << ", conflict = " << d_state.isInConflict() + << std::endl; + return false; +} + void TheoryBags::notifyFact(TNode atom, bool polarity, TNode fact, @@ -245,22 +308,24 @@ bool TheoryBags::collectModelValues(TheoryModel* m, processedBags.insert(r); - std::set solverElements = d_state.getElements(r); - std::set elements; - // only consider terms in termSet and ignore other elements in the solver - std::set_intersection(termSet.begin(), - termSet.end(), - solverElements.begin(), - solverElements.end(), - std::inserter(elements, elements.begin())); - Trace("bags-model") << "Elements of bag " << n << " are: " << std::endl - << elements << std::endl; + const std::vector>& solverElements = + d_state.getElementCountPairs(r); + std::vector> elements; + for (std::pair pair : solverElements) + { + if (termSet.find(pair.first) == termSet.end()) + { + continue; + } + elements.push_back(pair); + } + std::map elementReps; - for (const Node& e : elements) + for (std::pair pair : elements) { - Node key = d_state.getRepresentative(e); - Node countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, r); - Node value = m->getRepresentative(countTerm); + Node key = d_state.getRepresentative(pair.first); + Node countSkolem = pair.second; + Node value = m->getRepresentative(countSkolem); elementReps[key] = value; } Node rep = NormalForm::constructBagFromElements(tn, elementReps); @@ -299,7 +364,12 @@ void TheoryBags::preRegisterTerm(TNode n) } } -void TheoryBags::presolve() {} +void TheoryBags::presolve() +{ + Debug("bags-presolve") << "Started presolve" << std::endl; + d_strat.initializeStrategy(); + Debug("bags-presolve") << "Finished presolve" << std::endl; +} /**************************** eq::NotifyClass *****************************/ diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 8d15947ef..cc76c5453 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -25,6 +25,7 @@ #include "theory/bags/inference_generator.h" #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" +#include "theory/bags/strategy.h" #include "theory/bags/term_registry.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" @@ -72,6 +73,11 @@ class TheoryBags : public Theory void preRegisterTerm(TNode n) override; void presolve() override; + /** run strategy for effort e */ + void runStrategy(Theory::Effort e); + /** run the given inference step */ + bool runInferStep(InferStep s, int effort); + private: /** Functions to handle callbacks from equality engine */ class NotifyClass : public TheoryEqNotifyClass @@ -114,6 +120,9 @@ class TheoryBags : public Theory /** bag reduction */ BagReduction d_bagReduction; + /** The representation of the strategy */ + Strategy d_strat; + void eqNotifyNewClass(TNode n); void eqNotifyMerge(TNode n1, TNode n2); void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index af18d3eef..a2dcdec8c 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -107,6 +107,8 @@ const char* toString(InferenceId i) case InferenceId::BAGS_NON_NEGATIVE_COUNT: return "BAGS_NON_NEGATIVE_COUNT"; case InferenceId::BAGS_BAG_MAKE: return "BAGS_BAG_MAKE"; + case InferenceId::BAGS_BAG_MAKE_SPLIT: return "BAGS_BAG_MAKE_SPLIT"; + case InferenceId::BAGS_COUNT_SKOLEM: return "BAGS_COUNT_SKOLEM"; case InferenceId::BAGS_EQUALITY: return "BAGS_EQUALITY"; case InferenceId::BAGS_DISEQUALITY: return "BAGS_DISEQUALITY"; case InferenceId::BAGS_EMPTY: return "BAGS_EMPTY"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 8eaeeab75..8d9078503 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -170,6 +170,8 @@ enum class InferenceId // ---------------------------------- bags theory BAGS_NON_NEGATIVE_COUNT, BAGS_BAG_MAKE, + BAGS_BAG_MAKE_SPLIT, + BAGS_COUNT_SKOLEM, BAGS_EQUALITY, BAGS_DISEQUALITY, BAGS_EMPTY, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6bca782f1..3c0e79596 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1627,6 +1627,7 @@ set(regress_1_tests regress1/bags/fuzzy1.smt2 regress1/bags/fuzzy2.smt2 regress1/bags/fuzzy3.smt2 + regress1/bags/fuzzy3b.smt2 regress1/bags/fuzzy4.smt2 regress1/bags/fuzzy5.smt2 regress1/bags/fuzzy6.smt2 diff --git a/test/regress/regress1/bags/fuzzy3b.smt2 b/test/regress/regress1/bags/fuzzy3b.smt2 new file mode 100644 index 000000000..926455710 --- /dev/null +++ b/test/regress/regress1/bags/fuzzy3b.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun d () (Tuple Int Int)) +(assert (= A (bag.difference_remove A (bag d 1)))) +(check-sat) diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index ff98c308a..af24abc39 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -189,7 +189,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) ASSERT_TRUE(response1.d_status == REWRITE_AGAIN_FULL && response1.d_node == zero); - // (bag.count x (bag x c) = (ite (>= c 1) c 0) + // (bag.count x (bag x c) = c, c > 0 is a constant Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, three); Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); @@ -197,7 +197,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) Node geq = d_nodeManager->mkNode(GEQ, three, one); Node ite = d_nodeManager->mkNode(ITE, geq, three, zero); ASSERT_TRUE(response2.d_status == REWRITE_AGAIN_FULL - && response2.d_node == ite); + && response2.d_node == three); } TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)