c++ - 在 z3 中存储 implies() 函数的参数

Question

我想创建一个函数，可以将 implies() 函数的左右参数存储在 2 个不同的表达式变量中。带有代码的解决方案非常值得赞赏。谢谢。

这是我以前尝试过的。

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

void walk(int tab, expr e)
{
    string blanks(tab, ' ');

    if(e.is_const())
    {
        cout << blanks << "ARGUMENT: " << e << endl;
    }
    else
    {
        cout << blanks << "APP: " << e.decl().name() << endl;
        for(int i = 0; i < e.num_args(); i++)
        {
            walk(tab + 5, e.arg(i));
        }
    }
}

int main()
{
    context c;
    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr z = c.bool_const("z");
    expr e = implies(z,(x && y));
    walk(0, e);
}

这是输出:

APP: =>
     ARGUMENT: z
     APP: and
          ARGUMENT: x
          ARGUMENT: y

Answer 1

我将通过示例明确说明我的评论:

if (e.is_implies()) {
    cout << "left side: " <<endl;
    walk(4, e.arg(0));
    cout << "right side: " <<endl;
    walk(4, e.arg(1));
}

这使用了 expr 类的 is_implies 和 arg 方法。 documentation