如何使用 Z3 C++ API 来证明基于输入参数的理论？答案

【问题标题】：How to use Z3 C++ API to prove a theory based on input parameter?如何使用 Z3 C++ API 来证明基于输入参数的理论？
【发布时间】：2017-08-13 07:40:29
【问题描述】：

我正在尝试使用 Z3 C++ API 来实现以下目标：

(set-option :produce-proofs true)

(declare-const Weight Int)
(declare-const WeightLimit Int)
(declare-const P1 Bool)

(assert (= WeightLimit 10))

(assert (= P1 (>= Weight WeightLimit)))
(assert (= P1 true))

;Facts - Input
(assert (= Weight 100))

(check-sat)

我最终得到了以下功能：

void test() {
    try {        
        context ctx;        
        Z3_string str = "(declare-const Weight Int) (declare-const WeightLimit Int) (declare-const P1 Bool) (assert (= WeightLimit 10)) (assert (= P1 (>= Weight WeightLimit))) (assert (= P1 true)) (assert (= Weight 100)) (check-sat)"; //Generated by some other function
        expr fs(ctx, Z3_parse_smtlib2_string(Z3_context(ctx), str, 0, 0, 0, 0, 0, 0));

        solver s(ctx);
        s.add(fs);

        switch (s.check()) {
            case unsat:   std::cout << "not satisfied\n"; break;
            case sat:     std::cout << "satisfied\n"; break;
            case unknown: std::cout << "unknown\n"; break;
        } 

        model m = s.get_model();
        std::cout << m << "\n";

    }
    catch (z3::exception e) {
        std::cout << e.msg() << std::endl;
    }
}

有没有办法将权重值作为输入参数传递给函数而不是硬编码？

此外，如何使用 Z3 C++ API 设置选项？如果我不设置选项会有什么影响？

【问题讨论】：

我期待如果 Weight 以值 9 传递，则不应满足 (assert (= P1 (>= Weight WeightLimit))) 的理论。

标签： c++ z3 smt

【解决方案1】：

嗯，这需要由生成该字符串作为其输出的函数来处理，您注释为 "//由其他函数生成的那个"

您只需将Weight 作为参数传递给该函数，它应该使用正确的值来生成字符串。

如果出于某种原因该函数不对您可用，则您必须进行一些字符串处理；但当然这会非常脆弱且容易出错。

另一种选择是不传递一个字符串，而是使用 API 一次实际地断言一个事实；但从你的描述看来，这似乎也不是你的选择。

【讨论】：