summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/theory/quantifiers/trigger.cpp2
-rw-r--r--src/theory/sets/expr_patterns.h4
-rw-r--r--src/theory/sets/kinds8
-rw-r--r--src/theory/sets/theory_sets_private.cpp12
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp12
-rw-r--r--src/theory/sets/theory_sets_type_enumerator.h2
-rw-r--r--src/theory/sets/theory_sets_type_rules.h8
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback