Searched refs:d_totality_terms (Results 1 – 2 of 2) sorted by relevance
525 …if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].en… in newEqClass()1070 …if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].en… in addTotalityAxiom()1127 return d_totality_terms[0][i]; in getTotalityLemmaTerm()1293 if ((c - 1) < d_totality_terms[0].size()) in getCardinalityLiteral()1295 d_totality_terms[0][c - 1] = var; in getCardinalityLiteral()1299 d_totality_terms[0].push_back(var); in getCardinalityLiteral()1302 for (unsigned i = 1, size = d_totality_terms[0].size(); i < size; i++) in getCardinalityLiteral()1304 Node lem = var.eqNode(d_totality_terms[0][i - 1]).notNode(); in getCardinalityLiteral()
270 std::map< int, std::vector< Node > > d_totality_terms; variable