我正在尝试让Z3查找整数上某些函数的解释。我遇到了一个奇怪的小问题。我写了一小段代码来说明这一点：
#include "z3++.h"
#include<iostream>
using namespace std;
using namespace z3;
main()
{
context c;
sort I=c.int_sort();
func_decl trial1=function("trial1",I,I);
func_decl trial2=function("trial2",I,I,I);
solver s(c);
expr temp=trial1(1)==2;
cout<<temp<<endl;
s.add(temp);
//temp=trial2(1,2)==3;
temp=trial2(c.int_val(1),c.int_val(2))==3;
cout<<temp<<endl;
s.add(temp);
}
在此代码中，注释掉的行导致错误。但是我在下面写的替代方法很好用。我感到困惑的原因是，使用2个参数导致错误的构造对于1个参数（上面3行）可以正常工作。有限制吗？我想念什么吗？这不是一个严重的问题，只是好奇地知道。
Z3 C ++ API重载operator()了类的func_decl。这个想法是让我们使用自然的符号来创建小术语。当前可用的过载为：
expr operator()() const;
expr operator()(unsigned n, expr const * args) const;
expr operator()(expr_vector const& v) const;
expr operator()(expr const & a) const; expr operator()(int a) const;
expr operator()(expr const & a1, expr const & a2) const;
expr operator()(expr const & a1, int a2) const;
expr operator()(int a1, expr const & a2) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
请注意，没有重载operator()(int a1, int a2)。这就是为什么您的示例不起作用的原因。在这种情况下添加新的重载并不难，但是对于3个或更多的参数来说确实很乏味。C ++ API是在C API之上定义的。该文件z3++.h是自包含的。我们可以添加新的重载而无需重新编译Z3。我们只需要包括
expr operator()(int a1, int a2) const;
在class中func_decl，并在下面的代码段中执行其他func_decl::operator()重载之后。
inline expr func_decl::operator()(int a1, int a2) const {
Z3_ast args[2] = { ctx().num_val(a1, domain(0)), ctx().num_val(a1, domain(1)) };
Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
ctx().check_error();
return expr(ctx(), r);
}
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句