summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/api/cvc4cppkind.h3
-rw-r--r--src/expr/node_manager.cpp11
-rw-r--r--src/expr/node_manager.h12
-rw-r--r--src/expr/type_node.cpp7
-rw-r--r--src/theory/bags/bags_rewriter.cpp3
-rw-r--r--src/theory/bags/kinds10
-rw-r--r--src/theory/bags/make_bag_op.cpp48
-rw-r--r--src/theory/bags/make_bag_op.h63
-rw-r--r--src/theory/bags/theory_bags_type_enumerator.cpp3
-rw-r--r--src/theory/bags/theory_bags_type_rules.h49
-rw-r--r--test/unit/theory/CMakeLists.txt4
-rw-r--r--test/unit/theory/theory_bags_rewriter_white.h (renamed from test/unit/theory/theory_bags_rewriter_black.h)82
-rw-r--r--test/unit/theory/theory_bags_type_rules_white.h (renamed from test/unit/theory/theory_bags_type_rules_black.h)18
14 files changed, 241 insertions, 74 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4d96fa0b3..5966debc1 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -429,6 +429,8 @@ libcvc4_add_sources(
theory/bags/bags_statistics.h
theory/bags/inference_manager.cpp
theory/bags/inference_manager.h
+ theory/bags/make_bag_op.cpp
+ theory/bags/make_bag_op.h
theory/bags/normal_form.cpp
theory/bags/normal_form.h
theory/bags/rewrites.cpp
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 913a4a993..d6ee24f1e 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1841,7 +1841,8 @@ enum CVC4_PUBLIC Kind : int32_t
*/
MEMBER,
/**
- * The set of the single element given as a parameter.
+ * Construct a singleton set from an element given as a parameter.
+ * The returned set has same type of the element.
* Parameters: 1
* -[1]: Single element
* Create with:
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index f8057006c..e9f121047 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -961,6 +961,17 @@ Node NodeManager::mkSingleton(const TypeNode& t, const TNode n)
return singleton;
}
+Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m)
+{
+ Assert(n.getType().isSubtypeOf(t))
+ << "Invalid operands for mkBag. The type '" << n.getType()
+ << "' of node '" << n << "' is not a subtype of '" << t << "'."
+ << std::endl;
+ Node op = mkConst(MakeBagOp(t));
+ Node bag = mkNode(kind::MK_BAG, op, n, m);
+ return bag;
+}
+
Node NodeManager::mkAbstractValue(const TypeNode& type) {
Node n = mkConst(AbstractValue(++d_abstractValueCount));
n.setAttribute(TypeAttr(), type);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5427c3b6a..8f2237523 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -578,13 +578,23 @@ class NodeManager {
/**
* Create a singleton set from the given element n.
* @param t the element type of the returned set.
- * Note that the type of n needs to be a subtype of t.
+ * Note that the type of n needs to be a subtype of t.
* @param n the single element in the singleton.
* @return a singleton set constructed from the element n.
*/
Node mkSingleton(const TypeNode& t, const TNode n);
/**
+ * Create a bag from the given element n along with its multiplicity m.
+ * @param t the element type of the returned bag.
+ * Note that the type of n needs to be a subtype of t.
+ * @param n the element that is used to to construct the bag
+ * @param m the multiplicity of the element n
+ * @return a bag that contains m occurrences of n.
+ */
+ Node mkBag(const TypeNode& t, const TNode n, const TNode m);
+
+ /**
* Create a constant of type T. It will have the appropriate
* CONST_* kind defined for T.
*/
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 659b1eef2..e917a9d0d 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -574,11 +574,12 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
case kind::ARRAY_TYPE:
case kind::DATATYPE_TYPE:
case kind::PARAMETRIC_DATATYPE:
- case kind::SEQUENCE_TYPE: return TypeNode();
+ case kind::SEQUENCE_TYPE:
case kind::SET_TYPE:
+ case kind::BAG_TYPE:
{
- // we don't support subtyping for sets
- return TypeNode(); // return null type
+ // we don't support subtyping except for built in types Int and Real.
+ return TypeNode(); // return null type
}
case kind::SEXPR_TYPE:
Unimplemented()
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 1faaf55c0..c413a5e7e 100644
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -438,7 +438,8 @@ BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const
{
// (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1)
Node one = d_nm->mkConst(Rational(1));
- Node bag = d_nm->mkNode(MK_BAG, n[0][0], one);
+ TypeNode type = n[0].getType().getSetElementType();
+ Node bag = d_nm->mkBag(type, n[0][0], one);
return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON);
}
return BagsRewriteResponse(n, Rewrite::NONE);
diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
index 72326de08..86e89e0bd 100644
--- a/src/theory/bags/kinds
+++ b/src/theory/bags/kinds
@@ -47,7 +47,14 @@ 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 BAG_COUNT 2 "multiplicity of an element in a bag"
-operator MK_BAG 2 "constructs a bag from one element along with its multiplicity"
+
+constant MK_BAG_OP \
+ ::CVC4::MakeBagOp \
+ ::CVC4::MakeBagOpHashFunction \
+ "theory/bags/make_bag_op.h" \
+ "operator for MK_BAG; payload is an instance of the CVC4::MakeBagOp class"
+parameterized MK_BAG MK_BAG_OP 2 \
+"constructs a bag from one element along with its multiplicity"
# The operator bag-is-singleton returns whether the given bag is a singleton
operator BAG_IS_SINGLETON 1 "return whether the given bag is a singleton"
@@ -69,6 +76,7 @@ typerule DIFFERENCE_SUBTRACT ::CVC4::theory::bags::BinaryOperatorTypeRule
typerule DIFFERENCE_REMOVE ::CVC4::theory::bags::BinaryOperatorTypeRule
typerule BAG_IS_INCLUDED ::CVC4::theory::bags::IsIncludedTypeRule
typerule BAG_COUNT ::CVC4::theory::bags::CountTypeRule
+typerule MK_BAG_OP "SimpleTypeRule<RBuiltinOperator>"
typerule MK_BAG ::CVC4::theory::bags::MkBagTypeRule
typerule EMPTYBAG ::CVC4::theory::bags::EmptyBagTypeRule
typerule BAG_CARD ::CVC4::theory::bags::CardTypeRule
diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp
new file mode 100644
index 000000000..6a535afc2
--- /dev/null
+++ b/src/theory/bags/make_bag_op.cpp
@@ -0,0 +1,48 @@
+/********************* */
+/*! \file bag_op.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief a class for MK_BAG operator
+ **/
+
+#include <iostream>
+
+#include "expr/type_node.h"
+#include "make_bag_op.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const MakeBagOp& op)
+{
+ return out << "(mkBag_op " << op.getType() << ')';
+}
+
+size_t MakeBagOpHashFunction::operator()(const MakeBagOp& op) const
+{
+ return TypeNodeHashFunction()(op.getType());
+}
+
+MakeBagOp::MakeBagOp(const TypeNode& elementType)
+ : d_type(new TypeNode(elementType))
+{
+}
+
+MakeBagOp::MakeBagOp(const MakeBagOp& op) : d_type(new TypeNode(op.getType()))
+{
+}
+
+const TypeNode& MakeBagOp::getType() const { return *d_type; }
+
+bool MakeBagOp::operator==(const MakeBagOp& op) const
+{
+ return getType() == op.getType();
+}
+
+} // namespace CVC4
diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h
new file mode 100644
index 000000000..b47930879
--- /dev/null
+++ b/src/theory/bags/make_bag_op.h
@@ -0,0 +1,63 @@
+/********************* */
+/*! \file mk_bag_op.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief a class for MK_BAG operator
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__MAKE_BAG_OP_H
+#define CVC4__MAKE_BAG_OP_H
+
+#include <memory>
+
+namespace CVC4 {
+
+class TypeNode;
+
+/**
+ * The class is an operator for kind MK_BAG used to construct bags.
+ * It specifies the type of the element especially when it is a constant.
+ * e.g. the type of rational 1 is Int, however
+ * (mkBag (mkBag_op Real) 1) is of type (Bag Real), not (Bag Int).
+ * Note that the type passed to the constructor is the element's type, not the
+ * bag type.
+ */
+class MakeBagOp
+{
+ public:
+ MakeBagOp(const TypeNode& elementType);
+ MakeBagOp(const MakeBagOp& op);
+
+ /** return the type of the current object */
+ const TypeNode& getType() const;
+
+ bool operator==(const MakeBagOp& op) const;
+
+ private:
+ MakeBagOp();
+ /** a pointer to the type of the bag element */
+ std::unique_ptr<TypeNode> d_type;
+}; /* class MakeBagOp */
+
+std::ostream& operator<<(std::ostream& out, const MakeBagOp& op);
+
+/**
+ * Hash function for the MakeBagOpHashFunction objects.
+ */
+struct CVC4_PUBLIC MakeBagOpHashFunction
+{
+ size_t operator()(const MakeBagOp& op) const;
+}; /* struct MakeBagOpHashFunction */
+
+} // namespace CVC4
+
+#endif /* CVC4__MAKE_BAG_OP_H */
diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp
index 7975bb379..727407937 100644
--- a/src/theory/bags/theory_bags_type_enumerator.cpp
+++ b/src/theory/bags/theory_bags_type_enumerator.cpp
@@ -54,7 +54,8 @@ BagEnumerator& BagEnumerator::operator++()
{
// increase the multiplicity by one
Node one = d_nodeManager->mkConst(Rational(1));
- Node singleton = d_nodeManager->mkNode(kind::MK_BAG, d_element, one);
+ TypeNode elementType = d_elementTypeEnumerator.getType();
+ Node singleton = d_nodeManager->mkBag(elementType, d_element, one);
if (d_currentBag.getKind() == kind::EMPTYBAG)
{
d_currentBag = singleton;
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index 67293e222..75f57ec88 100644
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -42,19 +42,11 @@ struct BinaryOperatorTypeRule
TypeNode secondBagType = n[1].getType(check);
if (secondBagType != bagType)
{
- if (n.getKind() == kind::INTERSECTION_MIN)
- {
- bagType = TypeNode::mostCommonTypeNode(secondBagType, bagType);
- }
- else
- {
- bagType = TypeNode::leastCommonTypeNode(secondBagType, bagType);
- }
- if (bagType.isNull())
- {
- throw TypeCheckingExceptionPrivate(
- n, "operator expects two bags of comparable types");
- }
+ std::stringstream ss;
+ ss << "Operator " << n.getKind()
+ << " expects two bags of the same type. Found types '" << bagType
+ << "' and '" << secondBagType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
}
}
return bagType;
@@ -110,15 +102,9 @@ struct CountTypeRule
n, "checking for membership in a non-bag");
}
TypeNode elementType = n[0].getType(check);
- // TODO(projects#226): comments from sets
- //
- // T : (Bag Int)
- // B : (Bag Real)
- // (= (as T (Bag Real)) B)
- // (= (bag-count 0.5 B) 1)
- // ...where (bag-count 0.5 T) is inferred
-
- if (!elementType.isComparableTo(bagType.getBagElementType()))
+ // e.g. (count 1 (mkBag (mkBag_op Real) 1.0 3))) is 3 whereas
+ // (count 1.0 (mkBag (mkBag_op Int) 1 3))) throws a typing error
+ if (!elementType.isSubtypeOf(bagType.getBagElementType()))
{
std::stringstream ss;
ss << "member operating on bags of different types:\n"
@@ -136,7 +122,10 @@ struct MkBagTypeRule
{
static TypeNode computeType(NodeManager* nm, TNode n, bool check)
{
- Assert(n.getKind() == kind::MK_BAG);
+ Assert(n.getKind() == kind::MK_BAG && n.hasOperator()
+ && n.getOperator().getKind() == kind::MK_BAG_OP);
+ MakeBagOp op = n.getOperator().getConst<MakeBagOp>();
+ TypeNode expectedElementType = op.getType();
if (check)
{
if (n.getNumChildren() != 2)
@@ -153,9 +142,21 @@ struct MkBagTypeRule
ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1;
throw TypeCheckingExceptionPrivate(n, ss.str());
}
+
+ TypeNode actualElementType = n[0].getType(check);
+ // the type of the element should be a subtype of the type of the operator
+ // e.g. (mkBag (mkBag_op Real) 1 1) where 1 is an Int
+ if (!actualElementType.isSubtypeOf(expectedElementType))
+ {
+ std::stringstream ss;
+ ss << "The type '" << actualElementType
+ << "' of the element is not a subtype of '" << expectedElementType
+ << "' in term : " << n;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
}
- return nm->mkBagType(n[0].getType(check));
+ return nm->mkBagType(expectedElementType);
}
static bool computeIsConst(NodeManager* nodeManager, TNode n)
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index e541a24fb..481c80f26 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -14,8 +14,8 @@ cvc4_add_unit_test_white(evaluator_white theory)
cvc4_add_unit_test_white(logic_info_white theory)
cvc4_add_unit_test_white(sequences_rewriter_white theory)
cvc4_add_unit_test_white(theory_arith_white theory)
-cvc4_add_unit_test_white(theory_bags_rewriter_black theory)
-cvc4_add_unit_test_white(theory_bags_type_rules_black theory)
+cvc4_add_unit_test_white(theory_bags_rewriter_white theory)
+cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
cvc4_add_unit_test_white(theory_bv_white theory)
cvc4_add_unit_test_white(theory_engine_white theory)
diff --git a/test/unit/theory/theory_bags_rewriter_black.h b/test/unit/theory/theory_bags_rewriter_white.h
index 98f56fd44..b1c75fdbd 100644
--- a/test/unit/theory/theory_bags_rewriter_black.h
+++ b/test/unit/theory/theory_bags_rewriter_white.h
@@ -1,5 +1,5 @@
/********************* */
-/*! \file theory_bags_rewriter_black.h
+/*! \file theory_bags_rewriter_white.h
** \verbatim
** Top contributors (to current version):
** Mudathir Mohamed
@@ -9,7 +9,7 @@
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Black box testing of bags rewriter
+ ** \brief White box testing of bags rewriter
**/
#include <cxxtest/TestSuite.h>
@@ -28,7 +28,7 @@ using namespace std;
typedef expr::Attribute<Node, Node> attribute;
-class BagsTypeRuleBlack : public CxxTest::TestSuite
+class BagsTypeRuleWhite : public CxxTest::TestSuite
{
public:
void setUp() override
@@ -74,8 +74,8 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
Node y = elements[1];
Node c = d_nm->mkSkolem("c", d_nm->integerType());
Node d = d_nm->mkSkolem("d", d_nm->integerType());
- Node bagX = d_nm->mkNode(MK_BAG, x, c);
- Node bagY = d_nm->mkNode(MK_BAG, y, d);
+ Node bagX = d_nm->mkBag(d_nm->stringType(), x, c);
+ Node bagY = d_nm->mkBag(d_nm->stringType(), y, d);
Node emptyBag =
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
@@ -89,11 +89,12 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
void testMkBagConstantElement()
{
vector<Node> elements = getNStrings(1);
- Node negative =
- d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(-1)));
- Node zero = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(0)));
- Node positive =
- d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(1)));
+ Node negative = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(-1)));
+ Node zero = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(0)));
+ Node positive = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(1)));
Node emptybag =
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
@@ -114,10 +115,14 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
void testMkBagVariableElement()
{
Node skolem = d_nm->mkSkolem("x", d_nm->stringType());
- Node variable = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(-1)));
- Node negative = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(-1)));
- Node zero = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(0)));
- Node positive = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(1)));
+ Node variable =
+ d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(-1)));
+ Node negative =
+ d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(-1)));
+ Node zero =
+ d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(0)));
+ Node positive =
+ d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(1)));
Node emptybag =
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
@@ -140,7 +145,8 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
int n = 3;
Node skolem = d_nm->mkSkolem("x", d_nm->stringType());
Node emptyBag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(skolem.getType())));
- Node bag = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(n)));
+ Node bag =
+ d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(n)));
// (bag.count x emptybag) = 0
Node n1 = d_nm->mkNode(BAG_COUNT, skolem, emptyBag);
@@ -161,8 +167,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
vector<Node> elements = getNStrings(2);
Node emptyBag =
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
- Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n)));
- Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1)));
+ Node A = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n)));
+ Node B = d_nm->mkBag(
+ d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1)));
Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B);
Node unionMaxBA = d_nm->mkNode(UNION_MAX, B, A);
Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B);
@@ -241,8 +249,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
vector<Node> elements = getNStrings(2);
Node emptyBag =
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
- Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n)));
- Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1)));
+ Node A = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n)));
+ Node B = d_nm->mkBag(
+ d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1)));
Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B);
Node unionDisjointBA = d_nm->mkNode(UNION_DISJOINT, B, A);
Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B);
@@ -285,8 +295,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
vector<Node> elements = getNStrings(2);
Node emptyBag =
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
- Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n)));
- Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1)));
+ Node A = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n)));
+ Node B = d_nm->mkBag(
+ d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1)));
Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B);
Node unionMaxBA = d_nm->mkNode(UNION_MAX, B, A);
Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B);
@@ -365,8 +377,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
vector<Node> elements = getNStrings(2);
Node emptyBag =
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
- Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n)));
- Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1)));
+ Node A = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n)));
+ Node B = d_nm->mkBag(
+ d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1)));
Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B);
Node unionMaxBA = d_nm->mkNode(UNION_MAX, B, A);
Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B);
@@ -447,8 +461,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
vector<Node> elements = getNStrings(2);
Node emptyBag =
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
- Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n)));
- Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1)));
+ Node A = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n)));
+ Node B = d_nm->mkBag(
+ d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1)));
Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B);
Node unionMaxBA = d_nm->mkNode(UNION_MAX, B, A);
Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B);
@@ -515,7 +531,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
{
Node x = d_nm->mkSkolem("x", d_nm->stringType());
Node c = d_nm->mkConst(Rational(3));
- Node bag = d_nm->mkNode(MK_BAG, x, c);
+ Node bag = d_nm->mkBag(d_nm->stringType(), x, c);
// (bag.choose (mkBag x c)) = x where c is a constant > 0
Node n1 = d_nm->mkNode(BAG_CHOOSE, bag);
@@ -531,10 +547,12 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
Node zero = d_nm->mkConst(Rational(0));
Node c = d_nm->mkConst(Rational(3));
- Node bag = d_nm->mkNode(MK_BAG, x, c);
+ Node bag = d_nm->mkBag(d_nm->stringType(), x, c);
vector<Node> elements = getNStrings(2);
- Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(4)));
- Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(5)));
+ Node A = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(4)));
+ Node B = d_nm->mkBag(
+ d_nm->stringType(), elements[1], d_nm->mkConst(Rational(5)));
Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B);
// TODO(projects#223): enable this test after implementing bags normal form
@@ -566,7 +584,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
Node x = d_nm->mkSkolem("x", d_nm->stringType());
Node c = d_nm->mkSkolem("c", d_nm->integerType());
- Node bag = d_nm->mkNode(MK_BAG, x, c);
+ Node bag = d_nm->mkBag(d_nm->stringType(), x, c);
// TODO(projects#223): complete this function
// (bag.is_singleton emptybag) = false
@@ -593,7 +611,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
Node n = d_nm->mkNode(BAG_FROM_SET, singleton);
RewriteResponse response = d_rewriter->postRewrite(n);
Node one = d_nm->mkConst(Rational(1));
- Node bag = d_nm->mkNode(MK_BAG, x, one);
+ Node bag = d_nm->mkBag(d_nm->stringType(), x, one);
TS_ASSERT(response.d_node == bag
&& response.d_status == REWRITE_AGAIN_FULL);
}
@@ -601,7 +619,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
void testToSet()
{
Node x = d_nm->mkSkolem("x", d_nm->stringType());
- Node bag = d_nm->mkNode(MK_BAG, x, d_nm->mkConst(Rational(5)));
+ Node bag = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(5)));
// (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x)
Node n = d_nm->mkNode(BAG_TO_SET, bag);
diff --git a/test/unit/theory/theory_bags_type_rules_black.h b/test/unit/theory/theory_bags_type_rules_white.h
index d6c225bad..dfe2d4cac 100644
--- a/test/unit/theory/theory_bags_type_rules_black.h
+++ b/test/unit/theory/theory_bags_type_rules_white.h
@@ -28,7 +28,7 @@ using namespace std;
typedef expr::Attribute<Node, Node> attribute;
-class BagsTypeRuleBlack : public CxxTest::TestSuite
+class BagsTypeRuleWhite : public CxxTest::TestSuite
{
public:
void setUp() override
@@ -63,7 +63,8 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
void testCountOperator()
{
vector<Node> elements = getNStrings(1);
- Node bag = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(100)));
+ Node bag = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(100)));
Node count = d_nm->mkNode(BAG_COUNT, elements[0], bag);
Node node = d_nm->mkConst(Rational(10));
@@ -76,11 +77,12 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
void testMkBagOperator()
{
vector<Node> elements = getNStrings(1);
- Node negative =
- d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(-1)));
- Node zero = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(0)));
- Node positive =
- d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(1)));
+ Node negative = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(-1)));
+ Node zero = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(0)));
+ Node positive = d_nm->mkBag(
+ d_nm->stringType(), elements[0], d_nm->mkConst(Rational(1)));
// only positive multiplicity are constants
TS_ASSERT(!MkBagTypeRule::computeIsConst(d_nm.get(), negative));
@@ -99,7 +101,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite
void testToSetOperator()
{
vector<Node> elements = getNStrings(1);
- Node bag = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(10)));
+ Node bag = d_nm->mkBag(d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10)));
TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(BAG_TO_SET, bag));
TS_ASSERT(d_nm->mkNode(BAG_TO_SET, bag).getType().isSet());
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback