Home
last modified time | relevance | path

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

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith3.cpp1192 Expr isolatedMonomial = right; in isolateVariable() local
1195 isolatedMonomial = pickMonomial(right); in isolateVariable()
1199 if (isMult(isolatedMonomial)) { in isolateVariable()
1204 isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS(); in isolateVariable()
1266 isolatedMonomial.toString()); in lessThanVar()
1268 separateMonomial(isolatedMonomial, c, var0); in lessThanVar()
1372 Expr isolatedMonomial = in projectInequalities() local
1648 Expr isolatedMonomial = right[1]; in pickMonomial() local
1653 if(lessThanVar(isolatedMonomial,*i)) in pickMonomial()
1654 isolatedMonomial = *i; in pickMonomial()
[all …]
H A Dtheory_arith_old.cpp1542 Expr isolatedMonomial = right; in isolateVariable() local
1545 isolatedMonomial = pickMonomial(right); in isolateVariable()
1552 alreadyProjected[e] = isolatedMonomial; in isolateVariable()
1556 if (isMult(isolatedMonomial)) { in isolateVariable()
1561 isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS(); in isolateVariable()
1627 isolatedMonomial.toString()); in lessThanVar()
1629 separateMonomial(isolatedMonomial, c, var0); in lessThanVar()
2023 Expr isolatedMonomial = right[1]; in pickMonomial() local
2028 if(lessThanVar(isolatedMonomial,*i)) in pickMonomial()
2029 isolatedMonomial = *i; in pickMonomial()
[all …]
H A Dtheory_arith_new.cpp932 bool TheoryArithNew::lessThanVar(const Expr& isolatedMonomial, const Expr& var2) in lessThanVar() argument
934 DebugAssert(!isRational(var2) && !isRational(isolatedMonomial), in lessThanVar()
936 isolatedMonomial.toString()); in lessThanVar()
938 separateMonomial(isolatedMonomial, c, var0); in lessThanVar()