使用C++ API在Z3中收集變量

Question

我想使用Z3 C++ API定義像「x_1」...「X_1000」這樣的變量集合。這可以使用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) 

如果不是，最好的方法是什麼？

Answer 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 << "\n" << "solving...\n" << s.check() << "\n"; 
    model m = s.get_model(); 
    std::cout << "solution\n" << m; 
} 

UPDATE 我added new C++ APIs使用expr_vector創建普遍性和存在量詞。 新的API已在unstable分支中提供。 以下是一個示例：

void exists_expr_vector_example() { 
    std::cout << "exists expr_vector example\n"; 
    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; 
}