rename kind::IN to kind::MEMBER (fixes some windows build conflicts)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9b598e1133152f068a075579e8d7dbb83f0d84a5..b9a15b3b29acbb5f3798f42f0b2f3d50e45580e1 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1309,7 +1309,7 @@ builtinOp[CVC4::Kind& kind]
   | SETINT_TOK    { $kind = CVC4::kind::INTERSECTION; }
   | SETMINUS_TOK  { $kind = CVC4::kind::SETMINUS; }
   | SETSUB_TOK    { $kind = CVC4::kind::SUBSET; }
-  | SETIN_TOK     { $kind = CVC4::kind::IN; }
+  | SETIN_TOK     { $kind = CVC4::kind::MEMBER; }
   | SETSINGLETON_TOK { $kind = CVC4::kind::SET_SINGLETON; }
 
   // NOTE: Theory operators go here

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a2a925d13805197556f24bd854c5f1a5c8e0f10c..6eb91431f538ecf5b14da37259724b25fd5d03d2 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -398,7 +398,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::INTERSECTION:
   case kind::SETMINUS:
   case kind::SUBSET:
-  case kind::IN:
+  case kind::MEMBER:
   case kind::SET_TYPE:
   case kind::SET_SINGLETON: out << smtKindString(k) << " "; break;
 
@@ -592,7 +592,7 @@ static string smtKindString(Kind k) throw() {
   case kind::INTERSECTION: return "intersection";
   case kind::SETMINUS: return "setminus";
   case kind::SUBSET: return "subseteq";
-  case kind::IN: return "in";
+  case kind::MEMBER: return "in";
   case kind::SET_TYPE: return "Set";
   case kind::SET_SINGLETON: return "setenum";
   default:

diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h
index 089549457c76190709eb3725bbe70672b898fe51..75127f5d8560a414e5308cc2e64efd00e43ba9c4 100644 (file)
--- a/src/theory/sets/expr_patterns.h
+++ b/src/theory/sets/expr_patterns.h
@@ -34,8 +34,8 @@ static Node OR(TNode a, TNode b, TNode c) {
   return NodeManager::currentNM()->mkNode(kind::OR, a, b, c);
 }
 
-static Node IN(TNode a, TNode b) {
-  return NodeManager::currentNM()->mkNode(kind::IN, a, b);
+static Node MEMBER(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::MEMBER, a, b);
 }
 
 static Node EQUAL(TNode a, TNode b) {

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index bae0c5f1de6c18b2e50552e602fb57a2bc8b31f0..68941489f4bf8c7ae2c7ff70f9a081cc81468fdc 100644 (file)
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -37,7 +37,7 @@ operator UNION 2 "set union"
 operator INTERSECTION 2 "set intersection"
 operator SETMINUS 2 "set subtraction"
 operator SUBSET 2 "subset"
-operator IN 2 "set membership"
+operator MEMBER 2 "set membership"
 
 operator SET_SINGLETON 1 "singleton set"
 
@@ -45,7 +45,7 @@ typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
 typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule
 typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule
 typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule
-typerule IN ::CVC4::theory::sets::SetInTypeRule
+typerule MEMBER ::CVC4::theory::sets::SetMemberTypeRule
 typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
 typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
 

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 8fd4905542eb411fc0dc324d2fec9a14aba81ced..0ff5f231d36d434fb27f9f08a4762357d7a1c816 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -58,7 +58,7 @@ void TheorySetsPrivate::check(Theory::Effort level) {
       assertEquality(fact, fact, /* learnt = */ false);
       break;
 
-    case kind::IN:
+    case kind::MEMBER:
       Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
                     << "be in " << atom[1] << std::endl;
       assertMemebership(fact, fact, /* learnt = */ false);
@@ -155,7 +155,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
   eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
                         &d_equalityEngine);
   TNode S = (*j);
-  Node cur_atom = IN(x, S);
+  Node cur_atom = MEMBER(x, S);
 
   /**
    * It is sufficient to do emptyset propagation outside the loop as
@@ -171,7 +171,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
 
   for(; !j.isFinished(); ++j) {
     TNode S = (*j);
-    Node cur_atom = IN(x, S);
+    Node cur_atom = MEMBER(x, S);
 
     // propagation : children
     Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
@@ -213,22 +213,22 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
   // axiom: literal <=> left_literal AND right_literal
   switch(S.getKind()) {
   case kind::INTERSECTION:
-    literal       =       IN(x, S)      ;
-    left_literal  =       IN(x, S[0])   ;
-    right_literal =       IN(x, S[1])   ;
+    literal       =       MEMBER(x, S)      ;
+    left_literal  =       MEMBER(x, S[0])   ;
+    right_literal =       MEMBER(x, S[1])   ;
     break;
   case kind::UNION:
-    literal       = NOT(  IN(x, S)     );
-    left_literal  = NOT(  IN(x, S[0])  );
-    right_literal = NOT(  IN(x, S[1])  );
+    literal       = NOT(  MEMBER(x, S)     );
+    left_literal  = NOT(  MEMBER(x, S[0])  );
+    right_literal = NOT(  MEMBER(x, S[1])  );
     break;
   case kind::SETMINUS:
-    literal       =       IN(x, S)      ;
-    left_literal  =       IN(x, S[0])   ;
-    right_literal = NOT(  IN(x, S[1])  );
+    literal       =       MEMBER(x, S)      ;
+    left_literal  =       MEMBER(x, S[0])   ;
+    right_literal = NOT(  MEMBER(x, S[1])  );
     break;
   case kind::SET_SINGLETON: {
-    Node atom = IN(x, S);
+    Node atom = MEMBER(x, S);
     if(holds(atom, true)) {
       learnLiteral(EQUAL(x, S[0]), true, atom);
     } else if(holds(atom, false)) {
@@ -253,9 +253,9 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
     << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
     << std::endl;
 
-  Assert( present( IN(x, S)    ) ||
-          present( IN(x, S[0]) ) ||
-          present( IN(x, S[1]) ) );
+  Assert( present( MEMBER(x, S)    ) ||
+          present( MEMBER(x, S[0]) ) ||
+          present( MEMBER(x, S[1]) ) );
 
   if( holds(literal) ) {
     // 1a. literal => left_literal
@@ -313,15 +313,15 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
   Node n;
   switch(S.getKind()) {
   case kind::UNION:
-    if( holds(IN(x, S)) &&
-        !present( IN(x, S[0]) ) )
-      addToPending( IN(x, S[0]) );
+    if( holds(MEMBER(x, S)) &&
+        !present( MEMBER(x, S[0]) ) )
+      addToPending( MEMBER(x, S[0]) );
     break;
   case kind::SETMINUS: // intentional fallthrough
   case kind::INTERSECTION:
-    if( holds(IN(x, S[0])) &&
-        !present( IN(x, S[1]) ))
-      addToPending( IN(x, S[1]) );
+    if( holds(MEMBER(x, S[0])) &&
+        !present( MEMBER(x, S[1]) ))
+      addToPending( MEMBER(x, S[1]) );
     break;
   default:
     Assert(false, "MembershipEngine::doSettermPropagation");
@@ -352,7 +352,7 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
     return;
   }
 
-  Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IN);
+  Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::MEMBER);
 
   Node learnt_literal = polarity ? Node(atom) : NOT(atom);
   d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
@@ -441,7 +441,7 @@ void TheorySetsPrivate::registerReason(TNode reason, bool save)
     registerReason(reason[1], false);
   } else if(reason.getKind() == kind::NOT) {
     registerReason(reason[0], false);
-  } else if(reason.getKind() == kind::IN) {
+  } else if(reason.getKind() == kind::MEMBER) {
     d_equalityEngine.addTerm(reason);
     Assert(present(reason));
   } else if(reason.getKind() == kind::EQUAL) {
@@ -465,7 +465,7 @@ void TheorySetsPrivate::finishPropagation()
     std::pair<Node,Node> np = d_propagationQueue.front();
     d_propagationQueue.pop();
     TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
-    if(atom.getKind() == kind::IN) {
+    if(atom.getKind() == kind::MEMBER) {
       assertMemebership(np.first, np.second, /* learnt = */ true);
     } else {
       assertEquality(np.first, np.second, /* learnt = */ true);
@@ -475,7 +475,7 @@ void TheorySetsPrivate::finishPropagation()
 
 void TheorySetsPrivate::addToPending(Node n) {
   if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
-    if(n.getKind() == kind::IN) {
+    if(n.getKind() == kind::MEMBER) {
       d_pending.push(n);
     } else {
       Assert(n.getKind() == kind::EQUAL);
@@ -501,7 +501,7 @@ Node TheorySetsPrivate::getLemma() {
     d_pending.pop();
 
     Assert(!present(n));
-    Assert(n.getKind() == kind::IN);
+    Assert(n.getKind() == kind::MEMBER);
 
     lemma = OR(n, NOT(n));
   } else {
@@ -510,7 +510,7 @@ Node TheorySetsPrivate::getLemma() {
 
     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
     Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
-    Node l1 = IN(x, n[0]), l2 = IN(x, n[1]);
+    Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
 
     // d_equalityEngine.addTerm(x);
     // d_equalityEngine.addTerm(l1);
@@ -547,7 +547,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
   d_equalityEngine.addFunctionKind(kind::SETMINUS);
 
-  d_equalityEngine.addFunctionKind(kind::IN);
+  d_equalityEngine.addFunctionKind(kind::MEMBER);
   d_equalityEngine.addFunctionKind(kind::SUBSET);
 }/* TheorySetsPrivate::TheorySetsPrivate() */
 
@@ -606,7 +606,7 @@ Node TheorySetsPrivate::explain(TNode literal)
 
   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
      d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
-  } else if(atom.getKind() == kind::IN) {
+  } else if(atom.getKind() == kind::MEMBER) {
     if( !d_equalityEngine.hasTerm(atom)) {
       d_equalityEngine.addTerm(atom);
     }
@@ -630,7 +630,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
     // TODO: what's the point of this
     d_equalityEngine.addTriggerEquality(node);
     break;
-  case kind::IN:
+  case kind::MEMBER:
     // TODO: what's the point of this
     d_equalityEngine.addTriggerPredicate(node);
     break;
@@ -641,7 +641,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
   }
   if(node.getKind() == kind::SET_SINGLETON) {
     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
-    learnLiteral(IN(node[0], node), true, true_node);
+    learnLiteral(MEMBER(node[0], node), true, true_node);
     //intentional fallthrough
   }
 }
@@ -792,18 +792,18 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
 {
   for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
-                       << IN(*i, d_eqEngine->getRepresentative(S))
+                       << MEMBER(*i, d_eqEngine->getRepresentative(S))
                        << std::endl;
 
-    d_eqEngine->addTerm(IN(d_eqEngine->getRepresentative(*i),
-                           d_eqEngine->getRepresentative(S)));
+    d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(*i),
+                              d_eqEngine->getRepresentative(S)));
 
     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
         !j.isFinished(); ++j) {
 
       TNode x = (*i);
       TNode S = (*j);
-      Node cur_atom = IN(x, S);
+      Node cur_atom = MEMBER(x, S);
 
       // propagation : empty set
       if(polarity && S.getKind() == kind::EMPTYSET) {

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 11a2e929722c0e7c5ee4566087134c4d5ee100a9..76e60f5355d2c507848515017d99fdd8456ed787 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -31,7 +31,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
 
   switch(node.getKind()) {
 
-  case kind::IN: {
+  case kind::MEMBER: {
     if(!node[0].isConst() || !node[1].isConst())
       break;
 

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 026c90ca4e6e6fe0522de7fb8b97ddbe65f8491a..35534de3009a911942078db357f2b21132fa83e4 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -101,10 +101,10 @@ struct SetSubsetTypeRule {
   }
 };/* struct SetSubsetTypeRule */
 
-struct SetInTypeRule {
+struct SetMemberTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
-    Assert(n.getKind() == kind::IN);
+    Assert(n.getKind() == kind::MEMBER);
     TypeNode setType = n[1].getType(check);
     if( check ) {
       if(!setType.isSet()) {