HolSmtLib 今も Z3 証拠復興固定幅の言葉と HOL から翻訳 SMT LIB 2 形式に伴う目標をサポートします。HolQbfLib は、両方の妥当性と証明書の無効性のため Squolem 2.02 のチェックをサポートします。wordsSyntax.mk_word_replicate 数字に適用すると結果として得られる言葉と固定幅の言葉の幅を計算します。システムは小数の構文をサポートします。この構文部門フォーム n 規約マップ/10 m。コア システムでは、この構文は実際、合理的、かつ複雑な理論のために有効です。
タグ:
Enhancements, Bugfixes, Stable
HolSmtLib now also supports Z3 proof reconstruction for goals that involve fixed-width words and a translation from HOL into SMT-LIB 2 format. HolQbfLib supports checking for both validity and invalidity of certificates for Squolem 2.02. wordsSyntax.mk_word_replicate computes the width of the resulting word when applied to a numeral and a fixed-width word. The system supports syntax for decimal fractions. This syntax maps to division terms of the form n / 10m. In the core system, this syntax is enabled for the real, rational, and complex theories.
