summaryrefslogtreecommitdiff
path: root/src/theory/sets
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sets')
-rw-r--r--src/theory/sets/cardinality_extension.cpp4
-rw-r--r--src/theory/sets/kinds27
-rw-r--r--src/theory/sets/normal_form.h6
-rw-r--r--src/theory/sets/singleton_op.cpp50
-rw-r--r--src/theory/sets/singleton_op.h63
-rw-r--r--src/theory/sets/theory_sets_private.cpp5
-rw-r--r--src/theory/sets/theory_sets_rels.cpp27
-rw-r--r--src/theory/sets/theory_sets_rels.h2
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp14
-rw-r--r--src/theory/sets/theory_sets_type_enumerator.cpp3
-rw-r--r--src/theory/sets/theory_sets_type_rules.h57
11 files changed, 202 insertions, 56 deletions
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 07672605d..21344ee73 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -1028,7 +1028,7 @@ void CardinalityExtension::mkModelValueElementsFor(
// the current members of this finite type.
Node slack = nm->mkSkolem("slack", elementType);
- Node singleton = nm->mkNode(SINGLETON, slack);
+ Node singleton = nm->mkSingleton(elementType, slack);
els.push_back(singleton);
d_finite_type_slack_elements[elementType].push_back(slack);
Trace("sets-model") << "Added slack element " << slack << " to set "
@@ -1037,7 +1037,7 @@ void CardinalityExtension::mkModelValueElementsFor(
else
{
els.push_back(
- nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType)));
+ nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType)));
}
}
}
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index fd941ab29..57120e42e 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -35,15 +35,23 @@ enumerator SET_TYPE \
"theory/sets/theory_sets_type_enumerator.h"
# operators
-operator UNION 2 "set union"
-operator INTERSECTION 2 "set intersection"
-operator SETMINUS 2 "set subtraction"
-operator SUBSET 2 "subset predicate; first parameter a subset of second"
-operator MEMBER 2 "set membership predicate; first parameter a member of second"
-operator SINGLETON 1 "the set of the single element given as a parameter"
-operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
-operator CARD 1 "set cardinality operator"
-operator COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)"
+operator UNION 2 "set union"
+operator INTERSECTION 2 "set intersection"
+operator SETMINUS 2 "set subtraction"
+operator SUBSET 2 "subset predicate; first parameter a subset of second"
+operator MEMBER 2 "set membership predicate; first parameter a member of second"
+
+constant SINGLETON_OP \
+ ::CVC4::SingletonOp \
+ ::CVC4::SingletonOpHashFunction \
+ "theory/sets/singleton_op.h" \
+ "operator for singletons; payload is an instance of the CVC4::SingletonOp class"
+parameterized SINGLETON SINGLETON_OP 1 \
+"constructs a set of a single element. First parameter is a SingletonOp. Second is a term"
+
+operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
+operator CARD 1 "set cardinality operator"
+operator COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)"
nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it."
# A set comprehension is specified by:
@@ -82,6 +90,7 @@ typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SUBSET ::CVC4::theory::sets::SubsetTypeRule
typerule MEMBER ::CVC4::theory::sets::MemberTypeRule
+typerule SINGLETON_OP "SimpleTypeRule<RBuiltinOperator>"
typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
typerule INSERT ::CVC4::theory::sets::InsertTypeRule
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 8989fbc15..2654344f3 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -44,11 +44,13 @@ class NormalForm {
}
else
{
+ TypeNode elementType = setType.getSetElementType();
ElementsIterator it = elements.begin();
- Node cur = nm->mkNode(kind::SINGLETON, *it);
+ Node cur = nm->mkSingleton(elementType, *it);
while (++it != elements.end())
{
- cur = nm->mkNode(kind::UNION, nm->mkNode(kind::SINGLETON, *it), cur);
+ Node singleton = nm->mkSingleton(elementType, *it);
+ cur = nm->mkNode(kind::UNION, singleton, cur);
}
return cur;
}
diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp
new file mode 100644
index 000000000..d7f318314
--- /dev/null
+++ b/src/theory/sets/singleton_op.cpp
@@ -0,0 +1,50 @@
+/********************* */
+/*! \file singleton_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 singleton operator for sets
+ **/
+
+#include "singleton_op.h"
+
+#include <iostream>
+
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const SingletonOp& op)
+{
+ return out << "(singleton_op " << op.getType() << ')';
+}
+
+size_t SingletonOpHashFunction::operator()(const SingletonOp& op) const
+{
+ return TypeNodeHashFunction()(op.getType());
+}
+
+SingletonOp::SingletonOp(const TypeNode& elementType)
+ : d_type(new TypeNode(elementType))
+{
+}
+
+SingletonOp::SingletonOp(const SingletonOp& op)
+ : d_type(new TypeNode(op.getType()))
+{
+}
+
+const TypeNode& SingletonOp::getType() const { return *d_type; }
+
+bool SingletonOp::operator==(const SingletonOp& op) const
+{
+ return getType() == op.getType();
+}
+
+} // namespace CVC4
diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h
new file mode 100644
index 000000000..57118999a
--- /dev/null
+++ b/src/theory/sets/singleton_op.h
@@ -0,0 +1,63 @@
+/********************* */
+/*! \file singleton_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 singleton operator for sets
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__SINGLETON_OP_H
+#define CVC4__SINGLETON_OP_H
+
+#include <memory>
+
+namespace CVC4 {
+
+class TypeNode;
+
+/**
+ * The class is an operator for kind SINGLETON used to construct singleton sets.
+ * It specifies the type of the single element especially when it is a constant.
+ * e.g. the type of rational 1 is Int, however
+ * (singleton (singleton_op Real) 1) is of type (Set Real), not (Set Int).
+ * Note that the type passed to the constructor is the element's type, not the
+ * set type.
+ */
+class SingletonOp
+{
+ public:
+ SingletonOp(const TypeNode& elementType);
+ SingletonOp(const SingletonOp& op);
+
+ /** return the type of the current object */
+ const TypeNode& getType() const;
+
+ bool operator==(const SingletonOp& op) const;
+
+ private:
+ SingletonOp();
+ /** a pointer to the type of the singleton element */
+ std::unique_ptr<TypeNode> d_type;
+}; /* class Singleton */
+
+std::ostream& operator<<(std::ostream& out, const SingletonOp& op);
+
+/**
+ * Hash function for the SingletonHashFunction objects.
+ */
+struct CVC4_PUBLIC SingletonOpHashFunction
+{
+ size_t operator()(const SingletonOp& op) const;
+}; /* struct SingletonOpHashFunction */
+
+} // namespace CVC4
+
+#endif /* CVC4__SINGLETON_OP_H */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 51f49ad1d..18df43e9f 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1143,9 +1143,10 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
const std::map<Node, Node>& emems = d_state.getMembers(eqc);
if (!emems.empty())
{
+ TypeNode elementType = eqc.getType().getSetElementType();
for (const std::pair<const Node, Node>& itmm : emems)
{
- Node t = nm->mkNode(kind::SINGLETON, itmm.first);
+ Node t = nm->mkSingleton(elementType, itmm.first);
els.push_back(t);
}
}
@@ -1357,7 +1358,7 @@ TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)
TypeNode setType = set.getType();
Node boundVar = nm->mkBoundVar(setType.getSetElementType());
- Node singleton = nm->mkNode(kind::SINGLETON, boundVar);
+ Node singleton = nm->mkSingleton(setType.getSetElementType(), boundVar);
Node equal = set.eqNode(singleton);
std::vector<Node> variables = {boundVar};
Node boundVars = nm->mkNode(BOUND_VAR_LIST, variables);
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index ebbc24d12..617b458c9 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -247,12 +247,13 @@ void TheorySetsRels::check(Theory::Effort level)
}
else if (erType.isTuple() && !eqc_node.isConst() && !eqc_node.isVar())
{
+ std::vector<TypeNode> tupleTypes = erType.getTupleTypes();
for (unsigned i = 0, tlen = erType.getTupleLength(); i < tlen; i++)
{
- Node element = RelsUtils::nthElementOfTuple( eqc_node, i );
-
- if( !element.isConst() ) {
- makeSharedTerm( element );
+ Node element = RelsUtils::nthElementOfTuple(eqc_node, i);
+ if (!element.isConst())
+ {
+ makeSharedTerm(element, tupleTypes[i]);
}
}
}
@@ -863,7 +864,7 @@ void TheorySetsRels::check(Theory::Effort level)
sendInfer(fact, reason, "JOIN-Split-1");
fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]);
sendInfer(fact, reason, "JOIN-Split-2");
- makeSharedTerm( shared_x );
+ makeSharedTerm(shared_x, shared_type);
}
/*
@@ -1153,8 +1154,9 @@ void TheorySetsRels::check(Theory::Effort level)
}
return equal;
} else if(!a.getType().isBoolean()){
- makeSharedTerm(a);
- makeSharedTerm(b);
+ // TODO(project##230): Find a safe type for the singleton operator
+ makeSharedTerm(a, a.getType());
+ makeSharedTerm(b, b.getType());
}
return false;
}
@@ -1183,14 +1185,15 @@ void TheorySetsRels::check(Theory::Effort level)
return false;
}
- void TheorySetsRels::makeSharedTerm( Node n ) {
+ void TheorySetsRels::makeSharedTerm(Node n, TypeNode t)
+ {
if (d_shared_terms.find(n) != d_shared_terms.end())
{
return;
}
Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl;
// force a proxy lemma to be sent for the singleton containing n
- Node ss = NodeManager::currentNM()->mkNode(SINGLETON, n);
+ Node ss = NodeManager::currentNM()->mkSingleton(t, n);
d_treg.getProxy(ss);
d_shared_terms.insert(n);
}
@@ -1216,9 +1219,11 @@ void TheorySetsRels::check(Theory::Effort level)
Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl;
std::vector<Node> tuple_elements;
tuple_elements.push_back((n[0].getType().getDType())[0].getConstructor());
- for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) {
+ std::vector<TypeNode> tupleTypes = n[0].getType().getTupleTypes();
+ for (unsigned int i = 0; i < n[0].getType().getTupleLength(); i++)
+ {
Node element = RelsUtils::nthElementOfTuple(n[0], i);
- makeSharedTerm(element);
+ makeSharedTerm(element, tupleTypes[i]);
tuple_elements.push_back(element);
}
Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 9b8fd0cb7..95a13f4d5 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -176,7 +176,7 @@ private:
/** Helper functions */
bool hasTerm( Node a );
- void makeSharedTerm( Node );
+ void makeSharedTerm(Node, TypeNode t);
void reduceTupleVar( Node );
bool hasMember( Node, Node );
void computeTupleReps( Node );
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index d821a0059..847bf34eb 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -161,7 +161,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
std::inserter(newSet, newSet.begin()));
Node newNode = NormalForm::elementsToSet(newSet, node.getType());
- Assert(newNode.isConst());
+ Assert(newNode.isConst() && newNode.getType() == node.getType());
Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
return RewriteResponse(REWRITE_DONE, newNode);
}
@@ -488,12 +488,14 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
}
else if (k == kind::INSERT)
{
- Node insertedElements = nm->mkNode(kind::SINGLETON, node[0]);
size_t setNodeIndex = node.getNumChildren()-1;
- for(size_t i = 1; i < setNodeIndex; ++i) {
- insertedElements = nm->mkNode(kind::UNION,
- insertedElements,
- nm->mkNode(kind::SINGLETON, node[i]));
+ TypeNode elementType = node[setNodeIndex].getType().getSetElementType();
+ Node insertedElements = nm->mkSingleton(elementType, node[0]);
+
+ for (size_t i = 1; i < setNodeIndex; ++i)
+ {
+ Node singleton = nm->mkSingleton(elementType, node[i]);
+ insertedElements = nm->mkNode(kind::UNION, insertedElements, singleton);
}
return RewriteResponse(REWRITE_AGAIN,
nm->mkNode(kind::UNION,
diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp
index 321b9ffcd..1d932b590 100644
--- a/src/theory/sets/theory_sets_type_enumerator.cpp
+++ b/src/theory/sets/theory_sets_type_enumerator.cpp
@@ -89,7 +89,8 @@ SetEnumerator& SetEnumerator::operator++()
// get a new element and return it as a singleton set
Node element = *d_elementEnumerator;
d_elementsSoFar.push_back(element);
- d_currentSet = d_nodeManager->mkNode(kind::SINGLETON, element);
+ TypeNode elementType = d_elementEnumerator.getType();
+ d_currentSet = d_nodeManager->mkSingleton(elementType, element);
d_elementEnumerator++;
}
else
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 3e2834aaf..20e5e57e2 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -31,9 +31,8 @@ struct SetsBinaryOperatorTypeRule
TNode n,
bool check)
{
- Assert(n.getKind() == kind::UNION ||
- n.getKind() == kind::INTERSECTION ||
- n.getKind() == kind::SETMINUS);
+ Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION
+ || n.getKind() == kind::SETMINUS);
TypeNode setType = n[0].getType(check);
if (check)
{
@@ -45,19 +44,11 @@ struct SetsBinaryOperatorTypeRule
TypeNode secondSetType = n[1].getType(check);
if (secondSetType != setType)
{
- if (n.getKind() == kind::INTERSECTION)
- {
- setType = TypeNode::mostCommonTypeNode(secondSetType, setType);
- }
- else
- {
- setType = TypeNode::leastCommonTypeNode(secondSetType, setType);
- }
- if (setType.isNull())
- {
- throw TypeCheckingExceptionPrivate(
- n, "operator expects two sets of comparable types");
- }
+ std::stringstream ss;
+ ss << "Operator " << n.getKind()
+ << " expects two sets of the same type. Found types '" << setType
+ << "' and '" << secondSetType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
}
}
return setType;
@@ -132,18 +123,40 @@ struct MemberTypeRule {
}
};/* struct MemberTypeRule */
-struct SingletonTypeRule {
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+struct SingletonTypeRule
+{
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
{
- Assert(n.getKind() == kind::SINGLETON);
- return nodeManager->mkSetType(n[0].getType(check));
+ Assert(n.getKind() == kind::SINGLETON && n.hasOperator()
+ && n.getOperator().getKind() == kind::SINGLETON_OP);
+
+ SingletonOp op = n.getOperator().getConst<SingletonOp>();
+ TypeNode type1 = op.getType();
+ if (check)
+ {
+ TypeNode type2 = n[0].getType(check);
+ TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2);
+ // the type of the element should be a subtype of the type of the operator
+ // e.g. (singleton (singleton_op Real) 1) where 1 is an Int
+ if (leastCommonType.isNull() || leastCommonType != type1)
+ {
+ std::stringstream ss;
+ ss << "The type '" << type2 << "' of the element is not a subtype of '"
+ << type1 << "' in term : " << n;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ return nodeManager->mkSetType(type1);
}
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
+ {
Assert(n.getKind() == kind::SINGLETON);
return n[0].isConst();
}
-};/* struct SingletonTypeRule */
+}; /* struct SingletonTypeRule */
struct EmptySetTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback