Home
last modified time | relevance | path

Searched defs:ineqThm (Results 1 – 5 of 5) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith3.cpp1066 const Theorem& ineqThm = d_buffer[d_bufferIdx]; in processBuffer() local
1421 const Theorem& ineqThm = ineqEntry.ineq(); in projectInequalities() local
H A Dtheory_arith_old.cpp1048 Theorem ineqThm; in processBuffer() local
1784 … const Theorem& ineqThm = ineqEntry.ineq(); //inequalityToFind(ineqEntry.ineq(), isolatedVarOnRHS); in projectInequalities() local
H A Darith_theorem_producer.cpp3215 Theorem ArithTheoremProducer::nonLinearIneqSignSplit(const Theorem& ineqThm) { in nonLinearIneqSignSplit()
H A Darith_theorem_producer3.cpp3049 Theorem ArithTheoremProducer3::nonLinearIneqSignSplit(const Theorem& ineqThm) { in nonLinearIneqSignSplit()
H A Darith_theorem_producer_old.cpp3697 Theorem ArithTheoremProducerOld::nonLinearIneqSignSplit(const Theorem& ineqThm) { in nonLinearIneqSignSplit()