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
#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"
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
}
}
+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);
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)
// (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>() > 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);
}
#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"
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);
*/
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
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<Node>& SolverState::getBags() { return d_bags; }
-const std::set<Node>& SolverState::getElements(Node B)
+std::set<Node> SolverState::getElements(Node B)
{
Node bag = getRepresentative(B);
+ std::set<Node> elements;
+ std::vector<std::pair<Node, Node>> pairs = d_bagElements[bag];
+ for (std::pair<Node, Node> pair : pairs)
+ {
+ elements.insert(pair.first);
+ }
+ return elements;
+}
+
+const std::vector<std::pair<Node, Node>>& SolverState::getElementCountPairs(
+ Node n)
+{
+ Node bag = getRepresentative(n);
return d_bagElements[bag];
}
d_deq.clear();
}
-void SolverState::initialize()
+std::vector<Node> SolverState::initialize()
{
reset();
- collectBagsAndCountTerms();
collectDisequalBagTerms();
+ return collectBagsAndCountTerms();
}
-void SolverState::collectBagsAndCountTerms()
+std::vector<Node> SolverState::collectBagsAndCountTerms()
{
+ std::vector<Node> lemmas;
+
eq::EqClassesIterator repIt = eq::EqClassesIterator(d_ee);
while (!repIt.isFinished())
{
// 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;
}
}
Trace("bags-eqc") << "bag representatives: " << d_bags << endl;
- Trace("bags-eqc") << "bag elements: " << d_bagElements << endl;
+ return lemmas;
}
void SolverState::collectDisequalBagTerms()
/**
* @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
* (assert (= 0 (bag.count x B)))
* element x is associated with bag B, albeit x is definitely not in B.
*/
- const std::set<Node>& getElements(Node B);
- /** initialize bag and count terms */
- void initialize();
+ std::set<Node> getElements(Node B);
+ /**
+ * initialize bag and count terms
+ * @return a list of skolem lemmas to be asserted
+ * */
+ std::vector<Node> initialize();
/** return disequal bag terms */
const std::set<Node>& getDisequalBagTerms();
+ /**
+ * return a list of bag elements and their skolem counts
+ */
+ const std::vector<std::pair<Node, Node>>& getElementCountPairs(Node n);
private:
/** clear all bags data structures */
/**
* 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<Node> collectBagsAndCountTerms();
/**
* collect disequal bag terms. This function is called during postCheck.
*/
NodeManager* d_nm;
/** collection of bag representatives */
std::set<Node> d_bags;
- /** bag -> associated elements */
- std::map<Node, std::set<Node>> 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<Node, std::vector<std::pair<Node, Node>>> d_bagElements;
/** Disequal bag terms */
std::set<Node> d_deq;
}; /* class SolverState */
--- /dev/null
+/******************************************************************************
+ * 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<std::pair<InferStep, size_t> >::iterator Strategy::stepBegin(
+ Theory::Effort e)
+{
+ std::map<Theory::Effort, std::pair<size_t, size_t> >::const_iterator it =
+ d_strat_steps.find(e);
+ Assert(it != d_strat_steps.end());
+ return d_infer_steps.begin() + it->second.first;
+}
+
+std::vector<std::pair<InferStep, size_t> >::iterator Strategy::stepEnd(
+ Theory::Effort e)
+{
+ std::map<Theory::Effort, std::pair<size_t, size_t> >::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<InferStep, int>(s, effort));
+ if (addBreak)
+ {
+ d_infer_steps.push_back(std::pair<InferStep, int>(BREAK, 0));
+ }
+}
+
+void Strategy::initializeStrategy()
+{
+ // initialize the strategy if not already done so
+ if (!d_strategy_init)
+ {
+ std::map<Theory::Effort, unsigned> step_begin;
+ std::map<Theory::Effort, unsigned> 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<const Theory::Effort, unsigned>& it_begin : step_begin)
+ {
+ Theory::Effort e = it_begin.first;
+ std::map<Theory::Effort, unsigned>::iterator it_end = step_end.find(e);
+ Assert(it_end != step_end.end());
+ d_strat_steps[e] =
+ std::pair<unsigned, unsigned>(it_begin.second, it_end->second);
+ }
+ }
+}
+
+} // namespace bags
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * 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 <map>
+#include <vector>
+
+#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<std::pair<InferStep, size_t> >::iterator stepBegin(
+ Theory::Effort e);
+ std::vector<std::pair<InferStep, size_t> >::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<std::pair<InferStep, size_t> > d_infer_steps;
+ /** the range (begin, end) of steps to run at given efforts */
+ std::map<Theory::Effort, std::pair<size_t, size_t> > d_strat_steps;
+}; /* class Strategy */
+
+} // namespace bags
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__BAGS__STRATEGY_H */
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;
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<Node> 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();
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 " : "");
Assert(!d_im.hasPendingLemma());
}
+void TheoryBags::runStrategy(Theory::Effort e)
+{
+ std::vector<std::pair<InferStep, size_t>>::iterator it = d_strat.stepBegin(e);
+ std::vector<std::pair<InferStep, size_t>>::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,
processedBags.insert(r);
- std::set<Node> solverElements = d_state.getElements(r);
- std::set<Node> 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<std::pair<Node, Node>>& solverElements =
+ d_state.getElementCountPairs(r);
+ std::vector<std::pair<Node, Node>> elements;
+ for (std::pair<Node, Node> pair : solverElements)
+ {
+ if (termSet.find(pair.first) == termSet.end())
+ {
+ continue;
+ }
+ elements.push_back(pair);
+ }
+
std::map<Node, Node> elementReps;
- for (const Node& e : elements)
+ for (std::pair<Node, Node> 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);
}
}
-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 *****************************/
#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"
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
/** 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);
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";
// ---------------------------------- bags theory
BAGS_NON_NEGATIVE_COUNT,
BAGS_BAG_MAKE,
+ BAGS_BAG_MAKE_SPLIT,
+ BAGS_COUNT_SKOLEM,
BAGS_EQUALITY,
BAGS_DISEQUALITY,
BAGS_EMPTY,
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
--- /dev/null
+(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)
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);
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)
projects / cvc5.git / commitdiff