Searched refs:inferSubstitution (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | extended_rewrite.h | 222 bool inferSubstitution(Node n,
|
| H A D | extended_rewrite.cpp | 447 inferSubstitution(n[0], vars, subs, true); in extendedRewriteIte()
1020 if (inferSubstitution(eq, vars, subs)) in extendedRewriteEqRes()
1562 bool ExtendedRewriter::inferSubstitution(Node n, in inferSubstitution() function in CVC4::theory::quantifiers::ExtendedRewriter
1572 bool cret = inferSubstitution(nc, vars, subs, usePred); in inferSubstitution()
|