Searched refs:mightMatchOurIdentity (Results 1 – 7 of 7) sorted by relevance
230 if (topSymbol->leftId() && topSymbol->mightMatchOurIdentity(t0)) in analyseCollapses2()237 if (topSymbol->rightId() && topSymbol->mightMatchOurIdentity(t1)) in analyseCollapses2()
62 bool mightMatchOurIdentity(const Term* subterm) const;
181 BinarySymbol::mightMatchOurIdentity(const Term* subterm) const in mightMatchOurIdentity() function in BinarySymbol
1533 * binarySymbol.cc (mightMatchOurIdentity):2058 * binarySymbol.cc (mightMatchOurIdentity): use Term::leq() (2 places)2098 * binarySymbol.cc (mightMatchOurIdentity): use <=(Term*, Sort&)2282 * binarySymbol.cc (mightMatchOurIdentity): compare() replaced by equal()2299 * binarySymbol.cc (mightMatchOurIdentity): commented out assertion2302 (mightMatchOurIdentity): must return true if subterm is our2580 * binarySymbol.cc (mightMatchOurIdentity): added Assert to check2582 (mightMatchOurIdentity): return false if null identity because2596 * binarySymbol.cc (mightMatchOurIdentity): added2620 (class BinarySymbol): added decl for mightMatchOurIdentity()
382 if (idPossible(i) && s->mightMatchOurIdentity(t)) in analyseCollapses2()436 t.matchOurIdentity = s->mightMatchOurIdentity(t.term); in insertAbstractionVariables()
516 if (!(topSymbol->mightMatchOurIdentity(p.term))) in analyseCollapses2()570 p.matchOurIdentity = topSymbol->mightMatchOurIdentity(p.term); in insertAbstractionVariables()
4116 (mightMatchOurIdentity): deleted4117 (analyseCollapses): use BinarySymbol::mightMatchOurIdentity()4118 (insertAbstractionVariables): use BinarySymbol::mightMatchOurIdentity()4124 mightCollapseToOurSymbol() and mightMatchOurIdentity()4145 (mightMatchOurIdentity): added