de.uka.ilkd.key.smt.counterexample

Class AbstractSideProofCounterExampleGenerator

java.lang.Object

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

de.uka.ilkd.key.smt.counterexample.AbstractSideProofCounterExampleGenerator

Direct Known Subclasses:

CounterExampleAction.NoMainWindowCounterExampleGenerator

public abstract class AbstractSideProofCounterExampleGenerator
extends AbstractCounterExampleGenerator

Implementation of AbstractCounterExampleGenerator which instantiates the new Proof as side proof.

Constructor Summary

Constructors

Constructor and Description
AbstractSideProofCounterExampleGenerator()

Method Summary

Modifier and Type	Method and Description
protected Proof	createProof(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent, java.lang.String proofName) Creates a new Proof.

Methods inherited from class de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator

createNewSequent, createSolverListener, isSolverAvailable, searchCounterExample, semanticsBlastingCompleted

Methods inherited from class java.lang.Object

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

Constructor Detail

AbstractSideProofCounterExampleGenerator

public AbstractSideProofCounterExampleGenerator()

Method Detail

createProof

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

Creates a new Proof.

Specified by:

createProof in class AbstractCounterExampleGenerator

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