添加Z3中功能的相反

Adding contraints on functions in Z3

本文关键字：功能 Z3 添加      更新时间：2023-10-16

我试图让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将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);
 }
相关文章：