Home
last modified time | relevance | path

Searched refs:tLTalpha (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
1424 tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm; in projectInequalities()
1425 thm = normalizeProjectIneqs(betaLTt, tLTalpha); in projectInequalities()
1454 Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2; in normalizeProjectIneqs() local
1456 Expr ineq2 = tLTalpha.getExpr(); in normalizeProjectIneqs()
1493 intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha, in normalizeProjectIneqs()
1527 tLTalpha = canonPred(thm2); in normalizeProjectIneqs()
1528 ineq2 = tLTalpha.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
1790 tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm; in projectInequalities()
1792 thm = normalizeProjectIneqs(betaLTt, tLTalpha); in projectInequalities()
1827 Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2; in normalizeProjectIneqs() local
1829 Expr ineq2 = tLTalpha.getExpr(); in normalizeProjectIneqs()
1866 intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha, in normalizeProjectIneqs()
1869 intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha, in normalizeProjectIneqs()
1899 tLTalpha = canonPred(thm2); in normalizeProjectIneqs()
1900 ineq2 = tLTalpha.getExpr(); in normalizeProjectIneqs()
1909 Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha); in normalizeProjectIneqs()
[all …]