package de.bmoth.app;

import com.microsoft.z3.*;
import com.microsoft.z3.enumerations.Z3_sort_kind;
import de.bmoth.backend.z3.FormulaToZ3Translator;
import de.bmoth.backend.z3.SolutionFinder;
import javafx.fxml.FXML;
import javafx.fxml.Initializable;
import javafx.scene.control.TextArea;
import javafx.scene.input.KeyCode;

import java.net.URL;
import java.util.ResourceBundle;
import java.util.Set;

public class ReplController implements Initializable {

    @FXML
    TextArea replText;

    private Context ctx;
    private Solver s;

    @Override
    public void initialize(URL fxmlFileLocation, ResourceBundle resources) {

        ctx = new Context();
        s = ctx.mkSolver();

        replText.setOnKeyPressed(keyEvent -> {
            if (keyEvent.getCode() == KeyCode.ENTER) {
                String[] predicate = replText.getText().split("\n");
                String solution = processPredicate(predicate[predicate.length - 1]);
                replText.appendText(solution);
                replText.commitValue();
            }
        });
    }

    private String processPredicate(String predicate) {
        ctx = new Context();
        s = ctx.mkSolver();
        BoolExpr constraint = FormulaToZ3Translator.translatePredicate(predicate, ctx);
        SolutionFinder finder = new SolutionFinder(constraint, s, ctx);
        Set<Model> solutions = finder.findSolutions(1);
        StringBuilder output = new StringBuilder();
        for (Model solution : solutions) {
            FuncDecl[] functionDeclarations = solution.getConstDecls();
            for (FuncDecl decl : functionDeclarations) {
                output.append(decl.getName()).append("=");
                try {
                    if (decl.getArity() == 0 && decl.getRange().getSortKind() != Z3_sort_kind.Z3_ARRAY_SORT) {
                        // this is a constant
                        output.append(solution.getConstInterp(decl));
                    } else {
                        // not a constant, e.g. some representation of a set
                        output.append(solution.getFuncInterp(decl));
                    }
                    output.append(", ");
                } catch (com.microsoft.z3.Z3Exception e) {
                    e.printStackTrace();
                }
            }

        }
        if (solutions.isEmpty()) {
            return "\nUNSATISFIABLE";
        } else {
            return "\n{" + output.substring(0, output.length() - 2) + "}";
        }
    }
}

@@ -1262,24 +1262,25 @@
 , ctx);%0A
+%0A
         
 Solution
@@ -1275,80 +1275,70 @@
     
-SolutionFinder finder = new SolutionFinder(constraint, s, ctx
+s.add(constraint);%0A        Status check = s.check(
 );%0A
+%0A
         
 Set%3C
@@ -1337,53 +1337,80 @@
     
-Set%3CModel%3E solutions = finder.findSolutions(1
+if (check == Status.SATISFIABLE) %7B%0A            Model model = s.getModel(
 );%0A 
@@ -1412,24 +1412,28 @@
 ();%0A        
+  
+  
 StringBuilde
@@ -1468,51 +1468,8 @@
 ();%0A
-        for (Model solution : solutions) %7B%0A
     
@@ -1510,24 +1510,21 @@
 tions = 
-solution
+model
 .getCons
@@ -1862,32 +1862,29 @@
 tput.append(
-solution
+model
 .getConstInt
@@ -2039,24 +2039,21 @@
 .append(
-solution
+model
 .getFunc
@@ -2266,49 +2266,50 @@
   %7D%0A
-%0A
       
-  %7D%0A
       
-  
 if (
-solutions.isEmpty(
+model.toString().equals(%22%22
 )) %7B
@@ -2313,32 +2313,36 @@
 ) %7B%0A            
+  
+  
 return %22%5CnUNSATI
@@ -2339,24 +2339,23 @@
  %22%5Cn
-UNSATISFIABLE%22;%0A
+%22 + check;%0A    
     
@@ -2359,32 +2359,36 @@
        %7D else %7B%0A
+    
             retu
@@ -2446,16 +2446,95 @@
  + %22%7D%22;%0A
+            %7D%0A        %7D else %7B%0A            return %22%5Cn%22 + Status.UNSATISFIABLE;%0A
         

refactor processPredicate(...) to not rely on solution finder anymore and meet requirements of testIssue71()