public abstract class AbstractSideProofCounterExampleGenerator extends AbstractCounterExampleGenerator
AbstractCounterExampleGenerator
which instantiates
the new Proof
as side proof.Constructor and Description |
---|
AbstractSideProofCounterExampleGenerator() |
Modifier and Type | Method and Description |
---|---|
protected Proof |
createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
createNewSequent, createSolverListener, isSolverAvailable, searchCounterExample, semanticsBlastingCompleted
public AbstractSideProofCounterExampleGenerator()
protected Proof createProof(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent, java.lang.String proofName) throws ProofInputException
Proof
.createProof
in class AbstractCounterExampleGenerator
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 Exception