| java.lang.Object
 de.uka.ilkd.key.proof.decproc.DecProcTranslation
All known Subclasses: de.uka.ilkd.key.proof.decproc.ICSTranslation, de.uka.ilkd.key.proof.decproc.SimplifyTranslation,
| DecProcTranslation | | abstract public class DecProcTranslation (Code) | | Represents a try to remove code duplication.
|
| Method Summary | |
| protected void | collectQuantifiedVars(Vector quantifiedVars, Term term)
| | public String | getText()
| | public int | getUniqueHashCode(Object qv)
Returns a unique HashCode for the object qv.
Unique means unique for the goal given to the calling class.
This function does not depend on .hashcode() to deliver unique
hash codes like the memory address of the object. | | public int | getUniqueHashCodeForUninterpretedTerm(Term term)
Returns a unique HashCode for the term qv.
Unique means unique for the goal given to the calling class.
This function does not depend on .hashcode() to deliver
unique hash codes like the memory address of the object. | | abstract protected StringBuffer | translate(Term term, int skolemization, Vector quantifiedVars)
Translates the given term into the decision procedure's 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). | | abstract protected StringBuffer | translate(Sequent sequent)
| | abstract protected StringBuffer | translate(Semisequent ss, int skolemization)
Translates the given Semisequent into the decision procedure's input
syntax and returns the resulting StringBuffer sb.
Parameters:
ss - the SemiSequent which should be written in the decisionprocedure's 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 for ICS ("not"s are notcounted). |
| ANTECEDENT | | final protected static int ANTECEDENT(Code) | | |
| SUCCEDENT | | final protected static int SUCCEDENT(Code) | | |
| YESNOT | | final protected static int YESNOT(Code) | | |
| constraintSet | | final protected ConstraintSet constraintSet(Code) | | The Constraint under which the sequent is to be proven
|
| localMetavariables | | final protected SetOfMetavariable localMetavariables(Code) | | |
| moduloConstraints | | final protected List moduloConstraints(Code) | | |
| moduloCounter | | protected int moduloCounter(Code) | | |
| moduloReplacements | | final protected HashMap moduloReplacements(Code) | | |
| nogger | | static Logger nogger(Code) | | |
| notes | | final protected StringBuffer notes(Code) | | StringBuffer to store text which could be usefull for the user
|
| predicate | | final protected StringBuffer predicate(Code) | | StringBuffer contains all declared predicate symbols.
|
| predicateSet | | final protected Set predicateSet(Code) | | remember all printed predicates
|
| text | | protected String text(Code) | | The translation result is stored in this variable.
|
| usedLocalMv | | final protected HashSet usedLocalMv(Code) | | To handle local metavariabls we have to quantify them existentially. We
do not need to quantify already substituted metavariables.
|
| variableMap | | final protected HashMap variableMap(Code) | | Some terms should need a unique HashCode (CVC doesn't handle quantors,
ProgramVariables from different blocks could have the same name),
functions and user named skolemfunctions can get the same name. The
difference to variables is that the have quantified variables so they
have to be compared moduloRenaming. Comparing terms without variables
with .equals() instead of .equalsModRenaming() should give a speed
improvement.
|
| DecProcTranslation | | public DecProcTranslation(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 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. |
| collectQuantifiedVars | | protected void collectQuantifiedVars(Vector quantifiedVars, Term term)(Code) | | Just copies the quantified variables of term into quantifiedVars
Parameters:
quantifiedVars -
Parameters:
term - |
| getText | | public String getText()(Code) | | Returns the sequent given with the constructor in Simplify
syntax (as far as possible)
|
| getUniqueHashCode | | public int getUniqueHashCode(Object qv)(Code) | | Returns a unique HashCode for the object qv.
Unique means unique for the goal given to the calling class.
This function does not depend on .hashcode() to deliver unique
hash codes like the memory address of the object. It uses a
hashMap and compares every new Object in O(n) (n number of
Objects with the same .hashCode()) to all others.
Parameters:
v - the Object the hashcode should be returned. |
| getUniqueHashCodeForUninterpretedTerm | | public int getUniqueHashCodeForUninterpretedTerm(Term term)(Code) | | Returns a unique HashCode for the term qv.
Unique means unique for the goal given to the calling class.
This function does not depend on .hashcode() to deliver
unique hash codes like the memory address of the object.
It uses a hashMap and compares
every new Object in O(n) (n number of Objects
with the same .hashCode()) to all others.
It compares with .equalsModRenaming().
Parameters:
term - the Term the hashcode should be returned. |
| translate | | abstract protected StringBuffer translate(Term term, int skolemization, Vector quantifiedVars) throws SimplifyException(Code) | | Translates the given term into the decision procedure's 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). ForSimplify this parameter is ignored.
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. |
| translate | | abstract protected StringBuffer translate(Sequent sequent) throws SimplifyException(Code) | | Translates the given sequent into the decision procedure's input syntax
Parameters:
s - the Sequent which should be translated the translated version of s |
| translate | | abstract protected StringBuffer translate(Semisequent ss, int skolemization) throws SimplifyException(Code) | | Translates the given Semisequent into the decision procedure's input
syntax and returns the resulting StringBuffer sb.
Parameters:
ss - the SemiSequent which should be written in the decisionprocedure's 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 for ICS ("not"s are notcounted). For Simplify this parameter is ignored. |
|
|