From: Kshitij Bansal Date: Fri, 28 Feb 2014 13:14:43 +0000 (-0500) Subject: rename kind::IN to kind::MEMBER (fixes some windows build conflicts) X-Git-Tag: cvc5-1.0.0~7055^2~1 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=db6215dddeb90719a24793a50c87635125fd2817;p=cvc5.git 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 9b598e113..b9a15b3b2 100644 --- 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 a2a925d13..6eb91431f 100644 --- 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 089549457..75127f5d8 100644 --- 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 bae0c5f1d..68941489f 100644 --- 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 8fd490554..0ff5f231d 100644 --- 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 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(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 11a2e9297..76e60f535 100644 --- 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 026c90ca4..35534de30 100644 --- 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()) {