c++ - 在 Z3 中添加函数约束

Question

我正试图让 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 行)的情况下工作正常。那是一个限制吗？我错过了什么吗？这并不是一个严重的问题，只是想知道。

Answer 1

Z3 C++ API 为类 func_decl 重载了 operator()。这个想法是让我们使用自然符号来创建小术语。当前可用的重载是:

    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;

在 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);
 }