c++ - 使用 C++ 在 Z3 中使用 Z3_parse_smtlib2_string 获取 Unsat Core

Question

我需要使用 Z3_parse_smtlib2_string 将一些 SMTLIB 字符串解析为使用 C++ API 的 Z3，并使用 Z3 C++ API 找到它的 unsat 核心。

我知道还有其他方法可以找到 unsat 核心，如所述 here和 here这更容易，也不那么麻烦，但我真的希望能够只使用从字符串解析到 Z3 的数据结构来做到这一点。原因是我正在尝试使用 Z3 使某些东西自动化。

很明显，如果我将这个 SMTLIB 程序传递给 Z3，它就是 UNSAT。

(declare-const p0 Bool)
(assert(= p0 true)) (assert(= p0 false))
(assert (exists ((x Int)) (= 3 x)))

我想做的是能够使用 Z3 以编程方式获取 unsat 核心。我所做的是将每一行分别读入 Z3，并使用 solver.add(expr, name) 为它们命名，使用下面的程序。

void my_test() {
    context c1;
    solver s(c1);

    std::string declare = "(declare-const p0 Bool)";
    std::string testing = "(assert(= p0 true)) (assert(= p0 false))";
    std::string obvious = "(assert (exists ((x Int)) (= 3 x)))";

    Z3_ast parsed1 = Z3_parse_smtlib2_string(c1, declare.c_str(), 0,0,0,0,0,0);
    expr e1(c1, parsed1);

    Z3_ast parsed2 = Z3_parse_smtlib2_string(c1, testing.c_str(), 0,0,0,0,0,0);
    expr e2(c1, parsed2);
    std::cout << "what: " << e2 << std::endl;

    Z3_ast parsed3 = Z3_parse_smtlib2_string(c1, obvious.c_str(), 0,0,0,0,0,0);
    expr e3(c1, parsed3);

    s.add(e1, "declare");
    s.add(e2, "testing");
    s.add(e3, "obvious");

    if (s.check() == z3::sat) {
        std::cout << "SAT!\n";
        model m = s.get_model();
        std::cout << m << std::endl;
    } else {
        std::cout << "UNSAT!\n";
        expr_vector core = s.unsat_core();
        std::cout << core << "\n";
        std::cout << "size: " << core.size() << "\n";
        for (unsigned i = 0; i < core.size(); i++) {
            std::cout << core[i] << "\n";
        }
    }
}

我希望 unsat 核心只是 declare，因为这显然是错误的，而其他表达式显然是有效的。然而，Z3 给了我这样的回应:

(error "line 1 column 11: unknown constant p0")
(error "line 1 column 31: unknown constant p0")
what: true
SAT!
(define-fun testing () Bool
  true)
(define-fun declare () Bool
  true)
(define-fun obvious () Bool
  true)

这显然是错误的，因为引用 (assert(= p0 true)) (assert(= p0 false)) 的 declare 是 SAT!显然这应该是 UNSAT。另外，我确实声明了 p0，但 Z3 似乎不知道我已经声明了它。

知道我做错了什么吗？

Answer 1

第二次调用 Z3_parse_smtlib2_string 不知道第一次调用中的声明:

Z3_ast parsed2 = Z3_parse_smtlib2_string(c1, testing.c_str(), 0,0,0,0,0,0);

最后一串零的意思是“不要假设任何其他东西”，所以它不知道 p0 存在。有关详细信息，请参阅 Z3_parse_smtlib2_string in the API documentation ;在你的情况下你想传递一个非空的decls。