z3 - プログラムでZ3を呼び出すにはどうすればよいですか

Question

こんにちは私はZ3SMTソルバーを初めて使用します。関連するAPIを使用して、プログラムでZ3を呼び出すことができることを知っています。しかし、私はZ3SMTソルバーで次のことをしたいと思います。

1. プログラムで1つの入力ファイルをZ3にフィードするにはどうすればよいですか？
2. ソリューションを段階的に取得するにはどうすればよいですか？

例えば：

while ((check-sat) returns sat)
  get the assignments for all boolean vairables

最後に、数式を解いた後、結果を1つの出力ファイルに保存するようにZ3に依頼するにはどうすればよいですか？

私が見ることができるアイデアやドキュメントはありますか？

百万ありがとう!!!

Answer 1

Z3 ディストリビューションには、いくつかの (プログラム API) の例が含まれています。

• examples/c/test_capi.c: C インターフェイスを使用した多くの小さな例。
• examples/dotnet/test_managed.cs: C# での同様の例
• examples/maxsat/maxsat.c: Z3 API 上の MaxSAT プロシージャ (C)。
• examples/ocaml/test_mlapi.ml: ML の例
• examples/theory/test_user_theory.c: 外部理論 (プラグイン) を実装する方法を示す例。