public abstract class AbstractCounterExampleGenerator
extends java.lang.Object
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 and Description |
---|
AbstractCounterExampleGenerator() |
Modifier and Type | Method and Description |
---|---|
protected Sequent |
createNewSequent(Sequent oldSequent)
|
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. |
public static boolean isSolverAvailable()
true
solver is available, false
solver is not available.public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent) throws ProofInputException
Sequent
.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.ProofInputException
- Occurred Exception.protected abstract Proof createProof(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent, java.lang.String proofName) throws ProofInputException
Proof
.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.Proof
.ProofInputException
- Ocurred Exceptionprotected void semanticsBlastingCompleted(UserInterfaceControl ui)
SemanticsBlastingMacro
has been executed.ui
- The UserInterfaceControl
to use.protected abstract SolverLauncherListener createSolverListener(SMTSettings settings, Proof proof)
SolverLauncherListener
which handles the results
of the launched SMT solver.settings
- The SMTSettings
.proof
- The Proof
on which the SMT solver will be performed.SolverLauncherListener
to use.