| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_fvar_collector.c | 49 static term_t forall1(term_t var, term_t body) { in forall1() function
155 ivector_push(&all, forall1(a, yices_not(bin_app(q, a, a)))); in init_terms()
156 ivector_push(&all, forall1(b, yices_not(bin_app(q, a, a)))); in init_terms()
159 forall1(x, yices_arith_geq_atom(x, y))))); in init_terms()
|
| /dports/math/libpgmath/flang-d07daf3/tools/flang1/flang1exe/ |
| H A D | commopt.c | 350 int forall, forall1; in fuse_forall() local
433 int forall, forall1; in is_same_idx() local
450 forall1 = STD_AST(std1); in is_same_idx()
451 list1 = A_LISTG(forall1); in is_same_idx()
481 int forall1, forall2; in same_forall_size() local
498 forall1 = STD_AST(std1); in same_forall_size()
570 int forall1, forall2; in same_forall_bnds() local
587 forall1 = STD_AST(std1); in same_forall_bnds()
966 int forall, forall1; in is_fusable() local
1044 nd1 = A_OPT1G(forall1); in is_fusable()
[all …]
|
| H A D | vsub.c | 1675 int std1, forall1, forall2, orig_lhs; in scatter_dependency() local
1745 forall1 = mk_stmt(A_FORALL, 0); in scatter_dependency()
1746 A_LISTP(forall1, A_LISTG(forall)); in scatter_dependency()
1750 A_IFSTMTP(forall1, asn1); in scatter_dependency()
1751 add_stmt_before(forall1, std); in scatter_dependency()
1759 forall1 = make_forall(shape, dest, 0, 0); in scatter_dependency()
1760 ast2 = normalize_forall(forall1, ast, 0); in scatter_dependency()
1761 A_IFSTMTP(forall1, ast2); in scatter_dependency()
1762 A_IFEXPRP(forall1, 0); in scatter_dependency()
1763 std1 = add_stmt_before(forall1, std); in scatter_dependency()
[all …]
|
| H A D | commgen.c | 888 int forall1, fusedstd, asn1, header; in is_use_lhs_final() local
908 forall1 = STD_AST(header); in is_use_lhs_final()
909 if (forall != forall1) { in is_use_lhs_final()
910 asn1 = A_IFSTMTG(forall1); in is_use_lhs_final()
917 nd1 = A_OPT1G(forall1); in is_use_lhs_final()
920 forall1 = STD_AST(fusedstd); in is_use_lhs_final()
921 if (forall != forall1) { in is_use_lhs_final()
922 asn1 = A_IFSTMTG(forall1); in is_use_lhs_final()
|
| H A D | outconv.c | 3320 int forall, forall1; in is_same_mask_in_fused() local
3341 forall1 = STD_AST(fusedstd); in is_same_mask_in_fused()
3342 expr1 = A_IFEXPRG(forall1); in is_same_mask_in_fused()
3371 forall1 = STD_AST(fusedstd); in is_same_mask_in_fused()
3372 A_IFEXPRP(forall1, 0); in is_same_mask_in_fused()
|
| H A D | comm.c | 861 int forall1; in un_fuse() local
869 forall1 = STD_AST(fusedstd); in un_fuse()
870 nd1 = A_OPT1G(forall1); in un_fuse()
|
| /dports/math/boolector/boolector-3.2.2/test/ |
| H A D | test_normquant.cpp | 182 BtorNode *forall0, *forall1, *exists, *x[3], *_and; in TEST_F() local
194 forall1 = btor_node_invert (btor_exp_forall (d_btor, x[2], exists)); in TEST_F()
204 result = btor_normalize_quantifiers_node (d_btor, forall1); in TEST_F()
213 btor_node_release (d_btor, forall1); in TEST_F()
240 BtorNode *expected, *forall0, *forall1, *_or, *X, *Y[2], *ugte, *ulte; in TEST_F() local
261 forall1 = btor_exp_forall (d_btor, Y[1], ugte); in TEST_F()
262 _or = btor_exp_bv_and (d_btor, forall0, forall1); in TEST_F()
283 btor_node_release (d_btor, forall1); in TEST_F()
|