Z3 API：固定小数点SMTLib文字列の解析時にクラッシュする

Question

Z3のC/C++ APIを使用して、SMTLib2形式の固定小数点制約（特にSeaHorn製ファイル）を解析しようとしています。しかし、文字列の解析時に私のアプリケーションがクラッシュする（私はZ3_fixedpoint_from_stringメソッドを使用しています）。私が扱っているZ3バージョンはバージョン4.5.1 64ビットです。

私がソースからコンパイルしたZ3バイナリを使って作品を解析しようとしましたが、Z3_fixedpoint_from_stringを呼び出すとセグメンテーションフォルトが発生します。私は問題点を、固定小数点コンテキストに関係を追加することに関連していると考えています。私のマシン上でワンセグ障害を作り出す簡単な例は以下の通りです：無効の読み取りと書き込みの

#include "z3.h" 

int main() 
{ 
    Z3_context c = Z3_mk_context(Z3_mk_config()); 
    Z3_fixedpoint f = Z3_mk_fixedpoint(c); 

    Z3_fixedpoint_from_string (c, f, "(declare-rel R())"); 

    Z3_del_context(c); 
} 

valgrindのと、このコードを実行する多くのことを報告します。したがって、これはAPIの使用方法ではなく、どこかに問題があります。残念ながら、プログラムで固定小数点エンジンを使用する方法の例は見つかりませんでした。しかし、例えばZ3_fixedpoint_from_string (c, f, "(declare-var x Int)");を呼び出すとうまく動作します。

ところで、Z3_del_fixedpoint()はどこですか？

Answer 1

固定小数点オブジェクト "f"は参照カウントです。発信者は、作成直後に参照カウントを取得する必要があります。これを制御するためにC++のスマートポインタを使用する方が簡単です。他のオブジェクトの制御方法と同様です。 C++ APIには固定小数点オブジェクト用のラッパーがありませんので、他のラッパーのスタイルで独自に作成する必要があります。

del_fixedpointではなく、参照カウンタを使用します。

class fixedpoint : public object { 
    Z3_fixedpoint m_fp; 
public: 
    fixedpoint(context& c):object(c) { mfp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); } 
    ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); } 
    operator Z3_fixedpoint() const { return m_fp; } 

    void from_string(char const* s) { 
     Z3_fixedpoint_from_string (ctx(), m_fp, s); 
    } 

}; 

int main() 
{ 
    context c; 
    fixedpoint f(c); 
    f.from_string("....");  
}