Z3 Rust : About Arrray

[FoxMakarov]

Hello, I am coming again! First of all, thank you for your answer to my previous question.

In my program, I am trying to use the Struct Array. I learn this structure from the DOCS.RS. One of the construct method is

pub fn fresh_const(
        ctx: &'ctx Context,
        prefix: &str,
        domain: &Sort<'ctx>,
        range: &Sort<'ctx>,
    ) -> Array<'ctx> {
        let sort = Sort::array(ctx, domain, range);
        Self::new(ctx, unsafe {
            let pp = CString::new(prefix).unwrap();
            let p = pp.as_ptr();
            let guard = Z3_MUTEX.lock().unwrap();
            Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
        })
    }

I think this 'Array' structrue is similar to ‘Map’ in Java. And about its 'domain' and 'range', i guess it may show the type of key and value. So I try to use 'Array' to describe a two-dimensional array.

let domain_sort = Sort::int(&context);
    let range_sort = Sort::int(&context);
    let array_sort = Sort::array(context, &domain_sort, &range_sort);

    let first_dim_sort = Sort::int(&context);
    let array = Array::fresh_const(&context,  (pre_str.clone() +  "_array") .as_str(), &first_dim_sort, &array_sort);

    let x = dims[0];
    let y = dims[1];
    for i in 0 .. x {
        let index_first_dim = Int::from_i64(context, i as i64);

        let domain_sort = Sort::int(&context);
        let range_sort = Sort::int(&context);
        let array_val = Array::fresh_const(context, (pre_str.clone() +  "_array_second:") .as_str(), &domain_sort, &range_sort);

        for j in 0 .. y {
            let index_second_dim = Int::from_i64(context, j as i64);
            let value = Int::fresh_const(context, (pre_str.clone() +  "_array_second_value") .as_str());
            array_val.store(&index_second_dim, &value);
        }

        array.store(&index_first_dim, &array_val);
        let m = array.children().len();
        println!("children : {} {} {}", m, x , y);
    }

I don't know whether it's correct. Actually, I want to create a two-dimensional array whose elements are ‘z3::ast::Int’. I create a ‘Sort::array’ using ‘Sort::int’ as its domain and range. Then I create the 2-d array using ‘Sort::int’ as domain and this ‘Sort::array’ as range.

Maybe you've noticed my println!(). I learned a method ‘children()’ which can return the children of this node. I want to ensure that I have stored the element successfully, but its output ‘array.children().len()’ is always 0. This method cannot get its element or I am wrong? I am very confused.

There is a method “eq”. If I want to indicate that the elements in A and B are equal at the corresponding positions, I can directly use ‘A.eq(B)’? Or I have to traverse the Arrays and let every A’s element == B’s element?

The create process is very complicated, and it is also very complicated for me to traverse the array.

for i in 0..dims[0] {
                let now_x = m.select(&Int::from_i64(self.context, i as i64)).as_array().unwrap();
                let now_y = n.select(&Int::from_i64(self.context, i as i64)).as_array().unwrap();
                for j in 0..dims[1] {
                    let x_value = now_x.select(&Int::from_i64(self.context, j as i64)).as_int();
                    let y_value = now_y.select(&Int::from_i64(self.context, j as i64)).as_int();
                    // x_value.eq(y_value)
                    }
            }

I need to use a ‘dims : [usize; 2]’ to record how many elements it has in each dimension. But sometimes dims’s value need z3 to calculate causing difficulty in programming. This problem may be shown as ‘code want to use a value calculated by z3 before z3 begin to calculate’. I will show an example of the same problem.

This example is part of a huge SMT expression. In this part, there are two array input : in1, in2 and one array output. If in2[i] == 1, then the i-th element in in1 will exist in output. Otherwise it will disappear. For example.

in1 = [10, 20, 30, 40]
in2 = [1, 1, 0, 1]
=>
Output = [10, 20, 40]

We use this code to deal with it

for i in 0..size0[0] {
            for j in 0..size0[1] {
                    let ans = in2[0][j]._eq(&one(context, bit_width)).ite(&in1[i][j], &const0);

                    println!("ans : {:?}", ans);
                    println!("ans_i64 : {:?}", ans.as_i64());

                    if ans != const0 {
                        result[i].push(ans);

                }
            }
        }

The code is wrong and the print output is

ans : (ite (= 1 1) 10 0)
ans_i64 : None
ans : (ite (= 1 1) 20 0)
ans_i64 : None
ans : (ite (= 0 1) 30 0)
ans_i64 : None
ans : (ite (= 1 1) 40 0)
ans_i64 : None

We can know the smt expression is built correctly. But we want to get the value of this expression while it is still an expression before it is put into the solver for calculation. I know there's a serious bug here, but I don't know how to fix it. According to your experience, what should I do to complete this task?

[NikolajBjorner]

@waywardmonkeys is extremely responsive here, but you might file the issue here: https://github.com/prove-rs/z3.rs

[FoxMakarov]

OKOK. Thank you, I will Try!