So erstellen Sie eine Schnittstelle für Solver-Objekt und verwenden Sie es (Z3-Solver)

Question

Ich bin neu in C#. Ich habe eine Klasse mit einigen Methoden, die das Solver-Objekt verwenden. Aber für jede Methode muss ich erneut eine Instanz des Solver-Objekts erstellen, um es zu verwenden. Kann mir jemand sagen, wie man dies vermeiden kann, indem man Schnittstellen benutzt? Eine Schnittstelle zu machen ist kein Problem, aber wie man es benutzt, sobald es gemacht worden ist ??

ZB: Das ist meine Schnittstelle, die eine Solver

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

    } 

Dieses enthält eine Methode, die ISolver Schnittstelle implementiert

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

     } 

Ich möchte diese (Anmerkung nach innen einige Methoden verwenden: I haben nur eine einzige Klasse, die verschiedene Methoden enthält) Eine der folgenden Methoden ist:

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 "); 
} 

und das andere ist:

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

Wie Solver s = ctx.MkSolver mehr zu verwenden(); in jeder Methode mit dieser Schnittstelle. Jede Hilfe wäre willkommen. Vielen Dank.

Answer 1

Ich kann nicht sehen, wie Sie die Linie Solver s = ctx.MkSolver() mit einer Schnittstelle loswerden wollen. Stattdessen würde ich die Solver Instanz in einer Mitgliedsvariablen Ihrer Klasse speichern. Und vielleicht eine Eigenschaft für die einfache Nutzung hinzufügen:

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

    // ... 

Der Code, den Sie in Ihrer Frage zeigen, legt nahe, dass ctx im Rahmen Ihrer Klasse verfügbaren ist, so habe ich es in dieser Eigenschaft auch.

Sie können nun diese Eigenschaft in Ihre Methoden verwenden:

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 "); 
} 

Und:

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