はZ3に簡素化してpull_nested_quantifiersオプションの作業をしていますか？

Question

私は、最も外側のレベルに数式内のすべてのネストされた数量を引くしたいと思います。私はZ3で動作するように、次のコマンドを期待したが、彼らはそうではない。

(set-option :pull-nested-quantifiers true) 
(simplify (exists ((x Int)) (and (>= x 0) 
          (forall ((y Int)) (and (>= y 1) (> x y)))))) 

:pull-nested-quantifiersの目的は何ですか？ SMT-LIBまたはZ3 APIを使用してネストされた量指定子を取得するにはどうすればよいですか？ Z3 3.xでは

Answer 1

、simplifyコマンドは、汎用ローカル簡素化の手順が適用されます。 「プルネストされた量指定子」は前処理ステップです。将来のリリースでは戦略/戦略として利用できるようになります。 Z3 3.2はすでにSMT 2.0フロントエンドには多くの組み込みの戦略/戦術を持っています。次のリリースでは、はるかに大きな戦術があります。これらはAPIでも利用可能になります。あなたには、いくつかのプロジェクトのために、この機能が必要な場合は、ちょうど私に電子メールを送信し、私はあなたのための非正式版（ベータ版）を行います。

最後に、汎用量子にネスト（普遍的な）量子がない場合、モデルベースの量子化器のインスタンス化MBQIモジュールがよりうまく機能するため、この前処理ステップがあります。 Z3は実存を排除し、新鮮な定数でxに置き換えられますので、あなたの例では、okです。