Я написал программу Z3 (начиная с test_capi.c), которая зацикливается на некотором числовом «параметре» и добавляет ограничения для каждого цикла цикла, которые зависят от ограничений предыдущего цикла. Идея состоит в том, что в каждом цикле выбираются 2 элемента a,d, которые будут либо теми же старыми a,d, либо новыми a,d, выбранными pointer_a, pointer_d из упорядоченных списков u_a, u_d.
Код работает для одних циклов, но не для других (дает сбой по сравнению с ошибкой сегментации). Более странно, что при смене кода меняется количество циклов, на которых работает код. Так что приведенный ниже код работает и является 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, и мне не повезло с другими большими числами. Цель состояла в том, чтобы довести его до параметра = 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
check. - person Jabberwocky schedule 04.03.2016