public class SmtLibTranslator extends AbstractSMTTranslator
AbstractSMTTranslator.Configuration, AbstractSMTTranslator.FunctionWrapper
Modifier and Type | Field and Description |
---|---|
private static StringBuffer |
ALLSTRING |
private static StringBuffer |
ANDSTRING |
private static StringBuffer |
BOOL |
private static StringBuffer |
DISTINCT |
private static StringBuffer |
EQSTRING |
private static StringBuffer |
EXISTSTRING |
private static StringBuffer |
FALSESTRING |
private static StringBuffer |
GEQSTRING |
private static StringBuffer |
GTSTRING |
private static StringBuffer |
IMPLYSTRING |
private static StringBuffer |
INTSTRING |
private static StringBuffer |
LEQSTRING |
private static StringBuffer |
LOGICALIFTHENELSE |
private static StringBuffer |
LTSTRING |
private static StringBuffer |
MINUSSTRING |
private static StringBuffer |
MULTSTRING |
private static StringBuffer |
NOTSTRING |
private static StringBuffer |
NULLSORTSTRING |
private static StringBuffer |
NULLSTRING |
private static StringBuffer |
ORSTRING |
private static StringBuffer |
PLUSSTRING |
private static StringBuffer |
TERMIFTHENELSE |
private static StringBuffer |
TRUESTRING |
text, usedDisplaySort, usedRealSort, YESNOT
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.
|
Modifier and Type | Method and Description |
---|---|
protected StringBuffer |
buildCompleteText(StringBuffer formula,
ArrayList<StringBuffer> assumptions,
ArrayList<ContextualBlock> assumptionBlocks,
ArrayList<ArrayList<StringBuffer>> functions,
ArrayList<ArrayList<StringBuffer>> predicates,
ArrayList<ContextualBlock> predicateBlocks,
ArrayList<StringBuffer> types,
SortHierarchy sortHierarchy,
SMTSettings settings)
Build the text, that can be read by the final decider.
|
private StringBuffer |
buildFunction(StringBuffer name,
ArrayList<StringBuffer> args) |
protected StringBuffer |
getBoolSort()
The String used for boolean values.
|
protected StringBuffer |
getIntegerSort()
The String used for integer values.
|
protected StringBuffer |
getNullName() |
protected boolean |
isMultiSorted()
Returns, whether the Structure, this translator creates should be a
Structure, that is multi sorted.
|
protected StringBuffer |
translateDistinct(AbstractSMTTranslator.FunctionWrapper[] fw) |
protected StringBuffer |
translateFunction(StringBuffer name,
ArrayList<StringBuffer> args)
Translate a function.
|
protected StringBuffer |
translateFunctionName(StringBuffer name)
Get the name for a function symbol.
|
protected StringBuffer |
translateIntegerDiv(StringBuffer arg1,
StringBuffer arg2)
Translate the integer division.
|
protected StringBuffer |
translateIntegerGeq(StringBuffer arg1,
StringBuffer arg2)
Translate the greater or equal.
|
protected StringBuffer |
translateIntegerGt(StringBuffer arg1,
StringBuffer arg2)
Translate the greater than.
|
protected StringBuffer |
translateIntegerLeq(StringBuffer arg1,
StringBuffer arg2)
Translate the less or equal.
|
protected StringBuffer |
translateIntegerLt(StringBuffer arg1,
StringBuffer arg2)
Translate the less than.
|
protected StringBuffer |
translateIntegerMinus(StringBuffer arg1,
StringBuffer arg2)
Translate the integer minus.
|
protected StringBuffer |
translateIntegerMod(StringBuffer arg1,
StringBuffer arg2)
Translate the integer modulo.
|
protected StringBuffer |
translateIntegerMult(StringBuffer arg1,
StringBuffer arg2)
Translate the integer multiplication.
|
protected StringBuffer |
translateIntegerPlus(StringBuffer arg1,
StringBuffer arg2)
Translate the integer plus.
|
protected StringBuffer |
translateIntegerUnaryMinus(StringBuffer arg)
Translate a unary minus.
|
protected StringBuffer |
translateIntegerValue(long val)
Translate a sort.
|
protected StringBuffer |
translateLogicalAll(StringBuffer var,
StringBuffer type,
StringBuffer form)
Build the logical forall formula.
|
protected StringBuffer |
translateLogicalAnd(StringBuffer arg1,
StringBuffer arg2)
Build the logical konjunction.
|
protected StringBuffer |
translateLogicalConstant(StringBuffer name)
Build the Stringbuffer for an constant.
|
protected StringBuffer |
translateLogicalEquivalence(StringBuffer arg1,
StringBuffer arg2)
Build the logical equivalence.
|
protected StringBuffer |
translateLogicalExist(StringBuffer var,
StringBuffer type,
StringBuffer form)
Build the logical exists formula.
|
protected StringBuffer |
translateLogicalFalse()
Translate the logical false.
|
protected StringBuffer |
translateLogicalIfThenElse(StringBuffer cond,
StringBuffer ifterm,
StringBuffer elseterm)
Translate the logical if_then_else construct.
|
protected StringBuffer |
translateLogicalImply(StringBuffer arg1,
StringBuffer arg2)
Build the logical implication.
|
protected StringBuffer |
translateLogicalNot(StringBuffer arg)
Build the Stringbuffer for a logical NOT.
|
protected StringBuffer |
translateLogicalOr(StringBuffer arg1,
StringBuffer arg2)
Build the logical disjunction.
|
protected StringBuffer |
translateLogicalTrue()
Translate the logical true.
|
protected StringBuffer |
translateLogicalVar(StringBuffer name)
Build the Stringbuffer for an variable.
|
protected StringBuffer |
translateNull()
Translate the NULL element
|
protected StringBuffer |
translateNullSort()
Translate the NULL element's Sort.
|
protected StringBuffer |
translateObjectEqual(StringBuffer arg1,
StringBuffer arg2)
Build the Stringbuffer for an object equivalence.
|
protected StringBuffer |
translatePredicate(StringBuffer name,
ArrayList<StringBuffer> args)
Translate a predicate.
|
protected StringBuffer |
translatePredicateName(StringBuffer name)
Get the name for a predicate symbol.
|
protected StringBuffer |
translateSort(String name,
boolean isIntVal)
Translate a sort.
|
protected StringBuffer |
translateTermIfThenElse(StringBuffer cond,
StringBuffer ifterm,
StringBuffer elseterm)
Translate the if_then_else construct for terms (i.e.
|
buildInjectiveFunctionAssumption, createGenericVariables, getConfig, getExceptionsOfTacletTranslation, getSettings, getTacletSetTranslation, getTypePredicate, isSomeIntegerSort, makeUnique, translateBprodFunction, translateBsumFunction, translateComment, translateFunc, translateLogicalAll, translateLogicalAll, translateProblem, translateTerm, translateUniqueness, translateUnknown, translateVariable
private static StringBuffer INTSTRING
private static StringBuffer BOOL
private static StringBuffer FALSESTRING
private static StringBuffer TRUESTRING
private static StringBuffer ALLSTRING
private static StringBuffer EXISTSTRING
private static StringBuffer ANDSTRING
private static StringBuffer ORSTRING
private static StringBuffer NOTSTRING
private static StringBuffer EQSTRING
private static StringBuffer IMPLYSTRING
private static StringBuffer PLUSSTRING
private static StringBuffer MINUSSTRING
private static StringBuffer MULTSTRING
private static StringBuffer LTSTRING
private static StringBuffer GTSTRING
private static StringBuffer LEQSTRING
private static StringBuffer GEQSTRING
private static StringBuffer NULLSTRING
private static StringBuffer NULLSORTSTRING
private static StringBuffer LOGICALIFTHENELSE
private static StringBuffer TERMIFTHENELSE
private static StringBuffer DISTINCT
public SmtLibTranslator(Sequent sequent, Services services, AbstractSMTTranslator.Configuration config)
sequent
- The sequent which shall be translated.services
- The Services Object belonging to the sequent.public SmtLibTranslator(Services s, AbstractSMTTranslator.Configuration config)
protected StringBuffer translateNull()
AbstractSMTTranslator
translateNull
in class AbstractSMTTranslator
protected StringBuffer getNullName()
getNullName
in class AbstractSMTTranslator
protected StringBuffer translateNullSort()
AbstractSMTTranslator
translateNullSort
in class AbstractSMTTranslator
protected StringBuffer getBoolSort()
AbstractSMTTranslator
getBoolSort
in class AbstractSMTTranslator
protected StringBuffer buildCompleteText(StringBuffer formula, ArrayList<StringBuffer> assumptions, ArrayList<ContextualBlock> assumptionBlocks, ArrayList<ArrayList<StringBuffer>> functions, ArrayList<ArrayList<StringBuffer>> predicates, ArrayList<ContextualBlock> predicateBlocks, ArrayList<StringBuffer> types, SortHierarchy sortHierarchy, SMTSettings settings)
AbstractSMTTranslator
buildCompleteText
in class AbstractSMTTranslator
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.protected StringBuffer translateSort(String name, boolean isIntVal)
translateSort
in class AbstractSMTTranslator
name
- the sorts nameisIntVal
- true, if the sort should represent some kind of
integerprotected boolean isMultiSorted()
AbstractSMTTranslator
isMultiSorted
in class AbstractSMTTranslator
protected StringBuffer getIntegerSort()
AbstractSMTTranslator
getIntegerSort
in class AbstractSMTTranslator
protected StringBuffer translateFunction(StringBuffer name, ArrayList<StringBuffer> args)
AbstractSMTTranslator
translateFunction
in class AbstractSMTTranslator
name
- The Symbol of the function.args
- The arguments of the function.protected StringBuffer translateFunctionName(StringBuffer name)
AbstractSMTTranslator
translateFunctionName
in class AbstractSMTTranslator
name
- The name that can be used to create the symbol.protected StringBuffer translateIntegerDiv(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerDiv
in class AbstractSMTTranslator
arg1
- The first val of the division.arg2
- second val of the division.protected StringBuffer translateIntegerGeq(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerGeq
in class AbstractSMTTranslator
arg1
- The first val of the greater or equal.arg2
- second val of the greater or equal.protected StringBuffer translateIntegerGt(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerGt
in class AbstractSMTTranslator
arg1
- The first val of the greater than.arg2
- second val of the greater than.protected StringBuffer translateIntegerLeq(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerLeq
in class AbstractSMTTranslator
arg1
- The first val of the less or equal.arg2
- second val of the less or equal.protected StringBuffer translateIntegerLt(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerLt
in class AbstractSMTTranslator
arg1
- The first val of the less than.arg2
- second val of the less than.protected StringBuffer translateIntegerMinus(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerMinus
in class AbstractSMTTranslator
arg1
- The first val of the substraction.arg2
- second val of the substraction.protected StringBuffer translateIntegerMod(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerMod
in class AbstractSMTTranslator
arg1
- The first val of the modulo.arg2
- second val of the modulo.protected StringBuffer translateIntegerMult(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerMult
in class AbstractSMTTranslator
arg1
- The first val of the multiplication.arg2
- second val of the multiplication.protected StringBuffer translateIntegerPlus(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateIntegerPlus
in class AbstractSMTTranslator
arg1
- first val of the sum.arg2
- second val of the sum.protected StringBuffer translateIntegerUnaryMinus(StringBuffer arg)
AbstractSMTTranslator
translateIntegerUnaryMinus
in class AbstractSMTTranslator
arg
- the argument of the unary minus.protected StringBuffer translateIntegerValue(long val)
AbstractSMTTranslator
translateIntegerValue
in class AbstractSMTTranslator
protected StringBuffer translateLogicalConstant(StringBuffer name)
AbstractSMTTranslator
translateLogicalConstant
in class AbstractSMTTranslator
protected StringBuffer translateLogicalVar(StringBuffer name)
AbstractSMTTranslator
translateLogicalVar
in class AbstractSMTTranslator
protected StringBuffer translateLogicalAll(StringBuffer var, StringBuffer type, StringBuffer form)
AbstractSMTTranslator
translateLogicalAll
in class AbstractSMTTranslator
var
- the bounded variable.type
- the type of the bounded variable.form
- The formula containing the bounded variable.protected StringBuffer translateLogicalAnd(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateLogicalAnd
in class AbstractSMTTranslator
arg1
- The first formula.arg2
- The second formula.protected StringBuffer translateLogicalEquivalence(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateLogicalEquivalence
in class AbstractSMTTranslator
arg1
- The first formula.arg2
- The second formula.protected StringBuffer translateLogicalExist(StringBuffer var, StringBuffer type, StringBuffer form)
AbstractSMTTranslator
translateLogicalExist
in class AbstractSMTTranslator
var
- the bounded variable.type
- the type of the bounded variable.form
- The formula containing the bounded variable.protected StringBuffer translateLogicalFalse()
AbstractSMTTranslator
translateLogicalFalse
in class AbstractSMTTranslator
protected StringBuffer translateLogicalImply(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateLogicalImply
in class AbstractSMTTranslator
arg1
- The first formula.arg2
- The second formula.protected StringBuffer translateLogicalNot(StringBuffer arg)
AbstractSMTTranslator
translateLogicalNot
in class AbstractSMTTranslator
arg
- The Formula to be negated.protected StringBuffer translateLogicalOr(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateLogicalOr
in class AbstractSMTTranslator
arg1
- The first formula.arg2
- The second formula.protected StringBuffer translateLogicalTrue()
AbstractSMTTranslator
translateLogicalTrue
in class AbstractSMTTranslator
protected StringBuffer translateObjectEqual(StringBuffer arg1, StringBuffer arg2)
AbstractSMTTranslator
translateObjectEqual
in class AbstractSMTTranslator
arg1
- The first formula of the equivalence.arg2
- The second formula of the equivalence.protected StringBuffer translateLogicalIfThenElse(StringBuffer cond, StringBuffer ifterm, StringBuffer elseterm)
AbstractSMTTranslator
translateLogicalIfThenElse
in class AbstractSMTTranslator
cond
- the condition term.ifterm
- the formula used, if cond=trueelseterm
- the term used, if cond=falseprotected StringBuffer translateTermIfThenElse(StringBuffer cond, StringBuffer ifterm, StringBuffer elseterm) throws IllegalFormulaException
AbstractSMTTranslator
translateTermIfThenElse
in class AbstractSMTTranslator
cond
- the condition formulaifterm
- the term used if cond = true.elseterm
- the term used if cond = false.IllegalFormulaException
- if this construct is not supported.protected StringBuffer translatePredicate(StringBuffer name, ArrayList<StringBuffer> args)
AbstractSMTTranslator
translatePredicate
in class AbstractSMTTranslator
name
- The Symbol of the predicate.args
- The arguments of the predicate.protected StringBuffer translatePredicateName(StringBuffer name)
AbstractSMTTranslator
translatePredicateName
in class AbstractSMTTranslator
name
- The name that can be used to create the symbol.protected StringBuffer translateDistinct(AbstractSMTTranslator.FunctionWrapper[] fw)
translateDistinct
in class AbstractSMTTranslator
private StringBuffer buildFunction(StringBuffer name, ArrayList<StringBuffer> args)