Searched refs:pre_new_ret (Results 1 – 1 of 1) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | extended_rewrite.cpp | 83 Node pre_new_ret; in extendedRewrite() local
86 pre_new_ret = nm->mkNode(OR, ret[0].negate(), ret[1]); in extendedRewrite()
87 debugExtendedRewrite(ret, pre_new_ret, "IMPLIES elim"); in extendedRewrite()
91 pre_new_ret = nm->mkNode(EQUAL, ret[0].negate(), ret[1]); in extendedRewrite()
92 debugExtendedRewrite(ret, pre_new_ret, "XOR elim"); in extendedRewrite()
96 pre_new_ret = extendedRewriteNnf(ret); in extendedRewrite()
97 debugExtendedRewrite(ret, pre_new_ret, "NNF"); in extendedRewrite()
99 if (!pre_new_ret.isNull()) in extendedRewrite()
101 ret = extendedRewrite(pre_new_ret); in extendedRewrite()
104 << "...ext-pre-rewrite : " << n << " -> " << pre_new_ret << std::endl; in extendedRewrite()
|