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: package de.uka.ilkd.key.strategy;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.proof.Proof;
015: import de.uka.ilkd.key.strategy.feature.*;
016:
017: /**
018: * Strategy tailored to VBT aimed symbolic execution.
019: */
020: public class VBTStrategy extends JavaCardDLStrategy {
021:
022: protected static StrategyProperties setupStrategyProperties() {
023: final StrategyProperties res = new StrategyProperties();
024: res.setProperty(StrategyProperties.SPLITTING_OPTIONS_KEY,
025: StrategyProperties.SPLITTING_NORMAL);
026: res.setProperty(StrategyProperties.LOOP_OPTIONS_KEY,
027: StrategyProperties.LOOP_EXPAND);
028: res.setProperty(StrategyProperties.METHOD_OPTIONS_KEY,
029: StrategyProperties.METHOD_EXPAND);
030: res.setProperty(StrategyProperties.QUERY_OPTIONS_KEY,
031: StrategyProperties.QUERY_NONE);
032: res.setProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY,
033: StrategyProperties.QUANTIFIERS_INSTANTIATE);
034: return res;
035: }
036:
037: protected VBTStrategy(Proof p_proof,
038: StrategyProperties strategyProperties) {
039: super (p_proof, strategyProperties);
040:
041: clearRuleSetBindings(getCostComputationDispatcher(), "test_gen");
042: bindRuleSet(getCostComputationDispatcher(), "test_gen", add(
043: longConst(-1000),
044: NonDuplicateAppModPositionFeature.INSTANCE));
045: clearRuleSetBindings(getCostComputationDispatcher(),
046: "test_gen_quan_num");
047: bindRuleSet(getCostComputationDispatcher(),
048: "test_gen_quan_num", add(longConst(30000),
049: NonDuplicateAppModPositionFeature.INSTANCE));
050: clearRuleSetBindings(getCostComputationDispatcher(),
051: "split_cond");
052: bindRuleSet(getCostComputationDispatcher(), "split_cond", -1000);
053: clearRuleSetBindings(getCostComputationDispatcher(), "split");
054: bindRuleSet(getCostComputationDispatcher(), "split", -1000);
055:
056: clearRuleSetBindings(getCostComputationDispatcher(), "beta");
057: bindRuleSet(getCostComputationDispatcher(), "beta", -1000);
058:
059: clearRuleSetBindings(getCostComputationDispatcher(),
060: "inReachableStateImplication");
061: bindRuleSet(getCostComputationDispatcher(),
062: "inReachableStateImplication", inftyConst());
063: clearRuleSetBindings(getCostComputationDispatcher(),
064: "cut_direct");
065: bindRuleSet(getCostComputationDispatcher(), "cut_direct",
066: inftyConst());
067: clearRuleSetBindings(getCostComputationDispatcher(),
068: "simplify_prog");
069: bindRuleSet(getCostComputationDispatcher(), "simplify_prog",
070: 10000);
071: clearRuleSetBindings(getCostComputationDispatcher(),
072: "simplify_prog_subset");
073: bindRuleSet(getCostComputationDispatcher(),
074: "simplify_prog_subset", 10000);
075: }
076:
077: protected VBTStrategy(Proof p_proof) {
078:
079: this (p_proof, setupStrategyProperties());
080:
081: }
082:
083: protected boolean arithDefOps() {
084: return true;
085: }
086:
087: public Name name() {
088: return new Name("VBTStrategy");
089: }
090:
091: public static class Factory extends StrategyFactory {
092:
093: public Factory() {
094: }
095:
096: public Strategy create(Proof p_proof,
097: StrategyProperties strategyProperties) {
098: return new VBTStrategy(p_proof);
099: }
100:
101: public Name name() {
102: return new Name("VBTStrategy");
103: }
104: }
105: }
|