| java.lang.Object
 de.uka.ilkd.key.proof.decproc.DecProcTranslation
de.uka.ilkd.key.proof.decproc.SimplifyTranslation
| SimplifyTranslation | | public class SimplifyTranslation extends DecProcTranslation (Code) | |
author:
daniels
author:
The class responsible for converting a sequent into the Simplify input language.
author:
It is public because ASM-KeY inherits form it to provide a version suppporting
author:
asm operators. |
| Field Summary | |
| static Logger | logger
|
| Method Summary | |
| final protected void | addPredicate(String name, int arity)
Adds a predicate to the internal set and adds a line to declare the
predicate to the declarator stringbuffer. | | final protected StringBuffer | getUniqueVariableName(Named op)
produces a unique name for the given Variable, enclosed in '|' and with a
unique hashcode. | | protected StringBuffer | opNotKnownWarning(Term term)
| | final protected StringBuffer | printlastfirst(Term t)
For some terms (AttributeOps) the order in KeY is different than the
order of the user or Simplify expects. | | protected String | produceClosure(StringBuffer s)
Goes through the collected metavariables and quantifies them with
universal-quantifieres if they are global and with existential
quantifiers if they are local. | | final protected StringBuffer | translate(Sequent sequent)
| | final protected StringBuffer | translate(Sequent sequent, boolean lightWeight)
Translates the given sequent into "Simplify" input syntax and adds the
resulting string to the StringBuffer sb. | | final protected StringBuffer | translate(Semisequent ss, int skolemization)
| | final protected StringBuffer | translate(Semisequent ss, int skolemization, boolean lightWeight)
Translates the given Semisequent into "Simplify" input syntax and adds
the resulting string to the StringBuffer sb. | | final protected StringBuffer | translate(ConstrainedFormula cf, boolean lightWeight)
Translates the given ConstrainedFormula into "Simplify" input syntax and
adds the resulting string to the StringBuffer sb. | | final public StringBuffer | translate(Term term, Vector quantifiedVars)
Translates the given term into "Simplify" input syntax and adds the
resulting string to the StringBuffer sb.
Parameters:
term - the Term which should be written in Simplify syntax
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. | | final protected StringBuffer | translate(Term term, int skolemization, Vector quantifiedVars)
| | final protected StringBuffer | translateAttributeOpTerm(Term term, Vector quantifiedVars)
Takes an AttributeOp and translates it into the Simplify syntax.
Parameters:
term - The term to be converted.
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. | | final protected StringBuffer | translateSimpleTerm(Term term, String name, Vector quantifiedVars)
Takes a term and translates it with its argument in the Simplify syntax.
Parameters:
term - The term to be converted.
Parameters:
name - The name that should be used for the term (should be unique,it should be taken care of that somewhere else (if desired)).
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. | | final protected StringBuffer | translateUnaryMinus(Term term, String name, Vector quantifiedVars)
Translates the unary minus ~m into a "0 -" construct. | | protected StringBuffer | translateUnknown(Term term)
Takes care of sequent tree parts that were not matched in translate(term,
skolemization). | | final protected StringBuffer | translateVariable(Operator op)
Used to give a variable (program, logic, meta) a unique name. | | final protected StringBuffer | uninterpretedTerm(Term term, boolean modRenaming)
|
| logger | | static Logger logger(Code) | | |
| SimplifyTranslation | | public SimplifyTranslation(Sequent sequent, ConstraintSet cs, SetOfMetavariable localmv, Services services, boolean lightWeight) throws SimplifyException(Code) | | Just a constructor which starts the conversion to Simplify syntax. The
result can be fetched with
See Also: getText-
Parameters:
sequent - The sequent which shall be translated.
Parameters:
cs - The constraints which shall be incorporated.
Parameters:
localmv - The local metavariables, should be the ones introduced afterthe last branch. |
| addPredicate | | final protected void addPredicate(String name, int arity)(Code) | | Adds a predicate to the internal set and adds a line to declare the
predicate to the declarator stringbuffer.
Parameters:
name - The name of the predicate (no KeY representation jas toexist).
Parameters:
arity - The arity of the term. |
| getUniqueVariableName | | final protected StringBuffer getUniqueVariableName(Named op)(Code) | | produces a unique name for the given Variable, enclosed in '|' and with a
unique hashcode.
Parameters:
op - The variable to get a new name. |
| printlastfirst | | final protected StringBuffer printlastfirst(Term t)(Code) | | For some terms (AttributeOps) the order in KeY is different than the
order of the user or Simplify expects.
the simplified version of the Term t in reversed order
Parameters:
t - the Term which should be written in Simplify syntax, but inreverse order compared to the internal order in KeY |
| produceClosure | | protected String produceClosure(StringBuffer s)(Code) | | Goes through the collected metavariables and quantifies them with
universal-quantifieres if they are global and with existential
quantifiers if they are local.
Parameters:
s - The StringBuffer the quantifieres shall be pre- and the trailing parantheses be appended. |
| translate | | final protected StringBuffer translate(Sequent sequent, boolean lightWeight) throws SimplifyException(Code) | | Translates the given sequent into "Simplify" input syntax and adds the
resulting string to the StringBuffer sb.
Parameters:
s - the Sequent which should be written in Simplify syntax |
| translate | | final protected StringBuffer translate(Semisequent ss, int skolemization, boolean lightWeight) throws SimplifyException(Code) | | Translates the given Semisequent into "Simplify" input syntax and adds
the resulting string to the StringBuffer sb.
Parameters:
ss - the SemiSequent which should be written in Simplify syntax
Parameters:
antesucc - true for antecedent, false for succedent |
| translate | | final protected StringBuffer translate(ConstrainedFormula cf, boolean lightWeight) throws SimplifyException(Code) | | Translates the given ConstrainedFormula into "Simplify" input syntax and
adds the resulting string to the StringBuffer sb.
Parameters:
cf - the ConstrainedFormula which should be written in Simplifysyntax |
| translate | | final public StringBuffer translate(Term term, Vector quantifiedVars) throws SimplifyException(Code) | | Translates the given term into "Simplify" input syntax and adds the
resulting string to the StringBuffer sb.
Parameters:
term - the Term which should be written in Simplify syntax
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. It is only used for the translation of moduloterms, but must be looped through until we get there. |
| translateAttributeOpTerm | | final protected StringBuffer translateAttributeOpTerm(Term term, Vector quantifiedVars) throws SimplifyException(Code) | | Takes an AttributeOp and translates it into the Simplify syntax.
Parameters:
term - The term to be converted.
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. It is only used for the translation of moduloterms, but must be looped through until we get there. |
| translateSimpleTerm | | final protected StringBuffer translateSimpleTerm(Term term, String name, Vector quantifiedVars) throws SimplifyException(Code) | | Takes a term and translates it with its argument in the Simplify syntax.
Parameters:
term - The term to be converted.
Parameters:
name - The name that should be used for the term (should be unique,it should be taken care of that somewhere else (if desired)).
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. It is only used for the translation of moduloterms, but must be looped through until we get there. |
| translateUnaryMinus | | final protected StringBuffer translateUnaryMinus(Term term, String name, Vector quantifiedVars) throws SimplifyException(Code) | | Translates the unary minus ~m into a "0 -" construct. Could be solved
better with a newly created term!!!
Parameters:
term - The term to be converted.
Parameters:
name - The name that should be used for the term (should be unique,it should be taken care of that somewhere else (if desired)).
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. It is only used for the translation of moduloterms, but must be looped through until we get there. |
| translateUnknown | | protected StringBuffer translateUnknown(Term term) throws SimplifyException(Code) | | Takes care of sequent tree parts that were not matched in translate(term,
skolemization). In this class it just produces a warning, nothing more.
It is provided as a hook for subclasses.
Parameters:
term - The Term given to translate
throws:
SimplifyException - |
| translateVariable | | final protected StringBuffer translateVariable(Operator op)(Code) | | Used to give a variable (program, logic, meta) a unique name.
Parameters:
op - The variable to be translated/renamed. |
|
|