| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | theory_arith_old.cpp | 817 separateMonomial(lhs, a, x); in processSimpleIntEq()
1192 separateMonomial(monomial, c, m); in updateStats()
1630 separateMonomial(var2, c, var1); in lessThanVar()
2040 separateMonomial(*i, c, var); in pickMonomial()
2764 separateMonomial(varSide, c, x); in findRationalBound()
5422 separateMonomial(t, c, v); in getUpperBound()
5494 separateMonomial(t, c, v); in getLowerBound()
5725 separateMonomial(t, c, v); in isConstrainedAbove()
5776 separateMonomial(t, c, v); in isConstrainedBelow()
5905 separateMonomial(t, c, var); in isUnconstrained()
[all …]
|
| H A D | theory_arith3.cpp | 779 separateMonomial(right[1], c, x); in processSimpleIntEq()
837 separateMonomial(lhs, a, x); in processSimpleIntEq()
842 separateMonomial(rhs, c, v); in processSimpleIntEq()
852 separateMonomial(*i, c, v); in processSimpleIntEq()
1121 separateMonomial(monomial, c, m); in updateStats()
1268 separateMonomial(isolatedMonomial, c, var0); in lessThanVar()
1269 separateMonomial(var2, c, var1); in lessThanVar()
1376 separateMonomial(isolatedMonomial, a, monomialVar); in projectInequalities()
1458 separateMonomial(ineq2[0], c, x); in normalizeProjectIneqs()
1665 separateMonomial(*i, c, var); in pickMonomial()
[all …]
|
| H A D | theory_arith_new.cpp | 524 separateMonomial(right, c, x); in processSimpleIntEq()
534 separateMonomial(right[1], c, x); in processSimpleIntEq()
593 separateMonomial(lhs, a, x); in processSimpleIntEq()
598 separateMonomial(rhs, c, v); in processSimpleIntEq()
608 separateMonomial(*i, c, v); in processSimpleIntEq()
824 separateMonomial(monomial, c, m); in updateStats()
938 separateMonomial(isolatedMonomial, c, var0); in lessThanVar()
939 separateMonomial(var2, c, var1); in lessThanVar()
944 void TheoryArithNew::separateMonomial(const Expr& e, Expr& c, Expr& var) { in separateMonomial() function in TheoryArithNew
1335 separateMonomial(varSide, c, x); in findRationalBound()
|
| H A D | arith_theorem_producer_old.cpp | 1855 d_theoryArith->separateMonomial(ax, a_expr, x); in darkGrayShadow2ab()
1856 d_theoryArith->separateMonomial(bx, b_expr, x); in darkGrayShadow2ab()
1949 d_theoryArith->separateMonomial(ax, a_expr, x); in darkGrayShadow2ba()
1950 d_theoryArith->separateMonomial(bx, b_expr, x); in darkGrayShadow2ba()
2200 d_theoryArith->separateMonomial(ax, aExpr, x); in grayShadowConst()
2319 d_theoryArith->separateMonomial(right, aExpr, x); in intVarEqnConst()
2324 d_theoryArith->separateMonomial(right[1], aExpr, x); in intVarEqnConst()
2721 d_theoryArith->separateMonomial(lhs, a, x); in eqElimIntRule()
2740 d_theoryArith->separateMonomial(rhs, c, v); in eqElimIntRule()
2756 d_theoryArith->separateMonomial(rhs[i+1], c, v); in eqElimIntRule()
|
| H A D | arith_theorem_producer.cpp | 2040 d_theoryArith->separateMonomial(ax, aExpr, x); in grayShadowConst()
2160 d_theoryArith->separateMonomial(right, aExpr, x); in intVarEqnConst()
2165 d_theoryArith->separateMonomial(right[1], aExpr, x); in intVarEqnConst()
2544 d_theoryArith->separateMonomial(lhs, a, x); in eqElimIntRule()
2563 d_theoryArith->separateMonomial(rhs, c, v); in eqElimIntRule()
2579 d_theoryArith->separateMonomial(rhs[i+1], c, v); in eqElimIntRule()
|
| H A D | arith_theorem_producer3.cpp | 1998 d_theoryArith->separateMonomial(ax, aExpr, x); in grayShadowConst()
2117 d_theoryArith->separateMonomial(right, aExpr, x); in intVarEqnConst()
2122 d_theoryArith->separateMonomial(right[1], aExpr, x); in intVarEqnConst()
2519 d_theoryArith->separateMonomial(lhs, a, x); in eqElimIntRule()
2538 d_theoryArith->separateMonomial(rhs, c, v); in eqElimIntRule()
2554 d_theoryArith->separateMonomial(rhs[i+1], c, v); in eqElimIntRule()
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | theory_arith3.h | 231 void separateMonomial(const Expr& e, Expr& c, Expr& var);
|
| H A D | theory_arith.h | 126 virtual void separateMonomial(const Expr& e, Expr& c, Expr& var) = 0;
|
| H A D | theory_arith_new.h | 187 void separateMonomial(const Expr& e, Expr& c, Expr& var);
|
| H A D | theory_arith_old.h | 255 void separateMonomial(const Expr& e, Expr& c, Expr& var);
|