由网友(杀戮横行)分享简介:我想定义一个变量集合,如"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);...我想定义一个变量集合,如"x_1"..."X_1000",使用Z3 C++API。这可以使用for循环来完成吗?我的意思是这样的:
![JS api 一](https://p.xsw88.cn/allimgs/daicuo/20230903/3477.png)
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;
}
![JS api 一](https://p.xsw88.cn/allimgs/daicuo/20230903/3477.png)
更新
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;
}
相关推荐
最新文章