ソルバーオブジェクトのインターフェイスを作成して使用する方法（Z3ソルバー）

Question

C＃を初めて使用しています。私は、ソルバーオブジェクトを使用するいくつかのメソッドを持つクラスを持っています。しかし、それぞれのメソッドのために私はそれを使用するソルバーオブジェクトのインスタンスを再度作成する必要があります。インターフェイスを使ってこれを避ける方法を教えてもらえますか？ インターフェイスを作成するのは問題ではありませんが、インターフェイスが作成されたらどのように使用するのですか？

例： これはこれは私がいくつかのメソッドの内部でこれを使用したい（注意ISolverインタフェース

public void Solve(Solver s) 
     { 
      Context ctx = new Context(); 
      ctx.MkSolver(); 

     } 

を実装するメソッドであるソルバー

public interface ISolver 
    { 
     public void Solve(Solver s); 

    } 

が含まれている私のインターフェイス、次のとおりです。I異なるメソッドを含む1つのクラスのみを持つ） メソッドの1つは、次のとおりです。

public void MyCheck(Expression expr) 
{ 
    BoolExpr boolVal = dispatch(expr); 
    Solver s = ctx.MkSolver(); 
    Console.WriteLine(boolVal); 
    s.Assert(boolVal); 
    Console.WriteLine("\n "); 
    Console.WriteLine(s.Check()); 
    Console.WriteLine(ReturnTrueFalse(s)); 
    Console.WriteLine("\n "); 
} 

そして他方は：

public bool isContradiction(Expression expr) 
{ 
    BoolExpr boolVal = dispatch(expr); 
    Solver s = ctx.MkSolver(); 
    s.Assert(boolVal); 
    Status result = s.Check(); 
    return result == Status.UNSATISFIABLE; 
} 

ソルバーS = ctx.MkSolver（）の使用を停止する方法。を、このインターフェイスを使用することによって、すべての方法で使用できます。どんな助けもありがとう。ありがとう。

Answer 1

インターフェイスを使用して、Solver s = ctx.MkSolver()という行をどのように取り除きたいのか分かりません。代わりに、クラスのメンバ変数にSolverインスタンスを格納します。そしておそらく簡単に使用するプロパティを追加します。

public class YourClass 
{ 
    private Solver _solver; 
    private Solver MySolver 
    { 
     get { 
      if (_solver == null) _solver = ctx.MkSolver(); 
      return _solver; 
     } 
    } 

    // ... 

、あなたの質問に示したコードは、ctxはあまりにも、あなたのクラスのスコープ内に空くので、私は、このプロパティにそれを使用していることを示唆しています。

今、あなたの方法でこのプロパティを使用することができます。

public void MyCheck(Expression expr) 
{ 
    BoolExpr boolVal = dispatch(expr); 
    Console.WriteLine(boolVal); 
    MySolver.Assert(boolVal); // use property 
    Console.WriteLine("\n "); 
    Console.WriteLine(MySolver.Check()); 
    Console.WriteLine(ReturnTrueFalse(s)); 
    Console.WriteLine("\n "); 
} 

そして：

​​