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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017: package de.uka.ilkd.key.strategy.quantifierHeuristics;
018:
019: import junit.framework.TestCase;
020: import de.uka.ilkd.key.gui.configuration.ProofSettings;
021: import de.uka.ilkd.key.java.VarAndType;
022: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
023: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.logic.sort.*;
027: import de.uka.ilkd.key.proof.*;
028: import de.uka.ilkd.key.rule.TacletForTests;
029: import de.uka.ilkd.key.rule.UpdateSimplifier;
030: import de.uka.ilkd.key.rule.updatesimplifier.AssignmentPairImpl;
031: import de.uka.ilkd.key.rule.updatesimplifier.Update;
032:
033: //most Code are copyed from Logic.TestUpdateFactory
034:
035: public class TestTriggersSet extends TestCase {
036:
037: private Proof proof;
038:
039: private TermFactory tf = TermFactory.DEFAULT;
040: private TermBuilder tb = TermBuilder.DF;
041:
042: private Namespace variables = new Namespace();
043:
044: private Namespace functions = new Namespace();
045:
046: private Namespace sorts = new Namespace();
047:
048: //sort
049: private Sort r;
050: private Sort s;
051: private Sort t;
052: //private Sort ints ;
053:
054: //constant function
055: private Function r_a;
056: private Function r_b;
057: private Function r_c;
058:
059: private Function s_a;
060: private Function s_b;
061: private Function s_c;
062:
063: private Function t_a;
064: private Function t_b;
065: private Function t_c;
066:
067: //Rigid function
068: private Function frr; // r->r
069: private Function f2rr; // r->r
070: private Function fsr; // s-> r
071: private Function ftr; // t->r
072: private Function fstr;// s->t->r
073: private Function frstr;//r->s->t->r;
074:
075: private Function gss; // s->s
076: private Function grs; // r->s
077: private Function gts; // t->s
078: private Function grts; //r->t->s
079: private Function grsts;//r->s->t->s
080:
081: private Function htt; // t->t
082: private Function hrt; // r -> t
083: private Function hst; // s->t
084: private Function hrst;// r->s->t
085: private Function hrstt;//t->s->t->t
086:
087: //Formular function
088: private Function pp;//Formula->Formula
089: private Function pr;//r->Formula
090: private Function ps;//s->Formula
091: private Function pt;//t->Formula
092: private Function prs;//r->s->Formula
093: private Function pst;//s->t->Formula
094: private Function prt;//r->t->Formula
095: private Function prst;//r->s->t->Formula
096: // private Function pi;//ints->Formula
097: private Goal g;
098:
099: public TestTriggersSet() {
100: super ();
101: }
102:
103: public void setUp() {
104: //sort
105: r = new PrimitiveSort(new Name("r"));
106: s = new PrimitiveSort(new Name("s"));
107: t = new PrimitiveSort(new Name("t"));
108: //ints = ProofSettings.DEFAULT_SETTINGS.getLDTSettings().getIntegerSemantics().getIntSort();
109: sorts.add(r);
110: sorts.add(s);
111: sorts.add(t);
112: //sorts.add(ints);
113:
114: //constant
115: r_a = new RigidFunction(new Name("r_a"), r, new Sort[0]);
116: r_b = new RigidFunction(new Name("r_b"), r, new Sort[0]);
117: r_c = new RigidFunction(new Name("r_c"), r, new Sort[0]);
118: functions.add(r_a);
119: functions.add(r_b);
120: functions.add(r_c);
121:
122: s_a = new RigidFunction(new Name("s_a"), s, new Sort[0]);
123: s_b = new RigidFunction(new Name("s_b"), s, new Sort[0]);
124: s_c = new RigidFunction(new Name("s_c"), s, new Sort[0]);
125: functions.add(s_a);
126: functions.add(s_b);
127: functions.add(s_c);
128:
129: t_a = new RigidFunction(new Name("t_a"), s, new Sort[0]);
130: t_b = new RigidFunction(new Name("t_b"), s, new Sort[0]);
131: t_c = new RigidFunction(new Name("t_c"), s, new Sort[0]);
132: functions.add(t_a);
133: functions.add(t_b);
134: functions.add(t_c);
135:
136: //function
137: frr = new RigidFunction(new Name("frr"), r, new Sort[] { r });
138: f2rr = new RigidFunction(new Name("f2rr"), r, new Sort[] { r });
139: fsr = new RigidFunction(new Name("fsr"), r, new Sort[] { s });
140: ftr = new RigidFunction(new Name("ftr"), r, new Sort[] { t });
141: fstr = new RigidFunction(new Name("fst"), r,
142: new Sort[] { s, t });
143: frstr = new RigidFunction(new Name("frstr"), r, new Sort[] { r,
144: s, t });
145:
146: functions.add(frr);
147: functions.add(f2rr);
148: functions.add(fsr);
149: functions.add(ftr);
150: functions.add(fstr);
151: functions.add(frstr);
152:
153: gss = new RigidFunction(new Name("gss"), s, new Sort[] { s });
154: grs = new RigidFunction(new Name("grs"), s, new Sort[] { r });
155: gts = new RigidFunction(new Name("gts"), s, new Sort[] { t });
156: grts = new RigidFunction(new Name("grts"), s,
157: new Sort[] { r, t });
158: grsts = new RigidFunction(new Name("grsts"), s, new Sort[] { r,
159: s, t });
160:
161: functions.add(gss);
162: functions.add(grs);
163: functions.add(gts);
164: functions.add(grts);
165: functions.add(grsts);
166:
167: htt = new RigidFunction(new Name("htt"), t, new Sort[] { t });
168: hrt = new RigidFunction(new Name("hrt"), t, new Sort[] { r });
169: hst = new RigidFunction(new Name("hst"), t, new Sort[] { s });
170: hrst = new RigidFunction(new Name("hrst"), t,
171: new Sort[] { r, s });
172: hrstt = new RigidFunction(new Name("hrstt"), t, new Sort[] { r,
173: s, t });
174:
175: functions.add(htt);
176: functions.add(hrt);
177: functions.add(hst);
178: functions.add(hrst);
179: functions.add(hrstt);
180:
181: //Formula function
182: pp = new RigidFunction(new Name("pp"), Sort.FORMULA,
183: new Sort[] { Sort.FORMULA });
184: pr = new RigidFunction(new Name("pr"), Sort.FORMULA,
185: new Sort[] { r });
186: ps = new RigidFunction(new Name("ps"), Sort.FORMULA,
187: new Sort[] { s });
188: pt = new RigidFunction(new Name("pt"), Sort.FORMULA,
189: new Sort[] { t });
190: prs = new RigidFunction(new Name("prs"), Sort.FORMULA,
191: new Sort[] { r, s });
192: prt = new RigidFunction(new Name("prt"), Sort.FORMULA,
193: new Sort[] { r, t });
194: pst = new RigidFunction(new Name("pst"), Sort.FORMULA,
195: new Sort[] { s, t });
196: prst = new RigidFunction(new Name("prst"), Sort.FORMULA,
197: new Sort[] { r, s, t });
198: //pi=new RigidFunction(new Name("pi"),Sort.FORMULA,new Sort[]{});
199: functions.add(pp);
200: functions.add(pr);
201: functions.add(ps);
202: functions.add(pt);
203: functions.add(prs);
204: functions.add(prt);
205: functions.add(pst);
206: functions.add(prst);
207: //functions.add(pi);
208:
209: proof = new Proof(TacletForTests.services());
210: g = new Goal(
211: new Node(proof, Sequent.EMPTY_SEQUENT),
212: new RuleAppIndex(new TacletAppIndex(new TacletIndex()),
213: new BuiltInRuleAppIndex(new BuiltInRuleIndex())));
214: proof.setRoot(g.node());
215: proof.add(g);
216:
217: proof.setNamespaces(new NamespaceSet(variables, functions,
218: sorts, new Namespace(), new Namespace(),
219: new Namespace()));
220:
221: }
222:
223: private Term parseTerm(String termstr) {
224: return TacletForTests.parseTerm(termstr, new NamespaceSet(
225: variables, functions, sorts, new Namespace(),
226: new Namespace(), new Namespace()));
227: }
228:
229: public void testTrigger1() {
230: String term1 = "\\forall s x;(ps(x))";
231: Term allterm = parseTerm(term1);
232: Term trigger1 = allterm.sub(0);
233: TriggersSet ts = TriggersSet.create(allterm);
234: int triggerNum = ts.getAllTriggers().size();
235: assertEquals(1, triggerNum);
236: Term trigger2 = ts.getAllTriggers().iterator().next()
237: .getTriggerTerm();
238: assertEquals(trigger1, trigger2);
239: }
240:
241: public void testTrigger2() {
242: String term1 = "\\forall r x;(frr(x)=frr(frr(x)))";
243: Term allterm = parseTerm(term1);
244: Term trigger1 = allterm.sub(0).sub(1);
245: TriggersSet ts = TriggersSet.create(allterm);
246: int triggerNum = ts.getAllTriggers().size();
247: assertEquals(1, triggerNum);
248: Term trigger2 = ts.getAllTriggers().iterator().next()
249: .getTriggerTerm();
250: assertEquals(trigger1, trigger2);
251: }
252: }
|