public class SmtLib2Translator extends AbstractSMTTranslator
AbstractSMTTranslator.Configuration, AbstractSMTTranslator.FunctionWrapper
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 |
DIVSTRING |
private static java.lang.StringBuffer |
EQSTRING |
private static java.lang.StringBuffer |
EXISTSTRING |
private static java.lang.StringBuffer |
FALSESTRING |
private static java.lang.String |
GAP |
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 |
text, usedDisplaySort, usedRealSort, YESNOT
Constructor and Description |
---|
SmtLib2Translator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
SmtLib2Translator(Services s,
AbstractSMTTranslator.Configuration config)
For translating only terms and not complete sequents.
|
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) |
private java.lang.StringBuffer |
createAssumptions(java.util.ArrayList<java.lang.StringBuffer> assumptions,
java.util.ArrayList<ContextualBlock> assumptionBlocks) |
private void |
createFunctionDeclaration(java.util.ArrayList<java.lang.StringBuffer> function,
boolean isPredicate,
java.lang.StringBuffer result) |
private void |
createFunctionDeclaration(java.lang.StringBuffer result,
java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> functions) |
private void |
createFunctionDeclarations(java.lang.StringBuffer result,
java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> predicates,
java.util.ArrayList<ContextualBlock> predicateBlocks,
java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> functions) |
private void |
createPredicateDeclaration(java.lang.StringBuffer result,
java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> predicates,
java.util.ArrayList<ContextualBlock> predicateBlocks) |
private void |
createSortDeclaration(java.util.ArrayList<java.lang.StringBuffer> types,
java.lang.StringBuffer result) |
private void |
createSortDeclaration(java.lang.StringBuffer type,
java.lang.StringBuffer result) |
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 |
translateComment(int newLines,
java.lang.String comment) |
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.
|
buildInjectiveFunctionAssumption, createGenericVariables, getConfig, getExceptionsOfTacletTranslation, getSettings, getTacletSetTranslation, getTypePredicate, isSomeIntegerSort, makeUnique, translateBprodFunction, translateBsumFunction, translateFunc, translateLogicalAll, translateLogicalAll, translateProblem, translateTerm, translateUniqueness, translateUnknown, translateVariable
private static java.lang.StringBuffer INTSTRING
private static final java.lang.StringBuffer BOOL
private static final java.lang.String GAP
private static java.lang.StringBuffer FALSESTRING
private static java.lang.StringBuffer TRUESTRING
private static java.lang.StringBuffer ALLSTRING
private static java.lang.StringBuffer EXISTSTRING
private static java.lang.StringBuffer ANDSTRING
private static java.lang.StringBuffer ORSTRING
private static java.lang.StringBuffer NOTSTRING
private static java.lang.StringBuffer EQSTRING
private static java.lang.StringBuffer IMPLYSTRING
private static java.lang.StringBuffer PLUSSTRING
private static java.lang.StringBuffer MINUSSTRING
private static java.lang.StringBuffer MULTSTRING
private static java.lang.StringBuffer DIVSTRING
private static java.lang.StringBuffer LTSTRING
private static java.lang.StringBuffer GTSTRING
private static java.lang.StringBuffer LEQSTRING
private static java.lang.StringBuffer GEQSTRING
private static java.lang.StringBuffer NULLSTRING
private static java.lang.StringBuffer NULLSORTSTRING
private static java.lang.StringBuffer LOGICALIFTHENELSE
private static java.lang.StringBuffer TERMIFTHENELSE
private static java.lang.StringBuffer DISTINCT
public SmtLib2Translator(Sequent sequent, Services services, AbstractSMTTranslator.Configuration config)
sequent
- The sequent which shall be translated.services
- The Services Object belonging to the sequent.public SmtLib2Translator(Services s, AbstractSMTTranslator.Configuration config)
protected java.lang.StringBuffer translateNull()
AbstractSMTTranslator
translateNull
in class AbstractSMTTranslator
protected java.lang.StringBuffer getNullName()
getNullName
in class AbstractSMTTranslator
protected java.lang.StringBuffer translateNullSort()
AbstractSMTTranslator
translateNullSort
in class AbstractSMTTranslator
protected java.lang.StringBuffer getBoolSort()
AbstractSMTTranslator
getBoolSort
in class AbstractSMTTranslator
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)
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.private java.lang.StringBuffer createAssumptions(java.util.ArrayList<java.lang.StringBuffer> assumptions, java.util.ArrayList<ContextualBlock> assumptionBlocks)
private void createFunctionDeclarations(java.lang.StringBuffer result, java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> predicates, java.util.ArrayList<ContextualBlock> predicateBlocks, java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> functions)
private void createFunctionDeclaration(java.lang.StringBuffer result, java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> functions)
private void createPredicateDeclaration(java.lang.StringBuffer result, java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> predicates, java.util.ArrayList<ContextualBlock> predicateBlocks)
private void createFunctionDeclaration(java.util.ArrayList<java.lang.StringBuffer> function, boolean isPredicate, java.lang.StringBuffer result)
private void createSortDeclaration(java.util.ArrayList<java.lang.StringBuffer> types, java.lang.StringBuffer result)
private void createSortDeclaration(java.lang.StringBuffer type, java.lang.StringBuffer result)
protected java.lang.StringBuffer translateSort(java.lang.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 java.lang.StringBuffer getIntegerSort()
AbstractSMTTranslator
getIntegerSort
in class AbstractSMTTranslator
protected java.lang.StringBuffer translateFunction(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args)
AbstractSMTTranslator
translateFunction
in class AbstractSMTTranslator
name
- The Symbol of the function.args
- The arguments of the function.protected java.lang.StringBuffer translateFunctionName(java.lang.StringBuffer name)
AbstractSMTTranslator
translateFunctionName
in class AbstractSMTTranslator
name
- The name that can be used to create the symbol.protected java.lang.StringBuffer translateIntegerDiv(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateIntegerDiv
in class AbstractSMTTranslator
arg1
- The first val of the division.arg2
- second val of the division.protected java.lang.StringBuffer translateIntegerGeq(java.lang.StringBuffer arg1, java.lang.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 java.lang.StringBuffer translateIntegerGt(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateIntegerGt
in class AbstractSMTTranslator
arg1
- The first val of the greater than.arg2
- second val of the greater than.protected java.lang.StringBuffer translateIntegerLeq(java.lang.StringBuffer arg1, java.lang.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 java.lang.StringBuffer translateIntegerLt(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateIntegerLt
in class AbstractSMTTranslator
arg1
- The first val of the less than.arg2
- second val of the less than.protected java.lang.StringBuffer translateIntegerMinus(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateIntegerMinus
in class AbstractSMTTranslator
arg1
- The first val of the substraction.arg2
- second val of the substraction.protected java.lang.StringBuffer translateIntegerMod(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateIntegerMod
in class AbstractSMTTranslator
arg1
- The first val of the modulo.arg2
- second val of the modulo.protected java.lang.StringBuffer translateIntegerMult(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateIntegerMult
in class AbstractSMTTranslator
arg1
- The first val of the multiplication.arg2
- second val of the multiplication.protected java.lang.StringBuffer translateIntegerPlus(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateIntegerPlus
in class AbstractSMTTranslator
arg1
- first val of the sum.arg2
- second val of the sum.protected java.lang.StringBuffer translateIntegerUnaryMinus(java.lang.StringBuffer arg)
AbstractSMTTranslator
translateIntegerUnaryMinus
in class AbstractSMTTranslator
arg
- the argument of the unary minus.protected java.lang.StringBuffer translateIntegerValue(long val)
AbstractSMTTranslator
translateIntegerValue
in class AbstractSMTTranslator
protected java.lang.StringBuffer translateLogicalConstant(java.lang.StringBuffer name)
AbstractSMTTranslator
translateLogicalConstant
in class AbstractSMTTranslator
protected java.lang.StringBuffer translateLogicalVar(java.lang.StringBuffer name)
AbstractSMTTranslator
translateLogicalVar
in class AbstractSMTTranslator
protected java.lang.StringBuffer translateLogicalAll(java.lang.StringBuffer var, java.lang.StringBuffer type, java.lang.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 java.lang.StringBuffer translateLogicalAnd(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateLogicalAnd
in class AbstractSMTTranslator
arg1
- The first formula.arg2
- The second formula.protected java.lang.StringBuffer translateLogicalEquivalence(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateLogicalEquivalence
in class AbstractSMTTranslator
arg1
- The first formula.arg2
- The second formula.protected java.lang.StringBuffer translateLogicalExist(java.lang.StringBuffer var, java.lang.StringBuffer type, java.lang.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 java.lang.StringBuffer translateLogicalFalse()
AbstractSMTTranslator
translateLogicalFalse
in class AbstractSMTTranslator
protected java.lang.StringBuffer translateLogicalImply(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateLogicalImply
in class AbstractSMTTranslator
arg1
- The first formula.arg2
- The second formula.protected java.lang.StringBuffer translateLogicalNot(java.lang.StringBuffer arg)
AbstractSMTTranslator
translateLogicalNot
in class AbstractSMTTranslator
arg
- The Formula to be negated.protected java.lang.StringBuffer translateLogicalOr(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateLogicalOr
in class AbstractSMTTranslator
arg1
- The first formula.arg2
- The second formula.protected java.lang.StringBuffer translateLogicalTrue()
AbstractSMTTranslator
translateLogicalTrue
in class AbstractSMTTranslator
protected java.lang.StringBuffer translateObjectEqual(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
AbstractSMTTranslator
translateObjectEqual
in class AbstractSMTTranslator
arg1
- The first formula of the equivalence.arg2
- The second formula of the equivalence.protected java.lang.StringBuffer translateLogicalIfThenElse(java.lang.StringBuffer cond, java.lang.StringBuffer ifterm, java.lang.StringBuffer elseterm)
AbstractSMTTranslator
translateLogicalIfThenElse
in class AbstractSMTTranslator
cond
- the condition term.ifterm
- the formula used, if cond=trueelseterm
- the term used, if cond=falseprotected java.lang.StringBuffer translateTermIfThenElse(java.lang.StringBuffer cond, java.lang.StringBuffer ifterm, java.lang.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 java.lang.StringBuffer translatePredicate(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args)
AbstractSMTTranslator
translatePredicate
in class AbstractSMTTranslator
name
- The Symbol of the predicate.args
- The arguments of the predicate.protected java.lang.StringBuffer translatePredicateName(java.lang.StringBuffer name)
AbstractSMTTranslator
translatePredicateName
in class AbstractSMTTranslator
name
- The name that can be used to create the symbol.protected java.lang.StringBuffer translateDistinct(AbstractSMTTranslator.FunctionWrapper[] fw)
translateDistinct
in class AbstractSMTTranslator
private java.lang.StringBuffer buildFunction(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args)
protected java.lang.StringBuffer translateComment(int newLines, java.lang.String comment)
translateComment
in class AbstractSMTTranslator