package de.bmoth.app;

/**
 * Created by jessy on 19.05.17.
 */
public class ReplController {
}

@@ -20,77 +20,1557 @@
 p;%0A%0A
-/**%0A * Created by jessy on 19.05.17.%0A */%0Apublic class ReplController %7B
+import com.microsoft.z3.BoolExpr;%0Aimport com.microsoft.z3.Context;%0Aimport com.microsoft.z3.Model;%0Aimport com.microsoft.z3.Solver;%0Aimport de.bmoth.backend.FormulaToZ3Translator;%0Aimport de.bmoth.backend.SolutionFinder;%0Aimport javafx.fxml.FXML;%0Aimport javafx.fxml.Initializable;%0Aimport javafx.scene.control.TextArea;%0Aimport javafx.scene.input.KeyCode;%0A%0Aimport java.net.URL;%0Aimport java.util.ResourceBundle;%0Aimport java.util.Set;%0A%0Apublic class ReplController implements Initializable %7B%0A%0A    @FXML%0A    TextArea replText = new TextArea();%0A%0A    private Context ctx;%0A    private Solver s;%0A%0A    @Override%0A    public void initialize(URL fxmlFileLocation, ResourceBundle resources) %7B%0A%0A        ctx = new Context();%0A        s = ctx.mkSolver();%0A%0A        replText.setOnKeyPressed(keyEvent -%3E %7B%0A            if (keyEvent.getCode() == KeyCode.ENTER) %7B%0A                String%5B%5D predicate = replText.getText().split(%22%5Cn%22);%0A                String solution = processPredicate(predicate%5Bpredicate.length-1%5D);%0A                replText.appendText(solution);%0A            %7D%0A        %7D);%0A    %7D%0A%0A    private String processPredicate(String predicate) %7B%0A        ctx = new Context();%0A        s = ctx.mkSolver();%0A        BoolExpr constraint = FormulaToZ3Translator.translatePredicate(predicate, ctx);%0A        SolutionFinder finder = new SolutionFinder(constraint, s, ctx);%0A        Set%3CModel%3E solutions = finder.findSolutions(1);%0A        if (solutions.size() == 0) %7B%0A            return %22%5CnUNSATISFIABLE%22;%0A        %7D else %7B%0A            return %22%5Cn%22 + solutions.toString();%0A        %7D%0A    %7D
 %0A%7D%0A

Read predicate and find one solution or return UNSATISFIABLE