diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-22 01:17:27 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-22 17:37:25 -0400 |
commit | b8ddf766460bfcf475e08ff52c889246e78f76cc (patch) | |
tree | b631495d0801191c1e6b283854b5b30c11547fea /src/theory | |
parent | 44d05f7def63e5f675f80dab8829c5759db7e065 (diff) |
Renaming of SMT2 operator names, kinds for set theory
* SET_SINGLETON kind renamed to just SINGLETON
* "setenum" smt2 opertor renamed to "singleton"[1]
* "in" smt2 operator renamed to "member"[2]
[1] It was anyhow accepting exactly one argument, so was bit misleading
to call set enumerator.
[2] The corresponding kind was called MEMBER, so this will also make them
consistent. Only inconsistency now is for subset: kind is called
SUBSET but operator is called "subseteq".
Diffstat (limited to 'src/theory')
-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 | 8 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 12 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 12 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 8 |
8 files changed, 25 insertions, 25 deletions
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 799261634..06d3be5a0 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -22,7 +22,7 @@ constant EMPTYSET \ "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" @@ -40,19 +40,19 @@ 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 SET_SINGLETON 1 "the set of the single element given as a parameter" +operator SINGLETON 1 "the set of the single element given as a 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 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 endtheory diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f768bd62d..c06f1bd5e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -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); @@ -535,9 +535,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; } @@ -948,7 +948,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 +1125,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_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 7b02c1bfb..ce469cc0c 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; } 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 eff81622d..2267ee22a 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -107,18 +107,18 @@ struct MemberTypeRule { } };/* 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 SetSingletonTypeRule */ +};/* struct SingletonTypeRule */ struct EmptySetTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) |