満足できるモデルをすべて作成する、Z3 .Net API

Question

私はZ3 .Net APIを使用しています。私はすべての満足のいくモデルを作成したいという単純なコードを持っています。コードは次のようにされています

 Model resultModel = pSolver.Model; 
     Console.WriteLine("x = {0}, y = {1}", 
      resultModel.Evaluate(pX), 
      resultModel.Evaluate(pY)); 

しかし、例えば、いくつかのモデルがあります：私はこのコードを使用するすべてのモデルを列挙したいとき

Solver solver = ctx.MkSolver(); 

    Expr x = ctx.MkConst("x", ctx.MkBoolSort()); 
    Expr y = ctx.MkConst("y", ctx.MkBoolSort()); 

    BoolExpr constraint1 = ctx.MkBoolConst("Constraint1"); 
    solver.AssertAndTrack(ctx.MkOr((BoolExpr)x, (BoolExpr)y), constraint1); 

問題はコードでその後でありますif（X = true）then（Y = Y）。

X = true, Y = true 
X = true, Y = false 

は私にこれらの答えを与えることができますか、私はこれらの答えを得るための内部コーディングを使用する必要がありますAPIの機能があります：このような状況のために私は次のようにInfactは二つのモデルがあることを示したいと思います。

Answer 1

一般的に、少なくともSMT-Libの認可を受けた方法ではない。ソルバーがモデルを提示するとき、それらは常に地上値に結びつき、SMTLibは「最小」モデルを持つための規定を提供しません。ここでの最小限の意味は明らかではないことに注意してください：あなたの例では、xとyは十分であり、もう一方は他の変数の選択に影響を与えることができます。どのソルバーが好むと思いますか？

このような最小モデルに興味がある場合、BDDベースのソルバーはあなたの友人です。 BDDで可変注文を修正するので、その変数順序に応じて「最小」モデルを簡単に読み取ることができます。しかし、SMTソルバーは通常そのような詳細を公開しておらず、そうしたエンジンがあれば簡単にアクセスすることもできません。 Z3の特別なケースでは、https://github.com/Z3Prover/z3/issuesにもっと有用なものを得るための低レベルのAPIがあるかどうかを調べることをお勧めします。このような「シンボリック」モデルを得ることは、SMTソルバーが一般的に提供するものではありません。