public abstract class AbstractSMTTranslator extends java.lang.Object implements SMTTranslator
Modifier and Type | Class and Description |
---|---|
static class |
AbstractSMTTranslator.Configuration |
protected static class |
AbstractSMTTranslator.FunctionWrapper
remember all function declarations
|
Modifier and Type | Field and Description |
---|---|
protected java.lang.String |
text
The translation result is stored in this variable.
|
protected java.util.HashMap<Sort,java.lang.StringBuffer> |
usedDisplaySort |
protected java.util.HashMap<Sort,java.lang.StringBuffer> |
usedRealSort |
protected static int |
YESNOT |
Constructor and Description |
---|
AbstractSMTTranslator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
AbstractSMTTranslator(Services s,
AbstractSMTTranslator.Configuration config)
For translating only terms and not complete sequents.
|
Modifier and Type | Method and Description |
---|---|
protected abstract java.lang.StringBuffer |
buildCompleteText(java.lang.StringBuffer formula,
java.util.ArrayList<java.lang.StringBuffer> assum,
java.util.ArrayList<de.uka.ilkd.key.smt.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<de.uka.ilkd.key.smt.ContextualBlock> predicateBlocks,
java.util.ArrayList<java.lang.StringBuffer> types,
SortHierarchy sortHierarchy,
SMTSettings settings)
Build the text, that can be read by the final decider.
|
protected java.lang.StringBuffer |
buildInjectiveFunctionAssumption(AbstractSMTTranslator.FunctionWrapper fw) |
protected java.util.ArrayList<java.lang.StringBuffer> |
createGenericVariables(int count,
int start) |
protected abstract java.lang.StringBuffer |
getBoolSort()
The String used for boolean values.
|
AbstractSMTTranslator.Configuration |
getConfig() |
java.util.Collection<java.lang.Throwable> |
getExceptionsOfTacletTranslation() |
protected abstract java.lang.StringBuffer |
getIntegerSort()
The String used for integer values.
|
protected abstract java.lang.StringBuffer |
getNullName() |
protected SMTSettings |
getSettings() |
TacletSetTranslation |
getTacletSetTranslation() |
protected java.lang.StringBuffer |
getTypePredicate(Sort s,
java.lang.StringBuffer arg)
Get the type predicate for the given sort and the given expression.
|
protected abstract boolean |
isMultiSorted()
Returns, whether the Structure, this translator creates should be a
Structure, that is multi sorted.
|
protected boolean |
isSomeIntegerSort(Sort s) |
protected java.lang.StringBuffer |
makeUnique(java.lang.StringBuffer name) |
protected java.lang.StringBuffer |
translateBprodFunction(Term bprodterm,
java.util.ArrayList<java.lang.StringBuffer> sub)
translate a bprod function.
|
protected java.lang.StringBuffer |
translateBsumFunction(Term bsumterm,
java.util.ArrayList<java.lang.StringBuffer> sub)
translate a bsum function.
|
protected java.lang.StringBuffer |
translateComment(int newLines,
java.lang.String comment) |
protected java.lang.StringBuffer |
translateDistinct(AbstractSMTTranslator.FunctionWrapper[] functions) |
protected java.lang.StringBuffer |
translateFunc(Operator o,
java.util.ArrayList<java.lang.StringBuffer> sub)
translate a function.
|
protected abstract java.lang.StringBuffer |
translateFunction(java.lang.StringBuffer name,
java.util.ArrayList<java.lang.StringBuffer> args)
Translate a function.
|
protected abstract 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.util.ArrayList<java.lang.StringBuffer> variables,
java.util.ArrayList<Sort> sorts,
java.lang.StringBuffer result) |
protected java.lang.StringBuffer |
translateLogicalAll(java.lang.StringBuffer var,
Sort sort,
java.lang.StringBuffer result) |
protected abstract java.lang.StringBuffer |
translateLogicalAll(java.lang.StringBuffer var,
java.lang.StringBuffer type,
java.lang.StringBuffer form)
Build the logical forall formula.
|
protected abstract java.lang.StringBuffer |
translateLogicalAnd(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the logical konjunction.
|
protected abstract java.lang.StringBuffer |
translateLogicalConstant(java.lang.StringBuffer name)
Build the Stringbuffer for an constant.
|
protected abstract java.lang.StringBuffer |
translateLogicalEquivalence(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the logical equivalence.
|
protected abstract java.lang.StringBuffer |
translateLogicalExist(java.lang.StringBuffer var,
java.lang.StringBuffer type,
java.lang.StringBuffer form)
Build the logical exists formula.
|
protected abstract java.lang.StringBuffer |
translateLogicalFalse()
Translate the logical false.
|
protected abstract java.lang.StringBuffer |
translateLogicalIfThenElse(java.lang.StringBuffer cond,
java.lang.StringBuffer ifterm,
java.lang.StringBuffer elseterm)
Translate the logical if_then_else construct.
|
protected abstract java.lang.StringBuffer |
translateLogicalImply(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the logical implication.
|
protected abstract java.lang.StringBuffer |
translateLogicalNot(java.lang.StringBuffer arg)
Build the Stringbuffer for a logical NOT.
|
protected abstract java.lang.StringBuffer |
translateLogicalOr(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the logical disjunction.
|
protected abstract java.lang.StringBuffer |
translateLogicalTrue()
Translate the logical true.
|
protected abstract java.lang.StringBuffer |
translateLogicalVar(java.lang.StringBuffer name)
Build the Stringbuffer for an variable.
|
protected abstract java.lang.StringBuffer |
translateNull()
Translate the NULL element
|
protected abstract java.lang.StringBuffer |
translateNullSort()
Translate the NULL element's Sort.
|
protected abstract java.lang.StringBuffer |
translateObjectEqual(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the Stringbuffer for an object equivalence.
|
protected abstract java.lang.StringBuffer |
translatePredicate(java.lang.StringBuffer name,
java.util.ArrayList<java.lang.StringBuffer> args)
Translate a predicate.
|
protected abstract java.lang.StringBuffer |
translatePredicateName(java.lang.StringBuffer name)
Get the name for a predicate symbol.
|
java.lang.StringBuffer |
translateProblem(Sequent sequent,
Services services,
SMTSettings settings)
Translates a problem into the given syntax.
|
protected abstract java.lang.StringBuffer |
translateSort(java.lang.String name,
boolean isIntVal)
Translate a sort.
|
java.util.ArrayList<java.lang.StringBuffer> |
translateTaclets(Services services,
SMTSettings settings)
Translates the list
tacletFormulae to the given syntax. |
protected java.lang.StringBuffer |
translateTerm(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Translates the given term into input syntax and adds the resulting
string to the StringBuffer sb.
|
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.
|
protected java.lang.StringBuffer |
translateUniqueness(AbstractSMTTranslator.FunctionWrapper function,
java.util.Collection<AbstractSMTTranslator.FunctionWrapper> distinct)
Translates the unique-property of a function.
|
protected java.lang.StringBuffer |
translateUnknown(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Takes care of sequent tree parts that were not matched in
translate(term, skolemization).
|
protected java.lang.StringBuffer |
translateVariable(Operator op) |
protected static final int YESNOT
protected java.lang.String text
protected java.util.HashMap<Sort,java.lang.StringBuffer> usedDisplaySort
protected java.util.HashMap<Sort,java.lang.StringBuffer> usedRealSort
public AbstractSMTTranslator(Sequent sequent, Services services, AbstractSMTTranslator.Configuration config)
sequent
- The sequent which shall be translated.services
- The services object belonging to sequent.public AbstractSMTTranslator(Services s, AbstractSMTTranslator.Configuration config)
s
- public TacletSetTranslation getTacletSetTranslation()
public final java.lang.StringBuffer translateProblem(Sequent sequent, Services services, SMTSettings settings) throws IllegalFormulaException
SMTTranslator
translate(Term t, Services services)
is that assumptions
will be added.translateProblem
in interface SMTTranslator
sequent
- the sequent to be translated.IllegalFormulaException
public java.util.Collection<java.lang.Throwable> getExceptionsOfTacletTranslation()
protected final SMTSettings getSettings()
public AbstractSMTTranslator.Configuration getConfig()
protected abstract java.lang.StringBuffer buildCompleteText(java.lang.StringBuffer formula, java.util.ArrayList<java.lang.StringBuffer> assum, java.util.ArrayList<de.uka.ilkd.key.smt.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<de.uka.ilkd.key.smt.ContextualBlock> predicateBlocks, java.util.ArrayList<java.lang.StringBuffer> types, SortHierarchy sortHierarchy, SMTSettings settings)
formula
- The formula, that was built out of the internal
representation. It is built by ante implies succ.assum
- 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 abstract boolean isMultiSorted()
protected abstract java.lang.StringBuffer getIntegerSort()
protected abstract java.lang.StringBuffer getBoolSort()
protected abstract java.lang.StringBuffer translateLogicalNot(java.lang.StringBuffer arg)
arg
- The Formula to be negated.protected abstract java.lang.StringBuffer translateLogicalAnd(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract java.lang.StringBuffer translateLogicalOr(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract java.lang.StringBuffer translateLogicalImply(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract java.lang.StringBuffer translateLogicalEquivalence(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract java.lang.StringBuffer translateLogicalAll(java.lang.StringBuffer var, java.lang.StringBuffer type, java.lang.StringBuffer form)
var
- the bounded variable.type
- the type of the bounded variable.form
- The formula containing the bounded variable.protected abstract java.lang.StringBuffer translateLogicalExist(java.lang.StringBuffer var, java.lang.StringBuffer type, java.lang.StringBuffer form)
var
- the bounded variable.type
- the type of the bounded variable.form
- The formula containing the bounded variable.protected abstract java.lang.StringBuffer translateLogicalTrue()
protected abstract java.lang.StringBuffer translateLogicalFalse()
protected abstract java.lang.StringBuffer translateObjectEqual(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula of the equivalence.arg2
- The second formula of the equivalence.protected abstract java.lang.StringBuffer translateLogicalVar(java.lang.StringBuffer name)
protected abstract java.lang.StringBuffer translateLogicalConstant(java.lang.StringBuffer name)
protected abstract java.lang.StringBuffer translatePredicate(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args)
name
- The Symbol of the predicate.args
- The arguments of the predicate.protected abstract java.lang.StringBuffer translatePredicateName(java.lang.StringBuffer name)
name
- The name that can be used to create the symbol.protected abstract java.lang.StringBuffer translateFunction(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args)
name
- The Symbol of the function.args
- The arguments of the function.protected abstract java.lang.StringBuffer translateFunctionName(java.lang.StringBuffer name)
name
- The name that can be used to create the symbol.protected java.lang.StringBuffer translateIntegerPlus(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- first val of the sum.arg2
- second val of the sum.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerMinus(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the substraction.arg2
- second val of the substraction.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerUnaryMinus(java.lang.StringBuffer arg) throws IllegalFormulaException
arg
- the argument of the unary minus.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerMult(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the multiplication.arg2
- second val of the multiplication.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerDiv(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the division.arg2
- second val of the division.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerMod(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the modulo.arg2
- second val of the modulo.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerGt(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the greater than.arg2
- second val of the greater than.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerLt(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the less than.arg2
- second val of the less than.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerGeq(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the greater or equal.arg2
- second val of the greater or equal.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerLeq(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the less or equal.arg2
- second val of the less or equal.IllegalFormulaException
protected abstract java.lang.StringBuffer translateNull()
protected abstract java.lang.StringBuffer getNullName()
protected abstract java.lang.StringBuffer translateNullSort()
protected abstract java.lang.StringBuffer translateSort(java.lang.String name, boolean isIntVal)
name
- the sorts nameisIntVal
- true, if the sort should represent some kind of
integerprotected java.lang.StringBuffer translateIntegerValue(long val) throws IllegalFormulaException
IllegalFormulaException
protected abstract java.lang.StringBuffer translateLogicalIfThenElse(java.lang.StringBuffer cond, java.lang.StringBuffer ifterm, java.lang.StringBuffer elseterm)
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
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 translateUniqueness(AbstractSMTTranslator.FunctionWrapper function, java.util.Collection<AbstractSMTTranslator.FunctionWrapper> distinct) throws IllegalFormulaException
function
- the function itselfdistinct
- the set of functions, that should be distinct.IllegalFormulaException
protected java.lang.StringBuffer buildInjectiveFunctionAssumption(AbstractSMTTranslator.FunctionWrapper fw)
protected java.util.ArrayList<java.lang.StringBuffer> createGenericVariables(int count, int start)
protected java.lang.StringBuffer translateDistinct(AbstractSMTTranslator.FunctionWrapper[] functions)
protected java.lang.StringBuffer translateLogicalAll(java.util.ArrayList<java.lang.StringBuffer> variables, java.util.ArrayList<Sort> sorts, java.lang.StringBuffer result)
protected java.lang.StringBuffer translateLogicalAll(java.lang.StringBuffer var, Sort sort, java.lang.StringBuffer result)
protected java.lang.StringBuffer translateTerm(Term term, java.util.Vector<QuantifiableVariable> quantifiedVars, Services services) throws IllegalFormulaException
term
- the Term which should be written in Simplify syntaxquantifiedVars
- a Vector containing all variables that have been bound
in super-terms. It is only used for the translation of
modulo terms, but must be looped through until we get
there.IllegalFormulaException
protected java.lang.StringBuffer getTypePredicate(Sort s, java.lang.StringBuffer arg)
s
- The sort, the type predicate is wanted for.arg
- The expression, whose type should be defined.protected final java.lang.StringBuffer translateUnknown(Term term, java.util.Vector<QuantifiableVariable> quantifiedVars, Services services) throws IllegalFormulaException
term
- The Term given to translateIllegalFormulaException
protected final java.lang.StringBuffer translateVariable(Operator op)
protected final java.lang.StringBuffer translateFunc(Operator o, java.util.ArrayList<java.lang.StringBuffer> sub)
o
- the Operator used for this function.sub
- The StringBuffers representing the arguments of this
Function.protected final java.lang.StringBuffer translateBsumFunction(Term bsumterm, java.util.ArrayList<java.lang.StringBuffer> sub)
bsumterm
- The term used as third argument of the bsum function.protected final java.lang.StringBuffer translateBprodFunction(Term bprodterm, java.util.ArrayList<java.lang.StringBuffer> sub)
bprodterm
- The term used as third argument of the bsum function.protected boolean isSomeIntegerSort(Sort s)
protected java.lang.StringBuffer makeUnique(java.lang.StringBuffer name)
public java.util.ArrayList<java.lang.StringBuffer> translateTaclets(Services services, SMTSettings settings) throws IllegalFormulaException
tacletFormulae
to the given syntax.services
- used for translateTerm
IllegalFormulaException
protected java.lang.StringBuffer translateComment(int newLines, java.lang.String comment)
Copyright © 2003-2019 The KeY-Project.