summaryrefslogtreecommitdiff
path: root/src/theory/sets
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sets')
-rw-r--r--src/theory/sets/expr_patterns.h6
-rw-r--r--src/theory/sets/kinds17
-rw-r--r--src/theory/sets/options4
-rw-r--r--src/theory/sets/options_handlers.h17
-rw-r--r--src/theory/sets/scrutinize.h2
-rw-r--r--src/theory/sets/term_info.h2
-rw-r--r--src/theory/sets/theory_sets.cpp20
-rw-r--r--src/theory/sets/theory_sets.h8
-rw-r--r--src/theory/sets/theory_sets_private.cpp73
-rw-r--r--src/theory/sets/theory_sets_private.h6
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp23
-rw-r--r--src/theory/sets/theory_sets_rewriter.h2
-rw-r--r--src/theory/sets/theory_sets_type_enumerator.h19
-rw-r--r--src/theory/sets/theory_sets_type_rules.h46
14 files changed, 181 insertions, 64 deletions
diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h
index bc5b6b9e0..86f12082a 100644
--- a/src/theory/sets/expr_patterns.h
+++ b/src/theory/sets/expr_patterns.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -44,8 +44,8 @@ static Node MEMBER(TNode a, TNode b) {
return NodeManager::currentNM()->mkNode(kind::MEMBER, a, b);
}
-static Node SET_SINGLETON(TNode a) {
- return NodeManager::currentNM()->mkNode(kind::SET_SINGLETON, a);
+static Node SINGLETON(TNode a) {
+ return NodeManager::currentNM()->mkNode(kind::SINGLETON, a);
}
static Node EQUAL(TNode a, TNode b) {
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 12f114fc0..39e7883c6 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -19,10 +19,10 @@ constant EMPTYSET \
::CVC4::EmptySet \
::CVC4::EmptySetHashFunction \
"util/emptyset.h" \
- "empty set"
+ "the empty set constant; payload is an instance of the CVC4::EmptySet class"
# the type
-operator SET_TYPE 1 "set type"
+operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
cardinality SET_TYPE \
"::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
"theory/sets/theory_sets_type_rules.h"
@@ -38,21 +38,24 @@ enumerator SET_TYPE \
operator UNION 2 "set union"
operator INTERSECTION 2 "set intersection"
operator SETMINUS 2 "set subtraction"
-operator SUBSET 2 "subset"
-operator MEMBER 2 "set membership"
-operator SET_SINGLETON 1 "singleton set"
+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)"
typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
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 SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
+typerule INSERT ::CVC4::theory::sets::InsertTypeRule
construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
-construle SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule
+construle INSERT ::CVC4::theory::sets::InsertTypeRule
endtheory
diff --git a/src/theory/sets/options b/src/theory/sets/options
index dc6c6e907..1c95e78e4 100644
--- a/src/theory/sets/options
+++ b/src/theory/sets/options
@@ -8,7 +8,7 @@ module SETS "theory/sets/options.h" Sets
option setsPropagate --sets-propagate bool :default true
determines whether to propagate learnt facts to Theory Engine / SAT solver
-option setsEagerLemmas --sets-eager-lemmas bool :default false
- if true, will add lemmas even if not at FULL_EFFORT
+option setsEagerLemmas --sets-eager-lemmas bool :default true
+ add lemmas even at regular effort
endmodule
diff --git a/src/theory/sets/options_handlers.h b/src/theory/sets/options_handlers.h
index ff535945e..f0af6e7a3 100644
--- a/src/theory/sets/options_handlers.h
+++ b/src/theory/sets/options_handlers.h
@@ -1,3 +1,20 @@
+/********************* */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h
index 7343662c6..a4f3f6a6d 100644
--- a/src/theory/sets/scrutinize.h
+++ b/src/theory/sets/scrutinize.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/theory/sets/term_info.h b/src/theory/sets/term_info.h
index 2783faa79..3168817e2 100644
--- a/src/theory/sets/term_info.h
+++ b/src/theory/sets/term_info.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index c230b9ac5..b59beac8d 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -34,10 +34,6 @@ TheorySets::~TheorySets() {
delete d_internal;
}
-void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_internal->setMasterEqualityEngine(eq);
-}
-
void TheorySets::addSharedTerm(TNode n) {
d_internal->addSharedTerm(n);
}
@@ -50,8 +46,8 @@ void TheorySets::collectModelInfo(TheoryModel* m, bool fullModel) {
d_internal->collectModelInfo(m, fullModel);
}
-void TheorySets::propagate(Effort e) {
- d_internal->propagate(e);
+void TheorySets::computeCareGraph() {
+ d_internal->computeCareGraph();
}
Node TheorySets::explain(TNode node) {
@@ -59,7 +55,15 @@ Node TheorySets::explain(TNode node) {
}
void TheorySets::preRegisterTerm(TNode node) {
- return d_internal->preRegisterTerm(node);
+ d_internal->preRegisterTerm(node);
+}
+
+void TheorySets::propagate(Effort e) {
+ d_internal->propagate(e);
+}
+
+void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_internal->setMasterEqualityEngine(eq);
}
}/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 6ff41d5f5..a16832389 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -48,14 +48,14 @@ public:
~TheorySets();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
void addSharedTerm(TNode);
void check(Effort);
void collectModelInfo(TheoryModel*, bool fullModel);
+ void computeCareGraph();
+
Node explain(TNode);
std::string identify() const { return "THEORY_SETS"; }
@@ -64,6 +64,8 @@ public:
void propagate(Effort);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
};/* class TheorySets */
}/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f768bd62d..592b4bc37 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Kshitij Bansal
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -97,7 +97,7 @@ void TheorySetsPrivate::check(Theory::Effort level) {
Debug("sets") << "[sets] is complete = " << isComplete() << std::endl;
}
- if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
+ if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
d_external.d_out->lemma(getLemma());
return;
}
@@ -225,7 +225,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
if(S.getKind() == kind::UNION ||
S.getKind() == kind::INTERSECTION ||
S.getKind() == kind::SETMINUS ||
- S.getKind() == kind::SET_SINGLETON) {
+ S.getKind() == kind::SINGLETON) {
doSettermPropagation(x, S);
if(d_conflict) return;
}// propagation: children
@@ -276,7 +276,7 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
left_literal = MEMBER(x, S[0]) ;
right_literal = NOT( MEMBER(x, S[1]) );
break;
- case kind::SET_SINGLETON: {
+ case kind::SINGLETON: {
Node atom = MEMBER(x, S);
if(holds(atom, true)) {
learnLiteral(EQUAL(x, S[0]), true, atom);
@@ -408,6 +408,42 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
}/*TheorySetsPrivate::learnLiteral(...)*/
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+
+void TheorySetsPrivate::addSharedTerm(TNode n) {
+ Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+ d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
+}
+
+
+void TheorySetsPrivate::computeCareGraph() {
+ Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
+ for (unsigned i = 0; i < d_external.d_sharedTerms.size(); ++ i) {
+ TNode a = d_external.d_sharedTerms[i];
+ TypeNode aType = a.getType();
+ for (unsigned j = i + 1; j < d_external.d_sharedTerms.size(); ++ j) {
+ TNode b = d_external.d_sharedTerms[j];
+ if (b.getType() != aType) {
+ // We don't care about the terms of different types
+ continue;
+ }
+ switch (d_external.d_valuation.getEqualityStatus(a, b)) {
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ case EQUALITY_FALSE_AND_PROPAGATED:
+ // If we know about it, we should have propagated it, so we can skip
+ break;
+ default:
+ // Let's split on it
+ d_external.addCarePair(a, b);
+ break;
+ }
+ }
+ }
+}
+
+
/******************** Model generation ********************/
/******************** Model generation ********************/
/******************** Model generation ********************/
@@ -535,9 +571,9 @@ Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) con
return nm->mkConst(EmptySet(nm->toType(setType)));
} else {
Elements::iterator it = elements.begin();
- Node cur = SET_SINGLETON(*it);
+ Node cur = SINGLETON(*it);
while( ++it != elements.end() ) {
- cur = nm->mkNode(kind::UNION, cur, SET_SINGLETON(*it));
+ cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
}
return cur;
}
@@ -778,15 +814,19 @@ void TheorySetsPrivate::addToPending(Node n) {
Assert(n.getKind() == kind::EQUAL);
d_pendingDisequal.push(n);
}
+ d_external.d_out->lemma(getLemma());
+ Assert(isComplete());
}
}
bool TheorySetsPrivate::isComplete() {
- while(!d_pending.empty() && present(d_pending.front())) {
- Debug("sets-pending") << "[sets-pending] removing as already present: "
- << d_pending.front() << std::endl;
- d_pending.pop();
- }
+ // while(!d_pending.empty() &&
+ // (d_pendingEverInserted.find(d_pending.front()) != d_pendingEverInserted.end()
+ // || present(d_pending.front()) ) ) {
+ // Debug("sets-pending") << "[sets-pending] removing as already present: "
+ // << d_pending.front() << std::endl;
+ // d_pending.pop();
+ // }
return d_pending.empty() && d_pendingDisequal.empty();
}
@@ -886,11 +926,6 @@ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
-void TheorySetsPrivate::addSharedTerm(TNode n) {
- Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
- d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
-}
-
void TheorySetsPrivate::conflict(TNode a, TNode b)
{
if (a.getKind() == kind::CONST_BOOLEAN) {
@@ -948,7 +983,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
// d_equalityEngine.addTerm(node);
}
- if(node.getKind() == kind::SET_SINGLETON) {
+ if(node.getKind() == kind::SINGLETON) {
Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
learnLiteral(MEMBER(node[0], node), true, true_node);
//intentional fallthrough
@@ -1125,7 +1160,7 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
if(S.getKind() == kind::UNION ||
S.getKind() == kind::INTERSECTION ||
S.getKind() == kind::SETMINUS ||
- S.getKind() == kind::SET_SINGLETON) {
+ S.getKind() == kind::SINGLETON) {
d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
}// propagation: children
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 90dec7c0b..78a415529 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Kshitij Bansal
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -56,6 +56,8 @@ public:
void collectModelInfo(TheoryModel*, bool fullModel);
+ void computeCareGraph();
+
Node explain(TNode);
void preRegisterTerm(TNode node);
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 7b02c1bfb..01ad51733 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -32,11 +32,11 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
return false;
}
- if(setTerm.getKind() == kind::SET_SINGLETON) {
+ if(setTerm.getKind() == kind::SINGLETON) {
return elementTerm == setTerm[0];
}
- Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SET_SINGLETON,
+ Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SINGLETON,
"kind was %d, term: %s", setTerm.getKind(), setTerm.toString().c_str());
return elementTerm == setTerm[1][0] || checkConstantMembership(elementTerm, setTerm[0]);
@@ -44,7 +44,7 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
// switch(setTerm.getKind()) {
// case kind::EMPTYSET:
// return false;
- // case kind::SET_SINGLETON:
+ // case kind::SINGLETON:
// return elementTerm == setTerm[0];
// case kind::UNION:
// return checkConstantMembership(elementTerm, setTerm[0]) ||
@@ -195,7 +195,7 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette
case kind::EMPTYSET:
/* assign emptyset, which is default */
break;
- case kind::SET_SINGLETON:
+ case kind::SINGLETON:
Assert(setterm[0].isConst());
cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node);
break;
@@ -220,10 +220,10 @@ Node elementsToNormalConstant(Elements elements,
} else {
Elements::iterator it = elements.begin();
- Node cur = nm->mkNode(kind::SET_SINGLETON, *it);
+ Node cur = nm->mkNode(kind::SINGLETON, *it);
while( ++it != elements.end() ) {
cur = nm->mkNode(kind::UNION, cur,
- nm->mkNode(kind::SET_SINGLETON, *it));
+ nm->mkNode(kind::SINGLETON, *it));
}
return cur;
}
@@ -239,6 +239,15 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
// Further optimization, if constants but differing ones
+ if(node.getKind() == 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]));
+ }
+ return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::UNION, insertedElements, node[setNodeIndex]));
+ }//kind::INSERT
+
if(node.getType().isSet() && node.isConst()) {
//rewrite set to normal form
SettermElementsMap setTermElementsMap; // cache
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index 6ce418e85..58ee8bfb0 100644
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index 2f4cc6a2f..5d14006bb 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -1,3 +1,20 @@
+/********************* */
+/*! \file theory_sets_type_enumerator.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
#include "cvc4_private.h"
@@ -76,7 +93,7 @@ public:
Assert(d_index == 0 || d_index == 1);
if(d_index == 1) {
- n = d_nm->mkNode(kind::SET_SINGLETON, *(*(d_constituentVec[0])));
+ n = d_nm->mkNode(kind::SINGLETON, *(*(d_constituentVec[0])));
}
// for (unsigned i = 0; i < d_indexVec.size(); ++i) {
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 3b2acd956..eb270202a 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Kshitij Bansal
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -105,20 +105,20 @@ struct MemberTypeRule {
}
return nodeManager->booleanType();
}
-};/* struct SetInTypeRule */
+};/* struct MemberTypeRule */
-struct SetSingletonTypeRule {
+struct SingletonTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
- Assert(n.getKind() == kind::SET_SINGLETON);
+ Assert(n.getKind() == kind::SINGLETON);
return nodeManager->mkSetType(n[0].getType(check));
}
inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::SET_SINGLETON);
+ Assert(n.getKind() == kind::SINGLETON);
return n[0].isConst();
}
-};/* struct SetInTypeRule */
+};/* struct SingletonTypeRule */
struct EmptySetTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -128,7 +128,35 @@ struct EmptySetTypeRule {
Type setType = emptySet.getType();
return TypeNode::fromType(setType);
}
-};
+};/* struct EmptySetTypeRule */
+
+struct InsertTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::INSERT);
+ size_t numChildren = n.getNumChildren();
+ Assert( numChildren >= 2 );
+ TypeNode setType = n[numChildren-1].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "inserting into a non-set");
+ }
+ for(size_t i = 0; i < numChildren-1; ++i) {
+ TypeNode elementType = n[i].getType(check);
+ if(elementType != setType.getSetElementType()) {
+ throw TypeCheckingExceptionPrivate
+ (n, "type of element should be same as element type of set being inserted into");
+ }
+ }
+ }
+ return setType;
+ }
+
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ Assert(n.getKind() == kind::INSERT);
+ return n[0].isConst() && n[1].isConst();
+ }
+};/* struct InsertTypeRule */
struct SetsProperties {
@@ -146,7 +174,7 @@ struct SetsProperties {
Assert(type.isSet());
return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
}
-};
+};/* struct SetsProperties */
}/* CVC4::theory::sets namespace */
}/* CVC4::theory namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback