summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp6
-rw-r--r--src/api/cvc4cppkind.h17
-rw-r--r--src/parser/smt2/smt2.cpp5
-rw-r--r--src/theory/bags/bags_rewriter.cpp26
-rw-r--r--src/theory/bags/bags_rewriter.h14
-rw-r--r--src/theory/bags/kinds6
-rw-r--r--src/theory/bags/make_bag_op.cpp3
-rw-r--r--src/theory/bags/normal_form.cpp25
-rw-r--r--src/theory/bags/normal_form.h7
-rw-r--r--src/theory/bags/rewrites.cpp1
-rw-r--r--src/theory/bags/rewrites.h1
-rw-r--r--src/theory/bags/theory_bags.cpp1
-rw-r--r--src/theory/bags/theory_bags_type_rules.h30
13 files changed, 118 insertions, 24 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f4717158a..9b34b07cd 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -261,8 +261,9 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
{INTERSECTION_MIN, CVC4::Kind::INTERSECTION_MIN},
{DIFFERENCE_SUBTRACT, CVC4::Kind::DIFFERENCE_SUBTRACT},
{DIFFERENCE_REMOVE, CVC4::Kind::DIFFERENCE_REMOVE},
- {BAG_IS_INCLUDED, CVC4::Kind::BAG_IS_INCLUDED},
+ {SUBBAG, CVC4::Kind::SUBBAG},
{BAG_COUNT, CVC4::Kind::BAG_COUNT},
+ {DUPLICATE_REMOVAL, CVC4::Kind::DUPLICATE_REMOVAL},
{MK_BAG, CVC4::Kind::MK_BAG},
{EMPTYBAG, CVC4::Kind::EMPTYBAG},
{BAG_CARD, CVC4::Kind::BAG_CARD},
@@ -566,8 +567,9 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
{CVC4::Kind::INTERSECTION_MIN, INTERSECTION_MIN},
{CVC4::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT},
{CVC4::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE},
- {CVC4::Kind::BAG_IS_INCLUDED, BAG_IS_INCLUDED},
+ {CVC4::Kind::SUBBAG, SUBBAG},
{CVC4::Kind::BAG_COUNT, BAG_COUNT},
+ {CVC4::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL},
{CVC4::Kind::MK_BAG, MK_BAG},
{CVC4::Kind::EMPTYBAG, EMPTYBAG},
{CVC4::Kind::BAG_CARD, BAG_CARD},
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index d6ee24f1e..0bd4117dc 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -2030,14 +2030,15 @@ enum CVC4_PUBLIC Kind : int32_t
*/
DIFFERENCE_REMOVE,
/**
- * Bag is included (first multiplicities <= second multiplicities).
+ * Inclusion predicate for bags
+ * (multiplicities of the first bag <= multiplicities of the second bag).
* Parameters: 2
- * -[1]..[2]: Terms of set sort
+ * -[1]..[2]: Terms of bag sort
* Create with:
* mkTerm(Kind kind, Term child1, Term child2)
* mkTerm(Kind kind, const std::vector<Term>& children)
*/
- BAG_IS_INCLUDED,
+ SUBBAG,
/**
* Element multiplicity in a bag
* Parameters: 2
@@ -2048,6 +2049,16 @@ enum CVC4_PUBLIC Kind : int32_t
*/
BAG_COUNT,
/**
+ * Eliminate duplicates in a given bag. The returned bag contains exactly the
+ * same elements in the given bag, but with multiplicity one.
+ * Parameters: 1
+ * -[1]: a term of bag sort
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
+ DUPLICATE_REMOVAL,
+ /**
* The bag of the single element given as a parameter.
* Parameters: 1
* -[1]: Single element
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a226f7cbf..81a4bd4a6 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -695,9 +695,10 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
addOperator(api::INTERSECTION_MIN, "intersection_min");
addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract");
addOperator(api::DIFFERENCE_REMOVE, "difference_remove");
- addOperator(api::BAG_IS_INCLUDED, "bag.is_included");
+ addOperator(api::SUBBAG, "bag.is_included");
addOperator(api::BAG_COUNT, "bag.count");
- addOperator(api::MK_BAG, "mkBag");
+ addOperator(api::DUPLICATE_REMOVAL, "duplicate_removal");
+ addOperator(api::MK_BAG, "bag");
addOperator(api::BAG_CARD, "bag.card");
addOperator(api::BAG_CHOOSE, "bag.choose");
addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton");
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 26c54d4ec..f0540e9b7 100644
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -63,6 +63,7 @@ RewriteResponse BagsRewriter::postRewrite(TNode n)
{
case MK_BAG: response = rewriteMakeBag(n); break;
case BAG_COUNT: response = rewriteBagCount(n); break;
+ case DUPLICATE_REMOVAL: response = rewriteDuplicateRemoval(n); break;
case UNION_MAX: response = rewriteUnionMax(n); break;
case UNION_DISJOINT: response = rewriteUnionDisjoint(n); break;
case INTERSECTION_MIN: response = rewriteIntersectionMin(n); break;
@@ -98,7 +99,7 @@ RewriteResponse BagsRewriter::preRewrite(TNode n)
switch (k)
{
case EQUAL: response = rewriteEqual(n); break;
- case BAG_IS_INCLUDED: response = rewriteIsIncluded(n); break;
+ case SUBBAG: response = rewriteSubBag(n); break;
default: response = BagsRewriteResponse(n, Rewrite::NONE);
}
@@ -127,9 +128,9 @@ BagsRewriteResponse BagsRewriter::rewriteEqual(const TNode& n) const
return BagsRewriteResponse(n, Rewrite::NONE);
}
-BagsRewriteResponse BagsRewriter::rewriteIsIncluded(const TNode& n) const
+BagsRewriteResponse BagsRewriter::rewriteSubBag(const TNode& n) const
{
- Assert(n.getKind() == BAG_IS_INCLUDED);
+ Assert(n.getKind() == SUBBAG);
// (bag.is_included A B) = ((difference_subtract A B) == emptybag)
Node emptybag = d_nm->mkConst(EmptyBag(n[0].getType()));
@@ -168,6 +169,21 @@ BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const
return BagsRewriteResponse(n, Rewrite::NONE);
}
+BagsRewriteResponse BagsRewriter::rewriteDuplicateRemoval(const TNode& n) const
+{
+ Assert(n.getKind() == DUPLICATE_REMOVAL);
+ if (n[0].getKind() == MK_BAG && n[0][1].isConst()
+ && n[0][1].getConst<Rational>().sgn() == 1)
+ {
+ // (duplicate_removal (mkBag x n)) = (mkBag x 1)
+ // where n is a positive constant
+ Node one = NodeManager::currentNM()->mkConst(Rational(1));
+ Node bag = d_nm->mkBag(n[0][0].getType(), n[0][0], one);
+ return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_MK_BAG);
+ }
+ return BagsRewriteResponse(n, Rewrite::NONE);
+}
+
BagsRewriteResponse BagsRewriter::rewriteUnionMax(const TNode& n) const
{
Assert(n.getKind() == UNION_MAX);
@@ -453,8 +469,8 @@ BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const
{
// (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x)
// where n is a positive constant and T is the type of the bag's elements
- Node bag = d_nm->mkSingleton(n[0][0].getType(), n[0][0]);
- return BagsRewriteResponse(bag, Rewrite::TO_SINGLETON);
+ Node set = d_nm->mkSingleton(n[0][0].getType(), n[0][0]);
+ return BagsRewriteResponse(set, Rewrite::TO_SINGLETON);
}
return BagsRewriteResponse(n, Rewrite::NONE);
}
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index d36a21ccf..8be6b948a 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -17,8 +17,8 @@
#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
#define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
-#include "theory/rewriter.h"
#include "theory/bags/rewrites.h"
+#include "theory/rewriter.h"
namespace CVC4 {
namespace theory {
@@ -50,7 +50,7 @@ class BagsRewriter : public TheoryRewriter
*/
RewriteResponse postRewrite(TNode n) override;
/**
- * preRewrite nodes with kinds: EQUAL, BAG_IS_INCLUDED.
+ * preRewrite nodes with kinds: EQUAL, SUBBAG.
* See the rewrite rules for these kinds below.
*/
RewriteResponse preRewrite(TNode n) override;
@@ -66,7 +66,7 @@ class BagsRewriter : public TheoryRewriter
* rewrites for n include:
* - (bag.is_included A B) = ((difference_subtract A B) == emptybag)
*/
- BagsRewriteResponse rewriteIsIncluded(const TNode& n) const;
+ BagsRewriteResponse rewriteSubBag(const TNode& n) const;
/**
* rewrites for n include:
@@ -76,6 +76,7 @@ class BagsRewriter : public TheoryRewriter
* - otherwise = n
*/
BagsRewriteResponse rewriteMakeBag(const TNode& n) const;
+
/**
* rewrites for n include:
* - (bag.count x emptybag) = 0
@@ -85,6 +86,13 @@ class BagsRewriter : public TheoryRewriter
BagsRewriteResponse rewriteBagCount(const TNode& n) const;
/**
+ * rewrites for n include:
+ * - (duplicate_removal (mkBag x n)) = (mkBag x 1)
+ * where n is a positive constant
+ */
+ BagsRewriteResponse rewriteDuplicateRemoval(const TNode& n) const;
+
+ /**
* rewrites for n include:
* - (union_max A emptybag) = A
* - (union_max emptybag A) = A
diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
index 86e89e0bd..f84b811e7 100644
--- a/src/theory/bags/kinds
+++ b/src/theory/bags/kinds
@@ -45,8 +45,9 @@ operator DIFFERENCE_SUBTRACT 2 "bag difference1 (subtracts multiplicities)"
# {("a", 2), ("b", 3)} \\ {("a", 1)} = {("b", 3)}
operator DIFFERENCE_REMOVE 2 "bag difference remove (removes shared elements)"
-operator BAG_IS_INCLUDED 2 "inclusion predicate for bags (less than or equal multiplicities)"
+operator SUBBAG 2 "inclusion predicate for bags (less than or equal multiplicities)"
operator BAG_COUNT 2 "multiplicity of an element in a bag"
+operator DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)"
constant MK_BAG_OP \
::CVC4::MakeBagOp \
@@ -74,8 +75,9 @@ typerule UNION_DISJOINT ::CVC4::theory::bags::BinaryOperatorTypeRule
typerule INTERSECTION_MIN ::CVC4::theory::bags::BinaryOperatorTypeRule
typerule DIFFERENCE_SUBTRACT ::CVC4::theory::bags::BinaryOperatorTypeRule
typerule DIFFERENCE_REMOVE ::CVC4::theory::bags::BinaryOperatorTypeRule
-typerule BAG_IS_INCLUDED ::CVC4::theory::bags::IsIncludedTypeRule
+typerule SUBBAG ::CVC4::theory::bags::SubBagTypeRule
typerule BAG_COUNT ::CVC4::theory::bags::CountTypeRule
+typerule DUPLICATE_REMOVAL ::CVC4::theory::bags::DuplicateRemovalTypeRule
typerule MK_BAG_OP "SimpleTypeRule<RBuiltinOperator>"
typerule MK_BAG ::CVC4::theory::bags::MkBagTypeRule
typerule EMPTYBAG ::CVC4::theory::bags::EmptyBagTypeRule
diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp
index 6a535afc2..b60822783 100644
--- a/src/theory/bags/make_bag_op.cpp
+++ b/src/theory/bags/make_bag_op.cpp
@@ -12,10 +12,11 @@
** \brief a class for MK_BAG operator
**/
+#include "make_bag_op.h"
+
#include <iostream>
#include "expr/type_node.h"
-#include "make_bag_op.h"
namespace CVC4 {
diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
index f2dea62d3..081ed77aa 100644
--- a/src/theory/bags/normal_form.cpp
+++ b/src/theory/bags/normal_form.cpp
@@ -94,6 +94,7 @@ Node NormalForm::evaluate(TNode n)
{
case MK_BAG: return evaluateMakeBag(n);
case BAG_COUNT: return evaluateBagCount(n);
+ case DUPLICATE_REMOVAL: return evaluateDuplicateRemoval(n);
case UNION_DISJOINT: return evaluateUnionDisjoint(n);
case UNION_MAX: return evaluateUnionMax(n);
case INTERSECTION_MIN: return evaluateIntersectionMin(n);
@@ -240,6 +241,30 @@ Node NormalForm::evaluateBagCount(TNode n)
return nm->mkConst(Rational(0));
}
+Node NormalForm::evaluateDuplicateRemoval(TNode n)
+{
+ Assert(n.getKind() == DUPLICATE_REMOVAL);
+
+ // Examples
+ // --------
+ // - (duplicate_removal (emptybag String)) = (emptybag String)
+ // - (duplicate_removal (mkBag "x" 4)) = (emptybag "x" 1)
+ // - (duplicate_removal (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) =
+ // (disjoint_union (mkBag "x" 1) (mkBag "y" 1)
+
+ std::map<Node, Rational> oldElements = getBagElements(n[0]);
+ // copy elements from the old bag
+ std::map<Node, Rational> newElements(oldElements);
+ Rational one = Rational(1);
+ std::map<Node, Rational>::iterator it;
+ for (it = newElements.begin(); it != newElements.end(); it++)
+ {
+ it->second = one;
+ }
+ Node bag = constructBagFromElements(n[0].getType(), newElements);
+ return bag;
+}
+
Node NormalForm::evaluateUnionDisjoint(TNode n)
{
Assert(n.getKind() == UNION_DISJOINT);
diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h
index ef0edefff..5a7936fa3 100644
--- a/src/theory/bags/normal_form.h
+++ b/src/theory/bags/normal_form.h
@@ -115,6 +115,13 @@ class NormalForm
static Node evaluateBagCount(TNode n);
/**
+ * @param n has the form (duplicate_removal A) where A is a constant bag
+ * @return a constant bag constructed from the elements in A where each
+ * element has multiplicity one
+ */
+ static Node evaluateDuplicateRemoval(TNode n);
+
+ /**
* evaluates union disjoint node such that the returned node is a canonical
* bag that has the form
* (union_disjoint (mkBag e1 c1) ...
diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp
index be3b3cc71..d640bcdce 100644
--- a/src/theory/bags/rewrites.cpp
+++ b/src/theory/bags/rewrites.cpp
@@ -31,6 +31,7 @@ const char* toString(Rewrite r)
case Rewrite::CONSTANT_EVALUATION: return "CONSTANT_EVALUATION";
case Rewrite::COUNT_EMPTY: return "COUNT_EMPTY";
case Rewrite::COUNT_MK_BAG: return "COUNT_MK_BAG";
+ case Rewrite::DUPLICATE_REMOVAL_MK_BAG: return "DUPLICATE_REMOVAL_MK_BAG";
case Rewrite::FROM_SINGLETON: return "FROM_SINGLETON";
case Rewrite::IDENTICAL_NODES: return "IDENTICAL_NODES";
case Rewrite::INTERSECTION_EMPTY_LEFT: return "INTERSECTION_EMPTY_LEFT";
diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h
index dc1921e24..36e30ca68 100644
--- a/src/theory/bags/rewrites.h
+++ b/src/theory/bags/rewrites.h
@@ -36,6 +36,7 @@ enum class Rewrite : uint32_t
CONSTANT_EVALUATION,
COUNT_EMPTY,
COUNT_MK_BAG,
+ DUPLICATE_REMOVAL_MK_BAG,
FROM_SINGLETON,
IDENTICAL_NODES,
INTERSECTION_EMPTY_LEFT,
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 9dcad9bb1..9f62ea1c6 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -63,6 +63,7 @@ void TheoryBags::finishInit()
d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT);
d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE);
d_equalityEngine->addFunctionKind(BAG_COUNT);
+ d_equalityEngine->addFunctionKind(DUPLICATE_REMOVAL);
d_equalityEngine->addFunctionKind(MK_BAG);
d_equalityEngine->addFunctionKind(BAG_CARD);
d_equalityEngine->addFunctionKind(BAG_FROM_SET);
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index 7767938ed..cece40c9e 100644
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -61,18 +61,17 @@ struct BinaryOperatorTypeRule
}
}; /* struct BinaryOperatorTypeRule */
-struct IsIncludedTypeRule
+struct SubBagTypeRule
{
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
{
- Assert(n.getKind() == kind::BAG_IS_INCLUDED);
+ Assert(n.getKind() == kind::SUBBAG);
TypeNode bagType = n[0].getType(check);
if (check)
{
if (!bagType.isBag())
{
- throw TypeCheckingExceptionPrivate(
- n, "BAG_IS_INCLUDED operating on non-bag");
+ throw TypeCheckingExceptionPrivate(n, "SUBBAG operating on non-bag");
}
TypeNode secondBagType = n[1].getType(check);
if (secondBagType != bagType)
@@ -80,13 +79,13 @@ struct IsIncludedTypeRule
if (!bagType.isComparableTo(secondBagType))
{
throw TypeCheckingExceptionPrivate(
- n, "BAG_IS_INCLUDED operating on bags of different types");
+ n, "SUBBAG operating on bags of different types");
}
}
}
return nodeManager->booleanType();
}
-}; /* struct IsIncludedTypeRule */
+}; /* struct SubBagTypeRule */
struct CountTypeRule
{
@@ -118,6 +117,25 @@ struct CountTypeRule
}
}; /* struct CountTypeRule */
+struct DuplicateRemovalTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::DUPLICATE_REMOVAL);
+ TypeNode bagType = n[0].getType(check);
+ if (check)
+ {
+ if (!bagType.isBag())
+ {
+ std::stringstream ss;
+ ss << "Applying DUPLICATE_REMOVAL on a non-bag argument in term " << n;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ return bagType;
+ }
+}; /* struct DuplicateRemovalTypeRule */
+
struct MkBagTypeRule
{
static TypeNode computeType(NodeManager* nm, TNode n, bool check)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback