将 Z3 模型值导入 C++

Question

我正在编写一些代码来为 Z3 生成约束，然后求解结果。我可以通过命令Z3_model_to_string(ctx,m) 打印出结果，结果显示x1-> 1 x2->100 其中x1 和x2 都是int。我的问题是如何将这些整数值保存到 C++ 变量中以供将来分析？

这是我为 Z3 编写的部分代码

Z3_model m;
context ctx;
Z3_ast fs;
string str = "(declare-const x1 Int) (assert (> x1 0)) (declare-const x2 Int) (assert (not (< x2 100)))" //Generated by some other function
fs  = Z3_parse_smtlib2_string(Z3_context(ctx), str, 0, 0, 0, 0, 0, 0);
Z3_assert_cnstr(Z3_context(ctx), fs);
Z3_lbool result = Z3_check_and_get_model(Z3_context(ctx), &m);
switch (result) {
case Z3_L_FALSE:
    printf("unsat\n");
    break;
case Z3_L_UNDEF:
    printf("unknown\n");
    printf("potential model:\n%s\n", Z3_model_to_string(Z3_context(ctx), m));
    break;
case Z3_L_TRUE:
    printf("sat\n%s\n", Z3_model_to_string(Z3_context(ctx), m));
    break;
}
int num_constants = Z3_get_model_num_constants(Z3_context(ctx), m);
model aaa(ctx,m);
for (i = 0; i< num_constants; i++) {
    z3::expr r = aaa.get_const_interp(aaa.get_func_decl(i));
}

Answer 1

一旦你有了一个模型m，你就可以使用类模型中的get_const_intrp 和get_func_interp 函数来获取它们的值。对于简单整数变量的情况，模型中应该有n 常量（即常量函数），即m.num_consts() = n 和

expr r = m.get_const_interp(m.get_const_decl(i));

将返回模型中i-th 常量的解释。对于简单整数约束的情况，结果通常是描述数值的expr，即r.is_numeral() 应该为真。我们可以通过这些函数得到这些模型值的不同表示：

对于整数和其他类型：

Z3_get_numeral_string
Z3_get_numeral_decimal_string
Z3_get_numeral_int
Z3_get_numeral_uint
Z3_get_numeral_uint64
Z3_get_numeral_int64

对于实数/有理数：

Z3_get_numeral_small
Z3_get_numerator
Z3_get_denominator
Z3_get_numeral_rational_int64

名称的最后一部分表示将返回什么类型的对象。请注意，如果模型值不适合返回类型（例如，对于 int 范围而言，数字太大），这些函数将返回 false。如果期望所有模型值都很小，我们当然可以使用这些函数。安全（且缓慢）的方法是请求一个字符串，然后将其转换为您用于应用程序的任何大整数表示。

注意：C++ API 只是 C API 之上的一个薄层，这两个 API 旨在一起使用。许多函数只存在于 C 层，而像 ass 和 exprs 这样的 C++ 对象应该自动转换为 C API 的正确类型的指针。

这里是这个特殊情况的完整示例。我冒昧地以更像 C++ 的风格重写了一些代码：

#include <string>
using namespace std;

#include <z3++.h>
using namespace z3;

void main() {
    try {        
        context ctx;        
        Z3_string str = "(declare-const x1 Int) (assert (> x1 0)) (declare-const x2 Int) (assert (not (< x2 100)))"; //Generated by some other function
        expr fs(ctx, Z3_parse_smtlib2_string(Z3_context(ctx), str, 0, 0, 0, 0, 0, 0));

        solver s(ctx);
        s.add(fs);
        check_result cr = s.check();

        model aaa(ctx, s.get_model());
        int num_constants = aaa.num_consts();
        for (int i = 0; i < num_constants; i++) {
            func_decl fd = aaa.get_const_decl(i);
            z3::expr r = aaa.get_const_interp(fd);
        }
    }
    catch (z3::exception e) {
        std::cout << e.msg() << std::endl;
    }
}