z3 modelinden bir z3 dizisinin func ifadesini okuyun

Question

Bir formülde, tatmin edici olup olmadığını z3 kullanarak kontrol etmek istediğiniz 2 dizilim olduğunu varsayalım. Z3 satıldıysa, z3 modelindeki ilk dizide okumak ve bir anahtar, değer çifti ve bir varsayılan değer olarak yazdırmak istiyorum. Daha sonra onu bir haritaya dönüştürmek ve daha fazla analiz yapmak istiyorum.

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 

yerine

Ben ilk satırını açıklama ve ikinci kullanırsanız, yani aşağıdaki kod bloğunu kullanı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)); 

aşağıdaki çıktıyı almak

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

: İşte çalıştırmak örnek

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

:

ben arıyorum çıkışını almak

İşte sorun ne? M_get_func_decl (0) 'ın some_array_1' e karşılık gelen olduğunu nasıl anlarım? Örneğin, m.get_func_decl (1) kullanırsam, yanlış (anahtar, değer) çiftleri alırım. Başka bir deyişle, bir modelden bir func_interp dizisini (z3 expr olarak tanımlanır) nasıl alabilirim?

Answer 1

Dizi modelleri için gösterim gerçekten biraz kafa karıştırıcı.

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

anlamı dizisi some_array_1 model as-array çağrısı ile gösterilen bir dizi (şekilde yorumlanmalıdır fonksiyonu k!0 olmasıdır. Dolayısıyla bu sorunun, bağımsız değişken olan bir parametre işlevi olan , some_array_1 için model fonksiyonunun gerçek tanımına ulaşmak için, hangi fonksiyonun as-array aradığına bakmalıyız. Verilen örnekte, aşağıdaki gibi, öncelikle beklenen formatta bir dizi modele sahip olduğumuzdan emin olabiliriz. Birkaç iddiaları kontrol ederek:

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

fonksiyon beyanı model_fd sonra modele (k!0) tarafından atanan asıl işlevi tutan ve biz

Java'da

func_interp fun_interp = m.get_func_interp(model_fd);