| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | theory_arith3.cpp | 1455 Expr ineq1 = betaLTt.getExpr(); in normalizeProjectIneqs() local
1460 Theorem isIntBeta(isIntegerThm(ineq1[0])); in normalizeProjectIneqs()
1466 DebugAssert((isLE(ineq1) || isLT(ineq1)) && in normalizeProjectIneqs()
1477 Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1; in normalizeProjectIneqs()
1522 ineq1 = betaLTt.getExpr(); in normalizeProjectIneqs()
1533 Expr beta(ineq1[0]); in normalizeProjectIneqs()
1919 const Expr& ineq1(alphaLEax.getExpr()); in processFiniteInterval() local
1922 +ineq1.toString()); in processFiniteInterval()
1926 if(!isInteger(ineq1[0]) in processFiniteInterval()
1927 || !isInteger(ineq1[1]) in processFiniteInterval()
[all …]
|
| H A D | theory_arith_old.cpp | 1828 Expr ineq1 = betaLTt.getExpr(); in normalizeProjectIneqs() local
1833 Theorem isIntBeta(isIntegerThm(ineq1[0])); in normalizeProjectIneqs()
1839 DebugAssert((isLE(ineq1) || isLT(ineq1)) && in normalizeProjectIneqs()
1850 Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1; in normalizeProjectIneqs()
1895 ineq1 = betaLTt.getExpr(); in normalizeProjectIneqs()
1905 Expr beta(ineq1[0]); in normalizeProjectIneqs()
2375 const Expr& ineq1(alphaLEax.getExpr()); in processFiniteInterval() local
2378 +ineq1.toString()); in processFiniteInterval()
2382 if(!isInteger(ineq1[0]) in processFiniteInterval()
2383 || !isInteger(ineq1[1]) in processFiniteInterval()
[all …]
|
| H A D | theory_arith_new.cpp | 1170 const Expr& ineq1(alphaLEax.getExpr()); in processFiniteInterval() local
1172 DebugAssert(isLE(ineq1), "TheoryArithNew::processFiniteInterval: ineq1 = " in processFiniteInterval()
1173 +ineq1.toString()); in processFiniteInterval()
1177 if(!isInteger(ineq1[0]) in processFiniteInterval()
1178 || !isInteger(ineq1[1]) in processFiniteInterval()
1183 const Expr& ax = ineq1[1]; in processFiniteInterval()
1195 thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b))); in processFiniteInterval()
|
| H A D | arith_theorem_producer_old.cpp | 2114 Expr ineq1(leExpr(e+rat(c1), v)); in expandGrayShadow() local
2116 return newTheorem(ineq1 && ineq2, gThm.getAssumptionsRef(), pf); in expandGrayShadow()
3562 Expr ineq1(leExpr(e+rat(c1), v)); in expandGrayShadowRewrite() local
3564 return newRWTheorem(theShadow, ineq1 && ineq2, Assumptions::emptyAssump(), pf); in expandGrayShadowRewrite()
|
| /dports/science/dakota/dakota-6.13.0-release-public.src-UI/test/ |
| H A D | dakota_ampl_fma.in | 42 # response_descriptors = 'force' 'ineq1' 'energy' #s1,#s3,#s5,#s7
|
| /dports/math/yices/yices-2.6.2/src/mcsat/nra/ |
| H A D | nra_plugin.c | 503 term_t ineq1 = _o_yices_arith_geq_atom(arg, t); in nra_plugin_new_term_notify() local
507 prop->lemma(prop, ineq1); in nra_plugin_new_term_notify()
518 term_t ineq1 = _o_yices_arith_gt_atom(arg, t_1); in nra_plugin_new_term_notify() local
521 prop->lemma(prop, ineq1); in nra_plugin_new_term_notify()
|
| /dports/devel/llvm-cheri/llvm-project-37c49ff00e3eadce5d8703fdc4497f28458c64a8/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2863 isl_int * const *ineq1 = a; in cmp_ineq() local
2867 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2870 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| H A D | isl_map_simplify.c | 4637 __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2, in drop_div_and_try_again() argument
4640 if (ineq1 > ineq2) { in drop_div_and_try_again()
4641 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
4645 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
|
| /dports/devel/isl/isl-0.24/ |
| H A D | isl_convex_hull.c | 2862 isl_int * const *ineq1 = a; in cmp_ineq() local
2866 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2869 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| H A D | isl_map_simplify.c | 4756 __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2, in drop_div_and_try_again() argument
4759 if (ineq1 > ineq2) { in drop_div_and_try_again()
4760 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
4764 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
|
| /dports/math/barvinok/barvinok-0.41.5/isl/ |
| H A D | isl_convex_hull.c | 2862 isl_int * const *ineq1 = a; in cmp_ineq() local
2866 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2869 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| H A D | isl_map_simplify.c | 4756 __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2, in drop_div_and_try_again() argument
4759 if (ineq1 > ineq2) { in drop_div_and_try_again()
4760 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
4764 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
|
| /dports/devel/llvm-devel/llvm-project-f05c95f10fc1d8171071735af8ad3a9e87633120/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2862 isl_int * const *ineq1 = a; in cmp_ineq() local
2866 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2869 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| H A D | isl_map_simplify.c | 4756 __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2, in drop_div_and_try_again() argument
4759 if (ineq1 > ineq2) { in drop_div_and_try_again()
4760 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
4764 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
|
| /dports/devel/llvm12/llvm-project-12.0.1.src/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2862 isl_int * const *ineq1 = a; in cmp_ineq() local
2866 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2869 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| H A D | isl_map_simplify.c | 4756 __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2, in drop_div_and_try_again() argument
4759 if (ineq1 > ineq2) { in drop_div_and_try_again()
4760 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
4764 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
|
| /dports/devel/tinygo/tinygo-0.14.1/llvm-project/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2790 isl_int * const *ineq1 = a; in cmp_ineq() local
2794 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2797 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| H A D | isl_map_simplify.c | 4495 __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2, in drop_div_and_try_again() argument
4498 if (ineq1 > ineq2) { in drop_div_and_try_again()
4499 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
4503 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
|
| /dports/devel/wasi-compiler-rt12/llvm-project-12.0.1.src/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2862 isl_int * const *ineq1 = a; in cmp_ineq() local
2866 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2869 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| H A D | isl_map_simplify.c | 4756 __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2, in drop_div_and_try_again() argument
4759 if (ineq1 > ineq2) { in drop_div_and_try_again()
4760 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
4764 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
|
| /dports/devel/wasi-compiler-rt13/llvm-project-13.0.1.src/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2862 isl_int * const *ineq1 = a; in cmp_ineq() local
2866 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2869 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| H A D | isl_map_simplify.c | 4756 __isl_take isl_basic_map *bmap, int div, int ineq1, int ineq2, in drop_div_and_try_again() argument
4759 if (ineq1 > ineq2) { in drop_div_and_try_again()
4760 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
4764 isl_basic_map_drop_inequality(bmap, ineq1); in drop_div_and_try_again()
|
| /dports/devel/wasi-libcxx/llvm-project-13.0.1.src/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2862 isl_int * const *ineq1 = a; in cmp_ineq() local
2866 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2869 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| /dports/www/chromium-legacy/chromium-88.0.4324.182/third_party/llvm/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2861 isl_int * const *ineq1 = a; in cmp_ineq() local
2865 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2868 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|
| /dports/devel/llvm13/llvm-project-13.0.1.src/polly/lib/External/isl/ |
| H A D | isl_convex_hull.c | 2862 isl_int * const *ineq1 = a; in cmp_ineq() local
2866 cmp = isl_seq_cmp((*ineq1) + 1, (*ineq2) + 1, dim); in cmp_ineq()
2869 return isl_int_cmp((*ineq1)[0], (*ineq2)[0]); in cmp_ineq()
|