c++ - 如何使用 'bit-blast' 方法以命题逻辑形式打印给定的公式？

Question

我正在创建一个将位 vector 公式转换为命题逻辑形式的函数。 一种称为“位爆炸”的策略将此类位 vector 表达式处理为 PL 形式。

我一直在尝试创建一个接受位 vector 表达式并对其应用位爆炸策略的程序。但是由于我是这个主题的新手，所以我无法弄清楚如何在对表达式进行位爆破后打印出输出。

#include<z3++.h>  
#include<iostream>
using namespace std;
using namespace z3;

int main()
{   context c;
    tactic t = tactic(c, "bit-blast");
    expr x = c.bv_const("x", 16);
    expr y = c.bv_const("y", 16);
    expr z = c.bv_const("z", 16);
    goal g(c);
    g.add(z == x + y);
    std::cout<<g;


}

这是我试过的代码，但它不接受表达式“z = x + y” 但是我做的过程是正确的吗？ 如果不是，我应该如何在对其应用 bit-blast 后打印出表达式。？

谢谢。

Answer 1

使用==，而不是=。即，z == x + y。然后，您当然必须应用策略:

#include<z3++.h>
#include<iostream>
using namespace std;
using namespace z3;

int main()
{   context c;
    tactic t = tactic(c, "bit-blast");
    expr x = c.bv_const("x", 16);
    expr y = c.bv_const("y", 16);
    expr z = c.bv_const("z", 16);
    goal g(c);
    g.add(z == x + y);
    apply_result r = t(g);
    std::cout << r << endl;
    return 0;
}

这会打印经过位爆破的目标；太长了就不放了。

如果你想提取实际的表达式，你需要做更多的编程。 (顺便说一句:您确实需要先研究 API https://z3prover.github.io/api/html/z3_09_09_8h_source.html。)

这是一个示例(我正在更改原始表达式，因此输出足够小以便于理解。):

#include<z3++.h>
#include<iostream>
using namespace std;
using namespace z3;

int main()
{   context c;
    tactic t = tactic(c, "bit-blast");
    expr x = c.bv_const("x", 2);
    expr y = c.bv_const("y", 2);
    goal g(c);
    g.add(y == ~x);
    apply_result r = t(g);
    if(r.size() > 0)
    {
       expr res = r[0].as_expr();
       cout << res << endl;
    }
    else
    {
        cout << "tactic failed" << endl;
    }
    return 0;
}

这打印:

$ c++ a.cpp -lz3; ./a.out
(and (not (= k!0 k!2)) (not (= k!1 k!3)))

是的，你会得到 k!0 等作为索引，这对你来说很难关联回你的 x 和 y;但这是不可避免的:bit-blaster 将引入新变量，并且 API 具有重建​​所需内容的所有细节:https://z3prover.github.io/api/html/z3_09_09_8h_source.html