if(x.getType().isSet()) {
if(polarity) {
const CDTNodeList* l = d_termInfoManager->getNonMembers(S);
- for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+ for(CDTNodeList::iterator it = l->begin(); it != l->end(); ++it) {
TNode n = *it;
learnLiteral( /* atom = */ EQUAL(x, n),
/* polarity = */ false,
}
} else {
const CDTNodeList* l = d_termInfoManager->getMembers(S);
- for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+ for(CDTNodeList::iterator it = l->begin(); it != l->end(); ++it) {
TNode n = *it;
learnLiteral( /* atom = */ EQUAL(x, n),
/* polarity = */ false,
Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
<< x << element_of_str << S << std::endl;
const CDTNodeList* parentList = d_termInfoManager->getParents(S);
- for(typeof(parentList->begin()) k = parentList->begin();
+ for(CDTNodeList::const_iterator k = parentList->begin();
k != parentList->end(); ++k) {
doSettermPropagation(x, *k);
if(d_conflict) return;
context::CDList<Assertion>::const_iterator it = d_external.facts_begin(), it_end = d_external.facts_end();
- std::map<TNode, std::set<TNode> > equalities;
- std::set< pair<TNode, TNode> > disequalities;
- std::map<TNode, std::pair<std::set<TNode>, std::set<TNode> > > members;
+ typedef std::set<TNode> TNodeSet;
+
+ typedef std::map<TNode, TNodeSet > EqualityMap;
+ EqualityMap equalities;
+
+ typedef std::set< std::pair<TNode, TNode> > TNodePairSet;
+ TNodePairSet disequalities;
+ typedef std::map<TNode, std::pair<TNodeSet, TNodeSet > > MemberMap;
+ MemberMap members;
static std::map<TNode, int> numbering;
static int number = 0;
(polarity ? members[right].first : members[right].second).insert(left);
}
}
-#define FORIT(it, container) for(typeof((container).begin()) it=(container).begin(); (it) != (container).end(); ++(it))
- FORIT(kt, equalities) {
+ //#define FORIT(it, container) for(typeof((container).begin()) it=(container).begin(); (it) != (container).end(); ++(it))
+ //FORIT(kt, equalities)
+ for(EqualityMap::const_iterator kt =equalities.begin(); kt != equalities.end(); ++kt) {
Trace(tag) << " Eq class of t" << numbering[(*kt).first] << ": " << std::endl;
- FORIT(jt, (*kt).second) {
+
+ //FORIT(jt, (*kt).second)
+ const TNodeSet& kt_second = (*kt).second;
+ for(TNodeSet::const_iterator jt=kt_second.begin(); jt != kt_second.end(); ++jt) {
TNode S = (*jt);
if( S.getKind() != kind::UNION && S.getKind() != kind::INTERSECTION && S.getKind() != kind::SETMINUS) {
Trace(tag) << " " << *jt << ((*jt).getType().isSet() ? "\n": " ");
}
Trace(tag) << std::endl;
}
- FORIT(kt, disequalities) Trace(tag) << "NOT(t"<<numbering[(*kt).first]<<" = t" <<numbering[(*kt).second] <<")"<< std::endl;
- FORIT(kt, members) {
- if( (*kt).second.first.size() > 0) {
- Trace(tag) << "IN t" << numbering[(*kt).first] << ": ";
- FORIT(jt, (*kt).second.first) {
+ //FORIT(kt, disequalities)
+ for(TNodePairSet::const_iterator kt=disequalities.begin(); kt != disequalities.end(); ++kt){
+ Trace(tag) << "NOT(t"<<numbering[(*kt).first]<<" = t" <<numbering[(*kt).second] <<")"<< std::endl;
+ }
+ //FORIT(kt, members)
+ for(MemberMap::const_iterator kt=members.begin(); kt != members.end(); ++kt) {
+ const TNode& kt_key = (*kt).first;
+ const TNodeSet& kt_in_set = (*kt).second.first;
+ const TNodeSet& kt_out_set = (*kt).second.first;
+ if( kt_in_set.size() > 0) {
+ Trace(tag) << "IN t" << numbering[kt_key] << ": ";
+ //FORIT(jt, (*kt).second.first)
+ for(TNodeSet::const_iterator jt=kt_in_set.begin(); jt != kt_in_set.end(); ++jt) {
TNode x = (*jt);
if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
Trace(tag) << x << ", ";
}
Trace(tag) << std::endl;
}
- if( (*kt).second.second.size() > 0) {
- Trace(tag) << "NOT IN t" << numbering[(*kt).first] << ": ";
- FORIT(jt, (*kt).second.second) {
+ if( kt_out_set.size() > 0) {
+ Trace(tag) << "NOT IN t" << numbering[kt_key] << ": ";
+ //FORIT(jt, (*kt).second.second)
+ for(TNodeSet::const_iterator jt=kt_out_set.begin(); jt != kt_out_set.end(); ++jt){
TNode x = (*jt);
if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
Trace(tag) << x << ", ";
}
}
Trace(tag) << std::endl;
-#undef FORIT
+ //#undef FORIT
}
void TheorySetsPrivate::computeCareGraph() {
return cur;
}
}
-Node TheorySetsPrivate::elementsToShape(set<Node> elements, TypeNode setType) const
+
+Node TheorySetsPrivate::elementsToShape(std::set<Node> elements, TypeNode setType) const
{
NodeManager* nm = NodeManager::currentNM();
if(elements.size() == 0) {
return nm->mkConst<EmptySet>(EmptySet(nm->toType(setType)));
} else {
- typeof(elements.begin()) it = elements.begin();
+ std::set<Node>::const_iterator it = elements.begin();
Node cur = SINGLETON(*it);
while( ++it != elements.end() ) {
cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
Trace("sets-model") << "[sets-model] collectModelInfo(..., fullModel="
<< (fullModel ? "true)" : "false)") << std::endl;
- set<Node> terms;
+ std::set<Node> terms;
NodeManager* nm = NodeManager::currentNM();
// // this is for processCard -- commenting out for now
// if(Debug.isOn("sets-card")) {
- // for(typeof(d_cardTerms.begin()) it = d_cardTerms.begin();
+ // for(CDNodeSet::const_iterator it = d_cardTerms.begin();
// it != d_cardTerms.end(); ++it) {
// Debug("sets-card") << "[sets-card] " << *it << " = "
// << d_external.d_valuation.getModelValue(*it)
//processCard2 begin
if(Debug.isOn("sets-card")) {
- for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
+ for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) {
Node n = nm->mkNode(kind::CARD, *it);
Debug("sets-card") << "[sets-card] " << n << " = ";
// if(d_external.d_sharedTerms.find(n) == d_external.d_sharedTerms.end()) continue;
//processCard2 begin
leaves.clear();
- for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it)
+ for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it)
if(d_E.find(*it) == d_E.end())
leaves.insert(*it);
d_statistics.d_numLeaves.setData(leaves.size());
}
const CDNodeSet& terms = (d_termInfoManager->d_terms);
- for(typeof(terms.key_begin()) it = terms.key_begin(); it != terms.key_end(); ++it) {
+ for(CDNodeSet::key_iterator it = terms.key_begin(); it != terms.key_end(); ++it) {
Node node = (*it);
Kind k = node.getKind();
if(k == kind::UNION && node[0].getKind() == kind::SINGLETON ) {
void TheorySetsPrivate::presolve() {
- for(typeof(d_termInfoManager->d_terms.begin()) it = d_termInfoManager->d_terms.begin();
+ for(CDNodeSet::const_iterator it = d_termInfoManager->d_terms.begin();
it != d_termInfoManager->d_terms.end(); ++it) {
d_relTerms.insert(*it);
}
if(Trace.isOn("sets-relterms")) {
Trace("sets-relterms") << "[sets-relterms] ";
- for(typeof(d_relTerms.begin()) it = d_relTerms.begin();
+ for(CDNodeSet::const_iterator it = d_relTerms.begin();
it != d_relTerms.end(); ++it ) {
Trace("sets-relterms") << (*it) << ", ";
}
}
}
-TheorySetsPrivate::TermInfoManager::TermInfoManager
-(TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
- d_theory(theory),
- d_context(satContext),
- d_eqEngine(eq),
- d_terms(satContext),
- d_info()
-{ }
+TheorySetsPrivate::TermInfoManager::TermInfoManager(
+ TheorySetsPrivate& theory, context::Context* satContext,
+ eq::EqualityEngine* eq)
+ : d_theory(theory),
+ d_context(satContext),
+ d_eqEngine(eq),
+ d_terms(satContext),
+ d_info() {}
TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
- for( typeof(d_info.begin()) it = d_info.begin();
- it != d_info.end(); ++it) {
+ for (SetsTermInfoMap::iterator it = d_info.begin(); it != d_info.end();
+ ++it) {
delete (*it).second;
}
}
d_theory.registerCard(CARD(n));
}
- typeof(d_info.begin()) ita = d_info.find(d_eqEngine->getRepresentative(n[i]));
+ SetsTermInfoMap::iterator ita = d_info.find(d_eqEngine->getRepresentative(n[i]));
Assert(ita != d_info.end());
CDTNodeList* l = (*ita).second->elementsNotInThisSet;
- for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+ for(CDTNodeList::const_iterator it = l->begin(); it != l->end(); ++it) {
d_theory.d_settermPropagationQueue.push_back( std::make_pair( (*it), n ) );
}
l = (*ita).second->elementsInThisSet;
- for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+ for(CDTNodeList::const_iterator it = l->begin(); it != l->end(); ++it) {
d_theory.d_settermPropagationQueue.push_back( std::make_pair( (*it), n ) );
}
}
// propagation : parents
const CDTNodeList* parentList = getParents(S);
- for(typeof(parentList->begin()) k = parentList->begin();
+ for(CDTNodeList::const_iterator k = parentList->begin();
k != parentList->end(); ++k) {
d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
}// propagation : parents
<< ", b: " << d_eqEngine->getRepresentative(b)
<< std::endl;
- typeof(d_info.begin()) ita = d_info.find(a);
- typeof(d_info.begin()) itb = d_info.find(b);
+ SetsTermInfoMap::iterator ita = d_info.find(a);
+ SetsTermInfoMap::iterator itb = d_info.find(b);
Assert(ita != d_info.end());
Assert(itb != d_info.end());
d_theory.d_modelCache.clear();
}
-Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n)
-{
- if(d_terms.find(n) == d_terms.end()) {
+Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n) {
+ if (d_terms.find(n) == d_terms.end()) {
return Node();
}
Assert(n.getType().isSet());
- set<Node> elements, elements_const;
+ std::set<Node> elements;
+ std::set<Node> elements_const;
Node S = d_eqEngine->getRepresentative(n);
- typeof(d_theory.d_modelCache.begin()) it = d_theory.d_modelCache.find(S);
- if(it != d_theory.d_modelCache.end()) {
+ context::CDHashMap<Node, Node, NodeHashFunction>::const_iterator it =
+ d_theory.d_modelCache.find(S);
+ if (it != d_theory.d_modelCache.end()) {
return (*it).second;
}
const CDTNodeList* l = getMembers(S);
- for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+ for (CDTNodeList::const_iterator it = l->begin(); it != l->end(); ++it) {
TNode n = *it;
elements.insert(d_eqEngine->getRepresentative(n));
}
- BOOST_FOREACH(TNode e, elements) {
- if(e.isConst()) {
+ for(std::set<Node>::iterator it = elements.begin(); it != elements.end(); it++) {
+ TNode e = *it;
+ if (e.isConst()) {
elements_const.insert(e);
} else {
Node eModelValue = d_theory.d_external.d_valuation.getModelValue(e);
- if( eModelValue.isNull() ) return eModelValue;
+ if (eModelValue.isNull()) {
+ return eModelValue;
+ }
elements_const.insert(eModelValue);
}
}
return v;
}
-
-
-
/********************** Cardinality ***************************/
/********************** Cardinality ***************************/
/********************** Cardinality ***************************/
cardCreateEmptysetSkolem(t);
}
- for(typeof(d_termInfoManager->d_terms.begin()) it = d_termInfoManager->d_terms.begin();
+ for(CDNodeSet::const_iterator it = d_termInfoManager->d_terms.begin();
it != d_termInfoManager->d_terms.end(); ++it) {
Node n = (*it);
if(n.getKind() == kind::SINGLETON) {
// introduce cardinality of any set-term containing this term
NodeManager* nm = NodeManager::currentNM();
const CDTNodeList* parentList = d_termInfoManager->getParents(node[0]);
- for(typeof(parentList->begin()) it = parentList->begin();
+ for(CDTNodeList::const_iterator it = parentList->begin();
it != parentList->end(); ++it) {
registerCard(nm->mkNode(kind::CARD, *it));
}
edgesFd.clear();
edgesBk.clear();
disjoint.clear();
-
- for(typeof(d_processedCardPairs.begin()) it = d_processedCardPairs.begin();
- it != d_processedCardPairs.end(); ++it) {
+
+ for (std::map<std::pair<Node, Node>, bool>::const_iterator it =
+ d_processedCardPairs.begin();
+ it != d_processedCardPairs.end(); ++it) {
Node s = (it->first).first;
Assert(Rewriter::rewrite(s) == s);
Node t = (it->first).second;
tMs = Rewriter::rewrite(tMs);
edgesFd[s].insert(sNt);
- edgesFd[s].insert(sMt);
+ edgesFd[s].insert(sMt);
edgesBk[sNt].insert(s);
edgesBk[sMt].insert(s);
if(hasUnion) {
Node sUt = nm->mkNode(kind::UNION, s, t);
sUt = Rewriter::rewrite(sUt);
-
+
edgesFd[sUt].insert(sNt);
edgesFd[sUt].insert(sMt);
edgesFd[sUt].insert(tMs);
disjoint.insert(make_pair(sMt, tMs));
}
- if(Debug.isOn("sets-card-graph")) {
+ if (Debug.isOn("sets-card-graph")) {
Debug("sets-card-graph") << "[sets-card-graph] Fd:" << std::endl;
- for(typeof(edgesFd.begin()) it = edgesFd.begin();
- it != edgesFd.end(); ++it) {
- Debug("sets-card-graph") << "[sets-card-graph] " << (it->first) << std::endl;
- for(typeof( (it->second).begin()) jt = (it->second).begin();
- jt != (it->second).end(); ++jt) {
- Debug("sets-card-graph") << "[sets-card-graph] " << (*jt) << std::endl;
+ for (std::map<TNode, std::set<TNode> >::const_iterator it = edgesFd.begin();
+ it != edgesFd.end(); ++it) {
+ Debug("sets-card-graph") << "[sets-card-graph] " << (it->first)
+ << std::endl;
+ for (std::set<TNode>::const_iterator jt = (it->second).begin();
+ jt != (it->second).end(); ++jt) {
+ Debug("sets-card-graph") << "[sets-card-graph] " << (*jt)
+ << std::endl;
}
}
Debug("sets-card-graph") << "[sets-card-graph] Bk:" << std::endl;
- for(typeof(edgesBk.begin()) it = edgesBk.begin();
- it != edgesBk.end(); ++it) {
- Debug("sets-card-graph") << "[sets-card-graph] " << (it->first) << std::endl;
- for(typeof( (it->second).begin()) jt = (it->second).begin();
- jt != (it->second).end(); ++jt) {
- Debug("sets-card-graph") << "[sets-card-graph] " << (*jt) << std::endl;
+ for (std::map<TNode, std::set<TNode> >::const_iterator it = edgesBk.begin();
+ it != edgesBk.end(); ++it) {
+ Debug("sets-card-graph") << "[sets-card-graph] " << (it->first)
+ << std::endl;
+ for (std::set<TNode>::const_iterator jt = (it->second).begin();
+ jt != (it->second).end(); ++jt) {
+ Debug("sets-card-graph") << "[sets-card-graph] " << (*jt)
+ << std::endl;
}
}
}
-
-
leaves.clear();
-
- for(typeof(d_processedCardTerms.begin()) it = d_processedCardTerms.begin();
+
+ for(CDNodeSet::const_iterator it = d_processedCardTerms.begin();
it != d_processedCardTerms.end(); ++it) {
Node n = (*it)[0];
if( edgesFd.find(n) == edgesFd.end() ) {
Node TheorySetsPrivate::eqemptySoFar() {
std::vector<Node> V;
- for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
+ for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) {
Node rep = d_equalityEngine.getRepresentative(*it);
if(rep.getKind() == kind::EMPTYSET) {
V.push_back(EQUAL(rep, (*it)));
std::string tag = "sets-graph";
if(Trace.isOn("sets-graph")) {
Trace(tag) << "[sets-graph] Graph : " << std::endl;
- for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
+ for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) {
TNode v = *it;
// BOOST_FOREACH(TNode v, d_V) {
Trace(tag) << "[" << tag << "] " << v << " : ";
if(Trace.isOn("sets-graph-dot")) {
std::ostringstream oss;
oss << "digraph G { ";
- for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
+ for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) {
TNode v = *it;
if(d_E.find(v) != d_E.end()) {
BOOST_FOREACH(TNode w, d_E[v].get()) {
// Guess leaf nodes being empty or non-empty
NodeManager* nm = NodeManager::currentNM();
leaves.clear();
- for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
+ for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) {
TNode v = *it;
if(d_E.find(v) == d_E.end()) {
leaves.insert(v);
numLeavesCurrentlyNonEmpty = 0,
numLemmaAlreadyExisted = 0;
- for(typeof(leaves.begin()) it = leaves.begin(); it != leaves.end(); ++it) {
+ for(std::set<TNode>::iterator it = leaves.begin(); it != leaves.end(); ++it) {
bool generateLemma = true;
Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType((*it).getType())));
NodeManager* nm = NodeManager::currentNM();
// Introduce
- for(typeof(d_cardTerms.begin()) it = d_cardTerms.begin();
+ for(CDNodeSet::const_iterator it = d_cardTerms.begin();
it != d_cardTerms.end(); ++it) {
for(eq::EqClassIterator j(d_equalityEngine.getRepresentative((*it)[0]), &d_equalityEngine);
// merge_nodes(get_leaves(np.first), get_leaves(np.second), EQUAL(np.first, np.second));
merge_nodes(get_leaves(np.first), get_leaves(np.second), eqSoFar());
}
-
+
if(d_newLemmaGenerated) {
Trace("sets-card") << "[sets-card] New merge done. Returning." << std::endl;
return;
}
leaves.clear();
- for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
+ for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) {
TNode v = *it;
if(d_E.find(v) == d_E.end()) {
leaves.insert(v);
}
}
+ typedef std::set<TNode>::const_iterator TNodeSetIterator;
+
// Elements being either equal or disequal [Members Arrangement rule]
- Trace("sets-card") << "[sets-card] Processing elements equality/disequal to each other" << std::endl;
- for(typeof(leaves.begin()) it = leaves.begin();
- it != leaves.end(); ++it) {
- if(!d_equalityEngine.hasTerm(*it)) continue;
+ Trace("sets-card")
+ << "[sets-card] Processing elements equality/disequal to each other"
+ << std::endl;
+ for (TNodeSetIterator it = leaves.begin(); it != leaves.end(); ++it) {
+ if (!d_equalityEngine.hasTerm(*it)) continue;
Node n = d_equalityEngine.getRepresentative(*it);
Assert(n.getKind() == kind::EMPTYSET || leaves.find(n) != leaves.end());
- if(n != *it) continue;
+ 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) {
+ for (CDTNodeList::const_iterator 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)) {
+ for (TNodeSetIterator e1_it = elems.begin(); e1_it != elems.end();
+ ++e1_it) {
+ for (TNodeSetIterator 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));
lemma(lem, SETS_LEMMA_GRAPH);
// Assert Lower bound
Trace("sets-card") << "[sets-card] Processing assert lower bound" << std::endl;
- for(typeof(leaves.begin()) it = leaves.begin();
- it != leaves.end(); ++it) {
+ for(TNodeSetIterator it = leaves.begin(); it != leaves.end(); ++it) {
Trace("sets-cardlower") << "[sets-cardlower] Card Lower: " << *it << std::endl;
Assert(d_equalityEngine.hasTerm(*it));
Node n = d_equalityEngine.getRepresentative(*it);
// 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) {
+ for(CDTNodeList::const_iterator 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, *it)) );
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) {
+ for(TNodeSetIterator e1_it = elems.begin(); e1_it != elems.end(); ++e1_it) {
+ for(TNodeSetIterator 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) {
+ for(TNodeSetIterator e_it = elems.begin(); e_it != elems.end(); ++e_it) {
nb << nm->mkNode(kind::NOT, nm->mkNode(kind::MEMBER, *e_it, *it));
}
Node lem = Node(nb);
projects / cvc5.git / commitdiff