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

Question

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

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

#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;
}

这将打印位爆破的目标；比较长，这里就不放了。

如果你想提取实际的表达式，你需要做更多的编程。 （顺便说一句：你真的需要先学习APIhttps://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