| java.lang.Object
 de.uka.ilkd.key.proof.decproc.DecProcTranslation
de.uka.ilkd.key.proof.decproc.ICSTranslation
| 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.
This is Simplify stuff. | | final protected StringBuffer | getUniqueVariableName(Operator op)
| | 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. | | final 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(Semisequent ss, int skolemization)
Translates the given Semisequent into "ICS" input syntax
and returns the resulting StringBuffer sb. | | final protected StringBuffer | translate(ConstrainedFormula cf, int skolemization, boolean overWriteUsed)
Translates the given ConstrainedFormula into "ICS" input and returns the
resulting StringBuffer sb.
Parameters:
cf - the ConstrainedFormula which should be written in ICS syntax
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENTor with YESNOT if a "not" operation occurres above the termwhich will prevent skolemization ("not"s are not counted).
Parameters:
overWriteUsed - the ConstrainedFormulas generated in the modulo replacementprocess are not "used" elsewhere. | | final protected StringBuffer | translate(Term term, int skolemization, Vector quantifiedVars)
Translates the given term into "ICS" input syntax and and returns
the resulting StringBuffer sb.
Parameters:
term - the Term which should be written in Simplify syntax
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENTor with YESNOT if a "not" operation occurres above the termwhich will prevent skolemization ("not"s are not counted).
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. | | final protected StringBuffer | translateAttributeOpTerm(Term term, int skolemization, Vector quantifiedVars)
Takes an AttributeOp like a.b and translates into a_1(b_2)
Parameters:
term - The term to be converted.
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENTor with YESNOT if a "not" operation occurres above the termwhich will prevent skolemization ("not"s are not counted).
Parameters:
quantifiedVars - a Vector containing all variables that have been bound insuper-terms. | | final protected StringBuffer | translateBinaryInfixTerm(Term term, String name, int brackets, int skolemization, Vector quantifiedVars)
Takes a binary infix-term and translates it with its arguments into the
ICS syntax. | | final protected String | translateLimitTerm(String name)
| | final protected StringBuffer | translatePrefixTerm(Term term, String name, int brackets, int skolemization, Vector quantifiedVars)
Takes a prefix-term and translates it with its arguments into the ICS
syntax. | | protected StringBuffer | translateUnknown(Term term, int skolemization)
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. | | 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)
Takes a term which is ICS not capable of handling. |
| BOOLEAN | | final protected static int BOOLEAN(Code) | | |
| FUNCTION | | final protected static int FUNCTION(Code) | | |
| NONE | | final protected static int NONE(Code) | | |
| PREDICATE | | final protected static int PREDICATE(Code) | | |
| logger | | static Logger logger(Code) | | |
| ICSTranslation | | public ICSTranslation(Sequent sequent, ConstraintSet cs, SetOfMetavariable localmv, Services services) throws SimplifyException(Code) | | Just a constructor which starts the conversion to Simplify syntax.
The result can be fetched with @see 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 introducedafter the 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.
This is Simplify stuff. What does it do here? TOD
Parameters:
name - The name of the predicate (no KeY representation of it has to exist, sometimes constructs not supported by ICS are mapped to predicates).
Parameters:
arity - The arity of the term. |
| getUniqueVariableName | | final protected StringBuffer getUniqueVariableName(Operator op)(Code) | | produces a unique name for the given Variable, with a unique hashcode and
without characters ICS does not understand
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 in reverse order compared to the internal order in KeY |
| produceClosure | | final 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.
This method is completely useless at the moment since ICS cannot handle
quantifiers yet.
Parameters:
s - The StringBuffer the quantifieres shall be pre- and the trailing parantheses be appended. |
| translate | | final protected StringBuffer translate(Sequent sequent) throws SimplifyException(Code) | | Translates the given sequent into "ICS" input syntax
Parameters:
s - the Sequent which should be written in ICS syntax the translated version of s |
| translate | | final protected StringBuffer translate(Semisequent ss, int skolemization) throws SimplifyException(Code) | | Translates the given Semisequent into "ICS" input syntax
and returns the resulting StringBuffer sb.
Parameters:
ss - the SemiSequent which should be written in ICS syntax
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENT or with YESNOT if a "not" operation occurres above the term which will prevent skolemization ("not"s are not counted). |
| translate | | final protected StringBuffer translate(ConstrainedFormula cf, int skolemization, boolean overWriteUsed) throws SimplifyException(Code) | | Translates the given ConstrainedFormula into "ICS" input and returns the
resulting StringBuffer sb.
Parameters:
cf - the ConstrainedFormula which should be written in ICS syntax
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENTor with YESNOT if a "not" operation occurres above the termwhich will prevent skolemization ("not"s are not counted).
Parameters:
overWriteUsed - the ConstrainedFormulas generated in the modulo replacementprocess are not "used" elsewhere. This can be compensated withthis flag. |
| translate | | final protected StringBuffer translate(Term term, int skolemization, Vector quantifiedVars) throws SimplifyException(Code) | | Translates the given term into "ICS" input syntax and and returns
the resulting StringBuffer sb.
Parameters:
term - the Term which should be written in Simplify syntax
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENTor with YESNOT if a "not" operation occurres above the termwhich will prevent skolemization ("not"s are not counted).
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, int skolemization, Vector quantifiedVars) throws SimplifyException(Code) | | Takes an AttributeOp like a.b and translates into a_1(b_2)
Parameters:
term - The term to be converted.
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENTor with YESNOT if a "not" operation occurres above the termwhich will prevent skolemization ("not"s are not counted).
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 |
| translateBinaryInfixTerm | | final protected StringBuffer translateBinaryInfixTerm(Term term, String name, int brackets, int skolemization, Vector quantifiedVars) throws SimplifyException(Code) | | Takes a binary infix-term and translates it with its arguments into the
ICS syntax. Examples are x > y, [x | y]
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:
brackets - logical terms can (and should) be put into brackets (if theyare composite), function terms into rounded parantheses;indicate that with one of NONE, BOOLEAN, FUNCTION or PREDICATE
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENTor with YESNOT if a "not" operation occurres above the termwhich will prevent skolemization ("not"s are not counted).
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 |
| translateLimitTerm | | final protected String translateLimitTerm(String name)(Code) | |
Parameters:
name - The name of the term |
| translatePrefixTerm | | final protected StringBuffer translatePrefixTerm(Term term, String name, int brackets, int skolemization, Vector quantifiedVars) throws SimplifyException(Code) | | Takes a prefix-term and translates it with its arguments into the ICS
syntax. Examples are x, f(x), f(x, y)
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:
brackets - logical terms can (and should) be put into brackets (if theyare composite), function terms into rounded parantheses;indicate that with one of NONE, BOOLEAN, FUNCTION or PREDICATE
Parameters:
skolemization - Indicates whether the formula is in the ANTECEDENT, SUCCEDENTor with YESNOT if a "not" operation occurres above the termwhich will prevent skolemization ("not"s are not counted).
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, int skolemization) 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
Parameters:
skolemization - dto. new StringBuffer();
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. |
| uninterpretedTerm | | final protected StringBuffer uninterpretedTerm(Term term, boolean modRenaming)(Code) | | Takes a term which is ICS not capable of handling. This term is
translated into a predicate.
Parameters:
term - the Term ICS cannot handle directly
Parameters:
modRenaming - true iff equality should be modulo renaming or not. This willresult in the same names, if just the free variables aredifferent, but the rest isn't. |
|
|