Gibt es eine Möglichkeit, SMT-Solver zu verwenden, um herauszufinden, wie Funktionen zusammengesetzt werden?

Question

Ich bin ein Anfänger zu SMT-Lösern und ich versuche, sie für eine Variation der Programmsynthese zu verwenden. Wie auch immer, worauf das Problem hinausläuft, ist eine Folge von angewandten Operationen (Zusammensetzung vorher definierter Funktionen) zu finden, die für die gegebene Eingabe die angeforderte Ausgabe liefert.

Gibt es eine gängige Praxis, SMT-Solver zu verwenden, um herauszufinden, in welcher Reihenfolge Funktionen erstellt werden müssen, um eine bestimmte Ausgabe zu erreichen? Wenn Sie Lesematerial für mich haben, lese ich gerne.

Ich fing an, Z3 für die Aufgabe zu verwenden, aber wenn es irgendeine Argumentation gibt, andere SMT Löser zu wählen, schießen Sie!

Danke.

Answer 1

Sie müssen Konstanten definieren, die beschreiben, welche Operationen angewendet werden sollen. Definieren Sie zunächst eine zusammengesetzte Operation, die basierend auf der zu verwendenden Operation umschaltet:

int operation; //constant, constrain it to [0, 2] 
Expr result = 
operation == 0 ? applyFunction0(inputExpr) : 
operation == 1 ? applyFunction1(inputExpr) : 
applyFunction2(inputExpr); 

Sehr grober Pseudocode für den zu erstellenden Ausdruck. Der Operator ?: wird in Z3 auf ITE abgebildet.

Auf diese Weise kann Z3 einen geeigneten Wert für operation finden, um eine konkrete Operation auszuwählen. Sie können den konkreten Wert aus dem Modell erhalten.

Sie können diesen Ansatz durchlaufen, um mehrere Operationen nacheinander anzuwenden.