Searched refs:compactNonLinear (Results 1 – 1 of 1) sorted by relevance
1250 Expr compactNonLinear; in addToBuffer() local1268 compactNonLinear = compactNonLinearThm.getRHS(); in addToBuffer()1279 compactNonLinear = rhs; in addToBuffer()1280 compactNonLinearThm = reflexivityRule(compactNonLinear); in addToBuffer()1293 if (nonLinear && (isMult(rhs) || compactNonLinear != rhs)) { in addToBuffer()1294 TRACE("arith nonlinear", "compact version of ", rhs, " is " + compactNonLinear.toString()); in addToBuffer()1296 Theorem thm1 = (compactNonLinear != rhs ? in addToBuffer()1299 Rational c = (isMult(rhs) ? 0 : compactNonLinear[0].getRational()); in addToBuffer()