0

我编写了一个 Z3 程序（从 test_capi.c 开始），它在某个数字“参数”上循环，并为每个循环周期添加约束，这些约束取决于前一个循环的约束。这个想法是每个周期选择 2 项 a,d，这将是相同的旧 a,d 或新 a,d 由pointer_a、pointer_d 从有序列表 u_a、u_d 中选择。

该代码适用于某些循环计数，而不适用于其他循环计数（给出 sat 与分段错误）。更奇怪的是，代码工作的循环计数在更改代码时会发生变化。所以下面的代码有效并且是 SAT （我已经选择了 n_ABCD=check3 ），但它只给出了从 2 到 10 的“参数”的结果，除了 6 和参数 = 8、16、32 并且可能是一些其他数字，但我至少尝试过；它不适用于 31、33、64、128 和 512。当我将循环分成 2 个循环时，一个用于 pointer_a[] 和 pointer_d[] 约束，另一个用于 check_v 操作，代码适用于“参数”最多 9，然后是 12、14、17 和 27，我对其他更大的数字并不幸运。目标是将其运行到 parameter=1024 甚至更多。

关于为什么代码只能针对某些数字而不针对其他数字运行的任何解释？它与选择被评估的任意术语的工作方式有关吗？（make_var_feasible、update_and_pivot ......如下面的 gdb 跟踪）

char cated_string[20];
for(int i = 0; i< parameter; i++){

    sprintf(cated_string,"%s%d%s", "pointer_d[", i, "]");
    pointer_d[i] = mk_var(ctx, cated_string , bv32_sort);

    sprintf(cated_string,"%s%d%s", "pointer_a[", i, "]");
    pointer_a[i] = mk_var(ctx, cated_string , bv32_sort);

}

        u_d_ast       =  mk_var(ctx, "u_d_ast", array_sort);
        u_a_ast       =  mk_var(ctx, "u_a_ast", array_sort);

    for (unsigned int i = 0; i < parameter; i++) {index = Z3_mk_unsigned_int(ctx, i, bv32_sort);
        u_d_ast = Z3_mk_store(ctx, u_d_ast, index, u_d[i]);
        u_a_ast = Z3_mk_store(ctx, u_a_ast, index, u_a[i]);
    }

Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, pointer_d[0], n_zero) );
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, pointer_a[0], n_zero) );

a_v            =  mk_var(ctx, "a_v", array_sort); 
d_v            =  mk_var(ctx, "d_v", array_sort);
check_v        =  mk_var(ctx, "check_v" , array_sort); 
check_v        =  Z3_mk_store(ctx, check_v, n_zero, n_zero );
a_v            =  Z3_mk_store(ctx, a_v, n_zero, Z3_mk_select(ctx, u_a_ast, n_zero) ); 
d_v            =  Z3_mk_store(ctx, d_v, n_zero, Z3_mk_select(ctx, u_d_ast, n_zero) ); 

for (int i = 1; i< parameter; i++){
    ind   = Z3_mk_unsigned_int(ctx, i, bv32_sort);
    ind_1 = Z3_mk_unsigned_int(ctx, i-1, bv32_sort);

    check_old  = Z3_mk_select(ctx, check_v  , ind_1 );

    d_v   = Z3_mk_store(ctx, d_v, ind, Z3_mk_select(ctx, u_d_ast, pointer_d[i]) ); 
    d_new = Z3_mk_select(ctx, d_v , ind   );
    pointer_d_plus_1 = Z3_mk_bvadd(ctx, pointer_d[i-1], n_one);
    condition_d_pointer1[i] = Z3_mk_ge(ctx, Z3_mk_bv2int(ctx, pointer_d[i], false), Z3_mk_bv2int(ctx, pointer_d[i-1], false) );
    condition_d_pointer2[i] = Z3_mk_le(ctx, Z3_mk_bv2int(ctx, pointer_d[i], false), Z3_mk_bv2int(ctx, pointer_d_plus_1, false) );
    Z3_solver_assert(ctx, s, condition_d_pointer1[i]);
    Z3_solver_assert(ctx, s, condition_d_pointer2[i]);

    a_v   = Z3_mk_store(ctx, a_v, ind, Z3_mk_select(ctx, u_a_ast,  pointer_a[i]) ); 
    a_new = Z3_mk_select(ctx, a_v , ind   );
    pointer_a_plus_1 = Z3_mk_bvadd(ctx, pointer_a[i-1], n_one);
    condition_a_pointer1[i] = Z3_mk_ge(ctx, Z3_mk_bv2int(ctx, pointer_a[i], false), Z3_mk_bv2int(ctx, pointer_a[i-1], false) );
    condition_a_pointer2[i] = Z3_mk_le(ctx, Z3_mk_bv2int(ctx, pointer_a[i], false), Z3_mk_bv2int(ctx, pointer_a_plus_1, false) );
    Z3_solver_assert(ctx, s, condition_a_pointer1[i]);
    Z3_solver_assert(ctx, s, condition_a_pointer2[i]);

    d_xor_a         = Z3_mk_bvxor(ctx, d_new , a_new);
    check_new       = Z3_mk_bvxor(ctx, check_old, d_xor_a);
    check_v         = Z3_mk_store(ctx, check_v, ind, check_new);
}

check3 = Z3_mk_select(ctx, check_v , n_position );
eq = Z3_mk_eq(ctx, n_ABCD, check3);
Z3_solver_assert(ctx, s, eq ); 
check(ctx, s, Z3_L_TRUE);

尝试使用 gdb 运行失败的实例，它会给出以下消息：

Program received signal SIGSEGV, Segmentation fault.
0x00001blaab9fff68 in mpn_manager::div_normalize(unsigned int const*, unsigned long, unsigned int const*, unsigned long, mpn_manager::mpn_sbuffer&, mpn_manager::mpn_sbuffer&) const () from /lib/libz3.so
(gdb) backtrace
#0  0x00001blaab9ffd68 in mpn_manager::div_normalize(unsigned int const*, unsigned long, unsigned int const*, unsigned long, mpn_manager::mpn_sbuffer&, mpn_manager::mpn_sbuffer&) const () from /lib/libz3.so
#1  0x00001blaab9ffaf9 in mpn_manager::div(unsigned int const*, unsigned long, unsigned int const*, unsigned long, unsigned int*, unsigned int*) () from /lib/libz3.so
#2  0x00001blaab9e387e in void mpz_manager<true>::quot_rem_core<1>(mpz const&, mpz const&, mpz&, mpz&) () from /lib/libz3.so
#3  0x00001blaab9e4216 in mpz_manager<true>::rem(mpz const&, mpz const&, mpz&) () from /lib/libz3.so
#4  0x00001blaab9e4b71 in mpz_manager<true>::gcd(mpz const&, mpz const&, mpz&) () from /lib/libz3.so
#5  0x00001blaabdef04f in mpq_manager<true>::div(mpq const&, mpq const&, mpq&) () from /lib/libz3.so
#6  0x00001blaab139a0e in smt::theory_arith<smt::mi_ext>::update_and_pivot(int, int, rational const&, inf_rational const&) () from /lib/libz3.so
#7  0x00001blaab13a996 in smt::theory_arith<smt::mi_ext>::make_var_feasible(int) () from /lib/libz3.so
#8  0x00001blaab135aca in smt::theory_arith<smt::mi_ext>::make_feasible() () from /lib/libz3.so
#9  0x00001blaab136b13 in smt::theory_arith<smt::mi_ext>::propagate_core() () from /lib/libz3.so
#10 0x00001blaab22d9ad in smt::context::propagate() () from /lib/libz3.so
#11 0x00001blaab2328c0 in smt::context::bounded_search() () from /lib/libz3.so
#12 0x00001blaab231cd8 in smt::context::search() () from /lib/libz3.so
#13 0x00001blaab231b72 in smt::context::setup_and_check(bool) () from /lib/libz3.so
#14 0x00001blaaa10143f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#15 0x00001blaab665115 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#16 0x00001blaab65a333 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#17 0x00001blaab65a5ad in check_sat(tactic&, ref<goal>&, ref<model>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::string&) () from /lib/libz3.so
#18 0x00001blaab539703 in tactic2solver::check_sat_core(unsigned int, expr* const*) () from /lib/libz3.so
#19 0x00001blaab54208b in solver_na2as::check_sat(unsigned int, expr* const*) () from /lib/libz3.so
#20 0x00001blaab53d519 in combined_solver::check_sat(unsigned int, expr* const*) () from /lib/libz3.so
#21 0x00001blaaad73f8e in Z3_solver_check () from /lib/libz3.so
#22 0x0000000000402ce4 in check (ctx=0x622f48, s=0x66d948, expected_result=Z3_L_TRUE) at example.c:210
#23 0x0000000000405830 in main () at example.c:1129
4

1 回答 1

0

如此处：Check overflow with Z3 似乎问题是由于 Z3_mk_bv2int 损坏造成的。当我使用 mk_eq 然后 mk_or 而不是这些小于/大于或等于（或使用 gte、lte 的 bv 版本；即 Z3_mk_bvuge 和 Z3_mk_bvule）时，它适用于所有数字。

于 2016-03-08T15:30:06.067 回答