001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: /* Generated by Together */
012:
013: package de.uka.ilkd.key.logic.op;
014:
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.sort.*;
018:
019: /**
020: * This class represents an equality symbol for a given sort.
021: * The system will generate automatically for each sort exactly one
022: * equality symbol. For the special sort Formula the corresponding equality
023: * symbol is the equivalence-junctor {@link Op#EQV}.
024: */
025: public class Equality extends Op {
026:
027: private final Sort targetSort;
028:
029: /**
030: * generates a new equality symbol for the given target sort.
031: * Don't call this, but {@link Sort#getEqualitySymbol()}. In case of
032: * schemavariables without sort on both sides (e.g. two program SVs)
033: * @param targetSort - sort for which the equality symbol is generated.
034: */
035: Equality(Name name) {
036: this (name, Sort.ANY);
037: }
038:
039: /**
040: * generates a new equality symbol for the given target sort and a
041: * given name.
042: * Don't call this, but use {@link Op#EQV} or {@link Op#EQUALS}.
043: * @param targetSort - sort for which the equality symbol is generated.
044: * @param name - name for the equality symbol
045: */
046: Equality(Name name, Sort targetSort) {
047: super (name);
048: this .targetSort = targetSort;
049: }
050:
051: /**
052: * @return Sort of the term consisting of the given subterms if it would
053: * have this operator as top level operator
054: */
055: public Sort sort(Term[] term) {
056: return Sort.FORMULA;
057: }
058:
059: /**
060: * returns the sort of the <tt>i</tt>-th argument
061: */
062: public Sort argSort(int i) {
063: return targetSort == Sort.FORMULA ? Sort.FORMULA : Sort.ANY;
064: }
065:
066: /** @return arity of the Equality as int that is 2*/
067: public int arity() {
068: return 2;
069: }
070:
071: /**
072: * checks if the given term is syntactically valid at its top
073: * level assumed the top level operator were this, i.e. if the
074: * direct subterms can be subterms of a term with this top level
075: * operator, the method returns true. Furthermore, it is checked
076: * that no variables are bound for none of the subterms.
077: * If a subterm is a schemavariable, the whole term is accepted.
078: * @param term the Term to be checked.
079: * @return true iff the given term has
080: * subterms that are suitable for this function.
081: */
082: public boolean validTopLevel(Term term) {
083: if (term.arity() != arity()) {
084: return false;
085: }
086:
087: for (int i = 0; i < arity(); i++) {
088: Sort sort = term.sub(i).sort();
089: if (term.sub(i).op() instanceof SchemaVariable
090: || sort instanceof ProgramSVSort
091: || sort == AbstractMetaOperator.METASORT) {
092: return true;
093: }
094: }
095:
096: final Sort t0Sort = term.sub(0).sort();
097: final Sort t1Sort = term.sub(1).sort();
098:
099: if (t0Sort instanceof PrimitiveSort != t1Sort instanceof PrimitiveSort) {
100: return false;
101: }
102:
103: if (targetSort == Sort.FORMULA || t0Sort == Sort.FORMULA
104: || t1Sort == Sort.FORMULA) {
105: return t0Sort == Sort.FORMULA && t1Sort == Sort.FORMULA
106: && targetSort == Sort.FORMULA;
107: }
108:
109: return t0Sort.extendsTrans(targetSort)
110: && t1Sort.extendsTrans(targetSort);
111: }
112:
113: }
|