diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 13:28:09 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 13:28:09 -0400 |
commit | b06d25a020240fa455798308418ad802f9f40ea3 (patch) | |
tree | 8203c68da0861a823674b942595ae8cfbfeac256 /src | |
parent | 7c009ac38ef5ccda070d8d7fb3955273574e94eb (diff) | |
parent | fa53ae111cd314f455456a884f1247bb9b8e2c7b (diff) |
Merge pull request #47 from kbansal/sets
Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are:
SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset*
API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET
(those marked with [*] have changed or been added, others are as earlier)
In the set-logic string use FS to enable sets.
A not-so-well-tested perl command for translating old benchmarks:
perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; '
Diffstat (limited to 'src')
-rw-r--r-- | src/context/cdhashmap.h | 2 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 6 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 7 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 9 | ||||
-rw-r--r-- | src/theory/logic_info.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/expr_patterns.h | 4 | ||||
-rw-r--r-- | src/theory/sets/kinds | 17 | ||||
-rw-r--r-- | src/theory/sets/options | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 18 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 55 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 21 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 42 | ||||
-rw-r--r-- | src/util/emptyset.h | 8 |
19 files changed, 150 insertions, 65 deletions
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 7fb36bb3a..4d2b8570f 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -180,7 +180,7 @@ public: CDOhash_map(Context* context, CDHashMap<Key, Data, HashFcn>* map, - const Key& key, + const Key& key, const Data& data, bool atLevelZero = false, bool allocatedInCMM = false) : diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index cda696a03..8173c7269 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -144,9 +144,9 @@ public: /** Is the DecisionEngine in a state where it has solved everything? */ bool isDone() { Trace("decision") << "DecisionEngine::isDone() returning " - << (d_result != SAT_VALUE_UNKNOWN) - << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false") - << std::endl; + << (d_result != SAT_VALUE_UNKNOWN) + << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false") + << std::endl; return (d_result != SAT_VALUE_UNKNOWN); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8590229a2..457c9c82f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1115,7 +1115,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); } | EMPTYSET_TOK - { expr = MK_CONST( ::CVC4::EmptySet()); } + { expr = MK_CONST( ::CVC4::EmptySet(Type())); } // NOTE: Theory constants go here ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 5baa0b16f..0c4b1258f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -149,9 +149,10 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::UNION, "union"); addOperator(kind::INTERSECTION, "intersection"); addOperator(kind::SETMINUS, "setminus"); - addOperator(kind::SUBSET, "subseteq"); - addOperator(kind::MEMBER, "in"); - addOperator(kind::SET_SINGLETON, "setenum"); + addOperator(kind::SUBSET, "subset"); + addOperator(kind::MEMBER, "member"); + addOperator(kind::SINGLETON, "singleton"); + addOperator(kind::INSERT, "insert"); break; case THEORY_DATATYPES: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 15101b0e4..270e0dba0 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -418,7 +418,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::SUBSET: case kind::MEMBER: case kind::SET_TYPE: - case kind::SET_SINGLETON: out << smtKindString(k) << " "; break; + case kind::SINGLETON: out << smtKindString(k) << " "; break; // datatypes case kind::APPLY_TYPE_ASCRIPTION: { @@ -618,10 +618,11 @@ static string smtKindString(Kind k) throw() { case kind::UNION: return "union"; case kind::INTERSECTION: return "intersection"; case kind::SETMINUS: return "setminus"; - case kind::SUBSET: return "subseteq"; - case kind::MEMBER: return "in"; + case kind::SUBSET: return "subset"; + case kind::MEMBER: return "member"; case kind::SET_TYPE: return "Set"; - case kind::SET_SINGLETON: return "setenum"; + case kind::SINGLETON: return "singleton"; + case kind::INSERT: return "insert"; default: ; /* fall through */ } diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 78f4996b8..bc2f1286b 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -129,7 +129,7 @@ std::string LogicInfo::getLogicString() const { ++seen; } if(d_theories[THEORY_SETS]) { - ss << "_SETS"; + ss << "FS"; ++seen; } @@ -272,9 +272,9 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc arithNonLinear(); p += 4; } - if(!strncmp(p, "_SETS", 5)) { + if(!strncmp(p, "FS", 2)) { enableTheory(THEORY_SETS); - p += 5; + p += 2; } } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 9f25b0825..2c309899d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -74,7 +74,7 @@ unsigned TermDb::getNumGroundTerms( Node f ) { Node TermDb::getOperator( Node n ) { //return n.getOperator(); Kind k = n.getKind(); - if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON ){ + if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){ //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); Node op = n.getOperator(); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 77a4efff5..0d8f2c06d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -330,7 +330,7 @@ bool Trigger::isAtomicTrigger( Node n ){ bool Trigger::isAtomicTriggerKind( Kind k ) { return k==APPLY_UF || k==SELECT || k==STORE || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || - k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON; + k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON; } bool Trigger::isSimpleTrigger( Node n ){ diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h index bc5b6b9e0..93307d227 100644 --- a/src/theory/sets/expr_patterns.h +++ b/src/theory/sets/expr_patterns.h @@ -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/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index c230b9ac5..5d5e1f9ee 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -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..84d91de72 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -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..be2b48f81 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -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; } @@ -886,11 +922,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 +979,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 +1156,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..e5d7beb2c 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -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..8716d1065 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -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_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 2f4cc6a2f..97fbfe94f 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -76,7 +76,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..fa1183e07 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -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 */ diff --git a/src/util/emptyset.h b/src/util/emptyset.h index 2f6c54173..43a868e42 100644 --- a/src/util/emptyset.h +++ b/src/util/emptyset.h @@ -35,10 +35,14 @@ class CVC4_PUBLIC EmptySet { const SetType d_type; + EmptySet() { } public: - EmptySet() { } /* Null typed */ - EmptySet(SetType t):d_type(t) { } + /** + * Constructs an emptyset of the specified type. Note that the argument + * is the type of the set itself, NOT the type of the elements. + */ + EmptySet(SetType setType):d_type(setType) { } ~EmptySet() throw() { |