Searched refs:eqnThm (Results 1 – 3 of 3) sorted by relevance
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | theory_arith3.cpp | 437 Theorem eqnThm; in doSolve() local
441 eqnThm = thm; in doSolve()
444 eqnThm = canonPred(eqnThm); in doSolve()
448 Expr right = eqnThm.getRHS(); in doSolve()
451 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr())); in doSolve()
457 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr())); in doSolve()
458 right = eqnThm.getRHS(); in doSolve()
470 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); in doSolve()
473 Theorem res = iffMP(eqnThm, in doSolve()
480 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); in doSolve()
[all …]
|
| H A D | theory_arith_new.cpp | 336 Theorem eqnThm; in doSolve() local
340 eqnThm = thm; in doSolve()
342 eqnThm = iffMP(thm, d_rules->rightMinusLeft(e)); in doSolve()
343 eqnThm = canonPred(eqnThm); in doSolve()
347 Expr right = eqnThm.getRHS(); in doSolve()
350 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr())); in doSolve()
356 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr())); in doSolve()
357 right = eqnThm.getRHS(); in doSolve()
364 res = processRealEq(eqnThm); in doSolve()
366 res = symmetryRule(eqnThm); // Flip to e' = 0 in doSolve()
[all …]
|
| H A D | theory_arith_old.cpp | 453 Theorem eqnThm; in doSolve() local
457 eqnThm = thm; in doSolve()
460 eqnThm = canonPred(eqnThm); in doSolve()
464 Expr right = eqnThm.getRHS(); in doSolve()
467 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr())); in doSolve()
473 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr())); in doSolve()
475 right = eqnThm.getRHS(); in doSolve()
487 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); in doSolve()
490 Theorem res = iffMP(eqnThm, in doSolve()
497 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); in doSolve()
[all …]
|