diff options
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/expr_patterns.h | 6 | ||||
-rw-r--r-- | src/theory/sets/kinds | 17 | ||||
-rw-r--r-- | src/theory/sets/options | 4 | ||||
-rw-r--r-- | src/theory/sets/options_handlers.h | 17 | ||||
-rw-r--r-- | src/theory/sets/scrutinize.h | 2 | ||||
-rw-r--r-- | src/theory/sets/term_info.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 20 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 8 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 73 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 23 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.h | 19 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 46 |
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 */ |