Home
last modified time | relevance | path

Searched refs:betaLTt (Results 1 – 2 of 2) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith3.cpp1418 Theorem betaLTt, tLTalpha, thm; in projectInequalities() local
1423 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm; in projectInequalities()
1425 thm = normalizeProjectIneqs(betaLTt, tLTalpha); in projectInequalities()
1454 Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2; in normalizeProjectIneqs() local
1455 Expr ineq1 = betaLTt.getExpr(); in normalizeProjectIneqs()
1493 intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha, in normalizeProjectIneqs()
1521 betaLTt = canonPred(thm2); in normalizeProjectIneqs()
1522 ineq1 = betaLTt.getExpr(); in normalizeProjectIneqs()
1537 Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha); in normalizeProjectIneqs()
1544 processFiniteInterval(betaLTt, tLTalpha); in normalizeProjectIneqs()
[all …]
H A Dtheory_arith_old.cpp1781 Theorem betaLTt, tLTalpha, thm; in projectInequalities() local
1789 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm; in projectInequalities()
1792 thm = normalizeProjectIneqs(betaLTt, tLTalpha); in projectInequalities()
1827 Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2; in normalizeProjectIneqs() local
1828 Expr ineq1 = betaLTt.getExpr(); in normalizeProjectIneqs()
1866 intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha, in normalizeProjectIneqs()
1869 intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha, in normalizeProjectIneqs()
1894 betaLTt = canonPred(thm2); in normalizeProjectIneqs()
1895 ineq1 = betaLTt.getExpr(); in normalizeProjectIneqs()
1909 Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha); in normalizeProjectIneqs()
[all …]