Z3 中声明数据类型的等价物 API

Question

如何在 C++ z3 API:

中定义等价的记录

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

我在 z3++.h 文件中找到 tuple_sort here:

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

但出于某种原因，它 return 是 func_decl，而不是 sort。这是为什么？我的意思是，int_sort()、bool_sort()、real_sort() 所有 return sort。我在这里错过了什么？

Answer 1

看来我要找的是tuple_sort(...).range()。这是一个完整的例子：

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

Z3 中声明数据类型的等价物 API

Equivalent of declare-datatypes in Z3 API

record

z3

user-defined-data-types