Czytaj func interp tablicy z3 z modelu z3

Question

Załóżmy, że mam 2 tablice w formule, której sprawdzalność chcę sprawdzić przy użyciu Z3. Jeśli z3 zwraca sat, chcę przeczytać w pierwszej tablicy w modelu z3 i całkiem wydrukować go jako klucz, parę wartości i wartość domyślną. Później chcę przekonwertować go na mapę i przeprowadzić dalszą analizę. Oto przykład uruchomić:

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; 
} 

pojawia się następujący komunikat:

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 

Zamiast gdybym wykomentuj pierwszą linię i użyj sekund, czyli za pomocą poniższego fragmentu kodu:

// 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)); 

uzyskać wyjście szukam:

(key,value): (0,1) 
Default value:1 

Oto jednak problem? Jak mogę się dowiedzieć, że m.get_func_decl (0) jest tym, który odpowiada some_array_1? Na przykład, jeśli używam m.get_func_decl (1), otrzymuję błędne pary (klucz, wartość). Czy są inne słowa, w jaki sposób uzyskać func_interp tablicy (zdefiniowanej jako z3 expr) z modelu?

Answer 1

Reprezentacja modeli tablicowych jest rzeczywiście nieco myląca. Znaczenie

(define-fun some_array_1() (Array Int Int) 
    (_ as-array k!0)) 

jest to, że wzór matrycy some_array_1 jest funkcją k!0, która ma być interpretowana jako matrycy (oznaczanego przez wywołanie as-array. Ta ostatnia ma funkcję parametryczną, której nie ma argumenty dlatego , aby uzyskać rzeczywistą definicję funkcji modelu dla some_array_1, musimy sprawdzić, która funkcja wywołuje funkcje as-array. W podanym przykładzie możemy to zrobić w następujący sposób, najpierw upewniając się, że faktycznie mamy model tablicy w oczekiwanym formacie sprawdzając kilka twierdzeń:

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)); 

deklaracji funkcji model_fd następnie posiada rzeczywistą funkcję przypisaną przez model (k!0) i możemy uzyskać interpretację funkcji poprzez

func_interp fun_interp = m.get_func_interp(model_fd);