CODEWITHSUNDEEP
recordz3user-defined-data-types
OrenIshShalom
OrenIshShalom

Reputation: 7112

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?

Upvotes: 2

Views: 598

Answers (1)

OrenIshShalom
OrenIshShalom

Reputation: 7112

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

Upvotes: 1

Related Questions