package de.bmoth.app;

import com.microsoft.z3.*;
import de.bmoth.backend.z3.FormulaToZ3Translator;
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.logging.Logger;

public class ReplController implements Initializable {
    private final Logger logger = Logger.getLogger(getClass().getName());


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


    private String processPredicate(String predicate) {
        ctx = new Context();
        s = ctx.mkSolver();
        BoolExpr constraint = FormulaToZ3Translator.translatePredicate(predicate, ctx);
        s.add(constraint);
        Status check = s.check();

        if (check == Status.SATISFIABLE) {
            Model model = s.getModel();
            String output = new PrettyPrinter(model).getOutput();
            if (model.toString().equals("")) {
                return "\n" + check;
            } else {
                return "\n" + output.toString();
            }
        } else {
            return "\n" + Status.UNSATISFIABLE;
        }
    }
}

@@ -283,41 +283,8 @@
 dle;
-%0Aimport java.util.logging.Logger;
 %0A%0Apu
@@ -340,83 +340,8 @@
 e %7B%0A
-    private final Logger logger = Logger.getLogger(getClass().getName());%0A%0A
 %0A   
@@ -1459,27 +1459,16 @@
 + output
-.toString()
 ;%0A      

Remove smells in ReplController