用C++API实现Z3中的变量集合 [英] collection of variables in Z3 using C++ API

问题描述

我想定义一个变量集合，如"x_1"..."X_1000"，使用Z3 C++API。这可以使用for循环来完成吗？我的意思是这样的：

expr x[100] ;
for( i = 0; i < 1000 ; i++)
{  sprintf(str, "x_%d", i);
   x[i] = c.bool_const(str);
}

solver s(c);

for( i = 0; i < 1000 ; i++)
   s.add(x[i] >= 1)

如果不是，实现这一目标的最优雅方式应该是什么？

推荐答案

我们无法编写expr x[100]，因为expr类没有expr::expr()形式的构造函数。我们应该改用expr_vector。下面是一个示例(我还将其添加到Z3分发版的official C++ example中)。

void expr_vector_example() {
    context c;
    const unsigned N = 10;

    expr_vector x(c);

    for (unsigned i = 0; i < N; i++) { 
        std::stringstream x_name; 
        x_name << "x_" << i;
        x.push_back(c.int_const(x_name.str().c_str()));
    }

    solver s(c);
    for (unsigned i = 0; i < N; i++) {
        s.add(x[i] >= 1);
    }

    std::cout << s << "
" << "solving...
" << s.check() << "
";
    model m = s.get_model();
    std::cout << "solution
" << m;
}

更新 Iadded new C++ APIs，用于使用expr_vector创建通用量词和存在量词。 新的API已经在unstable分支中提供。 下面是一个例子：

void exists_expr_vector_example() {
    std::cout << "exists expr_vector example
";
    context c;
    const unsigned N = 10;

    expr_vector xs(c);
    expr x(c);
    expr b(c);
    b = c.bool_val(true); 

    for (unsigned i = 0; i < N; i++) { 
        std::stringstream x_name; 
        x_name << "x_" << i;
        x = c.int_const(x_name.str().c_str());
        xs.push_back(x);
        b = b && x >= 0;
    }

    expr ex(c);
    ex = exists(xs, b);
    std::cout << ex << std::endl;
}

这篇关于用C++API实现Z3中的变量集合的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！