在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)沒有過載。這就是你的例子不起作用的原因。爲這種情況增加一個新的重載並不難，但對於三個或更多的參數來說，它會變得非常乏味。 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); 
}