Home
last modified time | relevance | path

Searched refs:ratsLTe (Results 1 – 3 of 3) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith3.cpp2206 CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e]; in findBounds() local
2207 for(unsigned int i=0; i<ratsLTe->size(); i++) { in findBounds()
2208 DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!"); in findBounds()
2209 Expr ineq = (*ratsLTe)[i].ineq().getExpr(); in findBounds()
H A Dtheory_arith_new.cpp1357 CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e]; in findBounds() local
1358 for(unsigned int i=0; i<ratsLTe->size(); i++) { in findBounds()
1359 DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!"); in findBounds()
1360 Expr ineq = (*ratsLTe)[i].ineq().getExpr(); in findBounds()
H A Dtheory_arith_old.cpp2789 CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e]; in findBounds() local
2790 for(unsigned int i=0; i<ratsLTe->size(); i++) { in findBounds()
2791 DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!"); in findBounds()
2792 Expr ineq = (*ratsLTe)[i].ineq().getExpr(); in findBounds()