0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010:
0011: package de.uka.ilkd.key.logic.op;
0012:
0013: import java.util.*;
0014:
0015: import de.uka.ilkd.key.java.Services;
0016: import de.uka.ilkd.key.logic.*;
0017: import de.uka.ilkd.key.logic.sort.Sort;
0018: import de.uka.ilkd.key.rule.MatchConditions;
0019: import de.uka.ilkd.key.rule.updatesimplifier.GuardSatisfiabilityFormulaBuilder;
0020: import de.uka.ilkd.key.rule.updatesimplifier.GuardSimplifier;
0021: import de.uka.ilkd.key.util.Debug;
0022:
0023: /**
0024: * <p>
0025: * Operator for simultaneous, guarded and quantified updates. In concrete
0026: * syntax, such updates have the shape
0027: * <tt> [ for (Variables) ] [ if (Formula) ] lhs := value
0028: * ( , [ for (Variables) ] [ if (Formula) ] lhs := value ) * </tt>.
0029: * </p>
0030: * <p>
0031: * The update operator is uniquely defined by the contained locations, their
0032: * order, and the information which of the assigments are guarded (a boolean
0033: * array). This has some odd consequences of the sub terms of an update term as
0034: * given above:
0035: * <ol>
0036: * <li>Let <code> loc_1,...,loc_i </code> be local or static variables then
0037: * only the corresponding values <code>val_1, ..., val_n</code> are subterms
0038: * the locations itself are part of the operator.</li>
0039: * <li>For <code>loc_i (=r_i.a_i),...,loc_n(=r_n.a_n)</code> that refer to an
0040: * instance attribute, only their reference prefix <code>r_i</code> is a
0041: * subterm while the attribute <code> a_i </code> is part of the update
0042: * operator. If <code>loc_i</code> is an array <code>a[l]</code> then the
0043: * sort of <code> a </code> is fixed and <code>a, i</code> are sub terms</li>
0044: * </ol>
0045: * There are methods that return the location access part (attribute, local or
0046: * static variable) and also the complete n-th location as term.
0047: * </p>
0048: */
0049: public class QuanUpdateOperator implements IUpdateOperator {
0050:
0051: private final static TermFactory tf = TermFactory.DEFAULT;
0052: private final static TermBuilder tb = TermBuilder.DF;
0053:
0054: /**
0055: * The signature that uniquely identifies instances of the quantified update
0056: * operator. This consists of the list of locations that are updated and a
0057: * boolean array telling which of these elementary updates is also equipped
0058: * with a guard
0059: */
0060: private static class QuanUpdateSignature {
0061: /** the locations access operators used by the update op */
0062: public final ArrayOfLocation locations;
0063: /** which of the update entries are equipped with a guard? */
0064: public final boolean[] guards;
0065:
0066: public QuanUpdateSignature(final Location[] locations,
0067: final boolean[] guards) {
0068: this .locations = new ArrayOfLocation(locations);
0069: this .guards = (boolean[]) guards.clone();
0070: }
0071:
0072: /* (non-Javadoc)
0073: * @see java.lang.Object#equals(java.lang.Object)
0074: */
0075: public boolean equals(Object o2) {
0076: if (!(o2 instanceof QuanUpdateSignature))
0077: return false;
0078: final QuanUpdateSignature sig2 = (QuanUpdateSignature) o2;
0079: return locations.equals(sig2.locations)
0080: && Arrays.equals(guards, sig2.guards);
0081: }
0082:
0083: /* (non-Javadoc)
0084: * @see java.lang.Object#hashCode()
0085: */
0086: public int hashCode() {
0087: int res = locations.hashCode();
0088: // the following should be replaced with java.util.Arrays.hashCode
0089: // (Java 1.5)
0090: for (int i = 0; i != guards.length; ++i) {
0091: if (guards[i])
0092: ++res;
0093: res *= 3;
0094: }
0095: return res;
0096: }
0097: }
0098:
0099: /**
0100: * name of the operator
0101: */
0102: private final Name name;
0103:
0104: /** the arity of this operator */
0105: private final int arity;
0106:
0107: private final QuanUpdateSignature signature;
0108:
0109: /**
0110: * table to determine the position of the value to a given location
0111: */
0112: private final int[] valuePositionTable;
0113:
0114: /**
0115: * Map from <code>QuanUpdateSignature</code> to
0116: * <code>QuanUpdateOperator</code>
0117: */
0118: private static final HashMap updates = new HashMap();
0119:
0120: /**
0121: * returns the update operator for the given location order
0122: */
0123: public static QuanUpdateOperator createUpdateOp(Term[] locs,
0124: boolean[] guards) {
0125: Location[] locOps = new Location[locs.length];
0126: for (int i = locs.length - 1; i >= 0; i--) {
0127: locOps[i] = (Location) locs[i].op();
0128: }
0129: return createUpdateOp(locOps, guards);
0130: }
0131:
0132: /**
0133: * @param guards
0134: * boolean array telling which of the elementary updates are
0135: * guarded
0136: * @return the update operator for the given location order
0137: */
0138: public static QuanUpdateOperator createUpdateOp(Location[] locs,
0139: boolean[] guards) {
0140: final QuanUpdateSignature sig = new QuanUpdateSignature(locs,
0141: guards);
0142: QuanUpdateOperator result = (QuanUpdateOperator) updates
0143: .get(sig);
0144: if (result == null) {
0145: result = new QuanUpdateOperator(sig);
0146: updates.put(sig, result);
0147: }
0148: return result;
0149: }
0150:
0151: /**
0152: * creates the update operator for the given signature
0153: *
0154: * @param name the Name of the quanified update operator
0155: * @param signature the {@link QuanUpdateSignature} of the update
0156: * operator to be created
0157: */
0158: private QuanUpdateOperator(Name name, QuanUpdateSignature signature) {
0159: this .name = name;
0160: this .signature = signature;
0161: this .valuePositionTable = new int[signature.locations.size()];
0162:
0163: fillValuePositionTable();
0164: this .arity = signature.locations.size() == 0 ? 1
0165: : valuePositionTable[valuePositionTable.length - 1] + 2;
0166: }
0167:
0168: /**
0169: * the given locations are the one to be updated by this operator
0170: * @param location
0171: */
0172: private QuanUpdateOperator(QuanUpdateSignature signature) {
0173: this (new Name("quanUpdate(" + signature.locations + ")"),
0174: signature);
0175: }
0176:
0177: /**
0178: * Replace the locations of this operator without changing anything else.
0179: * This must not change the number of locations, i.e.
0180: * <code>newLocs.length==locationCount()</code>
0181: */
0182: public IUpdateOperator replaceLocations(Location[] newLocs) {
0183: Debug.assertTrue(newLocs.length == locationCount());
0184: return createUpdateOp(newLocs, signature.guards);
0185: }
0186:
0187: /**
0188: * returns the array of location operators which are updated
0189: */
0190: public ArrayOfLocation locationsAsArray() {
0191: return signature.locations;
0192: }
0193:
0194: /**
0195: * returns the number of locations
0196: *
0197: * @return the number of locations as int
0198: */
0199: public int locationCount() {
0200: return locationsAsArray().size();
0201: }
0202:
0203: /**
0204: * returns the operator of <tt>n</tt>-th location
0205: */
0206: public Location location(int n) {
0207: return locationsAsArray().getLocation(n);
0208: }
0209:
0210: /**
0211: * returns the number of the subterm representing the value to which
0212: * the locPos-th location is updated
0213: */
0214: public int valuePos(int locPos) {
0215: return valuePositionTable[locPos];
0216: }
0217:
0218: /**
0219: * @return <code>true</code> iff the elementary update with index
0220: * <code>locPos</code> is guarded
0221: */
0222: public boolean guardExists(int locPos) {
0223: return signature.guards[locPos];
0224: }
0225:
0226: /**
0227: * @return the number of the subterm representing the guard constraining the
0228: * <tt>locPos</tt> -th update, provided that this guard exists
0229: * (otherwise <code>-1</code>)
0230: */
0231: public int guardPos(int locPos) {
0232: if (!guardExists(locPos))
0233: return -1;
0234: if (locPos == 0)
0235: return 0;
0236: return valuePos(locPos - 1) + 1;
0237: }
0238:
0239: /**
0240: * @return the index of the first subterm belonging to update entry
0241: * <code>locPos</code>
0242: */
0243: public int entryBegin(int locPos) {
0244: if (locPos == 0)
0245: return 0;
0246: return valuePos(locPos - 1) + 1;
0247: }
0248:
0249: /**
0250: * @return the index after the last subterm belonging to update entry
0251: * <code>locPos</code>. The entry is described within
0252: * <tt>[entryBegin(i), entryEnd(i))</tt>
0253: */
0254: public int entryEnd(int locPos) {
0255: return valuePos(locPos) + 1;
0256: }
0257:
0258: /**
0259: * @return the index of the first subterm belonging to the location of entry
0260: * <code>locPos</code>
0261: */
0262: public int locationSubtermsBegin(int locPos) {
0263: if (guardExists(locPos))
0264: return entryBegin(locPos) + 1;
0265: return entryBegin(locPos);
0266: }
0267:
0268: /**
0269: * @return the index after the last subterm belonging to the location of
0270: * update entry <code>locPos</code>. The location is described
0271: * within
0272: * <tt>[locationSubtermsBegin(i), locationSubtermsEnd(i))</tt>
0273: */
0274: public int locationSubtermsEnd(int locPos) {
0275: return entryEnd(locPos) - 1;
0276: }
0277:
0278: /**
0279: * @return the variables that are quantified for the elementary update
0280: * <code>locPos</code>
0281: */
0282: public ArrayOfQuantifiableVariable boundVars(Term t, int locPos) {
0283: return t.varsBoundHere(valuePos(locPos));
0284: }
0285:
0286: /**
0287: * returns an array with all location positions of <code>loc</code>
0288: *
0289: * @param loc a n Operator accessing a location
0290: * @return all location positions of <code>loc</code>
0291: */
0292: public int[] getLocationPos(Operator loc) {
0293: int size = 0;
0294: final int[] tempResult = new int[locationCount()];
0295: for (int i = 0; i < tempResult.length; i++) {
0296: if (location(i) == loc) {
0297: tempResult[size] = i;
0298: size++;
0299: }
0300: }
0301: final int[] result = new int[size];
0302: System.arraycopy(tempResult, 0, result, 0, size);
0303:
0304: return result;
0305: }
0306:
0307: /**
0308: * computes the position table used to determine at which sub term position
0309: * the value used to update the i-th location can be found.
0310: */
0311: private void fillValuePositionTable() {
0312: int pos = 0;
0313: for (int i = 0; i < valuePositionTable.length; i++) {
0314: pos += location(i).arity();
0315: if (guardExists(i))
0316: ++pos;
0317: valuePositionTable[i] = pos;
0318: pos++;
0319: }
0320: }
0321:
0322: /**
0323: * returns the n-th location of the update as term
0324: *
0325: * @param t
0326: * Term with this operator as top level operator
0327: * @param n
0328: * an int specifying the position of the requested location
0329: * @return the n-th location of term t updated by this operator
0330: */
0331: public Term location(Term t, int n) {
0332: Debug.assertTrue(t.op() == this ,
0333: "Illegal update location access.");
0334:
0335: final Term[] sub = new Term[location(n).arity()];
0336:
0337: for (int i = locationSubtermsBegin(n), j = 0; i != locationSubtermsEnd(n); ++i, ++j)
0338: sub[j] = t.sub(i);
0339:
0340: return tf.createTerm(location(n), sub,
0341: new ArrayOfQuantifiableVariable(),
0342: JavaBlock.EMPTY_JAVABLOCK);
0343: }
0344:
0345: /**
0346: * returns value the n-th location is updated with
0347: *
0348: * @param t
0349: * Term with this operator as top level operator
0350: * @param n
0351: * an int specifying the position of the location
0352: * @return the value the n-th location is updated with
0353: */
0354: public Term value(Term t, int n) {
0355: Debug
0356: .assertTrue(t.op() == this ,
0357: "Illegal update value access.");
0358: return t.sub(valuePos(n));
0359: }
0360:
0361: /**
0362: * returns the guard of the n-th update entry; if this entry does not have a
0363: * guard, <tt>TRUE</tt> is returned
0364: *
0365: * @param t
0366: * Term with this operator as top level operator
0367: * @param n
0368: * an int specifying the position of the location
0369: * @return the guard of the n-th update entry
0370: */
0371: public Term guard(Term t, int n) {
0372: if (!guardExists(n))
0373: return getValidGuard();
0374: return t.sub(guardPos(n));
0375: }
0376:
0377: /** @return name of the operator */
0378: public Name name() {
0379: return name;
0380: }
0381:
0382: /**
0383: * returns the arity of the operator
0384: */
0385: public int arity() {
0386: return arity;
0387: }
0388:
0389: /**
0390: * the position of the term the quantified update is applied to
0391: * @return the sub term position of the target term
0392: */
0393: public int targetPos() {
0394: return arity() - 1;
0395: }
0396:
0397: /**
0398: * @return the index of the subterm representing the formula/term the update
0399: * is applied to
0400: */
0401: public Term target(Term t) {
0402: return t.sub(targetPos());
0403: }
0404:
0405: /**
0406: * returns the sort a term would have if constructed with this operator and
0407: * the given sunterms. It is assumed that the term would be allowed if
0408: * constructed.
0409: *
0410: * @param term
0411: * an array of Term containing the subterms of a (potential)
0412: * simultaneous update term
0413: * @return sort of the simultaneous update term consisting of the given
0414: * subterms, if this op would be the top symbol
0415: */
0416: public Sort sort(Term[] term) {
0417: return term[targetPos()].sort();
0418: }
0419:
0420: /**
0421: * @return true if the value of "term" having this operator as top-level
0422: * operator and may not be changed by modalities
0423: */
0424: public boolean isRigid(Term term) {
0425: return target(term).isRigid();
0426: }
0427:
0428: /**
0429: * checks whether the top level structure of the given {@link Term}is
0430: * syntactically valid, given the assumption that the top level operator of
0431: * the term is the same as this Operator. The assumption that the top level
0432: * operator and the operator are equal is NOT checked.
0433: *
0434: * @return true iff the top level structure of the {@link Term}is valid.
0435: */
0436: public boolean validTopLevel(Term term) {
0437: if (term.arity() != arity())
0438: return false;
0439: for (int i = 0; i != locationCount(); ++i) {
0440: if (guardExists(i)
0441: && term.sub(guardPos(i)).sort() != Sort.FORMULA)
0442: return false;
0443: }
0444: return true;
0445: }
0446:
0447: /**
0448: * two concrete update operators match if their defining locations match,
0449: * and if the same elementary updates are guarded (that means that different
0450: * taclets/rules have to be written for guarded and unguarded updates, which
0451: * is not too bad because one hardly ever writes taclets that match on
0452: * updates anyway ;-)
0453: *
0454: * @see de.uka.ilkd.key.logic.op.Operator#match
0455: * (SVSubstitute,
0456: * de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
0457: */
0458: public MatchConditions match(SVSubstitute subst,
0459: MatchConditions mc, Services services) {
0460: MatchConditions result = mc;
0461: if (this == subst)
0462: return result;
0463: if (subst.getClass() != getClass()) {
0464: Debug.out("FAILED matching. Incomaptible operators "
0465: + "(template, operator)", this , subst);
0466: return null;
0467: }
0468: final QuanUpdateOperator update = (QuanUpdateOperator) subst;
0469: if (locationCount() == update.locationCount()
0470: && Arrays.equals(signature.guards,
0471: update.signature.guards)) {
0472: for (int i = 0, locs = locationCount(); i < locs; i++) {
0473: result = location(i).match(update.location(i), result,
0474: services);
0475: if (result == null) { // fail fast
0476: Debug.out(
0477: "FAILED. QuanUpdateOperator location mismatch "
0478: + "(template, operator)", this ,
0479: update);
0480: return null;
0481: }
0482: }
0483: return result;
0484: }
0485: Debug
0486: .out(
0487: "FAILED matching. QuanUpdateOperator match failed because of"
0488: + " incompatible locations (template, operator)",
0489: this , subst);
0490: return null;
0491: }
0492:
0493: /**
0494: * returns a string representation of the update operator
0495: */
0496: public String toString() {
0497: StringBuffer sb = new StringBuffer("quanUpdate(");
0498: for (int i = 0; i < locationCount(); i++) {
0499: sb.append(location(i));
0500: if (i < locationCount() - 1) {
0501: sb.append(" || ");
0502: }
0503: }
0504: sb.append("}");
0505: return sb.toString();
0506: }
0507:
0508: /**
0509: * The term class for quantified updates requires that the same variables
0510: * are quantified for all parts of an update entry (subterms of the
0511: * left-hand side, guard and the value); in principle this could also be
0512: * done more generally and with different variables. Given arrays of
0513: * variables for each entry part, an common array is constructed here
0514: * (unification). This can include bound renaming.
0515: *
0516: * @param boundVarsPerSub
0517: * the arrays of variables bound for each subterm
0518: * @param subs
0519: * the subterms of the update entry. The components of this array
0520: * are modified if bound renaming is necessary
0521: * @return the arrays of variables bound for each location
0522: */
0523: public ArrayOfQuantifiableVariable[] toBoundVarsPerAssignment(
0524: ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs) {
0525: final ArrayOfQuantifiableVariable[] res = new ArrayOfQuantifiableVariable[locationCount()];
0526:
0527: for (int i = 0; i != locationCount(); ++i)
0528: res[i] = BoundVariableTools.DEFAULT.unifyBoundVariables(
0529: boundVarsPerSub, subs, entryBegin(i), entryEnd(i));
0530:
0531: return res;
0532: }
0533:
0534: /**
0535: * The comparator that is used to sort the different assignments in an
0536: * update as totally as possible. This is done by first grouping different
0537: * kinds of top-level operators (local program variables, static attributes,
0538: * instance attributes and array accesses, other operators). Thereafter, we
0539: * sort according to the name of an operator. Because of last-win semantics,
0540: * updates that potentially clash (here simply: have the same top-level
0541: * operator) are not permuted.
0542: */
0543: private static class ElUpdateLocationComparator implements
0544: Comparator {
0545: private int primitiveLongCompare(long i, long j) {
0546: return (i < j ? -1 : (i == j ? 0 : 1));
0547: }
0548:
0549: public int compare(Object o1, Object o2) {
0550: // deliberately raise a ClassCastException for unsuitable o1, o2
0551: final ElUpdateLocation elUpd1 = (ElUpdateLocation) o1;
0552: final Location pv1 = elUpd1.getLocation();
0553: final ElUpdateLocation elUpd2 = (ElUpdateLocation) o2;
0554: final Location pv2 = elUpd2.getLocation();
0555:
0556: if (elUpd1.locationNum == elUpd2.locationNum)
0557: return 0;
0558:
0559: int cmpResult = getLocationKind(pv1) - getLocationKind(pv2);
0560: if (cmpResult != 0)
0561: return cmpResult;
0562:
0563: cmpResult = pv1.name().compareTo(pv2.name());
0564:
0565: ////////////////////////////////////////////////////////////////////
0566: // beware, ugly HACK ahead:
0567: // because different array operators are different, but can still clash,
0568: // we must not reorder assignments to arrays
0569: if (pv1 instanceof ArrayOp && pv2 instanceof ArrayOp)
0570: cmpResult = 0;
0571: ////////////////////////////////////////////////////////////////////
0572:
0573: if (cmpResult != 0)
0574: return cmpResult;
0575:
0576: final boolean bPV1 = pv1 instanceof ProgramVariable;
0577: final boolean bPV2 = pv2 instanceof ProgramVariable;
0578: cmpResult = bPV1 ? (bPV2 ? primitiveLongCompare(
0579: ((ProgramVariable) pv1).id(),
0580: ((ProgramVariable) pv2).id()) : -1)
0581: : (bPV2 ? 1 : 0);
0582: if (cmpResult != 0)
0583: return cmpResult;
0584:
0585: return elUpd1.locationNum - elUpd2.locationNum;
0586: }
0587:
0588: private int getLocationKind(Location location) {
0589: if (location instanceof ProgramVariable) {
0590: final ProgramVariable pv = (ProgramVariable) location;
0591: if (pv.isStatic())
0592: return 1;
0593: else
0594: return 0;
0595: } else if (location instanceof AccessOp) {
0596: return 2;
0597: } else
0598: return 3;
0599: }
0600: }
0601:
0602: private final static Comparator elUpdateComparator = new ElUpdateLocationComparator();
0603:
0604: /**
0605: * Internal data structure to store all components of an elementary update:
0606: * bound variables, left-hand side, right-hand side and guard (the guard is
0607: * here assumed to exist always, i.e. <tt>true</tt> is used as trivial
0608: * guard).
0609: *
0610: * Two objects are consider equal if and only if the left-hand sides and the
0611: * guard are equal (modulo bound renaming)
0612: */
0613: private static class ElUpdateLocation extends GuardSimplifier {
0614: private Term lhs;
0615: private Term value;
0616:
0617: // used to make the ordering stable (important because of last-win
0618: // semantics)
0619: public final int locationNum;
0620:
0621: public ElUpdateLocation(final Term guard,
0622: final ArrayOfQuantifiableVariable boundVars,
0623: final Term lhs, final Term value, final int locationNum) {
0624: super (guard, boundVars);
0625: this .lhs = lhs;
0626: this .value = value;
0627: this .locationNum = locationNum;
0628:
0629: simplify();
0630: }
0631:
0632: public boolean isTrivialUpdate() {
0633: return getLhs().equalsModRenaming(getValue());
0634: }
0635:
0636: private final static BoundVariableTools bvt = BoundVariableTools.DEFAULT;
0637:
0638: public boolean equals(Object o2) {
0639: if (!(o2 instanceof ElUpdateLocation))
0640: return false;
0641: final ElUpdateLocation upd2 = (ElUpdateLocation) o2;
0642:
0643: if (!getLocation().equals(upd2.getLocation()))
0644: return false;
0645:
0646: return bvt.equalsModRenaming(getBoundVars(),
0647: getCondition(), upd2.getBoundVars(), upd2
0648: .getCondition())
0649: && bvt.equalsModRenaming(getBoundVars(), getLhs(),
0650: upd2.getBoundVars(), upd2.getLhs());
0651: }
0652:
0653: public int hashCode() {
0654: // we do not know how to compute a hash code for the other
0655: // components (terms of the left-hand side, condition) that is
0656: // stable under bound renaming
0657: // (that is, we are too lazy to implement one)
0658: return getLocation().hashCode();
0659: }
0660:
0661: public Location getLocation() {
0662: return (Location) getLhs().op();
0663: }
0664:
0665: public Term getLocationSub(int subNum) {
0666: return getLhs().sub(subNum);
0667: }
0668:
0669: public ArrayOfQuantifiableVariable getBoundVars() {
0670: return new ArrayOfQuantifiableVariable(getMinimizedVars()
0671: .toArray());
0672: }
0673:
0674: public SetOfQuantifiableVariable getBoundVarsAsSet() {
0675: SetOfQuantifiableVariable res = SetAsListOfQuantifiableVariable.EMPTY_SET;
0676: final IteratorOfQuantifiableVariable it = getMinimizedVars()
0677: .iterator();
0678: while (it.hasNext())
0679: res = res.add(it.next());
0680: return res;
0681: }
0682:
0683: public Term getLhs() {
0684: return lhs;
0685: }
0686:
0687: public Term getValue() {
0688: return value;
0689: }
0690:
0691: protected boolean isNeededVar(QuantifiableVariable var) {
0692: return getLhs().freeVars().contains(var)
0693: || getValue().freeVars().contains(var);
0694: }
0695:
0696: protected void substitute(QuantifiableVariable var,
0697: Term substTerm) {
0698: lhs = subst(var, substTerm, getLhs());
0699: value = subst(var, substTerm, getValue());
0700: }
0701:
0702: /**
0703: * @return a formula that implies that <code>this</code> assignment
0704: * subsumes/overrides the assignment <code>loc2</code> (i.e.,
0705: * if the formula evaluates to true, then <code>loc2</code> is
0706: * overridden by <code>this</code>). The result may contain
0707: * some of the variables <code>getBoundVars()</code>, which
0708: * are implicitly existentially quantified. One can use the
0709: * class <code>GuardSimplifier</code> to check whether the
0710: * condition is valid.
0711: */
0712: public Term getSubsumptionCondition(ElUpdateLocation loc2) {
0713: if (getLocation() != loc2.getLocation()
0714: || getLhs().javaBlock() != loc2.getLhs()
0715: .javaBlock())
0716: return tb.ff();
0717:
0718: final Term lhs2 = loc2
0719: .anonymiseVariables(anonymiseVariables(loc2
0720: .getLhs()));
0721:
0722: Term res = getCondition();
0723: for (int i = 0; i != lhs2.arity(); ++i) {
0724: if (getLhs().varsBoundHere(i).size() != 0
0725: || lhs2.varsBoundHere(i).size() != 0)
0726: // in this rather strange situation we don't know what
0727: // to do, so we rather be on the safe side and say no
0728: return tb.ff();
0729: res = tb.and(res, tb.equals(getLhs().sub(i), lhs2
0730: .sub(i)));
0731: }
0732:
0733: return res;
0734: }
0735:
0736: /**
0737: * Ensure that none of the variables <code>getBoundVars</code> occurs
0738: * free in <code>t</code>. This is done by substituting occurring
0739: * variables with fresh variables
0740: */
0741: private Term anonymiseVariables(Term t) {
0742: if (t.freeVars().size() == 0)
0743: return t;
0744:
0745: final ArrayOfQuantifiableVariable oldFreeVars = new ArrayOfQuantifiableVariable(
0746: t.freeVars().toArray());
0747: final QuantifiableVariable[] newFreeVarsTemp = new QuantifiableVariable[oldFreeVars
0748: .size()];
0749:
0750: bvt.resolveCollisions(oldFreeVars, newFreeVarsTemp,
0751: getBoundVarsAsSet());
0752:
0753: final ArrayOfQuantifiableVariable newFreeVars = new ArrayOfQuantifiableVariable(
0754: newFreeVarsTemp);
0755: return bvt.renameVariables(t, oldFreeVars, newFreeVars);
0756: }
0757: }
0758:
0759: /**
0760: * Create a term from a list of (quantified, guarded) elementary updates and
0761: * a target term/formula. The update of the result is optimized as far as
0762: * possible by sorting the elementary updates, removing unnecessary updates
0763: * and removing trivial guards. The four array arguments are supposed to
0764: * have the same size.
0765: */
0766: public static Term normalize(
0767: ArrayOfQuantifiableVariable[] boundVars, Term[] guards,
0768: Term[] leftHandSides, Term[] values, Term target) {
0769: final ElUpdateLocation[] normalformOrdering = normalize(
0770: boundVars, guards, leftHandSides, values);
0771:
0772: if (normalformOrdering == null)
0773: return createTerm(boundVars, guards, leftHandSides, values,
0774: target);
0775:
0776: return normalformOrdering.length == 0 ? target : createTerm(
0777: normalformOrdering, target);
0778: }
0779:
0780: /**
0781: * Create a term from a list of (quantified, guarded) elementary updates and
0782: * a target term/formula. The only optimisation that is applied at this
0783: * point is the removal of trivial guards
0784: */
0785: private static Term createTerm(
0786: ArrayOfQuantifiableVariable[] boundVars, Term[] guards,
0787: Term[] locations, Term[] values, Term target) {
0788: final boolean[] nontrivialGuards = determineNontrivialGuards(guards);
0789: final QuanUpdateOperator op = QuanUpdateOperator
0790: .createUpdateOp(locations, nontrivialGuards);
0791:
0792: ListOfTerm resultSubs = SLListOfTerm.EMPTY_LIST.prepend(target);
0793: for (int i = locations.length - 1; i >= 0; i--) {
0794: resultSubs = resultSubs.prepend(values[i]);
0795:
0796: for (int j = op.location(i).arity() - 1; j >= 0; j--)
0797: resultSubs = resultSubs.prepend(locations[i].sub(j));
0798:
0799: if (nontrivialGuards[i])
0800: resultSubs = resultSubs.prepend(guards[i]);
0801: }
0802:
0803: return tf.createQuanUpdateTermUnordered(op, resultSubs
0804: .toArray(), boundVars);
0805: }
0806:
0807: private static Term createTerm(ElUpdateLocation[] elUpdates,
0808: Term target) {
0809: final QuanUpdateOperator op = QuanUpdateOperator
0810: .createUpdateOp(locations(elUpdates),
0811: nontrivialGuards(elUpdates));
0812:
0813: ListOfTerm resultSubs = SLListOfTerm.EMPTY_LIST.prepend(target);
0814: for (int i = elUpdates.length - 1; i >= 0; i--) {
0815: resultSubs = resultSubs.prepend(elUpdates[i].getValue());
0816:
0817: for (int j = op.location(i).arity() - 1; j >= 0; j--)
0818: resultSubs = resultSubs.prepend(elUpdates[i]
0819: .getLocationSub(j));
0820:
0821: if (!elUpdates[i].isValidGuard())
0822: resultSubs = resultSubs.prepend(elUpdates[i]
0823: .getCondition());
0824: }
0825:
0826: return tf.createQuanUpdateTermUnordered(op, resultSubs
0827: .toArray(), boundVars(elUpdates));
0828: }
0829:
0830: private static ArrayOfQuantifiableVariable[] boundVars(
0831: ElUpdateLocation[] elUpdates) {
0832: final ArrayOfQuantifiableVariable[] res = new ArrayOfQuantifiableVariable[elUpdates.length];
0833: for (int i = 0; i != elUpdates.length; ++i)
0834: res[i] = elUpdates[i].getBoundVars();
0835: return res;
0836: }
0837:
0838: private static Location[] locations(ElUpdateLocation[] elUpdates) {
0839: final Location[] res = new Location[elUpdates.length];
0840: for (int i = 0; i != elUpdates.length; ++i)
0841: res[i] = elUpdates[i].getLocation();
0842: return res;
0843: }
0844:
0845: private static boolean[] nontrivialGuards(
0846: ElUpdateLocation[] elUpdates) {
0847: final boolean[] res = new boolean[elUpdates.length];
0848: for (int i = 0; i != elUpdates.length; ++i)
0849: res[i] = !elUpdates[i].isValidGuard();
0850: return res;
0851: }
0852:
0853: /**
0854: * @return a boolean array that contains <code>true</code> in those places
0855: * for which <code>guards</code> does not contain the formula
0856: * <code>true</code>
0857: */
0858: private static boolean[] determineNontrivialGuards(Term[] guards) {
0859: final boolean[] res = new boolean[guards.length];
0860: for (int i = 0; i != guards.length; ++i)
0861: res[i] = guards[i].op() != Op.TRUE;
0862: return res;
0863: }
0864:
0865: /**
0866: * Given the update operator (<code>this</code>), the variables that are
0867: * bound and the subterms, create a new term. This applies the same
0868: * optimisations as
0869: * <code>normalize (ArrayOfQuantifiableVariable[], Term[], Term[], Term[], Term )</code>
0870: */
0871: public Term normalize(
0872: ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs) {
0873:
0874: // could be implemented more efficiently
0875:
0876: final ArrayOfQuantifiableVariable[] boundVars = toBoundVarsPerAssignment(
0877: boundVarsPerSub, subs);
0878: final Term[] guards = new Term[locationCount()];
0879: final Term[] lhss = new Term[locationCount()];
0880: final Term[] values = new Term[locationCount()];
0881:
0882: for (int locNum = 0; locNum != locationCount(); ++locNum) {
0883: if (guardExists(locNum))
0884: guards[locNum] = subs[guardPos(locNum)];
0885: else
0886: guards[locNum] = getValidGuard();
0887:
0888: final Location loc = location(locNum);
0889: final Term[] locSubs = new Term[loc.arity()];
0890: System.arraycopy(subs, locationSubtermsBegin(locNum),
0891: locSubs, 0, loc.arity());
0892: lhss[locNum] = tf.createTerm(loc, locSubs,
0893: new ArrayOfQuantifiableVariable(),
0894: JavaBlock.EMPTY_JAVABLOCK);
0895:
0896: values[locNum] = subs[valuePos(locNum)];
0897: }
0898:
0899: final Term target = subs[subs.length - 1];
0900:
0901: return normalize(boundVars, guards, lhss, values, target);
0902: }
0903:
0904: /**
0905: * Determines the ordering of the locations according to the update term
0906: * normalform and returns an array describing the new order of the
0907: * locations. Updates with obviously unsatisfiable guards and trivial
0908: * updates are removed (if possible)
0909: */
0910: private static ElUpdateLocation[] normalize(
0911: ArrayOfQuantifiableVariable[] boundVars, Term[] guards,
0912: Term[] locations, Term[] values) {
0913:
0914: // three sets of assignments, one that is used to order the assignments
0915: // of an update, one to eliminate those updates that are literally
0916: // overwritten by later updates, and one to eliminate updates that are
0917: // subsumed by later quantified updates. The sets are filled
0918: // "from right to left"
0919: final TreeSet orderedAssignments = new TreeSet(
0920: elUpdateComparator);
0921: final Set laterAssignments = new HashSet();
0922: final List laterQuanAssignments = new ArrayList();
0923:
0924: for (int locNum = locations.length - 1; locNum >= 0; locNum--) {
0925: final ElUpdateLocation elUpd = new ElUpdateLocation(
0926: guards[locNum], boundVars[locNum],
0927: locations[locNum], values[locNum], locNum);
0928: if (elUpd.isUnsatisfiableGuard())
0929: continue;
0930:
0931: final Location location = elUpd.getLocation();
0932: if (location instanceof SchemaVariable
0933: || location instanceof MetaOperator) {
0934: return null;
0935: }
0936:
0937: if (laterAssignments.contains(elUpd)
0938: || isSubsumedAssignment(elUpd, laterQuanAssignments))
0939: continue;
0940:
0941: orderedAssignments.add(elUpd);
0942: laterAssignments.add(elUpd);
0943:
0944: if (elUpd.bindsVariables())
0945: laterQuanAssignments.add(elUpd);
0946: }
0947:
0948: final Set operators = new HashSet();
0949: final Iterator it = orderedAssignments.iterator();
0950: while (it.hasNext()) {
0951: final ElUpdateLocation elUpd = (ElUpdateLocation) it.next();
0952: final Location loc = elUpd.getLocation();
0953:
0954: // delete trivial updates (left-hand and right-hand side are
0955: // equal), but only if there was no predecessing update that
0956: // could possible cause a clash
0957: if (!operators.contains(loc) && elUpd.isTrivialUpdate()) {
0958: it.remove();
0959: continue;
0960: }
0961:
0962: operators.add(loc);
0963: }
0964:
0965: return (ElUpdateLocation[]) orderedAssignments
0966: .toArray(new ElUpdateLocation[orderedAssignments.size()]);
0967: }
0968:
0969: /**
0970: * @return <code>true</code> iff the assignment <code>elUpd</code> is
0971: * overridden/subsumed by any of the assignments in
0972: * <code>laterAssignments</code>. This check in particular works if
0973: * <code>laterAssignments</code> contains quantified assignments,
0974: * i.e., can detect subsumption in updates like
0975: * <code>a[0] := 4 || \for int i; a[i] := 2</code>
0976: */
0977: private static boolean isSubsumedAssignment(ElUpdateLocation elUpd,
0978: List laterAssignments) {
0979: final Iterator it = laterAssignments.iterator();
0980: while (it.hasNext()) {
0981: final ElUpdateLocation laterAss = (ElUpdateLocation) it
0982: .next();
0983: final Term subsumptionCond = laterAss
0984: .getSubsumptionCondition(elUpd);
0985: final GuardSatisfiabilityFormulaBuilder satisfiabilityBuilder = new GuardSatisfiabilityFormulaBuilder(
0986: subsumptionCond, laterAss.getBoundVars());
0987: if (satisfiabilityBuilder.isValidGuard())
0988: return true;
0989: }
0990: return false;
0991: }
0992:
0993: private final static Term validGuardCache = tf
0994: .createJunctorTerm(Op.TRUE);
0995:
0996: private static Term getValidGuard() {
0997: return validGuardCache;
0998: }
0999:
1000: }
|