Searched refs:d_cardinality_literal (Results 1 – 2 of 2) sorted by relevance
516 for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); in newEqClass()517 it != d_cardinality_literal.end(); ++it ){ in newEqClass()1060 eqs.push_back(d_cardinality_literal[d_cardinality].notNode()); in addCliqueLemma()1073 Node cardLit = d_cardinality_literal[ cardinality ]; in addTotalityAxiom()1264 std::map<int, Node>::iterator itcl = d_cardinality_literal.find(c); in getCardinalityLiteral()1265 if (itcl != d_cardinality_literal.end()) in getCardinalityLiteral()1271 d_cardinality_literal[c] = lit; in getCardinalityLiteral()
272 std::map< int, Node > d_cardinality_literal; variable