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

import java.util.Arrays;
import java.util.List;

/**
 * Caller for the Z3 Prover by Microsoft Research.
 */
public class Z3Prover extends StdProver {
	/**
	 * Construct a new prover caller with the default Z3 command line.
	 * 
	 * The default Z3 command line is <code>z3 -in -smt2 -nw</code>.
	 */
	public Z3Prover() {
		/* we will assume that z3 is in the PATH */
		this(Arrays.asList("z3", "-in", "-smt2", "-nw"));
	}

	/**
	 * Construct a new {@link Z3Prover} with the given command line.
	 * 
	 * @param command
	 *                the command line that is executed to run the Z3 prover binary
	 */
	public Z3Prover(final String command) {
		/* we will use SMTLib as the input format */
		super(command, new SMTLIBStrategy());
	}

	/**
	 * Construct a new {@link Z3Prover} with the given command line.
	 * 
	 * @param command
	 *                the command line that is executed to run the Z3 prover binary
	 */
	public Z3Prover(final List<String> command) {
		/* we will use SMTLib as the input format */
		super(command, new SMTLIBStrategy());
	}

	@Override
	public final ProverResult getResult(final String output) {
		return new Z3ProverResult(output);
	}
}
@@ -421,50 +421,12 @@
 his(
-Arrays.asList(%22z3%22, %22-in%22, %22-smt2%22, %22-nw%22)
+%22z3%22
 );%0A%09
@@ -481,36 +481,38 @@
 h the given 
-command line
+Z3 binary path
 .%0A%09 * %0A%09 * @
@@ -509,39 +509,38 @@
 %09 * %0A%09 * @param 
-command
+binary
 %0A%09 *            
@@ -543,36 +543,28 @@
         the 
-command line
+path
  that is exe
@@ -594,144 +594,177 @@
 ver 
-binary%0A%09 */%0A%09public Z3Prover(final String command) %7B%0A%09%09/* we will use SMTLib as the input format */%0A%09%09super(command, new SMTLIBStrategy(
+with the default parameters%0A%09 *                %3Ccode%3E-in -smt2 -nw%3C/code%3E%0A%09 */%0A%09public Z3Prover(final String binary) %7B%0A%09%09this(Arrays.asList(binary, %22-in%22, %22-smt2%22, %22-nw%22
 ));%0A

Make Z3Prover(String) take exactly a Z3 binary path