如何获得所有模型或所有凸评估

How to get all models or all convex evaluation?

本文关键字：评估 模型 何获得      更新时间：2023-10-16

我是Z3-Solver的新手，在C 中使用API，并希望解决一组不等式并找到结果。

我已经阅读了用python编写的答案，并尝试在C 中写下它，但是它重复打印一种模型。

5 <= x + y + z <= 16
AND -4 <= x - y <= 6
AND 1 <= y - z <= 3
AND -1 <= x - z <= 7
AND x >= 0 AND y >= 0 AND z >= 0

不等式被添加到求解器中，并进行了很多评估。

c是上下文，s是求解器。

    vector<const char*> variables {"x", "y", "z"};
    // ...
    // till here, s was added into several constraints
    while(s.check() == sat){
        model m = s.get_model();
        cout << m << "n######n";
        expr tmp = c.bool_val(false);
        for(int i = 0; i < variables.size(); ++ i){
            tmp = tmp || (m[c.int_const(variables[i])] != c.int_const(variables[i]));
        }
        s.add(tmp);
    }

和结果：

(define-fun z () Int
  0)
(define-fun y () Int
  2)
(define-fun x () Int
  3)
######
(define-fun z () Int
  0)
(define-fun y () Int
  2)
(define-fun x () Int
  3)
######
(define-fun z () Int
  0)
...

，它只是打印一个模型。我不确定哪里错了。

我如何获得所有模型或获得一个或多个凸集(例如{l1＆lt; = x＆lt; = u1 and l2＆lt; = x -y＆lt; = u2 and ...}(，但不是遍历所有评估。

顺便说一句，关于Python的教程很多(例如(，我可以在C 中学习Z3作为示例和API DOC。启动并不容易。

您的"模型反驳"循环不是很正确。由于您没有发布整个代码，因此很难确定是否还有其他问题，但这就是我的操作方式：

#include<vector>
#include"z3++.h"
using namespace std;
using namespace z3;
int main(void) {
    context c;
    expr_vector variables(c);
    variables.push_back(c.int_const("x"));
    variables.push_back(c.int_const("y"));
    variables.push_back(c.int_const("z"));
    expr x = variables[0];
    expr y = variables[1];
    expr z = variables[2];
    solver s(c);
    s.add(5 <= x+y+z);
    s.add(x+y+z <= 16);
    s.add(-4 <= x-y);
    s.add(x-y <= 6);
    s.add(-1 <= x-z);
    s.add(x-z <= 7);
    s.add(x >= 0);
    s.add(y >= 0);
    s.add(z >= 0);
    while (s.check() == sat) {
        model m = s.get_model();
        cout << m << endl;
        cout << "#######" << endl;
        expr tmp = c.bool_val(false);
        for(int i = 0; i < variables.size(); ++i) {
            tmp = tmp || (variables[i] != m.eval(variables[i]));
        }
        s.add(tmp);
    }
    return 0;
}

此代码运行并枚举所有"混凝土"模型。从您的问题来看，我也想知道您是否可以获得"符号"模型：SMT求解器是不可能的。SMT求解器仅产生混凝土(即所有地面术语(模型，因此，如果您需要从它们中概括，则必须在Z3边界之外执行此操作。

相关文章：