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:
012: package de.uka.ilkd.key.counterexample;
013:
014: /**
015: * The root of the Calculus Hierarchy, this class only produces the static
016: * clauses which are the same for all problems. The subclasses generate the further clauses.
017: * @see SortCalculus
018: * @see AxiomCalculus
019: * @see ConjCalculus
020: * @author Sonja Pieper
021: * @version 0.1
022: */
023: public class Calculus {
024:
025: private Clauses statics;
026: protected Clauses all;
027:
028: public Calculus() {
029:
030: statics = new Clauses();
031: statics.add(this .domainbound());
032: statics.add(this .functionality());
033: statics.add(this .sameRewriting());
034: statics.add(this .resultRewriting());
035: statics.add(this .argRewriting());
036:
037: all = new Clauses();
038: this .addClauses(statics);
039: }
040:
041: public void addClauses(Clauses c) {
042: this .all.add(c);
043: }
044:
045: public Clauses getStaticClauses() {
046: return statics;
047: }
048:
049: public Clauses getAllClauses() {
050: return all;
051: }
052:
053: private Clauses domainbound() {
054: Clauses cs = new Clauses();
055: cs.add(new Clause("", "max(" + CounterExample.config.domainmax
056: + ")"));
057: return cs;
058: }
059:
060: private Clauses functionality() {
061: Clauses cs = new Clauses();
062: cs.add(new Clause("intpr(F,X,Y),intpr(F,X,Y1),{Y\\==Y1}",
063: "same(Y,Y1)", "Functionality"));
064: cs.add(new Clause("is(X,Y),is(X,Y1),{Y\\==Y1}", "same(Y,Y1)"));
065: return cs;
066: }
067:
068: private Clauses sameRewriting() {
069: Clauses cs = new Clauses();
070: cs.add(new Clause("same(X,Y),is(X,Z)", "same(Z,Y)",
071: "Rewriting with same"));
072: cs.add(new Clause("same(X,Y),is(Y,Z)", "same(Z,X)"));
073: cs.add(new Clause("different(X,Y),is(X,Z)", "different(Z,Y)",
074: "Rewriting with different"));
075: cs.add(new Clause("different(X,Y),is(Y,Z)", "different(Z,X)"));
076: return cs;
077: }
078:
079: private Clauses resultRewriting() {
080: Clauses cs = new Clauses();
081: cs.add(new Clause("intpr(F,X,Y),is(Y,Y1)", "intpr(F,X,Y1)",
082: "Result rewriting"));
083: return cs;
084: }
085:
086: Clauses argRewriting() {
087: Clauses cs = new Clauses();
088:
089: /* rewriting rules where n is the number of args currently produced*/
090: for (int n = 0; n <= CounterExample.config.maxargs; n++) {
091:
092: if (n > 0) {
093: cs.addComment("Rewriting for functions with " + n
094: + " arguments");
095: }
096:
097: for (int current_arg = 0; current_arg < n; current_arg++) {
098: String args = new String();
099: String rewargs = new String();
100: for (int i = 1; i <= n; i++) {
101: args = args + "X" + i;
102: rewargs = (i == current_arg ? "Z" : "X" + i);
103: }
104: String aconj = "is(X" + current_arg + ",Z),intpr(F,tup"
105: + n + "(" + args + "),Y)";
106: String cnsq = "intpr(F,tup" + n + "(" + rewargs
107: + "),Y)";
108:
109: Clause rewrite_current_arg = new Clause(aconj, cnsq);
110: cs.add(rewrite_current_arg);
111: }
112: }
113:
114: return cs;
115: }
116:
117: public String toString() {
118: return all.toString();
119: }
120: }
|