summaryrefslogtreecommitdiff
path: root/src/theory/sets/card_unused_implementation.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sets/card_unused_implementation.cpp')
-rw-r--r--src/theory/sets/card_unused_implementation.cpp312
1 files changed, 0 insertions, 312 deletions
diff --git a/src/theory/sets/card_unused_implementation.cpp b/src/theory/sets/card_unused_implementation.cpp
deleted file mode 100644
index 488ee1026..000000000
--- a/src/theory/sets/card_unused_implementation.cpp
+++ /dev/null
@@ -1,312 +0,0 @@
-// Removing old cardinality implementation, dumping it here.
-
-///////////////////////////////////////////////////////////////
-// Commenting out processCard, creates confusion when writing
-// processCard2
-///////////////////////////////////////////////////////////////
-
-
-// void TheorySetsPrivate::processCard(Theory::Effort level) {
-// if(level != Theory::EFFORT_FULL) return;
-
-
-// Trace("sets-card") << "[sets-card] processCard( " << level << ")" << std::endl;
-// Trace("sets-card") << "[sets-card] # processed terms = " << d_processedCardTerms.size() << std::endl;
-// Trace("sets-card") << "[sets-card] # processed pairs = " << d_processedCardPairs.size() << std::endl;
-// NodeManager* nm = NodeManager::currentNM();
-
-// bool newLemmaGenerated = false;
-
-// // Introduce lemma
-// for(typeof(d_cardTerms.begin()) it = d_cardTerms.begin();
-// it != d_cardTerms.end(); ++it) {
-
-// for(eq::EqClassIterator j(d_equalityEngine.getRepresentative((*it)[0]), &d_equalityEngine);
-// !j.isFinished(); ++j) {
-
-// Node n = nm->mkNode(kind::CARD, (*j));
-
-// if(d_processedCardTerms.find(n) != d_processedCardTerms.end()) {
-// continue;
-// }
-
-// Trace("sets-card") << "[sets-card] Processing " << n << " in eq cl of " << (*it) << std::endl;
-
-// newLemmaGenerated = true;
-// d_processedCardTerms.insert(n);
-
-// Kind k = n[0].getKind();
-
-// if(k == kind::SINGLETON) {
-// d_external.d_out->lemma(nm->mkNode(kind::EQUAL,
-// n,
-// nm->mkConst(Rational(1))));
-// continue;
-// } else {
-// d_external.d_out->lemma(nm->mkNode(kind::GEQ,
-// n,
-// nm->mkConst(Rational(0))));
-// }
-
-// // rest of the processing is for compound terms
-// if(k != kind::UNION && k != kind::INTERSECTION && k != kind::SETMINUS) {
-// continue;
-// }
-
-// Node s = min(n[0][0], n[0][1]);
-// Node t = max(n[0][0], n[0][1]);
-// bool isUnion = (k == kind::UNION);
-// Assert(Rewriter::rewrite(s) == s);
-// Assert(Rewriter::rewrite(t) == t);
-
-// typeof(d_processedCardPairs.begin()) processedInfo = d_processedCardPairs.find(make_pair(s, t));
-
-// if(processedInfo == d_processedCardPairs.end()) {
-
-// Node sNt = nm->mkNode(kind::INTERSECTION, s, t);
-// sNt = Rewriter::rewrite(sNt);
-// Node sMt = nm->mkNode(kind::SETMINUS, s, t);
-// sMt = Rewriter::rewrite(sMt);
-// Node tMs = nm->mkNode(kind::SETMINUS, t, s);
-// tMs = Rewriter::rewrite(tMs);
-
-// Node card_s = nm->mkNode(kind::CARD, s);
-// Node card_t = nm->mkNode(kind::CARD, t);
-// Node card_sNt = nm->mkNode(kind::CARD, sNt);
-// Node card_sMt = nm->mkNode(kind::CARD, sMt);
-// Node card_tMs = nm->mkNode(kind::CARD, tMs);
-
-// Node lem;
-
-// // for s
-// lem = nm->mkNode(kind::EQUAL,
-// card_s,
-// nm->mkNode(kind::PLUS, card_sNt, card_sMt));
-// d_external.d_out->lemma(lem);
-
-// // for t
-// lem = nm->mkNode(kind::EQUAL,
-// card_t,
-// nm->mkNode(kind::PLUS, card_sNt, card_tMs));
-
-// d_external.d_out->lemma(lem);
-
-// // for union
-// if(isUnion) {
-// lem = nm->mkNode(kind::EQUAL,
-// n, // card(s union t)
-// nm->mkNode(kind::PLUS, card_sNt, card_sMt, card_tMs));
-// d_external.d_out->lemma(lem);
-// }
-
-// d_processedCardPairs.insert(make_pair(make_pair(s, t), isUnion));
-
-// } else if(isUnion && processedInfo->second == false) {
-
-// Node sNt = nm->mkNode(kind::INTERSECTION, s, t);
-// sNt = Rewriter::rewrite(sNt);
-// Node sMt = nm->mkNode(kind::SETMINUS, s, t);
-// sMt = Rewriter::rewrite(sMt);
-// Node tMs = nm->mkNode(kind::SETMINUS, t, s);
-// tMs = Rewriter::rewrite(tMs);
-
-// Node card_s = nm->mkNode(kind::CARD, s);
-// Node card_t = nm->mkNode(kind::CARD, t);
-// Node card_sNt = nm->mkNode(kind::CARD, sNt);
-// Node card_sMt = nm->mkNode(kind::CARD, sMt);
-// Node card_tMs = nm->mkNode(kind::CARD, tMs);
-
-// Assert(Rewriter::rewrite(n[0]) == n[0]);
-
-// Node lem = nm->mkNode(kind::EQUAL,
-// n, // card(s union t)
-// nm->mkNode(kind::PLUS, card_sNt, card_sMt, card_tMs));
-// d_external.d_out->lemma(lem);
-
-// processedInfo->second = true;
-// }
-
-// }//equivalence class loop
-
-// }//d_cardTerms loop
-
-// if(newLemmaGenerated) {
-// Trace("sets-card") << "[sets-card] New introduce done. Returning." << std::endl;
-// return;
-// }
-
-
-
-// // Leaves disjoint lemmas
-// buildGraph();
-
-// // Leaves disjoint lemmas
-// for(typeof(leaves.begin()) it = leaves.begin(); it != leaves.end(); ++it) {
-// TNode l1 = (*it);
-// if(d_equalityEngine.getRepresentative(l1).getKind() == kind::EMPTYSET) continue;
-// for(typeof(leaves.begin()) jt = leaves.begin(); jt != leaves.end(); ++jt) {
-// TNode l2 = (*jt);
-
-// if(d_equalityEngine.getRepresentative(l2).getKind() == kind::EMPTYSET) continue;
-
-// if( l1 == l2 ) continue;
-
-// Node l1_inter_l2 = nm->mkNode(kind::INTERSECTION, min(l1, l2), max(l1, l2));
-// l1_inter_l2 = Rewriter::rewrite(l1_inter_l2);
-// Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType(l1_inter_l2.getType())));
-// if(d_equalityEngine.hasTerm(l1_inter_l2) &&
-// d_equalityEngine.hasTerm(emptySet) &&
-// d_equalityEngine.areEqual(l1_inter_l2, emptySet)) {
-// Debug("sets-card-graph") << "[sets-card-graph] Disjoint (asserted): " << l1 << " and " << l2 << std::endl;
-// continue; // known to be disjoint
-// }
-
-// std::set<TNode> l1_ancestors = getReachable(edgesBk, l1);
-// std::set<TNode> l2_ancestors = getReachable(edgesBk, l2);
-
-// // have a disjoint edge
-// bool loop = true;
-// bool equality = false;
-// for(typeof(l1_ancestors.begin()) l1_it = l1_ancestors.begin();
-// l1_it != l1_ancestors.end() && loop; ++l1_it) {
-// for(typeof(l2_ancestors.begin()) l2_it = l2_ancestors.begin();
-// l2_it != l2_ancestors.end() && loop; ++l2_it) {
-// TNode n1 = (*l1_it);
-// TNode n2 = (*l2_it);
-// if(disjoint.find(make_pair(n1, n2)) != disjoint.find(make_pair(n2, n1))) {
-// loop = false;
-// }
-// if(n1 == n2) {
-// equality = true;
-// }
-// if(d_equalityEngine.hasTerm(n1) && d_equalityEngine.hasTerm(n2) &&
-// d_equalityEngine.areEqual(n1, n2)) {
-// equality = true;
-// }
-// }
-// }
-// if(loop == false) {
-// Debug("sets-card-graph") << "[sets-card-graph] Disjoint (always): " << l1 << " and " << l2 << std::endl;
-// continue;
-// }
-// if(equality == false) {
-// Debug("sets-card-graph") << "[sets-card-graph] No equality found: " << l1 << " and " << l2 << std::endl;
-// continue;
-// }
-
-// Node lem = nm->mkNode(kind::OR,
-// nm->mkNode(kind::EQUAL, l1_inter_l2, emptySet),
-// nm->mkNode(kind::LT, nm->mkConst(Rational(0)),
-// nm->mkNode(kind::CARD, l1_inter_l2)));
-
-// d_external.d_out->lemma(lem);
-// Trace("sets-card") << "[sets-card] Guessing disjointness of : " << l1 << " and " << l2 << std::endl;
-// if(Debug.isOn("sets-card-disjoint")) {
-// Debug("sets-card-disjoint") << "[sets-card-disjoint] Lemma for " << l1 << " and " << l2 << " generated because:" << std::endl;
-// for(typeof(disjoint.begin()) it = disjoint.begin(); it != disjoint.end(); ++it) {
-// Debug("sets-card-disjoint") << "[sets-card-disjoint] " << it->first << " " << it->second << std::endl;
-// }
-// }
-// newLemmaGenerated = true;
-// Trace("sets-card") << "[sets-card] New intersection being empty lemma generated. Returning." << std::endl;
-// return;
-// }
-// }
-
-// Assert(!newLemmaGenerated);
-
-
-
-// // Elements being either equal or disequal
-
-// for(typeof(leaves.begin()) it = leaves.begin();
-// it != leaves.end(); ++it) {
-// Assert(d_equalityEngine.hasTerm(*it));
-// Node n = d_equalityEngine.getRepresentative(*it);
-// Assert(n.getKind() == kind::EMPTYSET || leaves.find(n) != leaves.end());
-// if(n != *it) continue;
-// const CDTNodeList* l = d_termInfoManager->getMembers(*it);
-// std::set<TNode> elems;
-// for(typeof(l->begin()) l_it = l->begin(); l_it != l->end(); ++l_it) {
-// elems.insert(d_equalityEngine.getRepresentative(*l_it));
-// }
-// for(typeof(elems.begin()) e1_it = elems.begin(); e1_it != elems.end(); ++e1_it) {
-// for(typeof(elems.begin()) e2_it = elems.begin(); e2_it != elems.end(); ++e2_it) {
-// if(*e1_it == *e2_it) continue;
-// if(!d_equalityEngine.areDisequal(*e1_it, *e2_it, false)) {
-// Node lem = nm->mkNode(kind::EQUAL, *e1_it, *e2_it);
-// lem = nm->mkNode(kind::OR, lem, nm->mkNode(kind::NOT, lem));
-// d_external.d_out->lemma(lem);
-// newLemmaGenerated = true;
-// }
-// }
-// }
-// }
-
-// if(newLemmaGenerated) {
-// Trace("sets-card") << "[sets-card] Members arrangments lemmas. Returning." << std::endl;
-// return;
-// }
-
-
-// // Guess leaf nodes being empty or non-empty
-// for(typeof(leaves.begin()) it = leaves.begin(); it != leaves.end(); ++it) {
-// Node n = d_equalityEngine.getRepresentative(*it);
-// if(n.getKind() == kind::EMPTYSET) continue;
-// if(d_termInfoManager->getMembers(n)->size() > 0) continue;
-// Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType(n.getType())));
-// if(!d_equalityEngine.hasTerm(emptySet)) {
-// d_equalityEngine.addTerm(emptySet);
-// }
-// if(!d_equalityEngine.areDisequal(n, emptySet, false)) {
-// Node lem = nm->mkNode(kind::EQUAL, n, emptySet);
-// lem = nm->mkNode(kind::OR, lem, nm->mkNode(kind::NOT, lem));
-// Assert(d_cardLowerLemmaCache.find(lem) == d_cardLowerLemmaCache.end());
-// d_cardLowerLemmaCache.insert(lem);
-// d_external.d_out->lemma(lem);
-// newLemmaGenerated = true;
-// break;
-// }
-// }
-
-// if(newLemmaGenerated) {
-// Trace("sets-card") << "[sets-card] New guessing leaves being empty done." << std::endl;
-// return;
-// }
-
-// // Assert Lower bound
-// for(typeof(leaves.begin()) it = leaves.begin();
-// it != leaves.end(); ++it) {
-// Assert(d_equalityEngine.hasTerm(*it));
-// Node n = d_equalityEngine.getRepresentative(*it);
-// Assert(n.getKind() == kind::EMPTYSET || leaves.find(n) != leaves.end());
-// if(n != *it) continue;
-// const CDTNodeList* l = d_termInfoManager->getMembers(n);
-// std::set<TNode> elems;
-// for(typeof(l->begin()) l_it = l->begin(); l_it != l->end(); ++l_it) {
-// elems.insert(d_equalityEngine.getRepresentative(*l_it));
-// }
-// if(elems.size() == 0) continue;
-// NodeBuilder<> nb(kind::OR);
-// nb << ( nm->mkNode(kind::LEQ, nm->mkConst(Rational(elems.size())), nm->mkNode(kind::CARD, n)) );
-// if(elems.size() > 1) {
-// for(typeof(elems.begin()) e1_it = elems.begin(); e1_it != elems.end(); ++e1_it) {
-// for(typeof(elems.begin()) e2_it = elems.begin(); e2_it != elems.end(); ++e2_it) {
-// if(*e1_it == *e2_it) continue;
-// nb << (nm->mkNode(kind::EQUAL, *e1_it, *e2_it));
-// }
-// }
-// }
-// for(typeof(elems.begin()) e_it = elems.begin(); e_it != elems.end(); ++e_it) {
-// nb << nm->mkNode(kind::NOT, nm->mkNode(kind::MEMBER, *e_it, n));
-// }
-// Node lem = Node(nb);
-// if(d_cardLowerLemmaCache.find(lem) == d_cardLowerLemmaCache.end()) {
-// Trace("sets-card") << "[sets-card] Card Lower: " << lem << std::endl;
-// d_external.d_out->lemma(lem);
-// d_cardLowerLemmaCache.insert(lem);
-// newLemmaGenerated = true;
-// }
-// }
-// }
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback