2

私は2つのファイルを持っています。1つは変数定義ファイルで、もう1つは式ファイルです。式ファイルに変数定義ファイルを挿入する方法を教えてください。yices では、"(include "file")" を使用してそれを行うことができます。

4

1 に答える 1

2

includeZ3にはコマンドがありません。catただし、パイプを使用して、必要なことを行うことができます。たとえば、ファイルdef.smt2とform.smt2. 次に、次のコマンドを使用して連結し、Z3 を呼び出すことができます。

  cat def.smt2 form.smt2 | z3 -in -smt2

このオプションは、標準入力を使用すること、および入力が SMT 2.0 形式であることを-inz3 に指示します。-smt2

于 2013-11-11T16:59:45.827 に答える