从 z3 模型中仅提取一个值 [英] Extracting just one value from a z3 model

问题描述

我正在寻找与 get-value 等效的 z3 源 API.例如，当我有以下查询时，我可以轻松指定我希望看到哪些值:

I'm looking for the z3 source API equivalent of get-value. For example, when I have the following query, I can easily specify which values I want to be seen:

(declare-const s1 String)
(declare-const s2 String)

(assert (= 8 (str.len     s1         )))
(assert (= 3 (str.indexof s1    "M" 0)))

(assert (=  3 (str.len     s2         )))
(assert (= -1 (str.indexof s2 "\x00" 0)))

(check-sat)
;(get-value (s1))
(get-value (s1 s2))

我设法用 (C) 源 API 做同样的事情，但后来我只得到整个模型(s1 和 s2)并且似乎无法了解如何打印其中之一:

I manage to do the same thing with the (C) source API, but then I only get the entire model (s1 and s2) and can't seem to find how to print just one of them:

void string_example()
{
    Z3_ast M;
    Z3_ast s1;
    Z3_ast s2;
    Z3_ast x00;
    Z3_ast zero;
    Z3_ast three;
    Z3_ast eight;
    Z3_ast cond1;
    Z3_ast cond2;
    Z3_ast cond3;
    Z3_ast cond4;
    Z3_ast minusOne;
    Z3_ast strlen_s1;
    Z3_ast strlen_s2;
    Z3_ast strchr_s1_M;
    Z3_ast strchr_s2_x00;

    /***************/
    /* [0] Context */
    /***************/
    Z3_context ctx = mk_context();

    /**************/
    /* [1] Solver */
    /**************/
    Z3_solver solver = mk_solver(ctx);

    /*************/
    /* [2] Sorts */
    /*************/
    Z3_sort int_sort   =Z3_mk_int_sort(ctx);
    Z3_sort string_sort=Z3_mk_string_sort(ctx);

    /*********************************/
    /* [3] (declare-const zero  Int) */
    /*     (declare-const eight Int) */
    /*********************************/
    zero    =Z3_mk_int(ctx, 0,int_sort);
    three   =Z3_mk_int(ctx, 3,int_sort);
    eight   =Z3_mk_int(ctx, 8,int_sort);
    minusOne=Z3_mk_int(ctx,-1,int_sort);

    /*********************************/
    /* [4] (declare-const s1 String) */
    /*     (declare-const s2 String) */
    /*********************************/
    s1 = Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"s1"),string_sort);
    s2 = Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"s2"),string_sort);

    /**********************************************/
    /* [5] (assert (= (str.len someStringVar) 8)) */
    /**********************************************/
    strlen_s1 = Z3_mk_seq_length(ctx,s1);
    cond1 = Z3_mk_eq(ctx,strlen_s1,eight);
    Z3_solver_assert(ctx,solver,cond1);

    /*********************************************/
    /* [6] (assert (= (str.indexof s1 "M" 0) 3)) */
    /*********************************************/
    M = Z3_mk_string(ctx,"M");
    strchr_s1_M = Z3_mk_seq_index(ctx,s1,M,zero);
    cond2 = Z3_mk_eq(ctx,strchr_s1_M,three);
    Z3_solver_assert(ctx,solver,cond2);

    /***********************************/
    /* [7] (assert (= (str.len s2) 3)) */
    /***********************************/
    strlen_s2 = Z3_mk_seq_length(ctx,s2);
    cond3 = Z3_mk_eq(ctx,strlen_s2,three);
    Z3_solver_assert(ctx,solver,cond3);

    /*************************************************/
    /* [8] (assert (= (str.indexof s2 "\x00" 0) -1)) */
    /*************************************************/
    x00 = Z3_mk_string(ctx,"\\x00");
    strchr_s2_x00 = Z3_mk_seq_index(ctx,s2,x00,zero);
    cond4 = Z3_mk_eq(ctx,strchr_s2_x00,minusOne);
    Z3_solver_assert(ctx,solver,cond4);

    /*******************/
    /* [9] (check-sat) */
    /*******************/
    if (Z3_solver_check(ctx,solver))
    {
        printf("\nHere are my two strings:\n");
        printf("======================= \n\n");
        printf("%s\n",Z3_model_to_string(ctx,Z3_solver_get_model(ctx, solver)));
    }
    /**********************************/
    /* [10] delete solver and context */
    /**********************************/
    del_solver(ctx, solver);
    Z3_del_context(ctx);
}

输出如下:

Here are my two strings:
======================= 

s2 -> "\x01\x10\x01"
s1 -> "\x00\x00\x00M\x00\x00\x00\x00"

当我们添加以下代码时，我们只能提取 s1:

When we added the following code, we were able to extract only s1:

printf("\nHere is just s1:\n");
printf("================= \n\n");
Z3_model_eval(ctx,Z3_solver_get_model(ctx, solver),s1,1,&out);
printf("%s\n",Z3_get_string(ctx,out));

当我们添加以下代码时，我们只能按名称提取 s1:

When we added the following code, we were able to extract only s1 by name:

printf("\nHere is just s1:\n");
printf("================= \n\n");
Z3_model_eval(ctx,Z3_solver_get_model(ctx, solver),Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"s1"),Z3_mk_string_sort(ctx)),1,&out);
printf("%s\n",Z3_get_string(ctx,out));

推荐答案

最简单的方法是使用 Z3_model_eval 评估您在模型下选择的任何表达式，然后打印该表达式.

The easiest way is to use Z3_model_eval to evaluate any expression of your choice under the model and then to print that expression.

这篇关于从 z3 模型中仅提取一个值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！