de.uka.ilkd.key.smt.counterexample

Class AbstractCounterExampleGenerator

java.lang.Object

de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator

Direct Known Subclasses:

AbstractSideProofCounterExampleGenerator, CounterExampleAction.MainWindowCounterExampleGenerator

public abstract class AbstractCounterExampleGenerator
extends java.lang.Object

Implementations of this class are used find a counter example for a given Sequent using the SMT solver SolverType.Z3_CE_SOLVER.

This class provides the full logic independent from the a user interface. Subclasses are used to realize the user interface specific functionality.

When #searchCounterExample(KeYMediator, Proof, Sequent) is called a new Proof is instantiated by #createProof(KeYMediator, Proof, Sequent). Next the macro SemanticsBlastingMacro is performed on the new Proof and when done the SMT solver is started. The progress of the SMT solver and the final result can be observed by a SolverLauncherListener instantiated. by #createSolverListener(SMTSettings).

Constructor Summary

Constructors

Constructor and Description
AbstractCounterExampleGenerator()

Method Summary

Modifier and Type	Method and Description
protected Sequent	createNewSequent(Sequent oldSequent) Creates the Sequent for the new Proof created by #createProof(KeYMediator, Proof, Sequent).
protected abstract Proof	createProof(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent, java.lang.String proofName) Creates a new Proof.
protected abstract SolverLauncherListener	createSolverListener(SMTSettings settings, Proof proof) Creates the SolverLauncherListener which handles the results of the launched SMT solver.
static boolean	isSolverAvailable() Checks if the required SMT solver is available.
void	searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent) Searches a counter example for the given Sequent.
protected void	semanticsBlastingCompleted(UserInterfaceControl ui) This method is called after the SemanticsBlastingMacro has been executed.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

AbstractCounterExampleGenerator

public AbstractCounterExampleGenerator()

Method Detail

isSolverAvailable

public static boolean isSolverAvailable()

Checks if the required SMT solver is available.

Returns:

true solver is available, false solver is not available.

searchCounterExample

public void searchCounterExample(UserInterfaceControl ui,
                                 Proof oldProof,
                                 Sequent oldSequent)
                          throws ProofInputException

Searches a counter example for the given Sequent.

Parameters:

ui - The UserInterfaceControl to use.

oldProof - The old Proof used as template to instantiate a new one.

oldSequent - The Sequent to find a counter example for.

Throws:

ProofInputException - Occurred Exception.

createProof

protected abstract Proof createProof(UserInterfaceControl ui,
                                     Proof oldProof,
                                     Sequent oldSequent,
                                     java.lang.String proofName)
                              throws ProofInputException

Creates a new Proof.

Parameters:

ui - The UserInterfaceControl to use.

oldProof - The old Proof used as template to instantiate a new one.

oldSequent - The Sequent to find a counter example for.

proofName - The name for the new proof.

Returns:

The created Proof.

Throws:

ProofInputException - Ocurred Exception

createNewSequent

protected Sequent createNewSequent(Sequent oldSequent)

Creates the Sequent for the new Proof created by #createProof(KeYMediator, Proof, Sequent).

Parameters:

oldSequent - The Sequent to find a counter example for.

Returns:

The new Sequent.

semanticsBlastingCompleted

protected void semanticsBlastingCompleted(UserInterfaceControl ui)

This method is called after the SemanticsBlastingMacro has been executed.

Parameters:

ui - The UserInterfaceControl to use.

createSolverListener

protected abstract SolverLauncherListener createSolverListener(SMTSettings settings,
                                                               Proof proof)

Creates the SolverLauncherListener which handles the results of the launched SMT solver.

Parameters:

settings - The SMTSettings.

proof - The Proof on which the SMT solver will be performed.

Returns:

The SolverLauncherListener to use.