de.uka.ilkd.key.smt

Class SmtLibTranslator

java.lang.Object

de.uka.ilkd.key.smt.AbstractSMTTranslator

de.uka.ilkd.key.smt.SmtLibTranslator

All Implemented Interfaces:

SMTTranslator

public class SmtLibTranslator
extends AbstractSMTTranslator

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.smt.AbstractSMTTranslator

AbstractSMTTranslator.Configuration, AbstractSMTTranslator.FunctionWrapper

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.StringBuffer	ALLSTRING
private static java.lang.StringBuffer	ANDSTRING
private static java.lang.StringBuffer	BOOL
private static java.lang.StringBuffer	DISTINCT
private static java.lang.StringBuffer	EQSTRING
private static java.lang.StringBuffer	EXISTSTRING
private static java.lang.StringBuffer	FALSESTRING
private static java.lang.StringBuffer	GEQSTRING
private static java.lang.StringBuffer	GTSTRING
private static java.lang.StringBuffer	IMPLYSTRING
private static java.lang.StringBuffer	INTSTRING
private static java.lang.StringBuffer	LEQSTRING
private static java.lang.StringBuffer	LOGICALIFTHENELSE
private static java.lang.StringBuffer	LTSTRING
private static java.lang.StringBuffer	MINUSSTRING
private static java.lang.StringBuffer	MULTSTRING
private static java.lang.StringBuffer	NOTSTRING
private static java.lang.StringBuffer	NULLSORTSTRING
private static java.lang.StringBuffer	NULLSTRING
private static java.lang.StringBuffer	ORSTRING
private static java.lang.StringBuffer	PLUSSTRING
private static java.lang.StringBuffer	TERMIFTHENELSE
private static java.lang.StringBuffer	TRUESTRING

Fields inherited from class de.uka.ilkd.key.smt.AbstractSMTTranslator

text, usedDisplaySort, usedRealSort, YESNOT

Constructor Summary

Constructors

Constructor and Description
SmtLibTranslator(Sequent sequent, Services services, AbstractSMTTranslator.Configuration config) Just a constructor which starts the conversion to Simplify syntax.
SmtLibTranslator(Services s, AbstractSMTTranslator.Configuration config) For translating only terms and not complete sequents.

Method Summary

Modifier and Type	Method and Description
protected java.lang.StringBuffer	buildCompleteText(java.lang.StringBuffer formula, java.util.ArrayList<java.lang.StringBuffer> assumptions, java.util.ArrayList<ContextualBlock> assumptionBlocks, java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> functions, java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> predicates, java.util.ArrayList<ContextualBlock> predicateBlocks, java.util.ArrayList<java.lang.StringBuffer> types, SortHierarchy sortHierarchy, SMTSettings settings) Build the text, that can be read by the final decider.
private java.lang.StringBuffer	buildFunction(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args)
protected java.lang.StringBuffer	getBoolSort() The String used for boolean values.
protected java.lang.StringBuffer	getIntegerSort() The String used for integer values.
protected java.lang.StringBuffer	getNullName()
protected boolean	isMultiSorted() Returns, whether the Structure, this translator creates should be a Structure, that is multi sorted.
protected java.lang.StringBuffer	translateDistinct(AbstractSMTTranslator.FunctionWrapper[] fw)
protected java.lang.StringBuffer	translateFunction(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args) Translate a function.
protected java.lang.StringBuffer	translateFunctionName(java.lang.StringBuffer name) Get the name for a function symbol.
protected java.lang.StringBuffer	translateIntegerDiv(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the integer division.
protected java.lang.StringBuffer	translateIntegerGeq(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the greater or equal.
protected java.lang.StringBuffer	translateIntegerGt(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the greater than.
protected java.lang.StringBuffer	translateIntegerLeq(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the less or equal.
protected java.lang.StringBuffer	translateIntegerLt(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the less than.
protected java.lang.StringBuffer	translateIntegerMinus(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the integer minus.
protected java.lang.StringBuffer	translateIntegerMod(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the integer modulo.
protected java.lang.StringBuffer	translateIntegerMult(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the integer multiplication.
protected java.lang.StringBuffer	translateIntegerPlus(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Translate the integer plus.
protected java.lang.StringBuffer	translateIntegerUnaryMinus(java.lang.StringBuffer arg) Translate a unary minus.
protected java.lang.StringBuffer	translateIntegerValue(long val) Translate a sort.
protected java.lang.StringBuffer	translateLogicalAll(java.lang.StringBuffer var, java.lang.StringBuffer type, java.lang.StringBuffer form) Build the logical forall formula.
protected java.lang.StringBuffer	translateLogicalAnd(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Build the logical konjunction.
protected java.lang.StringBuffer	translateLogicalConstant(java.lang.StringBuffer name) Build the Stringbuffer for an constant.
protected java.lang.StringBuffer	translateLogicalEquivalence(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Build the logical equivalence.
protected java.lang.StringBuffer	translateLogicalExist(java.lang.StringBuffer var, java.lang.StringBuffer type, java.lang.StringBuffer form) Build the logical exists formula.
protected java.lang.StringBuffer	translateLogicalFalse() Translate the logical false.
protected java.lang.StringBuffer	translateLogicalIfThenElse(java.lang.StringBuffer cond, java.lang.StringBuffer ifterm, java.lang.StringBuffer elseterm) Translate the logical if_then_else construct.
protected java.lang.StringBuffer	translateLogicalImply(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Build the logical implication.
protected java.lang.StringBuffer	translateLogicalNot(java.lang.StringBuffer arg) Build the Stringbuffer for a logical NOT.
protected java.lang.StringBuffer	translateLogicalOr(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Build the logical disjunction.
protected java.lang.StringBuffer	translateLogicalTrue() Translate the logical true.
protected java.lang.StringBuffer	translateLogicalVar(java.lang.StringBuffer name) Build the Stringbuffer for an variable.
protected java.lang.StringBuffer	translateNull() Translate the NULL element
protected java.lang.StringBuffer	translateNullSort() Translate the NULL element's Sort.
protected java.lang.StringBuffer	translateObjectEqual(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) Build the Stringbuffer for an object equivalence.
protected java.lang.StringBuffer	translatePredicate(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args) Translate a predicate.
protected java.lang.StringBuffer	translatePredicateName(java.lang.StringBuffer name) Get the name for a predicate symbol.
protected java.lang.StringBuffer	translateSort(java.lang.String name, boolean isIntVal) Translate a sort.
protected java.lang.StringBuffer	translateTermIfThenElse(java.lang.StringBuffer cond, java.lang.StringBuffer ifterm, java.lang.StringBuffer elseterm) Translate the if_then_else construct for terms (i.e. ifterm and condterm are not of Sort FORMULA) If this method is nor overriden, a default implementation is used.

Methods inherited from class de.uka.ilkd.key.smt.AbstractSMTTranslator

buildInjectiveFunctionAssumption, createGenericVariables, getConfig, getExceptionsOfTacletTranslation, getSettings, getTacletSetTranslation, getTypePredicate, isSomeIntegerSort, makeUnique, translateBprodFunction, translateBsumFunction, translateComment, translateFunc, translateLogicalAll, translateLogicalAll, translateProblem, translateTerm, translateUniqueness, translateUnknown, translateVariable

Methods inherited from class java.lang.Object

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

Field Detail

INTSTRING

private static java.lang.StringBuffer INTSTRING

BOOL

private static java.lang.StringBuffer BOOL

FALSESTRING

private static java.lang.StringBuffer FALSESTRING

TRUESTRING

private static java.lang.StringBuffer TRUESTRING

ALLSTRING

private static java.lang.StringBuffer ALLSTRING

EXISTSTRING

private static java.lang.StringBuffer EXISTSTRING

ANDSTRING

private static java.lang.StringBuffer ANDSTRING

ORSTRING

private static java.lang.StringBuffer ORSTRING

NOTSTRING

private static java.lang.StringBuffer NOTSTRING

EQSTRING

private static java.lang.StringBuffer EQSTRING

IMPLYSTRING

private static java.lang.StringBuffer IMPLYSTRING

PLUSSTRING

private static java.lang.StringBuffer PLUSSTRING

MINUSSTRING

private static java.lang.StringBuffer MINUSSTRING

MULTSTRING

private static java.lang.StringBuffer MULTSTRING

LTSTRING

private static java.lang.StringBuffer LTSTRING

GTSTRING

private static java.lang.StringBuffer GTSTRING

LEQSTRING

private static java.lang.StringBuffer LEQSTRING

GEQSTRING

private static java.lang.StringBuffer GEQSTRING

NULLSTRING

private static java.lang.StringBuffer NULLSTRING

NULLSORTSTRING

private static java.lang.StringBuffer NULLSORTSTRING

LOGICALIFTHENELSE

private static java.lang.StringBuffer LOGICALIFTHENELSE

TERMIFTHENELSE

private static java.lang.StringBuffer TERMIFTHENELSE

DISTINCT

private static java.lang.StringBuffer DISTINCT

Constructor Detail

SmtLibTranslator

public SmtLibTranslator(Sequent sequent,
                        Services services,
                        AbstractSMTTranslator.Configuration config)

Just a constructor which starts the conversion to Simplify syntax. The result can be fetched with

Parameters:

sequent - The sequent which shall be translated.

services - The Services Object belonging to the sequent.

SmtLibTranslator

public SmtLibTranslator(Services s,
                        AbstractSMTTranslator.Configuration config)

For translating only terms and not complete sequents.

Method Detail

translateNull

protected java.lang.StringBuffer translateNull()

Description copied from class: AbstractSMTTranslator

Translate the NULL element

Specified by:

translateNull in class AbstractSMTTranslator

Returns:

the Stringbuffer used for nullelement

getNullName

protected java.lang.StringBuffer getNullName()

Specified by:

getNullName in class AbstractSMTTranslator

Returns:

Returns the name of the NULL element.

translateNullSort

protected java.lang.StringBuffer translateNullSort()

Description copied from class: AbstractSMTTranslator

Translate the NULL element's Sort.

Specified by:

translateNullSort in class AbstractSMTTranslator

Returns:

the StringBuffer used for Null.

getBoolSort

protected java.lang.StringBuffer getBoolSort()

Description copied from class: AbstractSMTTranslator

The String used for boolean values.

Specified by:

getBoolSort in class AbstractSMTTranslator

Returns:

The string used for boolean values.

buildCompleteText

protected java.lang.StringBuffer buildCompleteText(java.lang.StringBuffer formula,
                                                   java.util.ArrayList<java.lang.StringBuffer> assumptions,
                                                   java.util.ArrayList<ContextualBlock> assumptionBlocks,
                                                   java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> functions,
                                                   java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> predicates,
                                                   java.util.ArrayList<ContextualBlock> predicateBlocks,
                                                   java.util.ArrayList<java.lang.StringBuffer> types,
                                                   SortHierarchy sortHierarchy,
                                                   SMTSettings settings)

Description copied from class: AbstractSMTTranslator

Build the text, that can be read by the final decider. If the assumptions should be added to the formula, add them like assumtions impliy formula.

Specified by:

buildCompleteText in class AbstractSMTTranslator

Parameters:

formula - The formula, that was built out of the internal representation. It is built by ante implies succ.

assumptions - Assumptions made in this logic. Set of formulas, that are assumed to be true.

assumptionBlocks - List of ContextualBlocks, which refer to the position of different types of assumptions in the container assumptions. Use these objects to make detailed comments in the translations. For more information see the class ContextualBlock .

functions - List of functions. Each Listelement is built up like (name | sort1 | ... | sortn | resultsort)

predicates - List of predicates. Each Listelement is built up like (name | sort1 | ... | sortn)

predicateBlocks - List of ContextualBlocks, which refer to the position of different types of predicate in the container predicates. Use these objects to make detailed comments in the translations. For more information see the class ContextualBlock .

types - List of the used types.

Returns:

The Stringbuffer that can be read by the decider

translateSort

protected java.lang.StringBuffer translateSort(java.lang.String name,
                                               boolean isIntVal)

Translate a sort.

Specified by:

translateSort in class AbstractSMTTranslator

Parameters:

name - the sorts name

isIntVal - true, if the sort should represent some kind of integer

Returns:

Argument 1 of the return value is the sort used in var declarations, Argument2 is the sort used for type predicates

isMultiSorted

protected boolean isMultiSorted()

Description copied from class: AbstractSMTTranslator

Returns, whether the Structure, this translator creates should be a Structure, that is multi sorted. If false, a single sorted structure is created. Then all sorts are translated as integers.

Specified by:

isMultiSorted in class AbstractSMTTranslator

Returns:

true, if multi sorted logic is supported.

getIntegerSort

protected java.lang.StringBuffer getIntegerSort()

Description copied from class: AbstractSMTTranslator

The String used for integer values. This sort is also used in single sorted logics.

Specified by:

getIntegerSort in class AbstractSMTTranslator

Returns:

The String used for integers.

translateFunction

protected java.lang.StringBuffer translateFunction(java.lang.StringBuffer name,
                                                   java.util.ArrayList<java.lang.StringBuffer> args)

Description copied from class: AbstractSMTTranslator

Translate a function.

Specified by:

translateFunction in class AbstractSMTTranslator

Parameters:

name - The Symbol of the function.

args - The arguments of the function.

Returns:

the formula representing the function.

translateFunctionName

protected java.lang.StringBuffer translateFunctionName(java.lang.StringBuffer name)

Description copied from class: AbstractSMTTranslator

Get the name for a function symbol.

Specified by:

translateFunctionName in class AbstractSMTTranslator

Parameters:

name - The name that can be used to create the symbol.

Returns:

The unique function symbol.

translateIntegerDiv

protected java.lang.StringBuffer translateIntegerDiv(java.lang.StringBuffer arg1,
                                                     java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the integer division. Override this, if integer division is supported.

Overrides:

translateIntegerDiv in class AbstractSMTTranslator

Parameters:

arg1 - The first val of the division.

arg2 - second val of the division.

Returns:

The formula representing the integer division.

translateIntegerGeq

protected java.lang.StringBuffer translateIntegerGeq(java.lang.StringBuffer arg1,
                                                     java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the greater or equal. Override this, if integer greater or equal is supported.

Overrides:

translateIntegerGeq in class AbstractSMTTranslator

Parameters:

arg1 - The first val of the greater or equal.

arg2 - second val of the greater or equal.

Returns:

The formula representing the greater or equal.

translateIntegerGt

protected java.lang.StringBuffer translateIntegerGt(java.lang.StringBuffer arg1,
                                                    java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the greater than. Override this, if integer greater is supported.

Overrides:

translateIntegerGt in class AbstractSMTTranslator

Parameters:

arg1 - The first val of the greater than.

arg2 - second val of the greater than.

Returns:

The formula representing the greater than.

translateIntegerLeq

protected java.lang.StringBuffer translateIntegerLeq(java.lang.StringBuffer arg1,
                                                     java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the less or equal. Override this, if integer less or equal is supported.

Overrides:

translateIntegerLeq in class AbstractSMTTranslator

Parameters:

arg1 - The first val of the less or equal.

arg2 - second val of the less or equal.

Returns:

The formula representing the less or equal.

translateIntegerLt

protected java.lang.StringBuffer translateIntegerLt(java.lang.StringBuffer arg1,
                                                    java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the less than. Override this, if integer less is supported.

Overrides:

translateIntegerLt in class AbstractSMTTranslator

Parameters:

arg1 - The first val of the less than.

arg2 - second val of the less than.

Returns:

The formula representing the less than.

translateIntegerMinus

protected java.lang.StringBuffer translateIntegerMinus(java.lang.StringBuffer arg1,
                                                       java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the integer minus.

Overrides:

translateIntegerMinus in class AbstractSMTTranslator

Parameters:

arg1 - The first val of the substraction.

arg2 - second val of the substraction.

Returns:

The formula representing the integer substraction.

translateIntegerMod

protected java.lang.StringBuffer translateIntegerMod(java.lang.StringBuffer arg1,
                                                     java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the integer modulo. Override this, if integer modulo is supported.

Overrides:

translateIntegerMod in class AbstractSMTTranslator

Parameters:

arg1 - The first val of the modulo.

arg2 - second val of the modulo.

Returns:

The formula representing the integer modulo.

translateIntegerMult

protected java.lang.StringBuffer translateIntegerMult(java.lang.StringBuffer arg1,
                                                      java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the integer multiplication.

Overrides:

translateIntegerMult in class AbstractSMTTranslator

Parameters:

arg1 - The first val of the multiplication.

arg2 - second val of the multiplication.

Returns:

The formula representing the integer multiplication.

translateIntegerPlus

protected java.lang.StringBuffer translateIntegerPlus(java.lang.StringBuffer arg1,
                                                      java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Translate the integer plus.

Overrides:

translateIntegerPlus in class AbstractSMTTranslator

Parameters:

arg1 - first val of the sum.

arg2 - second val of the sum.

Returns:

The formula representing the integer plus.

translateIntegerUnaryMinus

protected java.lang.StringBuffer translateIntegerUnaryMinus(java.lang.StringBuffer arg)

Description copied from class: AbstractSMTTranslator

Translate a unary minus.

Overrides:

translateIntegerUnaryMinus in class AbstractSMTTranslator

Parameters:

arg - the argument of the unary minus.

Returns:

the formula representing tha unary minus function.

translateIntegerValue

protected java.lang.StringBuffer translateIntegerValue(long val)

Description copied from class: AbstractSMTTranslator

Translate a sort. Return the StringBuffer, that should be displayed at definitionpart. i.e. the name used for typepredicates an similair. Override this, if integers are supported.

Overrides:

translateIntegerValue in class AbstractSMTTranslator

Returns:

the sorts name

translateLogicalConstant

protected java.lang.StringBuffer translateLogicalConstant(java.lang.StringBuffer name)

Description copied from class: AbstractSMTTranslator

Build the Stringbuffer for an constant.

Specified by:

translateLogicalConstant in class AbstractSMTTranslator

Returns:

The StringBuffer representing the resulting Formular

translateLogicalVar

protected java.lang.StringBuffer translateLogicalVar(java.lang.StringBuffer name)

Description copied from class: AbstractSMTTranslator

Build the Stringbuffer for an variable.

Specified by:

translateLogicalVar in class AbstractSMTTranslator

Returns:

The StringBuffer representing the resulting Formular

translateLogicalAll

protected java.lang.StringBuffer translateLogicalAll(java.lang.StringBuffer var,
                                                     java.lang.StringBuffer type,
                                                     java.lang.StringBuffer form)

Description copied from class: AbstractSMTTranslator

Build the logical forall formula.

Specified by:

translateLogicalAll in class AbstractSMTTranslator

Parameters:

var - the bounded variable.

type - the type of the bounded variable.

form - The formula containing the bounded variable.

Returns:

The resulting formula.

translateLogicalAnd

protected java.lang.StringBuffer translateLogicalAnd(java.lang.StringBuffer arg1,
                                                     java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Build the logical konjunction.

Specified by:

translateLogicalAnd in class AbstractSMTTranslator

Parameters:

arg1 - The first formula.

arg2 - The second formula.

Returns:

The StringBuffer representing the resulting formular.

translateLogicalEquivalence

protected java.lang.StringBuffer translateLogicalEquivalence(java.lang.StringBuffer arg1,
                                                             java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Build the logical equivalence.

Specified by:

translateLogicalEquivalence in class AbstractSMTTranslator

Parameters:

arg1 - The first formula.

arg2 - The second formula.

Returns:

The StringBuffer representing the resulting formular

translateLogicalExist

protected java.lang.StringBuffer translateLogicalExist(java.lang.StringBuffer var,
                                                       java.lang.StringBuffer type,
                                                       java.lang.StringBuffer form)

Description copied from class: AbstractSMTTranslator

Build the logical exists formula.

Specified by:

translateLogicalExist in class AbstractSMTTranslator

Parameters:

var - the bounded variable.

type - the type of the bounded variable.

form - The formula containing the bounded variable.

Returns:

The resulting formula.

translateLogicalFalse

protected java.lang.StringBuffer translateLogicalFalse()

Description copied from class: AbstractSMTTranslator

Translate the logical false.

Specified by:

translateLogicalFalse in class AbstractSMTTranslator

Returns:

The StringBuffer the logical false value.

translateLogicalImply

protected java.lang.StringBuffer translateLogicalImply(java.lang.StringBuffer arg1,
                                                       java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Build the logical implication.

Specified by:

translateLogicalImply in class AbstractSMTTranslator

Parameters:

arg1 - The first formula.

arg2 - The second formula.

Returns:

The StringBuffer representing the resulting formular

translateLogicalNot

protected java.lang.StringBuffer translateLogicalNot(java.lang.StringBuffer arg)

Description copied from class: AbstractSMTTranslator

Build the Stringbuffer for a logical NOT.

Specified by:

translateLogicalNot in class AbstractSMTTranslator

Parameters:

arg - The Formula to be negated.

Returns:

The StringBuffer representing the resulting Formular

translateLogicalOr

protected java.lang.StringBuffer translateLogicalOr(java.lang.StringBuffer arg1,
                                                    java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Build the logical disjunction.

Specified by:

translateLogicalOr in class AbstractSMTTranslator

Parameters:

arg1 - The first formula.

arg2 - The second formula.

Returns:

The StringBuffer representing the resulting formular.

translateLogicalTrue

protected java.lang.StringBuffer translateLogicalTrue()

Description copied from class: AbstractSMTTranslator

Translate the logical true.

Specified by:

translateLogicalTrue in class AbstractSMTTranslator

Returns:

The StringBuffer the logical true value.

translateObjectEqual

protected java.lang.StringBuffer translateObjectEqual(java.lang.StringBuffer arg1,
                                                      java.lang.StringBuffer arg2)

Description copied from class: AbstractSMTTranslator

Build the Stringbuffer for an object equivalence.

Specified by:

translateObjectEqual in class AbstractSMTTranslator

Parameters:

arg1 - The first formula of the equivalence.

arg2 - The second formula of the equivalence.

Returns:

The StringBuffer representing teh resulting Formular

translateLogicalIfThenElse

protected java.lang.StringBuffer translateLogicalIfThenElse(java.lang.StringBuffer cond,
                                                            java.lang.StringBuffer ifterm,
                                                            java.lang.StringBuffer elseterm)

Description copied from class: AbstractSMTTranslator

Translate the logical if_then_else construct. All attributes are logical formulas. If the underlying language does not support this contruct, it is equivalent with (cond IMPLIES ifterm) AND (NOT(cond) IMPLIES thenterm) and can be reduced to this.

Specified by:

translateLogicalIfThenElse in class AbstractSMTTranslator

Parameters:

cond - the condition term.

ifterm - the formula used, if cond=true

elseterm - the term used, if cond=false

Returns:

ther StringBuffer representing the if then else construct

translateTermIfThenElse

protected java.lang.StringBuffer translateTermIfThenElse(java.lang.StringBuffer cond,
                                                         java.lang.StringBuffer ifterm,
                                                         java.lang.StringBuffer elseterm)
                                                  throws IllegalFormulaException

Description copied from class: AbstractSMTTranslator

Translate the if_then_else construct for terms (i.e. ifterm and condterm are not of Sort FORMULA) If this method is nor overriden, a default implementation is used. This might me less effective than a language supported translation. So, if allowed by the target language, override this.

Overrides:

translateTermIfThenElse in class AbstractSMTTranslator

Parameters:

cond - the condition formula

ifterm - the term used if cond = true.

elseterm - the term used if cond = false.

Returns:

the StringBuffer representing the if then else construct.

Throws:

IllegalFormulaException - if this construct is not supported.

translatePredicate

protected java.lang.StringBuffer translatePredicate(java.lang.StringBuffer name,
                                                    java.util.ArrayList<java.lang.StringBuffer> args)

Description copied from class: AbstractSMTTranslator

Translate a predicate.

Specified by:

translatePredicate in class AbstractSMTTranslator

Parameters:

name - The Symbol of the predicate.

args - The arguments of the predicate.

Returns:

the formula representing the predicate.

translatePredicateName

protected java.lang.StringBuffer translatePredicateName(java.lang.StringBuffer name)

Description copied from class: AbstractSMTTranslator

Get the name for a predicate symbol.

Specified by:

translatePredicateName in class AbstractSMTTranslator

Parameters:

name - The name that can be used to create the symbol.

Returns:

The unique predicate symbol.

translateDistinct

protected java.lang.StringBuffer translateDistinct(AbstractSMTTranslator.FunctionWrapper[] fw)

Overrides:

translateDistinct in class AbstractSMTTranslator

buildFunction

private java.lang.StringBuffer buildFunction(java.lang.StringBuffer name,
                                             java.util.ArrayList<java.lang.StringBuffer> args)