recordz3user-defined-data-types

Equivalent of declare-datatypes in Z3 API


How can I define the equivalent of records in the C++ z3 API:

(declare-datatypes ((State 0))
    (((rec
        (src   String)
        (dst   String)
        (res   Bool)
        (index Int))))
)
(assert (= (rec "abc" "def" true 80) ...)

I found the tuple_sort in z3++.h file here:

func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);

but for some reason, it returns func_decl, rather than sort. Why is that? I mean, int_sort(), bool_sort(), real_sort() all return sort. What am I missing here?


Solution

  • It seems what I was looking for is tuple_sort(...).range(). Here is a complete example:

    z3::context context;
    z3::solver solver(context);
    z3::params params(context);
    
    /******************************/
    /* native sorts: Int, Seq Int */
    /******************************/
    z3::sort int_sort     = context.int_sort();
    z3::sort seq_int_sort = context.seq_sort(int_sort);
    
    /****************************/
    /* user defined sort: State */
    /****************************/
    /****************************/
    /* number of fields ..... 2 */
    /****************************/
    const int state_number_of_fields = 2;
    
    /****************************/
    /* field 0 ........ myArray */
    /* field 1 .......... index */
    /****************************/
    const char *state_field_names[state_number_of_fields]=
    {
        "myArray",
        "index"
    };
    
    /****************************/
    /* sort 0 ......... Seq Int */
    /* sort 1 ............. Int */
    /****************************/
    const z3::sort state_field_sorts[state_number_of_fields]=
    {
        seq_int_sort,
        int_sort    
    };
    
    /*********************************/
    /* returned value: state getters */
    /*********************************/
    z3::func_decl_vector getters(context);
    
    /******************************************/
    /* First, we define the state constructor */
    /******************************************/
    z3::func_decl rec = context.tuple_sort(
        "State",
        state_number_of_fields,
        state_field_names,
        state_field_sorts,
        getters);
    
    /*******************************************/
    /* Then (finally) we define the state sort */
    /*******************************************/
    z3::sort state_sort = rec.range();
    
    /*******************************************/
    /* Function declaration: f: State -> State */
    /*******************************************/
    z3::func_decl f = z3::function("f",state_sort,state_sort);
    
    /**********************************************************/
    /* f is defined implicitly: for every state s, f(s) = ... */
    /**********************************************************/
    z3::expr s = context.constant("s",state_sort);
    
    z3::expr randomize_f(z3::expr &s)
    {
        auto myArray = getters[0](s);
        auto index   = getters[1](s);
        auto five     = context.int_val(5);
        auto seq_five = context.int_val(5).unit();
    
        return z3::ite(
            index > context.int_val(8),
            rec(seq_five,five),
            s);
    }
    
    /********/
    /* main */
    /********/
    int main(int argc, char **argv)
    {        
        /*********************/
        /* [1] define f_body */
        /*********************/
        z3::expr f_definition = z3::forall(s,f(s) == randomize_f(s));
    
        /**************************************************************/
        /* [2] f is defined implicitly: for every State s, f(s) = ... */
        /**************************************************************/
        solver.add(f_definition);
    
        /*****************/
        /* [4] check sat */
        /*****************/
        if (solver.check() == z3::sat)
        {
            std::cout << solver.get_model() << "\n";
        }
    
        /**************/
        /* [5] return */
        /**************/
        return 0;
    }