使用 C++ 和 Z3_parse_smtlib2_string 在 Z3 中获取 Unsat Core答案

【问题标题】：Getting Unsat Core in Z3 using C++, with Z3_parse_smtlib2_string使用 C++ 和 Z3_parse_smtlib2_string 在 Z3 中获取 Unsat Core
【发布时间】：2015-03-11 06:55:18
【问题描述】：

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

我知道还有其他方法可以找到 here 和 here 中描述的 unsat 核心，它们更容易且不那么麻烦，但我真的希望能够仅使用从字符串解析到 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似乎不知道我已经声明了它。

任何想法我做错了什么？

【问题讨论】：

标签： c++ parsing z3 smt

【解决方案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。

【讨论】：