我想创建一个函数,可以将 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
最佳答案
我将通过示例明确说明我的评论:
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
关于c++ - 在 z3 中存储 implies() 函数的参数,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/56492939/