Предположим, у меня есть 2 массива в формуле, выполнимость которых я хочу проверить, используя z3. Если z3 возвращает sat, я хочу прочитать первый массив в модели z3 и довольно распечатать его как ключ, пару значений и значение по умолчанию. Позже я хочу преобразовать его в карту и провести дальнейший анализ. Вот пример, который я запускаю:
void find_model_example_arr() {
std::cout << "find_model_example_involving_array\n";
context c;
sort arr_sort = c.array_sort(c.int_sort(), c.int_sort());
expr some_array_1 = c.constant("some_array_1", arr_sort);
expr some_array_2 = c.constant("some_array_2", arr_sort);
solver s(c);
s.add(select(some_array_1, 0) > 0);
s.add(select(some_array_2, 5) < -4);
std::cout << s.check() << "\n";
model m = s.get_model();
std::cout << m << "\n";
expr some_array_1_eval = m.eval(some_array_1);
std::cout << "\nsome_array_1_eval = " << some_array_1_eval << "\n";
func_decl some_array_1_eval_func_decl = some_array_1_eval.decl();
std::cout << "\nThe Z3 expr(fun_decl) for some_array_1_eval is : " << some_array_1_eval_func_decl << "\n";
// ERROR here
func_interp fun_interp = m.get_func_interp(some_array_1_eval_func_decl);
// This works well
//func_interp fun_interp = m.get_func_interp(m.get_func_decl(0));
std::cout << "\nThe Z3 expr(fun_interp) for the array is : " << fun_interp << "\n";
unsigned num_entries = fun_interp.num_entries();
for(unsigned i = 0; i < num_entries; i++)
{
z3::func_entry entry = fun_interp.entry(i);
z3::expr k = entry.arg(0);
z3::expr v = entry.value();
std::cout << "\n(key,value): (" << k << "," << v << ")";
}
z3::expr default_value = fun_interp.else_value();
std::cout << "\nDefault value:" << default_value;
}
Я получаю следующий вывод:
find_model_example_involving_array
sat
(define-fun some_array_1 () (Array Int Int)
(_ as-array k!0))
(define-fun some_array_2 () (Array Int Int)
(_ as-array k!1))
(define-fun k!0 ((x!1 Int)) Int
(ite (= x!1 0) 1
1))
(define-fun k!1 ((x!1 Int)) Int
(ite (= x!1 5) (- 5)
(- 5)))
some_array_1_eval = (_ as-array k!0)
The Z3 expr(fun_decl) for some_array_1_eval is :
(declare-fun as-array () (Array Int Int))
unexpected error: invalid argument
Вместо этого, если я закомментирую первую строку и использую вторую, т.е. использую следующий блок кода:
// ERROR here
// func_interp fun_interp = m.get_func_interp(some_array_1_eval_func_decl);
// This works well
func_interp fun_interp = m.get_func_interp(m.get_func_decl(0));
Я получаю вывод, который ищу:
(key,value): (0,1)
Default value:1
Вот в чем проблема? Как мне выяснить, что m.get_func_decl (0) — это тот, который соответствует some_array_1? Например, если я использую m.get_func_decl (1), я получаю неправильные пары (ключ, значение). Другими словами, как я могу получить func_interp массива (определенного как выражение z3) из модели?
Представление для моделей массива действительно немного сбивает с толку. Значение
(define-fun some_array_1 () (Array Int Int)
(_ as-array k!0))
является то, что модель для массива some_array_1
это функция k!0
который должен интерпретироваться как массив (обозначенный вызовом as-array
, Последняя является параметрической функцией, которая не имеет аргументов, поэтому, чтобы получить фактическое определение функции модели для some_array_1, мы должны посмотреть, какая функция as-array
звонки. В данном примере мы можем сделать это следующим образом, сначала убедившись, что у нас действительно есть модель массива в ожидаемом формате, проверив несколько утверждений:
assert(Z3_get_decl_kind(c, some_array_1_eval_func_decl) == Z3_OP_AS_ARRAY);
assert(Z3_is_app(c, some_array_1_eval));
assert(Z3_get_decl_num_parameters(c, some_array_1_eval_func_decl) == 1);
assert(Z3_get_decl_parameter_kind(c, some_array_1_eval_func_decl, 0) ==
Z3_PARAMETER_FUNC_DECL);
func_decl model_fd = func_decl(c,
Z3_get_decl_func_decl_parameter(c, some_array_1_eval_func_decl, 0));
Объявление функции model_fd
затем содержит фактическую функцию, назначенную моделью (k!0
) и мы можем получить интерпретацию функции через
func_interp fun_interp = m.get_func_interp(model_fd);
Других решений пока нет …