de.uka.ilkd.key.macros

Class SMTPreparationMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.SequentialProofMacro

de.uka.ilkd.key.macros.SMTPreparationMacro

All Implemented Interfaces:

ProofMacro

public class SMTPreparationMacro
extends SequentialProofMacro

A macro that performs all simplifications that are necessary in order to perform a translation of the sequent to SMT. These include symbolic execution and heap simplification.

Author:

js

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.macros.ProofMacro

ProofMacro.ProgressBarListener

Constructor Summary

Constructors

Constructor and Description
SMTPreparationMacro()

Method Summary

Modifier and Type	Method and Description
protected ProofMacro[]	createProofMacroArray() Creates the proof macro array.
java.lang.String	getCategory() Gets the category of this macro.
java.lang.String	getDescription() Gets the description of this macro.
java.lang.String	getName() Gets the name of this macro.

Methods inherited from class de.uka.ilkd.key.macros.SequentialProofMacro

applyTo, canApplyTo, getProofMacros

Methods inherited from class de.uka.ilkd.key.macros.AbstractProofMacro

applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

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

Constructor Detail

SMTPreparationMacro

public SMTPreparationMacro()

Method Detail

createProofMacroArray

protected ProofMacro[] createProofMacroArray()

Creates the proof macro array.

Override this method by returning an array with the macros you want to call in the order of execution.

Specified by:

createProofMacroArray in class SequentialProofMacro

Returns:

a non-null array which should not be altered afterwards.

getName

public java.lang.String getName()

Gets the name of this macro.

Used as menu entry

Returns:

a non-null constant string

getCategory

public java.lang.String getCategory()

Gets the category of this macro.

Used as name of the menu under which the macro is sorted. Return null if no submenu is to be created.

Returns:

a constant string, or null

getDescription

public java.lang.String getDescription()

Gets the description of this macro.

Used as tooltip.

Returns:

a non-null constant string