Searched refs:d_simplifiedThm (Results 1 – 4 of 4) sorted by relevance
106 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()
84 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()
57 CDO<Theorem> d_simplifiedThm; variable
127 CDO<Theorem> d_simplifiedThm; variable