package edu.kit.iti.formal.pse.worthwhile.prover;

import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;

/**
 * Implements a prover interface that uses stdin/stdout/stderr
 */
abstract class StdProver implements ProverCaller {
	/**
	 *
	 */
	private FormulaCompiler compiler;

	/**
	 * The path to the binary of the prover that should be called
	 */
	private String proverPath;

	/**
	 * Constructs a new caller with the given binary path and compiler object
	 * 
	 * @param path the path to the binary to call
	 * @param compiler the compiler to use to compile valid input for the prover
	 */
	protected StdProver(String path, FormulaCompiler compiler) {
		this.compiler = compiler;
	}

	/**
	 * Check an the given <code>Expression</code> for its validity
	 * 
	 * @param formula the expression to check
	 * @return the result returned by the prover
	 */
	public ProverResult checkFormula(Expression formula) {
		return null;
	}

	/**
	 * @return the compiler used to compile input for this prover
	 */
	public FormulaCompiler getCompiler() {
		return this.compiler;
	}

	/**
	 * @return the path to the prover binary called by this caller
	 */
	public String getProverPath() {
		return this.proverPath;
	}

	/**
	 * Convert output supplied by the prover to machine-readable
	 * <code>ProverResult</code>
	 * 
	 * @param output the String output returned from the called prover
	 * @return a result extracted from the prover output
	 */
	protected abstract ProverResult getResult(String output);

	/**
	 * @param compiler the compiler to set to compile input for this prover
	 */
	public void setCompiler(FormulaCompiler compiler) {
		this.compiler = compiler;
	}

	/**
	 * @param proverPath the path to the binary to call for this prover
	 */
	public void setProverPath(String proverPath) {
		this.proverPath = proverPath;
	}
}
@@ -461,26 +461,25 @@
 r object%0A%09 *
- 
 %0A
+
 %09 * @param p
@@ -758,25 +758,24 @@
 validity%0A%09 *
- 
 %0A%09 * @param 
@@ -909,24 +909,452 @@
  formula) %7B%0A
+%09%09String in = this.getCompiler().compileFormula(formula);%0A%09%09String out = this.executeProverBinary(in);%0A%09%09return this.getResult(out);%0A%09%7D%0A%0A%09/**%0A%09 * Call the prover with the given input string%0A%09 *%0A%09 * @param input the input string to pass to the prover%0A%09 * @return the output received on stdout from the prover%0A%09 */%0A%09// TODO: Throw some kind of %22can't find the binary exception%22%0A%09private String executeProverBinary(String input) %7B%0A
 %09%09return nul
@@ -1735,20 +1735,19 @@
 %3C/code%3E%0A
+
 %09 *
- 
 %0A%09 * @pa

Implement formular checking in StdProver