About Array

[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?

[waywardmonkeys]

I'm not sure! Maybe @Pat-Lafon has some ideas. I suspect you'll have to look to the underlying C API ...

[Pat-Lafon]

I don't have the full sense what you are attempting to do but I'll point out what I think are a few misconceptions to hopefully guide you down the right path.

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.

I think your notion here that an array is a map is misleading you. An array here is not mutable, calling store on an array does not update it but instead creates a new array that has that one element at said index updated.

children() here is referring the the children of the AST representation. This might make more sense if you try to print out the array itself.

println!("array : {array}");
/// array : hi_array!0

let x =array.store(&index_first_dim, &array_val);
println!("x : {x}");
/// x : (store hi_array!0 1 |hi_array_second:!5|)

println!("x_children : {:?}", x.children());
/// x_children : [hi_array!0, 1, |hi_array_second:!5|]

Here it maybe becomes a bit more clear that array is just the identifier, so it has no children. If you use array to build a new array x, then x is just that store with three children, the original array, in the index of the first dimension, and it's corresponding value.

In this way, a different way to view arrays is as function composition. You have an initial function called array which has an input domain of integers and an output range of arrays but the return values are unconstrained. Then you can build a new function x which when applied to 1 with give you the corresponding array_val and otherwise will fall back to calling array.

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’.

As you note, z3 will not actually do anything with these expressions you are constructing until you add them to a solver via an assert and ask it for a corresponding model. So looping over and printing out ans will just print out the AST like above.

[FoxMakarov]

Oh yes! Thank you so much.

I have tried the way you told me using a new array to get the return value. And it store the value successfully!

array_val_chilren : [(store (store (store (store |output_array_second:!56|
                            0
                            output_array_second_value!57)
                     1
                     output_array_second_value!58)
              2
              output_array_second_value!59)
       3
       output_array_second_value!60), 4, output_array_second_value!61]

But I still have a question. **If I want to traverse the simulated two-dimensional array, Is there any more suitable method?**Like use children()? My initial idea was to record its dimensions and then iterate over it like this

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

But because it has not been sent to the solver, the value selected at this time is an expression, and problems will occur when unwrap() is used.

As you note, z3 will not actually do anything with these expressions you are constructing until you add them to a solver via an assert and ask it for a corresponding model. So looping over and printing out ans will just print out the AST like above.

About this, thank you for your helping. We know our mistakes and we may try to find a new idea to realize this.