Home
last modified time | relevance | path

Searched refs:d_simplifiedThm (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/search/
H A Dsearch_simple.cpp106 d_simplifiedThm(core->getCM()->getCurrentContext()) in SearchSimple()
152 Theorem e_iff_e2(d_commonRules->iffContrapositive(d_simplifiedThm)); in checkValidMain()
185 d_simplifiedThm.set(d_core->getExprTrans()->preprocess(e.negate())); in checkValidInternal()
186 TRACE("search", "checkValid: simplifiedThm = ", d_simplifiedThm, ""); in checkValidInternal()
188 const Expr& not_e2 = d_simplifiedThm.get().getRHS(); in checkValidInternal()
225 Expr e2 = d_simplifiedThm.get().getRHS().negate(); in restartInternal()
H A Dsearch_fast.cpp84 d_simplifiedThm(core->getCM()->getCurrentContext()), in SearchEngineFast()
1678 Theorem e_iff_e2(d_commonRules->iffContrapositive(d_simplifiedThm)); in checkValidMain()
1720 d_simplifiedThm = d_core->getExprTrans()->preprocess(e.negate()); in checkValidInternal()
1721 TRACE("search", "checkValid: simplifiedThm = ", d_simplifiedThm, ""); in checkValidInternal()
1723 const Expr& not_e2 = d_simplifiedThm.get().getRHS(); in checkValidInternal()
1771 Expr e2 = d_simplifiedThm.get().getRHS().negate(); in restartInternal()
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dsearch_simple.h57 CDO<Theorem> d_simplifiedThm; variable
H A Dsearch_fast.h127 CDO<Theorem> d_simplifiedThm; variable