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.strategy;
0012:
0013: import de.uka.ilkd.key.logic.Name;
0014: import de.uka.ilkd.key.logic.PosInOccurrence;
0015: import de.uka.ilkd.key.logic.PosInTerm;
0016: import de.uka.ilkd.key.logic.TermBuilder;
0017: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
0018: import de.uka.ilkd.key.logic.op.Function;
0019: import de.uka.ilkd.key.logic.op.IUpdateOperator;
0020: import de.uka.ilkd.key.logic.op.IfThenElse;
0021: import de.uka.ilkd.key.logic.op.Junctor;
0022: import de.uka.ilkd.key.logic.op.Modality;
0023: import de.uka.ilkd.key.logic.op.Op;
0024: import de.uka.ilkd.key.logic.op.Operator;
0025: import de.uka.ilkd.key.logic.op.ProgramMethod;
0026: import de.uka.ilkd.key.logic.op.TermSymbol;
0027: import de.uka.ilkd.key.logic.sort.Sort;
0028: import de.uka.ilkd.key.proof.Goal;
0029: import de.uka.ilkd.key.proof.Proof;
0030: import de.uka.ilkd.key.proof.UseMethodContractRuleFilter;
0031: import de.uka.ilkd.key.rule.RuleApp;
0032: import de.uka.ilkd.key.strategy.feature.*;
0033: import de.uka.ilkd.key.strategy.quantifierHeuristics.*;
0034: import de.uka.ilkd.key.strategy.termProjection.*;
0035: import de.uka.ilkd.key.strategy.termfeature.*;
0036: import de.uka.ilkd.key.strategy.termgenerator.*;
0037:
0038: /**
0039: * Strategy tailored to be used as long as a java program can be found in
0040: * the sequent.
0041: */
0042: public class JavaCardDLStrategy extends AbstractFeatureStrategy {
0043:
0044: private final RuleSetDispatchFeature costComputationDispatcher;
0045: private final Feature costComputationF;
0046: private final RuleSetDispatchFeature approvalDispatcher;
0047: private final Feature approvalF;
0048: private final RuleSetDispatchFeature instantiationDispatcher;
0049: private final Feature instantiationF;
0050:
0051: protected final RuleSetDispatchFeature getCostComputationDispatcher() {
0052: return costComputationDispatcher;
0053: }
0054:
0055: protected final RuleSetDispatchFeature getInstantiationDispatcher() {
0056: return instantiationDispatcher;
0057: }
0058:
0059: private final StrategyProperties strategyProperties;
0060:
0061: protected JavaCardDLStrategy(Proof p_proof,
0062: StrategyProperties strategyProperties) {
0063:
0064: super (p_proof);
0065:
0066: this .strategyProperties = (StrategyProperties) strategyProperties
0067: .clone();
0068:
0069: this .tf = new ArithTermFeatures(p_proof.getServices()
0070: .getTypeConverter().getIntegerLDT());
0071: this .ff = new FormulaTermFeatures();
0072:
0073: costComputationDispatcher = setupCostComputationF(p_proof);
0074: approvalDispatcher = setupApprovalDispatcher(p_proof);
0075: instantiationDispatcher = setupInstantiationF(p_proof);
0076:
0077: costComputationF = setupGlobalF(costComputationDispatcher,
0078: p_proof);
0079: instantiationF = setupGlobalF(instantiationDispatcher, p_proof);
0080: approvalF = add(setupApprovalF(p_proof), approvalDispatcher);
0081: }
0082:
0083: private Feature setupGlobalF(Feature dispatcher, Proof p_proof) {
0084: final Feature simplifierF = selectSimplifier(-10000);
0085:
0086: final Feature ifMatchedF = ifZero(MatchedIfFeature.INSTANCE,
0087: longConst(+1));
0088:
0089: // final Feature splitF =
0090: // ScaleFeature.createScaled ( CountBranchFeature.INSTANCE, 400);
0091: final Feature ifThenElseF = ScaleFeature.createScaled(
0092: IfThenElseMalusFeature.INSTANCE, 500);
0093:
0094: final Feature strengthenConstraints = ifHeuristics(
0095: new String[] { "concrete", "closure" }, longConst(0),
0096: ifZero(ConstraintStrengthenFeatureUC.create(p_proof),
0097: inftyConst()));
0098:
0099: String methProp = strategyProperties
0100: .getProperty(StrategyProperties.METHOD_OPTIONS_KEY);
0101:
0102: final Feature methodSpecF;
0103: if (methProp.equals(StrategyProperties.METHOD_CONTRACT)) {
0104: methodSpecF = methodSpecFeature(longConst(-20));
0105: } else if (methProp.equals(StrategyProperties.METHOD_EXPAND)) {
0106: methodSpecF = methodSpecFeature(inftyConst());
0107: } else if (methProp.equals(StrategyProperties.METHOD_NONE)) {
0108: methodSpecF = methodSpecFeature(inftyConst());
0109: } else
0110: throw new RuntimeException("Unexpected strategy property "
0111: + methProp);
0112:
0113: return SumFeature.createSum(new Feature[] {
0114: AutomatedRuleFeature.INSTANCE,
0115: // splitF,
0116: dispatcher, NonDuplicateAppFeature.INSTANCE,
0117: strengthenConstraints, AgeFeature.INSTANCE,
0118: simplifierF, methodSpecF, ifMatchedF, ifThenElseF });
0119: }
0120:
0121: private Feature methodSpecFeature(Feature cost) {
0122: return ConditionalFeature.createConditional(
0123: UseMethodContractRuleFilter.INSTANCE, cost);
0124: }
0125:
0126: ////////////////////////////////////////////////////////////////////////////
0127: ////////////////////////////////////////////////////////////////////////////
0128: //
0129: // Feature terms that handle the computation of costs for taclet applications
0130: //
0131: ////////////////////////////////////////////////////////////////////////////
0132: ////////////////////////////////////////////////////////////////////////////
0133:
0134: private RuleSetDispatchFeature setupCostComputationF(Proof p_proof) {
0135: final IntegerLDT numbers = p_proof.getServices()
0136: .getTypeConverter().getIntegerLDT();
0137:
0138: final RuleSetDispatchFeature d = RuleSetDispatchFeature
0139: .create();
0140:
0141: bindRuleSet(d, "closure", -9000);
0142: bindRuleSet(d, "concrete", -10000);
0143: bindRuleSet(d, "alpha", -7000);
0144: bindRuleSet(d, "delta", -6000);
0145:
0146: bindRuleSet(d, "simplify_boolean", -200);
0147: bindRuleSet(d, "simplify", -200);
0148: bindRuleSet(d, "simplify_expression", -100);
0149: bindRuleSet(d, "executeIntegerAssignment", -100);
0150:
0151: bindRuleSet(d, "javaIntegerSemantics", -5000);
0152:
0153: setupSplitting(d);
0154:
0155: bindRuleSet(d, "test_gen", inftyConst());
0156:
0157: bindRuleSet(d, "gamma", add(not(isInstantiated("t")),
0158: ifZero(allowQuantifierSplitting(), longConst(0),
0159: longConst(50))));
0160: bindRuleSet(d, "gamma_destructive", inftyConst());
0161:
0162: setupReplaceKnown(d);
0163:
0164: bindRuleSet(d, "confluence_restricted", ifZero(
0165: MatchedIfFeature.INSTANCE,
0166: DiffFindAndIfFeature.INSTANCE));
0167:
0168: setupApplyEq(d, numbers);
0169:
0170: bindRuleSet(d, "insert_eq_nonrigid", applyTF(FocusProjection
0171: .create(0), IsNonRigidTermFeature.INSTANCE));
0172:
0173: bindRuleSet(d, "order_terms", add(ifZero(applyTF("commEqLeft",
0174: tf.intF), add(applyTF("commEqRight", tf.monomial),
0175: applyTF("commEqLeft", tf.polynomial), monSmallerThan(
0176: "commEqLeft", "commEqRight", numbers)),
0177: termSmallerThan("commEqLeft", "commEqRight")),
0178: longConst(-5000)));
0179:
0180: bindRuleSet(d, "simplify_literals", ifZero(
0181: ConstraintStrengthenFeatureUC.create(p_proof),
0182: longConst(0), longConst(-8000)));
0183:
0184: bindRuleSet(d, "simplify_instanceof_static", add(
0185: EqNonDuplicateAppFeature.INSTANCE, longConst(-500)));
0186:
0187: bindRuleSet(d, "evaluate_instanceof", longConst(-500));
0188:
0189: bindRuleSet(d, "instanceof_to_exists",
0190: TopLevelFindFeature.ANTEC);
0191:
0192: bindRuleSet(d, "try_apply_subst", add(
0193: EqNonDuplicateAppFeature.INSTANCE, longConst(-10000)));
0194:
0195: final TermBuffer super For = new TermBuffer();
0196: bindRuleSet(d, "split_if", add(sum(super For, SuperTermGenerator
0197: .upwards(any()), applyTF(super For, not(ff.program))),
0198: longConst(50)));
0199:
0200: final String[] exceptionsWithPenalty = new String[] {
0201: "java.lang.NullPointerException",
0202: "java.lang.ArrayIndexOutOfBoundsException",
0203: "java.lang.ArrayStoreException",
0204: "java.lang.ClassCastException" };
0205:
0206: bindRuleSet(d, "simplify_prog", ifZero(ThrownExceptionFeature
0207: .create(exceptionsWithPenalty, p_proof.getServices()),
0208: longConst(500),
0209: ifZero(isBelow(add(ff.forF, not(ff.atom))),
0210: longConst(200), longConst(-100))));
0211:
0212: // features influenced by the strategy options
0213:
0214: boolean useLoopExpand = strategyProperties.getProperty(
0215: StrategyProperties.LOOP_OPTIONS_KEY).equals(
0216: StrategyProperties.LOOP_EXPAND);
0217: boolean useLoopInvariant = strategyProperties.getProperty(
0218: StrategyProperties.LOOP_OPTIONS_KEY).equals(
0219: StrategyProperties.LOOP_INVARIANT);
0220: boolean programsToRight = expandQueries()
0221: || strategyProperties.getProperty(
0222: StrategyProperties.QUERY_OPTIONS_KEY).equals(
0223: StrategyProperties.QUERY_PROGRAMS_TO_RIGHT);
0224:
0225: String methProp = strategyProperties
0226: .getProperty(StrategyProperties.METHOD_OPTIONS_KEY);
0227:
0228: if (methProp.equals(StrategyProperties.METHOD_CONTRACT)) {
0229: bindRuleSet(d, "method_expand", longConst(100));
0230: } else if (methProp.equals(StrategyProperties.METHOD_EXPAND)) {
0231: bindRuleSet(d, "method_expand", longConst(100));
0232: } else if (methProp.equals(StrategyProperties.METHOD_NONE)) {
0233: bindRuleSet(d, "method_expand", inftyConst());
0234: } else
0235: throw new RuntimeException("Unexpected strategy property "
0236: + methProp);
0237:
0238: bindRuleSet(d, "loop_expand", useLoopExpand ? longConst(0)
0239: : inftyConst());
0240:
0241: bindRuleSet(d, "loop_invariant",
0242: useLoopInvariant ? longConst(100) : inftyConst());
0243:
0244: bindRuleSet(d, "loop_invariant_proposal", ifHeuristics(
0245: new String[] { "loop_invariant" }, longConst(0),
0246: inftyConst()));
0247:
0248: // delete cast
0249: bindRuleSet(d, "cast_deletion", ifZero(
0250: implicitCastNecessary(instOf("castedTerm")),
0251: longConst(-5000), inftyConst()));
0252:
0253: setupQueries(d);
0254:
0255: bindRuleSet(d, "inReachableStateImplication", add(
0256: NonDuplicateAppModPositionFeature.INSTANCE,
0257: longConst(100)));
0258:
0259: bindRuleSet(d, "inReachableStateExpandAntec", -200);
0260:
0261: bindRuleSet(d, "inReachableStateExpandRewrite", add(
0262: not(TopLevelFindFeature.ANTEC),
0263: NonDuplicateAppModPositionFeature.INSTANCE,
0264: longConst(-100)));
0265:
0266: bindRuleSet(d, "type_hierarchy_def", -6500);
0267:
0268: if (programsToRight)
0269: bindRuleSet(d, "boxDiamondConv",
0270: TopLevelFindFeature.ANTEC_WITH_UPDATE);
0271: else
0272: bindRuleSet(d, "boxDiamondConv", inftyConst());
0273:
0274: bindRuleSet(d, "cut", not(isInstantiated("cutFormula")));
0275:
0276: setupUserTaclets(d);
0277:
0278: setupArithPrimaryCategories(d);
0279: setupPolySimp(d, numbers);
0280: setupInEqSimp(d, p_proof, numbers);
0281:
0282: setupDefOpsPrimaryCategories(d);
0283:
0284: setupSystemInvariantSimp(d);
0285:
0286: if (quantifierInstantiatedEnabled()) {
0287: setupFormulaNormalisation(d, numbers);
0288: } else {
0289: bindRuleSet(d, "negationNormalForm", inftyConst());
0290: bindRuleSet(d, "moveQuantToLeft", inftyConst());
0291: bindRuleSet(d, "conjNormalForm", inftyConst());
0292: bindRuleSet(d, "apply_equations_andOr", inftyConst());
0293: bindRuleSet(d, "elimQuantifier", inftyConst());
0294: bindRuleSet(d, "distrQuantifier", inftyConst());
0295: bindRuleSet(d, "swapQuantifiers", inftyConst());
0296: bindRuleSet(d, "pullOutQuantifierAll", inftyConst());
0297: bindRuleSet(d, "pullOutQuantifierEx", inftyConst());
0298: }
0299:
0300: // For taclets that need instantiation, but where the instantiation is
0301: // deterministic and does not have to be repeated at a later point, we
0302: // setup the same feature terms as in the instantiation method. The
0303: // definitions in <code>setupInstantiationWithoutRetry</code> should
0304: // give cost infinity to those incomplete rule applications that will
0305: // never be instantiated (so that these applications can be removed from
0306: // the queue and do not have to be considered again).
0307: setupInstantiationWithoutRetry(d, p_proof);
0308:
0309: return d;
0310: }
0311:
0312: private void setupReplaceKnown(RuleSetDispatchFeature d) {
0313: final Feature commonF = add(ifZero(MatchedIfFeature.INSTANCE,
0314: DiffFindAndIfFeature.INSTANCE), longConst(-5000),
0315: ScaleFeature.createScaled(
0316: CountMaxDPathFeature.INSTANCE, 10.0));
0317:
0318: bindRuleSet(d, "replace_known_left", commonF);
0319: bindRuleSet(d, "replace_known_right", add(commonF, ifZero(
0320: DirectlyBelowSymbolFeature.create(Op.IMP, 1),
0321: longConst(100), ifZero(DirectlyBelowSymbolFeature
0322: .create(Op.EQV), longConst(100)))));
0323: }
0324:
0325: private void setupQueries(RuleSetDispatchFeature d) {
0326: // attention: usually this application is against the term order but
0327: // does not interfere as only applied below updates
0328: bindRuleSet(d, "query_normalize", ifZero(
0329: add(DirectlyBelowOpClassFeature
0330: .create(ProgramMethod.class), applyTF(
0331: FocusProjection.create(2), ff.update), applyTF(
0332: "t", IsNonRigidTermFeature.INSTANCE)),
0333: longConst(-10), inftyConst()));
0334:
0335: if (expandQueries())
0336: bindRuleSet(d, "queries", add(
0337: normalSplitting() ? not(isBelow(add(ff.forF,
0338: not(ff.atom)))) : longConst(0),
0339: NonDuplicateAppModPositionFeature.INSTANCE));
0340: else
0341: bindRuleSet(d, "queries", inftyConst());
0342: }
0343:
0344: private void setupUserTaclets(RuleSetDispatchFeature d) {
0345: for (int i = 1; i <= StrategyProperties.USER_TACLETS_NUM; ++i) {
0346: final String userTacletsProbs = strategyProperties
0347: .getProperty(StrategyProperties
0348: .USER_TACLETS_OPTIONS_KEY(i));
0349: if (StrategyProperties.USER_TACLETS_LOW
0350: .equals(userTacletsProbs))
0351: bindRuleSet(d, "userTaclets" + i, 10000);
0352: else if (StrategyProperties.USER_TACLETS_HIGH
0353: .equals(userTacletsProbs))
0354: bindRuleSet(d, "userTaclets" + i, -50);
0355: else
0356: bindRuleSet(d, "userTaclets" + i, inftyConst());
0357: }
0358: }
0359:
0360: private void setupSystemInvariantSimp(RuleSetDispatchFeature d) {
0361: bindRuleSet(d, "system_invariant", ifZero(
0362: MatchedIfFeature.INSTANCE, add(applyTF("negLit",
0363: tf.negLiteral), applyTFNonStrict("nonNegLit",
0364: tf.nonNegLiteral))));
0365: }
0366:
0367: ////////////////////////////////////////////////////////////////////////////
0368: ////////////////////////////////////////////////////////////////////////////
0369: //
0370: // Queries for the active taclet options
0371: //
0372: ////////////////////////////////////////////////////////////////////////////
0373: ////////////////////////////////////////////////////////////////////////////
0374:
0375: private boolean expandQueries() {
0376: return strategyProperties.getProperty(
0377: StrategyProperties.QUERY_OPTIONS_KEY).equals(
0378: StrategyProperties.QUERY_EXPAND);
0379: }
0380:
0381: private boolean arithNonLinInferences() {
0382: return StrategyProperties.NON_LIN_ARITH_COMPLETION
0383: .equals(strategyProperties
0384: .getProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY));
0385: }
0386:
0387: protected boolean arithDefOps() {
0388: return StrategyProperties.NON_LIN_ARITH_DEF_OPS
0389: .equals(strategyProperties
0390: .getProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY))
0391: || StrategyProperties.NON_LIN_ARITH_COMPLETION
0392: .equals(strategyProperties
0393: .getProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY));
0394: }
0395:
0396: private boolean instQuantifiersWithQueries() {
0397: return StrategyProperties.QUANTIFIERS_INSTANTIATE
0398: .equals(strategyProperties
0399: .getProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY));
0400: }
0401:
0402: private boolean quantifiersMightSplit() {
0403: return StrategyProperties.QUANTIFIERS_INSTANTIATE
0404: .equals(strategyProperties
0405: .getProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY))
0406: || StrategyProperties.QUANTIFIERS_NON_SPLITTING_WITH_PROGS
0407: .equals(strategyProperties
0408: .getProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY));
0409: }
0410:
0411: private Feature allowQuantifierSplitting() {
0412: if (StrategyProperties.QUANTIFIERS_INSTANTIATE
0413: .equals(strategyProperties
0414: .getProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY)))
0415: return longConst(0);
0416: if (StrategyProperties.QUANTIFIERS_NON_SPLITTING_WITH_PROGS
0417: .equals(strategyProperties
0418: .getProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY)))
0419: return sequentContainsNoPrograms();
0420: return inftyConst();
0421: }
0422:
0423: private Feature sequentContainsNoPrograms() {
0424: // return not ( expandQueries ()
0425: // ? SeqContainsExecutableCodeFeature.PROGRAMS_OR_QUERIES
0426: // : SeqContainsExecutableCodeFeature.PROGRAMS );
0427: return not(SeqContainsExecutableCodeFeature.PROGRAMS);
0428: }
0429:
0430: private boolean quantifierInstantiatedEnabled() {
0431: return !StrategyProperties.QUANTIFIERS_NONE
0432: .equals(strategyProperties
0433: .getProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY));
0434: }
0435:
0436: private Feature allowSplitting(ProjectionToTerm focus) {
0437: if (normalSplitting())
0438: return longConst(0);
0439:
0440: if (StrategyProperties.SPLITTING_DELAYED
0441: .equals(strategyProperties
0442: .getProperty(StrategyProperties.SPLITTING_OPTIONS_KEY)))
0443: return or(applyTF(focus,
0444: ContainsExecutableCodeTermFeature.PROGRAMS),
0445: sequentContainsNoPrograms());
0446:
0447: // else: SPLITTING_OFF
0448: return applyTF(focus,
0449: ContainsExecutableCodeTermFeature.PROGRAMS);
0450: }
0451:
0452: private boolean normalSplitting() {
0453: return StrategyProperties.SPLITTING_NORMAL
0454: .equals(strategyProperties
0455: .getProperty(StrategyProperties.SPLITTING_OPTIONS_KEY));
0456: }
0457:
0458: ////////////////////////////////////////////////////////////////////////////
0459: ////////////////////////////////////////////////////////////////////////////
0460: //
0461: // Application of beta- and cut-rules to handle disjunctions
0462: //
0463: ////////////////////////////////////////////////////////////////////////////
0464: ////////////////////////////////////////////////////////////////////////////
0465:
0466: private void setupSplitting(RuleSetDispatchFeature d) {
0467: final TermBuffer subFor = new TermBuffer();
0468: final Feature noCutsAllowed = sum(subFor,
0469: AllowedCutPositionsGenerator.INSTANCE, not(applyTF(
0470: subFor, ff.cutAllowed)));
0471:
0472: bindRuleSet(d, "beta", SumFeature.createSum(new Feature[] {
0473: noCutsAllowed,
0474: ifZero(PurePosDPathFeature.INSTANCE, longConst(-200)),
0475: ScaleFeature.createScaled(
0476: CountPosDPathFeature.INSTANCE, -3.0),
0477: ScaleFeature.createScaled(
0478: CountMaxDPathFeature.INSTANCE, 10.0),
0479: longConst(20) }));
0480:
0481: bindRuleSet(d, "split_cond", longConst(1));
0482:
0483: bindRuleSet(
0484: d,
0485: "cut_direct",
0486: SumFeature
0487: .createSum(new Feature[] {
0488: not(TopLevelFindFeature.ANTEC_OR_SUCC_WITH_UPDATE),
0489: AllowedCutPositionFeature.INSTANCE,
0490: ifZero(
0491: NotBelowQuantifierFeature.INSTANCE,
0492: add(applyTF("cutFormula",
0493: ff.cutAllowed),
0494: longConst(10)),
0495: SumFeature
0496: .createSum(new Feature[] {
0497: applyTF(
0498: "cutFormula",
0499: ff.cutAllowedBelowQuantifier),
0500: applyTF(
0501: FocusFormulaProjection.INSTANCE,
0502: ff.quantifiedClauseSet),
0503: ifZero(
0504: allowQuantifierSplitting(),
0505: longConst(0),
0506: longConst(100)) })) }));
0507: }
0508:
0509: private void setupSplittingApproval(RuleSetDispatchFeature d) {
0510: bindRuleSet(d, "beta",
0511: allowSplitting(FocusFormulaProjection.INSTANCE));
0512:
0513: bindRuleSet(d, "split_cond", allowSplitting(FocusProjection
0514: .create(0)));
0515:
0516: final TermBuffer subFor = new TermBuffer();
0517: final Feature compareCutAllowed = ifZero(applyTF(subFor,
0518: ff.cutAllowed), leq(applyTF("cutFormula",
0519: ff.cutPriority), applyTF(subFor, ff.cutPriority)));
0520:
0521: final Feature noBetterCut = sum(subFor,
0522: AllowedCutPositionsGenerator.INSTANCE,
0523: compareCutAllowed);
0524:
0525: bindRuleSet(d, "cut_direct",
0526: add(allowSplitting(FocusFormulaProjection.INSTANCE),
0527: ifZero(NotBelowQuantifierFeature.INSTANCE,
0528: noBetterCut)));
0529: }
0530:
0531: ////////////////////////////////////////////////////////////////////////////
0532: ////////////////////////////////////////////////////////////////////////////
0533: //
0534: // Application of equations
0535: //
0536: ////////////////////////////////////////////////////////////////////////////
0537: ////////////////////////////////////////////////////////////////////////////
0538:
0539: private void setupApplyEq(RuleSetDispatchFeature d,
0540: IntegerLDT numbers) {
0541: final TermBuffer equation = new TermBuffer();
0542: final TermBuffer left = new TermBuffer(), right = new TermBuffer();
0543:
0544: // applying equations less deep/less leftish in terms/formulas is preferred
0545: // this is important for reducing polynomials (start with the biggest
0546: // summands)
0547: bindRuleSet(
0548: d,
0549: "apply_equations",
0550: SumFeature
0551: .createSum(new Feature[] {
0552: ifZero(
0553: applyTF(FocusProjection
0554: .create(0), tf.intF),
0555: add(
0556: applyTF(FocusProjection
0557: .create(0),
0558: tf.monomial),
0559: ScaleFeature
0560: .createScaled(
0561: FindRightishFeature
0562: .create(numbers),
0563: 5.0))),
0564: ifZero(
0565: MatchedIfFeature.INSTANCE,
0566: add(
0567: CheckApplyEqFeature.INSTANCE,
0568: let(
0569: equation,
0570: AssumptionProjection
0571: .create(0),
0572: add(
0573: not(applyTF(
0574: equation,
0575: ff.update)),
0576: // there might be updates in front of the assumption
0577: // formula; in this case we wait until the updates have
0578: // been applied
0579: let(
0580: left,
0581: sub(
0582: equation,
0583: 0),
0584: let(
0585: right,
0586: sub(
0587: equation,
0588: 1),
0589: ifZero(
0590: applyTF(
0591: left,
0592: tf.intF),
0593: add(
0594: applyTF(
0595: left,
0596: tf.nonNegOrNonCoeffMonomial),
0597: applyTF(
0598: right,
0599: tf.polynomial),
0600: MonomialsSmallerThanFeature
0601: .create(
0602: right,
0603: left,
0604: numbers)),
0605: TermSmallerThanFeature
0606: .create(
0607: right,
0608: left)))))))),
0609: longConst(-4000) }));
0610: }
0611:
0612: ////////////////////////////////////////////////////////////////////////////
0613: ////////////////////////////////////////////////////////////////////////////
0614: //
0615: // Normalisation of formulas; this is mostly a pre-processing step for
0616: // handling quantified formulas
0617: //
0618: ////////////////////////////////////////////////////////////////////////////
0619: ////////////////////////////////////////////////////////////////////////////
0620:
0621: private void setupFormulaNormalisation(RuleSetDispatchFeature d,
0622: IntegerLDT numbers) {
0623:
0624: bindRuleSet(d, "negationNormalForm", add(
0625: not(NotBelowBinderFeature.INSTANCE), longConst(-500),
0626: ScaleFeature.createScaled(FindDepthFeature.INSTANCE,
0627: 10.0)));
0628:
0629: bindRuleSet(d, "moveQuantToLeft", add(
0630: quantifiersMightSplit() ? longConst(0) : applyTF(
0631: FocusFormulaProjection.INSTANCE,
0632: ff.quantifiedPureLitConjDisj), longConst(-550)));
0633:
0634: bindRuleSet(d, "conjNormalForm", add(not(applyTF(
0635: FocusFormulaProjection.INSTANCE, ff.propJunctor)),
0636: NotInScopeOfModalityFeature.INSTANCE, longConst(-150)));
0637:
0638: bindRuleSet(d, "elimQuantifier", -1000);
0639: bindRuleSet(d, "elimQuantifierWithCast", 50);
0640:
0641: final TermBuffer left = new TermBuffer();
0642: final TermBuffer right = new TermBuffer();
0643: bindRuleSet(d, "apply_equations_andOr", add(let(left,
0644: instOf("applyEqLeft"), let(right,
0645: instOf("applyEqRight"), ifZero(applyTF(left,
0646: tf.intF), add(applyTF(left,
0647: tf.nonNegOrNonCoeffMonomial), applyTF(
0648: right, tf.polynomial),
0649: MonomialsSmallerThanFeature.create(
0650: right, left, numbers)),
0651: TermSmallerThanFeature.create(right,
0652: left)))), longConst(-150)));
0653:
0654: bindRuleSet(d, "distrQuantifier", add(or(applyTF(
0655: FocusProjection.create(0), add(ff.quantifiedClauseSet,
0656: not(opSub(Op.ALL, ff.orF)),
0657: EliminableQuantifierTF.INSTANCE)), SumFeature
0658: .createSum(new Feature[] {
0659: OnlyInScopeOfQuantifiersFeature.INSTANCE,
0660: SplittableQuantifiedFormulaFeature.INSTANCE,
0661: ifZero(FocusInAntecFeature.INSTANCE,
0662: applyTF(FocusProjection.create(0),
0663: sub(ff.andF)), applyTF(
0664: FocusProjection.create(0),
0665: sub(ff.orF))) })),
0666: longConst(-300)));
0667:
0668: bindRuleSet(d, "swapQuantifiers", add(applyTF(FocusProjection
0669: .create(0), add(ff.quantifiedClauseSet,
0670: EliminableQuantifierTF.INSTANCE,
0671: sub(not(EliminableQuantifierTF.INSTANCE)))),
0672: longConst(-300)));
0673:
0674: // category "conjunctive normal form"
0675:
0676: bindRuleSet(d, "cnf_orComm", SumFeature
0677: .createSum(new Feature[] {
0678: applyTF("commRight", ff.clause),
0679: applyTFNonStrict("commResidue", ff.clauseSet),
0680: or(applyTF("commLeft", ff.andF), add(applyTF(
0681: "commLeft", ff.literal),
0682: literalsSmallerThan("commRight",
0683: "commLeft", numbers))),
0684: longConst(-100) }));
0685:
0686: bindRuleSet(d, "cnf_orAssoc",
0687: SumFeature
0688: .createSum(new Feature[] {
0689: applyTF("assoc0", ff.clause),
0690: applyTF("assoc1", ff.clause),
0691: applyTF("assoc2", ff.literal),
0692: longConst(-80) }));
0693:
0694: bindRuleSet(d, "cnf_andComm", SumFeature
0695: .createSum(new Feature[] {
0696: applyTF("commLeft", ff.clause),
0697: applyTF("commRight", ff.clauseSet),
0698: applyTFNonStrict("commResidue", ff.clauseSet),
0699: // at least one of the subformulas has to be a literal; otherwise,
0700: // sorting is not likely to have any big effect
0701: ifZero(add(
0702: applyTF("commLeft", not(ff.literal)),
0703: applyTF("commRight", rec(ff.andF,
0704: not(ff.literal)))),
0705: longConst(100), longConst(-60)),
0706: clausesSmallerThan("commRight", "commLeft",
0707: numbers) }));
0708:
0709: bindRuleSet(d, "cnf_andAssoc", SumFeature
0710: .createSum(new Feature[] {
0711: applyTF("assoc0", ff.clauseSet),
0712: applyTF("assoc1", ff.clauseSet),
0713: applyTF("assoc2", ff.clause), longConst(-10) }));
0714:
0715: bindRuleSet(d, "cnf_dist", SumFeature.createSum(new Feature[] {
0716: applyTF("distRight0", ff.clauseSet),
0717: applyTF("distRight1", ff.clauseSet),
0718: ifZero(applyTF("distLeft", ff.clause), longConst(-15),
0719: applyTF("distLeft", ff.clauseSet)),
0720: longConst(-35) }));
0721:
0722: final TermBuffer super For = new TermBuffer();
0723: final Feature onlyBelowQuanAndOr = sum(super For,
0724: SuperTermGenerator.upwards(any()), applyTF(super For,
0725: or(ff.quantifiedFor, ff.andF, ff.orF)));
0726:
0727: final Feature belowUnskolemisableQuantifier = ifZero(
0728: FocusInAntecFeature.INSTANCE, not(sum(super For,
0729: SuperTermGenerator.upwards(any()), not(applyTF(
0730: super For, op(Op.ALL))))), not(sum(
0731: super For, SuperTermGenerator.upwards(any()),
0732: not(applyTF(super For, op(Op.EX))))));
0733:
0734: bindRuleSet(d, "cnf_expandIfThenElse", add(
0735: not(NotBelowQuantifierFeature.INSTANCE),
0736: onlyBelowQuanAndOr, belowUnskolemisableQuantifier));
0737:
0738: final Feature pullOutQuantifierAllowed = add(
0739: not(NotBelowQuantifierFeature.INSTANCE),
0740: onlyBelowQuanAndOr, applyTF(FocusProjection.create(0),
0741: sub(ff.quantifiedClauseSet,
0742: ff.quantifiedClauseSet)));
0743:
0744: bindRuleSet(d, "pullOutQuantifierUnifying", -20);
0745:
0746: bindRuleSet(d, "pullOutQuantifierAll", add(
0747: pullOutQuantifierAllowed, ifZero(
0748: FocusInAntecFeature.INSTANCE, longConst(-20),
0749: longConst(-40))));
0750:
0751: bindRuleSet(d, "pullOutQuantifierEx", add(
0752: pullOutQuantifierAllowed, ifZero(
0753: FocusInAntecFeature.INSTANCE, longConst(-40),
0754: longConst(-20))));
0755: }
0756:
0757: private Feature clausesSmallerThan(String smaller, String bigger,
0758: IntegerLDT numbers) {
0759: return ClausesSmallerThanFeature.create(instOf(smaller),
0760: instOf(bigger), numbers);
0761: }
0762:
0763: ////////////////////////////////////////////////////////////////////////////
0764: ////////////////////////////////////////////////////////////////////////////
0765: //
0766: // Heuristic instantiation of quantified formulas
0767: //
0768: ////////////////////////////////////////////////////////////////////////////
0769: ////////////////////////////////////////////////////////////////////////////
0770:
0771: private void setupQuantifierInstantiation(RuleSetDispatchFeature d) {
0772: if (quantifierInstantiatedEnabled()) {
0773: final TermBuffer varInst = new TermBuffer();
0774: final Feature branchPrediction = InstantiationCostScalerFeature
0775: .create(InstantiationCost.create(varInst),
0776: allowQuantifierSplitting());
0777:
0778: bindRuleSet(
0779: d,
0780: "gamma",
0781: SumFeature
0782: .createSum(new Feature[] {
0783: FocusInAntecFeature.INSTANCE,
0784: applyTF(
0785: FocusProjection.create(0),
0786: add(
0787: ff.quantifiedClauseSet,
0788: instQuantifiersWithQueries() ? longTermConst(0)
0789: : ff.notContainsExecutable)),
0790: forEach(
0791: varInst,
0792: HeuristicInstantiation.INSTANCE,
0793: add(instantiate("t",
0794: varInst),
0795: branchPrediction)) }));
0796: } else {
0797: bindRuleSet(d, "gamma", inftyConst());
0798: }
0799: }
0800:
0801: private void setupQuantifierInstantiationApproval(
0802: RuleSetDispatchFeature d) {
0803: if (quantifierInstantiatedEnabled()) {
0804: final TermBuffer varInst = new TermBuffer();
0805:
0806: bindRuleSet(d, "gamma", add(isInstantiated("t"), not(sum(
0807: varInst, HeuristicInstantiation.INSTANCE, not(eq(
0808: instOf("t"), varInst)))),
0809: InstantiationCostScalerFeature.create(
0810: InstantiationCost.create(instOf("t")),
0811: longConst(0))));
0812: } else {
0813: bindRuleSet(d, "gamma", inftyConst());
0814: }
0815: }
0816:
0817: ////////////////////////////////////////////////////////////////////////////
0818: ////////////////////////////////////////////////////////////////////////////
0819: //
0820: // Handling of arithmetic
0821: //
0822: ////////////////////////////////////////////////////////////////////////////
0823: ////////////////////////////////////////////////////////////////////////////
0824:
0825: private static final int IN_EQ_SIMP_NON_LIN_COST = 1000;
0826: private static final int POLY_DIVISION_COST = -2250;
0827:
0828: private void setupArithPrimaryCategories(RuleSetDispatchFeature d) {
0829: // Gaussian elimination + Euclidian algorithm for linear equations;
0830: // Buchberger's algorithmus for handling polynomial equations over
0831: // the integers
0832:
0833: bindRuleSet(d, "polySimp_expand", -4500);
0834: bindRuleSet(d, "polySimp_directEquations", -3000);
0835: bindRuleSet(d, "polySimp_pullOutGcd", -2250);
0836: bindRuleSet(d, "polySimp_leftNonUnit", -2000);
0837: bindRuleSet(d, "polySimp_saturate", 0);
0838:
0839: // Omega test for handling linear arithmetic and inequalities over the
0840: // integers; cross-multiplication + case distinctions for nonlinear
0841: // inequalities
0842:
0843: bindRuleSet(d, "inEqSimp_expand", -4500);
0844: bindRuleSet(d, "inEqSimp_directInEquations", -3000);
0845: bindRuleSet(d, "inEqSimp_propagation", -2500);
0846: bindRuleSet(d, "inEqSimp_pullOutGcd", -2250);
0847: bindRuleSet(d, "inEqSimp_saturate", -2000);
0848: bindRuleSet(d, "inEqSimp_forNormalisation", -1000);
0849: bindRuleSet(d, "inEqSimp_special_nonLin", -1400);
0850:
0851: if (arithNonLinInferences())
0852: bindRuleSet(d, "inEqSimp_nonLin", IN_EQ_SIMP_NON_LIN_COST);
0853: else
0854: bindRuleSet(d, "inEqSimp_nonLin", inftyConst());
0855:
0856: // polynomial division, simplification of fractions and mods
0857: bindRuleSet(d, "polyDivision", POLY_DIVISION_COST);
0858:
0859: }
0860:
0861: private void setupPolySimp(RuleSetDispatchFeature d,
0862: IntegerLDT numbers) {
0863:
0864: // category "expansion" (normalising polynomial terms)
0865:
0866: bindRuleSet(d, "polySimp_elimSubNeg", longConst(-120));
0867:
0868: bindRuleSet(d, "polySimp_homo", add(applyTF("homoRight", add(
0869: not(tf.zeroLiteral), tf.polynomial)), or(applyTF(
0870: "homoLeft", or(tf.addF, tf.negMonomial)),
0871: not(monSmallerThan("homoRight", "homoLeft", numbers))),
0872: longConst(-120)));
0873:
0874: bindRuleSet(d, "polySimp_pullOutFactor", add(applyTFNonStrict(
0875: "pullOutLeft", tf.literal), applyTFNonStrict(
0876: "pullOutRight", tf.literal), longConst(-120)));
0877:
0878: bindRuleSet(d, "polySimp_elimOneLeft", -120);
0879:
0880: bindRuleSet(d, "polySimp_elimOneRight", -120);
0881:
0882: bindRuleSet(d, "polySimp_mulOrder", add(applyTF("commRight",
0883: tf.monomial), or(applyTF("commLeft", tf.addF), add(
0884: applyTF("commLeft", tf.atom), atomSmallerThan(
0885: "commLeft", "commRight", numbers))),
0886: longConst(-100)));
0887:
0888: bindRuleSet(d, "polySimp_mulAssoc", SumFeature
0889: .createSum(new Feature[] {
0890: applyTF("mulAssocMono0", tf.monomial),
0891: applyTF("mulAssocMono1", tf.monomial),
0892: applyTF("mulAssocAtom", tf.atom),
0893: longConst(-80) }));
0894:
0895: bindRuleSet(d, "polySimp_addOrder",
0896: SumFeature
0897: .createSum(new Feature[] {
0898: applyTF("commLeft", tf.monomial),
0899: applyTF("commRight", tf.polynomial),
0900: monSmallerThan("commRight", "commLeft",
0901: numbers), longConst(-60) }));
0902:
0903: bindRuleSet(d, "polySimp_addAssoc", SumFeature
0904: .createSum(new Feature[] {
0905: applyTF("addAssocPoly0", tf.polynomial),
0906: applyTF("addAssocPoly1", tf.polynomial),
0907: applyTF("addAssocMono", tf.monomial),
0908: longConst(-10) }));
0909:
0910: bindRuleSet(d, "polySimp_dist", SumFeature
0911: .createSum(new Feature[] {
0912: applyTF("distSummand0", tf.polynomial),
0913: applyTF("distSummand1", tf.polynomial),
0914: ifZero(applyTF("distCoeff", tf.monomial),
0915: longConst(-15), applyTF("distCoeff",
0916: tf.polynomial)),
0917: applyTF("distSummand0", tf.polynomial),
0918: applyTF("distSummand1", tf.polynomial),
0919: longConst(-35) }));
0920:
0921: // category "direct equations"
0922:
0923: bindRuleSet(d, "polySimp_balance",
0924: SumFeature
0925: .createSum(new Feature[] {
0926: applyTF("sepResidue", tf.polynomial),
0927: ifZero(isInstantiated("sepPosMono"),
0928: add(applyTF("sepPosMono",
0929: tf.nonNegMonomial),
0930: monSmallerThan(
0931: "sepResidue",
0932: "sepPosMono",
0933: numbers))),
0934: ifZero(isInstantiated("sepNegMono"),
0935: add(applyTF("sepNegMono",
0936: tf.negMonomial),
0937: monSmallerThan(
0938: "sepResidue",
0939: "sepNegMono",
0940: numbers))),
0941: longConst(-30) }));
0942:
0943: bindRuleSet(d, "polySimp_normalise", add(applyTF("invertRight",
0944: tf.zeroLiteral), applyTF("invertLeft", tf.negMonomial),
0945: longConst(-30)));
0946:
0947: // application of equations: some specialised rules that handle
0948: // monomials and their coefficients properly
0949:
0950: final TermBuffer eqLeft = new TermBuffer();
0951: final TermBuffer focus = new TermBuffer();
0952:
0953: final TermFeature atLeastTwoLCEquation = opSub(Op.EQUALS,
0954: opSub(tf.mul, tf.atom, tf.atLeastTwoLiteral), tf.intF);
0955:
0956: final Feature validEqApplication = add(not(eq(eqLeft, focus)),
0957: // otherwise, the normal equation rules can and should be used
0958: ifZero(applyTF(AssumptionProjection.create(0),
0959: atLeastTwoLCEquation), add(
0960: FocusInAntecFeature.INSTANCE, applyTF(
0961: FocusFormulaProjection.INSTANCE,
0962: atLeastTwoLCEquation))),
0963: ReducibleMonomialsFeature
0964: .createReducible(focus, eqLeft));
0965:
0966: final Feature eq_monomial_feature = add(
0967: not(DirectlyBelowSymbolFeature.create(tf.mul)), ifZero(
0968: MatchedIfFeature.INSTANCE, let(focus,
0969: FocusProjection.create(0), let(eqLeft,
0970: sub(AssumptionProjection
0971: .create(0), 0),
0972: validEqApplication))));
0973:
0974: bindRuleSet(d, "polySimp_applyEq", add(eq_monomial_feature,
0975: longConst(1)));
0976:
0977: bindRuleSet(d, "polySimp_applyEqRigid", add(
0978: eq_monomial_feature, longConst(2)));
0979:
0980: // category "saturate"
0981:
0982: bindRuleSet(
0983: d,
0984: "polySimp_critPair",
0985: ifZero(MatchedIfFeature.INSTANCE, add(monSmallerThan(
0986: "cpLeft1", "cpLeft2", numbers),
0987: not(TrivialMonomialLCRFeature.create(
0988: instOf("cpLeft1"), instOf("cpLeft2"))))));
0989: }
0990:
0991: // For taclets that need instantiation, but where the instantiation is
0992: // deterministic and does not have to be repeated at a later point, we
0993: // setup the same feature terms as in the instantiation method. The
0994: // definitions in <code>setupInstantiationWithoutRetry</code> should
0995: // give cost infinity to those incomplete rule applications that will
0996: // never be instantiated (so that these applications can be removed from
0997: // the queue and do not have to be considered again).
0998: private void setupPolySimpInstantiationWithoutRetry(
0999: RuleSetDispatchFeature d, Proof p_proof) {
1000: final IntegerLDT numbers = p_proof.getServices()
1001: .getTypeConverter().getIntegerLDT();
1002:
1003: // category "direct equations"
1004:
1005: setupPullOutGcd(d, "polySimp_pullOutGcd", false);
1006:
1007: // category "polynomial division"
1008:
1009: setupDivModDivision(d);
1010:
1011: // category "handling of equations with non-unit-coefficients on
1012: // left-hand side"
1013:
1014: bindRuleSet(
1015: d,
1016: "polySimp_newSym",
1017: ifZero(
1018: not(isInstantiated("newSymDef")),
1019: SumFeature
1020: .createSum(new Feature[] {
1021: applyTF("newSymLeft", tf.atom),
1022: applyTF("newSymLeftCoeff",
1023: tf.atLeastTwoLiteral),
1024: applyTF("newSymRight",
1025: tf.polynomial),
1026: instantiate(
1027: "newSymDef",
1028: MonomialColumnOp
1029: .create(
1030: instOf("newSymLeftCoeff"),
1031: instOf("newSymRight"))) })));
1032:
1033: final TermBuffer divisor = new TermBuffer();
1034: final TermBuffer dividend = new TermBuffer();
1035:
1036: bindRuleSet(
1037: d,
1038: "polySimp_applyEqPseudo",
1039: add(
1040: applyTF("aePseudoTargetLeft", tf.monomial),
1041: applyTF("aePseudoTargetRight", tf.polynomial),
1042: ifZero(
1043: MatchedIfFeature.INSTANCE,
1044: SumFeature
1045: .createSum(new Feature[] {
1046: DiffFindAndIfFeature.INSTANCE,
1047: applyTF(
1048: "aePseudoLeft",
1049: add(
1050: tf.nonCoeffMonomial,
1051: not(tf.atom))),
1052: applyTF(
1053: "aePseudoLeftCoeff",
1054: tf.atLeastTwoLiteral),
1055: applyTF(
1056: "aePseudoRight",
1057: tf.polynomial),
1058: MonomialsSmallerThanFeature
1059: .create(
1060: instOf("aePseudoRight"),
1061: instOf("aePseudoLeft"),
1062: numbers),
1063: let(
1064: divisor,
1065: instOf("aePseudoLeft"),
1066: let(
1067: dividend,
1068: instOf("aePseudoTargetLeft"),
1069: add(
1070: ReducibleMonomialsFeature
1071: .createReducible(
1072: dividend,
1073: divisor),
1074: instantiate(
1075: "aePseudoTargetFactor",
1076: ReduceMonomialsProjection
1077: .create(
1078: dividend,
1079: divisor))))) }))));
1080: }
1081:
1082: private void setupNewSymApproval(RuleSetDispatchFeature d,
1083: IntegerLDT numbers) {
1084: final TermBuffer antecFor = new TermBuffer();
1085: final Feature columnOpEq = applyTF(antecFor, opSub(tf.eq,
1086: opSub(tf.mul, tf.atom, tf.atLeastTwoLiteral),
1087: tf.polynomial));
1088: final Feature biggerLeftSide = MonomialsSmallerThanFeature
1089: .create(instOf("newSymLeft"), subAt(antecFor,
1090: PosInTerm.TOP_LEVEL.down(0).down(0)), numbers);
1091: bindRuleSet(d, "polySimp_newSym", add(
1092: isInstantiated("newSymDef"), sum(antecFor,
1093: SequentFormulasGenerator.antecedent(), not(add(
1094: columnOpEq, biggerLeftSide)))));
1095: }
1096:
1097: private Feature termSmallerThan(String smaller, String bigger) {
1098: return TermSmallerThanFeature.create(instOf(smaller),
1099: instOf(bigger));
1100: }
1101:
1102: private Feature monSmallerThan(String smaller, String bigger,
1103: IntegerLDT numbers) {
1104: return MonomialsSmallerThanFeature.create(instOf(smaller),
1105: instOf(bigger), numbers);
1106: }
1107:
1108: private Feature atomSmallerThan(String smaller, String bigger,
1109: IntegerLDT numbers) {
1110: return AtomsSmallerThanFeature.create(instOf(smaller),
1111: instOf(bigger), numbers);
1112: }
1113:
1114: private Feature literalsSmallerThan(String smaller, String bigger,
1115: IntegerLDT numbers) {
1116: return LiteralsSmallerThanFeature.create(instOf(smaller),
1117: instOf(bigger), numbers);
1118: }
1119:
1120: private void setupPullOutGcd(RuleSetDispatchFeature d,
1121: String ruleSet, boolean roundingUp) {
1122: final TermBuffer gcd = new TermBuffer();
1123:
1124: final Feature instantiateDivs;
1125: if (roundingUp)
1126: instantiateDivs = add(instantiate("elimGcdLeftDiv",
1127: DividePolynomialsProjection.createRoundingUp(gcd,
1128: instOf("elimGcdLeft"))), instantiate(
1129: "elimGcdRightDiv", DividePolynomialsProjection
1130: .createRoundingUp(gcd,
1131: instOf("elimGcdRight"))));
1132: else
1133: instantiateDivs = add(instantiate("elimGcdLeftDiv",
1134: DividePolynomialsProjection.createRoundingDown(gcd,
1135: instOf("elimGcdLeft"))), instantiate(
1136: "elimGcdRightDiv", DividePolynomialsProjection
1137: .createRoundingDown(gcd,
1138: instOf("elimGcdRight"))));
1139:
1140: bindRuleSet(d, ruleSet, add(applyTF("elimGcdLeft",
1141: tf.nonNegMonomial), applyTF("elimGcdRight",
1142: tf.polynomial), let(gcd, CoeffGcdProjection.create(
1143: instOf("elimGcdLeft"), instOf("elimGcdRight")), add(
1144: applyTF(gcd, tf.atLeastTwoLiteral), instantiate(
1145: "elimGcd", gcd), instantiateDivs))));
1146: }
1147:
1148: private void setupInEqSimp(RuleSetDispatchFeature d, Proof p_proof,
1149: IntegerLDT numbers) {
1150:
1151: // category "expansion" (normalising inequations)
1152:
1153: bindRuleSet(d, "inEqSimp_moveLeft", -90);
1154:
1155: bindRuleSet(d, "inEqSimp_makeNonStrict", -80);
1156:
1157: bindRuleSet(d, "inEqSimp_commute",
1158: SumFeature
1159: .createSum(new Feature[] {
1160: applyTF("commRight", tf.monomial),
1161: applyTF("commLeft", tf.polynomial),
1162: monSmallerThan("commLeft", "commRight",
1163: numbers), longConst(-40) }));
1164:
1165: // this is copied from "polySimp_homo"
1166: bindRuleSet(d, "inEqSimp_homo", add(applyTF("homoRight", add(
1167: not(tf.zeroLiteral), tf.polynomial)), or(applyTF(
1168: "homoLeft", or(tf.addF, tf.negMonomial)),
1169: not(monSmallerThan("homoRight", "homoLeft", numbers)))));
1170:
1171: // category "direct inequations"
1172:
1173: // this is copied from "polySimp_balance"
1174: bindRuleSet(d, "inEqSimp_balance", add(applyTF("sepResidue",
1175: tf.polynomial), ifZero(isInstantiated("sepPosMono"),
1176: add(applyTF("sepPosMono", tf.nonNegMonomial),
1177: monSmallerThan("sepResidue", "sepPosMono",
1178: numbers))), ifZero(
1179: isInstantiated("sepNegMono"), add(applyTF("sepNegMono",
1180: tf.negMonomial), monSmallerThan("sepResidue",
1181: "sepNegMono", numbers)))));
1182:
1183: // this is copied from "polySimp_normalise"
1184: bindRuleSet(d, "inEqSimp_normalise", add(applyTF("invertRight",
1185: tf.zeroLiteral), applyTF("invertLeft", tf.negMonomial)));
1186:
1187: // category "saturate"
1188:
1189: bindRuleSet(d, "inEqSimp_antiSymm", longConst(-20));
1190:
1191: bindRuleSet(
1192: d,
1193: "inEqSimp_exactShadow",
1194: SumFeature
1195: .createSum(new Feature[] {
1196: applyTF("esLeft", tf.nonCoeffMonomial),
1197: applyTFNonStrict("esCoeff2",
1198: tf.nonNegLiteral),
1199: applyTF("esRight2", tf.polynomial),
1200: ifZero(
1201: MatchedIfFeature.INSTANCE,
1202: SumFeature
1203: .createSum(new Feature[] {
1204: applyTFNonStrict(
1205: "esCoeff1",
1206: tf.nonNegLiteral),
1207: applyTF(
1208: "esRight1",
1209: tf.polynomial),
1210: not(PolynomialValuesCmpFeature
1211: .leq(
1212: instOf("esRight2"),
1213: instOf("esRight1"),
1214: instOfNonStrict("esCoeff1"),
1215: instOfNonStrict("esCoeff2"))) })) }));
1216:
1217: // category "propagation"
1218:
1219: bindRuleSet(
1220: d,
1221: "inEqSimp_contradInEqs",
1222: add(
1223: applyTF("contradLeft", tf.monomial),
1224: ifZero(
1225: MatchedIfFeature.INSTANCE,
1226: SumFeature
1227: .createSum(new Feature[] {
1228: DiffFindAndIfFeature.INSTANCE,
1229: applyTF(
1230: "contradRightSmaller",
1231: tf.polynomial),
1232: applyTF(
1233: "contradRightBigger",
1234: tf.polynomial),
1235: applyTFNonStrict(
1236: "contradCoeffSmaller",
1237: tf.posLiteral),
1238: applyTFNonStrict(
1239: "contradCoeffBigger",
1240: tf.posLiteral),
1241: PolynomialValuesCmpFeature
1242: .lt(
1243: instOf("contradRightSmaller"),
1244: instOf("contradRightBigger"),
1245: instOfNonStrict("contradCoeffBigger"),
1246: instOfNonStrict("contradCoeffSmaller")) }))));
1247:
1248: bindRuleSet(d, "inEqSimp_contradEqs", add(applyTF(
1249: "contradLeft", tf.monomial), ifZero(
1250: MatchedIfFeature.INSTANCE,
1251: SumFeature.createSum(new Feature[] {
1252: applyTF("contradRightSmaller", tf.polynomial),
1253: applyTF("contradRightBigger", tf.polynomial),
1254: PolynomialValuesCmpFeature.lt(
1255: instOf("contradRightSmaller"),
1256: instOf("contradRightBigger")) })),
1257: longConst(-60)));
1258:
1259: bindRuleSet(d, "inEqSimp_strengthen", longConst(-30));
1260:
1261: bindRuleSet(
1262: d,
1263: "inEqSimp_subsumption",
1264: add(
1265: applyTF("subsumLeft", tf.monomial),
1266: ifZero(
1267: MatchedIfFeature.INSTANCE,
1268: SumFeature
1269: .createSum(new Feature[] {
1270: DiffFindAndIfFeature.INSTANCE,
1271: applyTF(
1272: "subsumRightSmaller",
1273: tf.polynomial),
1274: applyTF(
1275: "subsumRightBigger",
1276: tf.polynomial),
1277: applyTFNonStrict(
1278: "subsumCoeffSmaller",
1279: tf.posLiteral),
1280: applyTFNonStrict(
1281: "subsumCoeffBigger",
1282: tf.posLiteral),
1283: PolynomialValuesCmpFeature
1284: .leq(
1285: instOf("subsumRightSmaller"),
1286: instOf("subsumRightBigger"),
1287: instOfNonStrict("subsumCoeffBigger"),
1288: instOfNonStrict("subsumCoeffSmaller")) }))));
1289:
1290: // category "handling of non-linear inequations"
1291:
1292: if (arithNonLinInferences()) {
1293: setupMultiplyInequations(d, longConst(100));
1294:
1295: bindRuleSet(d, "inEqSimp_split_eq", add(
1296: TopLevelFindFeature.SUCC, longConst(-100)));
1297:
1298: bindRuleSet(d, "inEqSimp_signCases",
1299: not(isInstantiated("signCasesLeft")));
1300: }
1301:
1302: // category "normalisation of formulas"
1303: // (e.g., quantified formulas, where the normal sequent calculus
1304: // does not do any normalisation)
1305:
1306: bindRuleSet(d, "inEqSimp_and_contradInEqs", SumFeature
1307: .createSum(new Feature[] {
1308: applyTF("contradLeft", tf.monomial),
1309: applyTF("contradRightSmaller", tf.polynomial),
1310: applyTF("contradRightBigger", tf.polynomial),
1311: PolynomialValuesCmpFeature.lt(
1312: instOf("contradRightSmaller"),
1313: instOf("contradRightBigger")) }));
1314:
1315: bindRuleSet(d, "inEqSimp_andOr_subsumption", SumFeature
1316: .createSum(new Feature[] {
1317: applyTF("subsumLeft", tf.monomial),
1318: applyTF("subsumRightSmaller", tf.polynomial),
1319: applyTF("subsumRightBigger", tf.polynomial),
1320: PolynomialValuesCmpFeature.leq(
1321: instOf("subsumRightSmaller"),
1322: instOf("subsumRightBigger")) }));
1323:
1324: bindRuleSet(d, "inEqSimp_and_subsumptionEq", SumFeature
1325: .createSum(new Feature[] {
1326: applyTF("subsumLeft", tf.monomial),
1327: applyTF("subsumRightSmaller", tf.polynomial),
1328: applyTF("subsumRightBigger", tf.polynomial),
1329: PolynomialValuesCmpFeature.lt(
1330: instOf("subsumRightSmaller"),
1331: instOf("subsumRightBigger")) }));
1332:
1333: final TermBuffer one = new TermBuffer();
1334: one
1335: .setContent(TermBuilder.DF.zTerm(p_proof.getServices(),
1336: "1"));
1337: final TermBuffer two = new TermBuffer();
1338: two
1339: .setContent(TermBuilder.DF.zTerm(p_proof.getServices(),
1340: "2"));
1341:
1342: bindRuleSet(
1343: d,
1344: "inEqSimp_or_tautInEqs",
1345: SumFeature
1346: .createSum(new Feature[] {
1347: applyTF("tautLeft", tf.monomial),
1348: applyTF("tautRightSmaller",
1349: tf.polynomial),
1350: applyTF("tautRightBigger",
1351: tf.polynomial),
1352: PolynomialValuesCmpFeature
1353: .leq(
1354: instOf("tautRightSmaller"),
1355: opTerm(
1356: numbers
1357: .getArithAddition(),
1358: one,
1359: instOf("tautRightBigger"))) }));
1360:
1361: bindRuleSet(d, "inEqSimp_or_weaken", SumFeature
1362: .createSum(new Feature[] {
1363: applyTF("weakenLeft", tf.monomial),
1364: applyTF("weakenRightSmaller", tf.polynomial),
1365: applyTF("weakenRightBigger", tf.polynomial),
1366: PolynomialValuesCmpFeature.eq(opTerm(numbers
1367: .getArithAddition(), one,
1368: instOf("weakenRightSmaller")),
1369: instOf("weakenRightBigger")) }));
1370:
1371: bindRuleSet(d, "inEqSimp_or_antiSymm", SumFeature
1372: .createSum(new Feature[] {
1373: applyTF("antiSymmLeft", tf.monomial),
1374: applyTF("antiSymmRightSmaller", tf.polynomial),
1375: applyTF("antiSymmRightBigger", tf.polynomial),
1376: PolynomialValuesCmpFeature.eq(opTerm(numbers
1377: .getArithAddition(), two,
1378: instOf("antiSymmRightSmaller")),
1379: instOf("antiSymmRightBigger")) }));
1380:
1381: }
1382:
1383: private void setupMultiplyInequations(RuleSetDispatchFeature d,
1384: Feature notAllowedF) {
1385: final TermBuffer intRel = new TermBuffer();
1386:
1387: /* final Feature partiallyBounded =
1388: not ( sum ( intRel, SequentFormulasGenerator.sequent (),
1389: not ( add ( applyTF ( intRel, tf.intRelation ),
1390: InEquationMultFeature
1391: .partiallyBounded ( instOf ( "multLeft" ),
1392: instOf ( "multFacLeft" ),
1393: sub ( intRel, 0 ) ) ) ) ) ); */
1394:
1395: final Feature totallyBounded = not(sum(
1396: intRel,
1397: SequentFormulasGenerator.sequent(),
1398: not(add(applyTF(intRel, tf.intRelation),
1399: InEquationMultFeature.totallyBounded(
1400: instOf("multLeft"),
1401: instOf("multFacLeft"), sub(intRel, 0))))));
1402:
1403: final Feature exactlyBounded = not(sum(
1404: intRel,
1405: SequentFormulasGenerator.sequent(),
1406: not(add(applyTF(intRel, tf.intRelation),
1407: InEquationMultFeature.exactlyBounded(
1408: instOf("multLeft"),
1409: instOf("multFacLeft"), sub(intRel, 0))))));
1410:
1411: // this is a bit hackish
1412: //
1413: // really, one would need a possibility to express that the cost
1414: // computation for the rule application should be post-poned (and
1415: // repeated at a later point) if the product of the left sides does not
1416: // have any similarity with existing left sides
1417: // (<code>AllowInEquationMultiplication</code> returns false). We
1418: // simulate this by returning non-infinite costs here, but by declining
1419: // the rule application in <code>isApprovedApp</code>). This is not
1420: // perfect, because it is not possible to distinguish between the
1421: // re-cost-computation delay and the normal costs for a rule application
1422: bindRuleSet(
1423: d,
1424: "inEqSimp_nonLin_multiply",
1425: add(
1426: applyTF("multLeft", tf.nonNegMonomial),
1427: applyTF("multRight", tf.polynomial),
1428: ifZero(
1429: MatchedIfFeature.INSTANCE,
1430: SumFeature
1431: .createSum(new Feature[] {
1432: applyTF(
1433: "multFacLeft",
1434: tf.nonNegMonomial),
1435: ifZero(applyTF(
1436: "multRight",
1437: tf.literal),
1438: longConst(-100)),
1439: ifZero(
1440: applyTF(
1441: "multFacRight",
1442: tf.literal),
1443: longConst(-100),
1444: applyTF(
1445: "multFacRight",
1446: tf.polynomial)),
1447: /* ifZero ( applyTF ( "multRight", tf.literal ),
1448: longConst ( -100 ),
1449: applyTF ( "multRight", tf.polynomial ) ),
1450: ifZero ( applyTF ( "multFacRight", tf.literal ),
1451: longConst ( -100 ),
1452: applyTF ( "multFacRight", tf.polynomial ) ), */
1453: not(TermSmallerThanFeature
1454: .create(
1455: FocusProjection
1456: .create(0),
1457: AssumptionProjection
1458: .create(0))),
1459: ifZero(
1460: exactlyBounded,
1461: longConst(0),
1462: ifZero(
1463: totallyBounded,
1464: longConst(100),
1465: notAllowedF)),
1466: /* ifZero ( partiallyBounded,
1467: longConst ( 400 ),
1468: notAllowedF ) ) ), */
1469: /* applyTF ( "multLeft", rec ( tf.mulF, longTermConst ( 20 ) ) ),
1470: applyTF ( "multFacLeft", rec ( tf.mulF, longTermConst ( 20 ) ) ),
1471: applyTF ( "multRight", rec ( tf.addF, longTermConst ( 4 ) ) ),
1472: applyTF ( "multFacRight", rec ( tf.addF, longTermConst ( 4 ) ) ), */
1473: }), notAllowedF)));
1474: }
1475:
1476: private void setupInEqSimpInstantiation(RuleSetDispatchFeature d,
1477: Proof p_proof) {
1478: // category "handling of non-linear inequations"
1479:
1480: setupSquaresAreNonNegative(d);
1481:
1482: if (arithNonLinInferences())
1483: setupInEqCaseDistinctions(d, p_proof);
1484: }
1485:
1486: // For taclets that need instantiation, but where the instantiation is
1487: // deterministic and does not have to be repeated at a later point, we
1488: // setup the same feature terms as in the instantiation method. The
1489: // definitions in <code>setupInstantiationWithoutRetry</code> should
1490: // give cost infinity to those incomplete rule applications that will
1491: // never be instantiated (so that these applications can be removed from
1492: // the queue and do not have to be considered again).
1493: private void setupInEqSimpInstantiationWithoutRetry(
1494: RuleSetDispatchFeature d, Proof p_proof) {
1495: // category "direct inequations"
1496:
1497: setupPullOutGcd(d, "inEqSimp_pullOutGcd_leq", false);
1498: setupPullOutGcd(d, "inEqSimp_pullOutGcd_geq", true);
1499:
1500: // more efficient (but not confluent) versions for the antecedent
1501: bindRuleSet(d, "inEqSimp_pullOutGcd_antec", -10);
1502:
1503: // category "handling of non-linear inequations"
1504:
1505: final TermBuffer divisor = new TermBuffer();
1506: final TermBuffer dividend = new TermBuffer();
1507:
1508: bindRuleSet(
1509: d,
1510: "inEqSimp_nonLin_divide",
1511: SumFeature
1512: .createSum(new Feature[] {
1513: applyTF("divProd", tf.nonCoeffMonomial),
1514: applyTFNonStrict("divProdBoundNonPos",
1515: tf.nonPosLiteral),
1516: applyTFNonStrict("divProdBoundNonNeg",
1517: tf.nonNegLiteral),
1518: ifZero(
1519: MatchedIfFeature.INSTANCE,
1520: let(
1521: divisor,
1522: instOf("divX"),
1523: let(
1524: dividend,
1525: instOf("divProd"),
1526: SumFeature
1527: .createSum(new Feature[] {
1528: applyTF(
1529: divisor,
1530: tf.nonCoeffMonomial),
1531: not(eq(
1532: dividend,
1533: divisor)),
1534: applyTFNonStrict(
1535: "divXBoundPos",
1536: tf.posLiteral),
1537: applyTFNonStrict(
1538: "divXBoundNeg",
1539: tf.negLiteral),
1540: ReducibleMonomialsFeature
1541: .createReducible(
1542: dividend,
1543: divisor),
1544: instantiate(
1545: "divY",
1546: ReduceMonomialsProjection
1547: .create(
1548: dividend,
1549: divisor)) })))) }));
1550:
1551: setupNonLinTermIsPosNeg(d, "inEqSimp_nonLin_pos", true);
1552: setupNonLinTermIsPosNeg(d, "inEqSimp_nonLin_neg", false);
1553: }
1554:
1555: private void setupNonLinTermIsPosNeg(RuleSetDispatchFeature d,
1556: String ruleSet, boolean pos) {
1557: final TermBuffer divisor = new TermBuffer();
1558: final TermBuffer dividend = new TermBuffer();
1559: final TermBuffer quotient = new TermBuffer();
1560: final TermBuffer antecFor = new TermBuffer();
1561:
1562: bindRuleSet(
1563: d,
1564: ruleSet,
1565: SumFeature
1566: .createSum(new Feature[] {
1567: applyTF("divProd", tf.nonCoeffMonomial),
1568: applyTFNonStrict("divProdBoundPos",
1569: tf.posLiteral),
1570: applyTFNonStrict("divProdBoundNeg",
1571: tf.negLiteral),
1572: ifZero(
1573: MatchedIfFeature.INSTANCE,
1574: let(
1575: divisor,
1576: instOf("divX"),
1577: let(
1578: dividend,
1579: instOf("divProd"),
1580: SumFeature
1581: .createSum(new Feature[] {
1582: applyTF(
1583: divisor,
1584: tf.nonCoeffMonomial),
1585: not(applyTF(
1586: dividend,
1587: eq(divisor))),
1588: applyTFNonStrict(
1589: "divXBoundNonPos",
1590: tf.nonPosLiteral),
1591: applyTFNonStrict(
1592: "divXBoundNonNeg",
1593: tf.nonNegLiteral),
1594: ReducibleMonomialsFeature
1595: .createReducible(
1596: dividend,
1597: divisor),
1598: let(
1599: quotient,
1600: ReduceMonomialsProjection
1601: .create(
1602: dividend,
1603: divisor),
1604: add(
1605: sum(
1606: antecFor,
1607: SequentFormulasGenerator
1608: .antecedent(),
1609: not(applyTF(
1610: antecFor,
1611: pos ? opSub(
1612: tf.geq,
1613: eq(quotient),
1614: tf.posLiteral)
1615: : opSub(
1616: tf.leq,
1617: eq(quotient),
1618: tf.negLiteral)))),
1619: instantiate(
1620: "divY",
1621: quotient))) })))) }));
1622: }
1623:
1624: private void setupSquaresAreNonNegative(RuleSetDispatchFeature d) {
1625: final TermBuffer intRel = new TermBuffer();
1626: final TermBuffer product = new TermBuffer();
1627: final TermBuffer factor = new TermBuffer();
1628:
1629: final Feature productContainsSquare = applyTF(sub(product, 0),
1630: or(eq(factor), opSub(tf.mul, any(), eq(factor))));
1631: final Feature productIsProduct = applyTF(product, opSub(tf.mul,
1632: any(), not(tf.mulF)));
1633:
1634: bindRuleSet(d, "inEqSimp_nonNegSquares", forEach(intRel,
1635: SequentFormulasGenerator.sequent(), ifZero(applyTF(
1636: intRel, tf.intRelation), forEach(product,
1637: SubtermGenerator.leftTraverse(sub(intRel, 0),
1638: tf.mulF), ifZero(productIsProduct,
1639: let(factor, sub(product, 1),
1640: ifZero(productContainsSquare,
1641: instantiate(
1642: "squareFac",
1643: factor))))))));
1644: }
1645:
1646: private void setupInEqCaseDistinctions(RuleSetDispatchFeature d,
1647: Proof p_proof) {
1648: final TermBuffer intRel = new TermBuffer();
1649: final TermBuffer atom = new TermBuffer();
1650: final TermBuffer zero = new TermBuffer();
1651: zero.setContent(TermBuilder.DF
1652: .zTerm(p_proof.getServices(), "0"));
1653: final TermBuffer rootInf = new TermBuffer();
1654:
1655: final Feature posNegSplitting = forEach(
1656: intRel,
1657: SequentFormulasGenerator.antecedent(),
1658: add(
1659: applyTF(intRel, tf.intRelation),
1660: forEach(
1661: atom,
1662: SubtermGenerator.leftTraverse(sub(
1663: intRel, 0), tf.mulF),
1664: SumFeature
1665: .createSum(new Feature[] {
1666: applyTF(
1667: atom,
1668: add(
1669: tf.atom,
1670: not(tf.literal))),
1671: allowPosNegCaseDistinction(atom),
1672: instantiate(
1673: "signCasesLeft",
1674: atom),
1675: longConst(IN_EQ_SIMP_NON_LIN_COST + 200)
1676: // ,
1677: // applyTF ( atom, rec ( any (), longTermConst ( 5 ) ) )
1678: }))));
1679:
1680: bindRuleSet(d, "inEqSimp_signCases", posNegSplitting);
1681:
1682: final Feature strengthening = forEach(intRel,
1683: SequentFormulasGenerator.antecedent(),
1684: SumFeature.createSum(new Feature[] {
1685: applyTF(intRel, add(or(tf.geqF, tf.leqF), sub(
1686: tf.atom, tf.literal))),
1687: instantiate("cutFormula", opTerm(tf.eq, sub(
1688: intRel, 0), sub(intRel, 1))),
1689: longConst(IN_EQ_SIMP_NON_LIN_COST + 300)
1690: // ,
1691: // applyTF ( sub ( intRel, 0 ),
1692: // rec ( any (), longTermConst ( 5 ) ) )
1693: }));
1694:
1695: final Feature rootInferences = forEach(intRel,
1696: SequentFormulasGenerator.antecedent(), add(
1697: isRootInferenceProducer(intRel), forEach(
1698: rootInf, RootsGenerator.create(intRel),
1699: add(instantiate("cutFormula", rootInf),
1700: ifZero(applyTF(rootInf,
1701: op(Op.OR)),
1702: longConst(50)), ifZero(
1703: applyTF(rootInf,
1704: op(Op.AND)),
1705: longConst(20)))),
1706: longConst(IN_EQ_SIMP_NON_LIN_COST)));
1707:
1708: bindRuleSet(d, "cut", oneOf(new Feature[] { strengthening,
1709: rootInferences }));
1710: }
1711:
1712: private Feature isRootInferenceProducer(TermBuffer intRel) {
1713: return applyTF(intRel, add(tf.intRelation, sub(
1714: tf.nonCoeffMonomial, tf.literal)));
1715: }
1716:
1717: private Feature allowPosNegCaseDistinction(TermBuffer atom) {
1718: final TermBuffer antecFor = new TermBuffer();
1719: final TermFeature eqAtom = eq(atom);
1720:
1721: return add(not(succIntEquationExists()),
1722: sum(antecFor, SequentFormulasGenerator.antecedent(),
1723: not(applyTF(antecFor, or(opSub(tf.eq, eqAtom,
1724: any()), opSub(tf.leq, eqAtom,
1725: tf.negLiteral), opSub(tf.geq, eqAtom,
1726: tf.posLiteral))))));
1727: }
1728:
1729: private Feature allowInEqStrengthening(TermBuffer atom,
1730: TermBuffer literal) {
1731: final TermBuffer antecFor = new TermBuffer();
1732:
1733: return add(not(succIntEquationExists()), not(sum(antecFor,
1734: SequentFormulasGenerator.antecedent(), not(applyTF(
1735: antecFor, add(or(tf.leqF, tf.geqF), sub(
1736: eq(atom), eq(literal))))))));
1737: }
1738:
1739: private Feature succIntEquationExists() {
1740: final TermBuffer succFor = new TermBuffer();
1741:
1742: return not(sum(succFor, SequentFormulasGenerator.succedent(),
1743: not(applyTF(succFor, tf.intEquation))));
1744: }
1745:
1746: private void setupInEqCaseDistinctionsApproval(
1747: RuleSetDispatchFeature d) {
1748: final TermBuffer atom = new TermBuffer();
1749: final TermBuffer literal = new TermBuffer();
1750: final TermBuffer intRel = new TermBuffer();
1751: final TermBuffer rootInf = new TermBuffer();
1752:
1753: bindRuleSet(d, "inEqSimp_signCases", add(
1754: isInstantiated("signCasesLeft"), let(atom,
1755: instOf("signCasesLeft"),
1756: allowPosNegCaseDistinction(atom))));
1757:
1758: // this is somewhat ugly. we should introduce some concept of "tagging"
1759: // rule application so that they can be recognised again later
1760: bindRuleSet(
1761: d,
1762: "cut",
1763: add(
1764: isInstantiated("cutFormula"),
1765: or(
1766: not(sum(
1767: intRel,
1768: SequentFormulasGenerator
1769: .antecedent(),
1770: ifZero(
1771: isRootInferenceProducer(intRel),
1772: sum(
1773: rootInf,
1774: RootsGenerator
1775: .create(intRel),
1776: not(eq(
1777: instOf("cutFormula"),
1778: rootInf)))))),
1779: ifZero(
1780: applyTF("cutFormula", opSub(
1781: tf.eq, tf.atom,
1782: tf.literal)),
1783: let(
1784: atom,
1785: sub(
1786: instOf("cutFormula"),
1787: 0),
1788: let(
1789: literal,
1790: sub(
1791: instOf("cutFormula"),
1792: 1),
1793: allowInEqStrengthening(
1794: atom,
1795: literal)))))));
1796: }
1797:
1798: ////////////////////////////////////////////////////////////////////////////
1799: ////////////////////////////////////////////////////////////////////////////
1800: //
1801: // Axiomatisation and algorithms for further arithmetic operations:
1802: // division, modulus, modular Java operations
1803: //
1804: ////////////////////////////////////////////////////////////////////////////
1805: ////////////////////////////////////////////////////////////////////////////
1806:
1807: private void setupDefOpsPrimaryCategories(RuleSetDispatchFeature d) {
1808:
1809: if (arithDefOps()) {
1810: // the axiom defining division only has to be inserted once, because
1811: // it adds equations to the antecedent
1812: bindRuleSet(d, "defOps_div", SumFeature
1813: .createSum(new Feature[] {
1814: NonDuplicateAppModPositionFeature.INSTANCE,
1815: applyTF("divNum", tf.polynomial),
1816: applyTF("divDenom", tf.polynomial),
1817: applyTF("divNum", tf.notContainsDivMod),
1818: applyTF("divDenom", tf.notContainsDivMod),
1819: ifZero(isBelow(ff.modalOperator),
1820: longConst(200)) }));
1821:
1822: bindRuleSet(d, "defOps_jdiv", SumFeature
1823: .createSum(new Feature[] {
1824: NonDuplicateAppModPositionFeature.INSTANCE,
1825: applyTF("divNum", tf.polynomial),
1826: applyTF("divDenom", tf.polynomial),
1827: applyTF("divNum", tf.notContainsDivMod),
1828: applyTF("divDenom", tf.notContainsDivMod),
1829: ifZero(isBelow(ff.modalOperator),
1830: longConst(200)) }));
1831:
1832: bindRuleSet(d, "defOps_jdiv_inline", add(applyTF("divNum",
1833: tf.literal), applyTF("divDenom", tf.polynomial),
1834: longConst(-5000)));
1835:
1836: setupDefOpsExpandMod(d);
1837:
1838: bindRuleSet(d, "defOps_expandRanges", -5000);
1839: bindRuleSet(d, "defOps_expandJNumericOp", -500);
1840: bindRuleSet(d, "defOps_modHomoEq", -5000);
1841: } else {
1842: bindRuleSet(d, "defOps_div", inftyConst());
1843: bindRuleSet(d, "defOps_jdiv", inftyConst());
1844:
1845: bindRuleSet(d, "defOps_jdiv_inline", add(applyTF("divNum",
1846: tf.literal), applyTF("divDenom", tf.literal),
1847: longConst(-4000)));
1848:
1849: bindRuleSet(d, "defOps_mod", add(applyTF("divNum",
1850: tf.literal), applyTF("divDenom", tf.literal),
1851: longConst(-4000)));
1852:
1853: bindRuleSet(d, "defOps_expandRanges", inftyConst());
1854: bindRuleSet(d, "defOps_expandJNumericOp", inftyConst());
1855: bindRuleSet(d, "defOps_modHomoEq", inftyConst());
1856: }
1857:
1858: }
1859:
1860: private void setupDefOpsExpandMod(RuleSetDispatchFeature d) {
1861: final TermBuffer super Term = new TermBuffer();
1862:
1863: final Feature subsumedModulus = add(applyTF(super Term, sub(
1864: opSub(tf.mod, any(), tf.literal), tf.zeroLiteral)),
1865: PolynomialValuesCmpFeature.divides(instOf("divDenom"),
1866: sub(sub(super Term, 0), 1)));
1867:
1868: final Feature exSubsumedModulus = add(applyTF("divDenom",
1869: tf.literal), not(sum(super Term, SuperTermGenerator
1870: .upwardsWithIndex(sub(or(tf.addF, tf.mulF), any())),
1871: not(subsumedModulus))));
1872:
1873: bindRuleSet(d, "defOps_mod", ifZero(add(applyTF("divNum",
1874: tf.literal), applyTF("divDenom", tf.literal)),
1875: longConst(-4000), SumFeature.createSum(new Feature[] {
1876: applyTF("divNum", tf.polynomial),
1877: applyTF("divDenom", tf.polynomial),
1878: ifZero(isBelow(ff.modalOperator),
1879: exSubsumedModulus, or(add(
1880: applyTF("divNum",
1881: tf.notContainsDivMod),
1882: applyTF("divDenom",
1883: tf.notContainsDivMod)),
1884: exSubsumedModulus)),
1885: longConst(-3500) })));
1886: }
1887:
1888: private Feature isBelow(TermFeature t) {
1889: final TermBuffer super Term = new TermBuffer();
1890: return not(sum(super Term, SuperTermGenerator.upwards(any()),
1891: not(applyTF(super Term, t))));
1892: }
1893:
1894: private void setupDivModDivision(RuleSetDispatchFeature d) {
1895:
1896: final TermBuffer denomLC = new TermBuffer();
1897: final TermBuffer numTerm = new TermBuffer();
1898: final TermBuffer divCoeff = new TermBuffer();
1899:
1900: // exact polynomial division
1901:
1902: final Feature checkNumTerm = ifZero(add(not(applyTF(numTerm,
1903: tf.addF)), ReducibleMonomialsFeature.createReducible(
1904: numTerm, denomLC)), add(instantiate("polyDivCoeff",
1905: ReduceMonomialsProjection.create(numTerm, denomLC)),
1906: inftyConst()));
1907:
1908: final Feature isReduciblePoly = sum(numTerm, SubtermGenerator
1909: .rightTraverse(instOf("divNum"), tf.addF), checkNumTerm);
1910:
1911: // polynomial division modulo equations of the antecedent
1912:
1913: final Feature checkCoeffE = ifZero(contains(divCoeff,
1914: FocusProjection.create(0)),
1915: // do not apply if the result contains the original term
1916: longConst(0), add(
1917: instantiate("polyDivCoeff", divCoeff),
1918: inftyConst()));
1919:
1920: final Feature isReduciblePolyE = sum(numTerm, SubtermGenerator
1921: .rightTraverse(instOf("divNum"), tf.addF), ifZero(
1922: applyTF(numTerm, tf.addF), longConst(0), sum(divCoeff,
1923: MultiplesModEquationsGenerator.create(numTerm,
1924: denomLC), checkCoeffE)));
1925:
1926: bindRuleSet(
1927: d,
1928: "defOps_divModPullOut",
1929: SumFeature
1930: .createSum(new Feature[] {
1931: not(add(applyTF("divNum", tf.literal),
1932: applyTF("divDenom", tf.literal))),
1933: applyTF("divNum", tf.polynomial),
1934: applyTF("divDenom", tf.polynomial),
1935: ifZero(
1936: applyTF("divDenom", tf.addF),
1937: let(denomLC, sub(
1938: instOf("divDenom"), 1),
1939: not(isReduciblePoly)),
1940: let(
1941: denomLC,
1942: instOf("divDenom"),
1943: ifZero(
1944: isReduciblePoly,
1945: // no possible division has been found so far
1946: add(
1947: NotInScopeOfModalityFeature.INSTANCE,
1948: ifZero(
1949: isReduciblePolyE,
1950: // try again later
1951: longConst(-POLY_DIVISION_COST)))))),
1952: longConst(100) }));
1953:
1954: }
1955:
1956: ////////////////////////////////////////////////////////////////////////////
1957: ////////////////////////////////////////////////////////////////////////////
1958: //
1959: // Feature terms that handle the approval of complete taclet applications
1960: //
1961: ////////////////////////////////////////////////////////////////////////////
1962: ////////////////////////////////////////////////////////////////////////////
1963:
1964: private Feature setupApprovalF(Proof p_proof) {
1965: return add(NonDuplicateAppFeature.INSTANCE,
1966: UCIncompatibleFeature.create(p_proof));
1967: }
1968:
1969: private RuleSetDispatchFeature setupApprovalDispatcher(Proof p_proof) {
1970: final RuleSetDispatchFeature d = RuleSetDispatchFeature
1971: .create();
1972:
1973: final IntegerLDT numbers = p_proof.getServices()
1974: .getTypeConverter().getIntegerLDT();
1975:
1976: if (arithNonLinInferences())
1977: setupMultiplyInequations(d, inftyConst());
1978:
1979: // these taclets are not supposed to be applied with metavariable
1980: // instantiations
1981: bindRuleSet(d, "inEqSimp_pullOutGcd", isInstantiated("elimGcd"));
1982: bindRuleSet(d, "polySimp_pullOutGcd", isInstantiated("elimGcd"));
1983:
1984: bindRuleSet(d, "inEqSimp_nonNegSquares",
1985: isInstantiated("squareFac"));
1986: bindRuleSet(d, "inEqSimp_nonLin_divide", isInstantiated("divY"));
1987: bindRuleSet(d, "inEqSimp_nonLin_pos", isInstantiated("divY"));
1988: bindRuleSet(d, "inEqSimp_nonLin_neg", isInstantiated("divY"));
1989:
1990: bindRuleSet(d, "inEqSimp_signCases",
1991: isInstantiated("signCasesLeft"));
1992:
1993: setupNewSymApproval(d, numbers);
1994:
1995: bindRuleSet(d, "defOps_div",
1996: NonDuplicateAppModPositionFeature.INSTANCE);
1997: bindRuleSet(d, "defOps_jdiv",
1998: NonDuplicateAppModPositionFeature.INSTANCE);
1999:
2000: if (arithNonLinInferences())
2001: setupInEqCaseDistinctionsApproval(d);
2002:
2003: bindRuleSet(d, "inReachableStateImplication",
2004: NonDuplicateAppModPositionFeature.INSTANCE);
2005:
2006: setupQuantifierInstantiationApproval(d);
2007: setupSplittingApproval(d);
2008:
2009: return d;
2010: }
2011:
2012: ////////////////////////////////////////////////////////////////////////////
2013: ////////////////////////////////////////////////////////////////////////////
2014: //
2015: // Feature terms that handle the instantiation of incomplete taclet
2016: // applications
2017: //
2018: ////////////////////////////////////////////////////////////////////////////
2019: ////////////////////////////////////////////////////////////////////////////
2020:
2021: private RuleSetDispatchFeature setupInstantiationF(Proof p_proof) {
2022: enableInstantiate();
2023:
2024: final RuleSetDispatchFeature d = RuleSetDispatchFeature
2025: .create();
2026:
2027: setupQuantifierInstantiation(d);
2028:
2029: setupArithPrimaryCategories(d);
2030: setupDefOpsPrimaryCategories(d);
2031:
2032: setupInstantiationWithoutRetry(d, p_proof);
2033:
2034: setupInEqSimpInstantiation(d, p_proof);
2035:
2036: disableInstantiate();
2037: return d;
2038: }
2039:
2040: /**
2041: * For taclets that need instantiation, but where the instantiation is
2042: * deterministic and does not have to be repeated at a later point, we setup
2043: * the same feature terms both in the cost computation method and in the
2044: * instantiation method. The definitions in
2045: * <code>setupInstantiationWithoutRetry</code> should give cost infinity
2046: * to those incomplete rule applications that will never be instantiated (so
2047: * that these applications can be removed from the queue and do not have to
2048: * be considered again).
2049: */
2050: private void setupInstantiationWithoutRetry(
2051: RuleSetDispatchFeature d, Proof p_proof) {
2052: setupPolySimpInstantiationWithoutRetry(d, p_proof);
2053: setupInEqSimpInstantiationWithoutRetry(d, p_proof);
2054: }
2055:
2056: public Name name() {
2057: return new Name("JavaCardDLStrategy");
2058: }
2059:
2060: /**
2061: * Evaluate the cost of a <code>RuleApp</code>.
2062: *
2063: * @return the cost of the rule application expressed as a
2064: * <code>RuleAppCost</code> object.
2065: * <code>TopRuleAppCost.INSTANCE</code> indicates that the rule
2066: * shall not be applied at all (it is discarded by the strategy).
2067: */
2068: public final RuleAppCost computeCost(RuleApp app,
2069: PosInOccurrence pio, Goal goal) {
2070: return costComputationF.compute(app, pio, goal);
2071: }
2072:
2073: /**
2074: * Re-Evaluate a <code>RuleApp</code>. This method is called immediately
2075: * before a rule is really applied
2076: *
2077: * @return true iff the rule should be applied, false otherwise
2078: */
2079: public final boolean isApprovedApp(RuleApp app,
2080: PosInOccurrence pio, Goal goal) {
2081: return !(approvalF.compute(app, pio, goal) instanceof TopRuleAppCost);
2082: }
2083:
2084: protected final RuleAppCost instantiateApp(RuleApp app,
2085: PosInOccurrence pio, Goal goal) {
2086: return instantiationF.compute(app, pio, goal);
2087: }
2088:
2089: public static class Factory extends StrategyFactory {
2090: public Factory() {
2091: }
2092:
2093: public Strategy create(Proof p_proof,
2094: StrategyProperties strategyProperties) {
2095: return new JavaCardDLStrategy(p_proof, strategyProperties);
2096: }
2097:
2098: public Name name() {
2099: return new Name("JavaCardDLStrategy");
2100: }
2101: }
2102:
2103: ////////////////////////////////////////////////////////////////////////////
2104: ////////////////////////////////////////////////////////////////////////////
2105: //
2106: // Termfeatures: characterisations of terms and formulas
2107: //
2108: ////////////////////////////////////////////////////////////////////////////
2109: ////////////////////////////////////////////////////////////////////////////
2110:
2111: private final ArithTermFeatures tf;
2112: private final FormulaTermFeatures ff;
2113:
2114: private class ArithTermFeatures {
2115:
2116: public ArithTermFeatures(IntegerLDT numbers) {
2117: Z = numbers.getNumberSymbol();
2118:
2119: add = numbers.getArithAddition();
2120: mul = numbers.getArithMultiplication();
2121: mod = numbers.getArithModulo();
2122: div = numbers.getArithDivision();
2123: jmod = numbers.getJModulo();
2124: jdiv = numbers.getJDivision();
2125:
2126: eq = Op.EQUALS;
2127: leq = numbers.getLessOrEquals();
2128: geq = numbers.getGreaterOrEquals();
2129:
2130: intS = numbers.getNumberSymbol().sort();
2131:
2132: intF = extendsTrans(intS);
2133:
2134: addF = op(add);
2135: mulF = op(mul);
2136: modF = op(mod);
2137: divF = op(div);
2138: jmodF = op(jmod);
2139: jdivF = op(jdiv);
2140:
2141: eqF = op(eq);
2142: geqF = op(geq);
2143: leqF = op(leq);
2144:
2145: literal = op(Z);
2146: negLiteral = opSub(Z, op(numbers.getNegativeNumberSign()));
2147: nonNegLiteral = opSub(Z, not(op(numbers
2148: .getNegativeNumberSign())));
2149: zeroLiteral = opSub(Z, opSub(
2150: numbers.getNumberLiteralFor(0), op(numbers
2151: .getNumberTerminator())));
2152: oneLiteral = opSub(Z, opSub(numbers.getNumberLiteralFor(1),
2153: op(numbers.getNumberTerminator())));
2154: nonPosLiteral = or(zeroLiteral, negLiteral);
2155: posLiteral = add(nonNegLiteral, not(zeroLiteral));
2156: atLeastTwoLiteral = add(posLiteral, not(oneLiteral));
2157:
2158: atom = add(not(addF), not(mulF));
2159: linearMonomial = or(atom, opSub(mul, atom, literal));
2160:
2161: // left-associatively arranged monomials, literals are only allowed
2162: // as right-most term
2163: monomial = or(atom, opSub(mul, rec(mulF, or(opSub(mul,
2164: any(), not(mulF)), add(not(addF), not(literal)))),
2165: atom));
2166:
2167: // left-associatively arranged polynomials
2168: polynomial = rec(addF, or(opSub(add, any(), not(addF)),
2169: monomial));
2170:
2171: nonNegMonomial = add(monomial, or(not(mulF), sub(any(),
2172: not(negLiteral))));
2173: posMonomial = opSub(mul, monomial, posLiteral);
2174: negMonomial = opSub(mul, monomial, negLiteral);
2175: nonCoeffMonomial = add(monomial, or(not(mulF), sub(any(),
2176: not(literal))));
2177: nonNegOrNonCoeffMonomial = add(monomial, or(not(mulF), sub(
2178: any(), not(negLiteral))));
2179: atLeastTwoCoeffMonomial = opSub(mul, monomial,
2180: atLeastTwoLiteral);
2181:
2182: intEquation = opSub(eq, add(intF, nonNegMonomial), add(
2183: intF, polynomial));
2184: linearEquation = opSub(eq, linearMonomial, add(intF,
2185: polynomial));
2186: monomialEquation = opSub(eq, add(intF, nonNegMonomial),
2187: add(intF, monomial));
2188: intInEquation = add(or(leqF, geqF), sub(nonNegMonomial,
2189: polynomial));
2190: linearInEquation = add(or(leqF, geqF), sub(linearMonomial,
2191: polynomial));
2192: intRelation = add(or(leqF, geqF, eqF), sub(add(intF,
2193: nonNegMonomial), polynomial));
2194:
2195: notContainsProduct = rec(any(), ifZero(mulF, not(sub(
2196: not(literal), not(literal)))));
2197: notContainsDivMod = rec(any(), add(
2198: add(not(divF), not(modF)), add(not(jdivF),
2199: not(jmodF))));
2200: }
2201:
2202: final Sort intS;
2203:
2204: final Function Z;
2205: final Function add;
2206: final Function mul;
2207: final Function mod;
2208: final Function div;
2209: final Function jmod;
2210: final Function jdiv;
2211:
2212: final Operator eq;
2213: final Function leq;
2214: final Function geq;
2215:
2216: final TermFeature intF;
2217:
2218: final TermFeature addF;
2219: final TermFeature mulF;
2220: final TermFeature modF;
2221: final TermFeature divF;
2222: final TermFeature jmodF;
2223: final TermFeature jdivF;
2224:
2225: final TermFeature eqF;
2226: final TermFeature leqF;
2227: final TermFeature geqF;
2228:
2229: final TermFeature atom;
2230: final TermFeature linearMonomial;
2231:
2232: // left-associatively arranged monomials
2233: final TermFeature monomial;
2234: // left-associatively arranged polynomials
2235: final TermFeature polynomial;
2236:
2237: final TermFeature literal;
2238: final TermFeature posLiteral;
2239: final TermFeature negLiteral;
2240: final TermFeature nonNegLiteral;
2241: final TermFeature nonPosLiteral;
2242: final TermFeature zeroLiteral;
2243: final TermFeature oneLiteral;
2244: final TermFeature atLeastTwoLiteral;
2245:
2246: final TermFeature nonNegMonomial;
2247: final TermFeature posMonomial;
2248: final TermFeature negMonomial;
2249: final TermFeature nonCoeffMonomial;
2250: final TermFeature nonNegOrNonCoeffMonomial;
2251: final TermFeature atLeastTwoCoeffMonomial;
2252:
2253: final TermFeature intEquation;
2254: final TermFeature linearEquation;
2255: final TermFeature monomialEquation;
2256: final TermFeature intInEquation;
2257: final TermFeature linearInEquation;
2258: final TermFeature intRelation;
2259:
2260: final TermFeature notContainsProduct;
2261: final TermFeature notContainsDivMod;
2262: }
2263:
2264: private class FormulaTermFeatures {
2265:
2266: public FormulaTermFeatures() {
2267: forF = extendsTrans(Sort.FORMULA);
2268:
2269: orF = op(Op.OR);
2270: andF = op(Op.AND);
2271: impF = op(Op.IMP);
2272: notF = op(Op.NOT);
2273: ifThenElse = OperatorClassTF.create(IfThenElse.class);
2274:
2275: query = OperatorClassTF.create(ProgramMethod.class);
2276:
2277: atom = AtomTermFeature.INSTANCE;
2278: propJunctor = or(OperatorClassTF.create(Junctor.class),
2279: op(Op.EQV));
2280: literal = or(atom, opSub(Op.NOT, atom));
2281:
2282: // left-associatively arranged clauses
2283: clause = rec(orF,
2284: or(opSub(Op.OR, any(), not(orF)), literal));
2285:
2286: // left-associatively arranged sets of clauses
2287: clauseSet = rec(andF, or(opSub(Op.AND, any(), not(andF)),
2288: clause));
2289:
2290: quantifiedFor = or(op(Op.ALL), op(Op.EX));
2291: quantifiedClauseSet = rec(quantifiedFor, or(quantifiedFor,
2292: clauseSet));
2293:
2294: quantifiedAnd = rec(quantifiedFor, or(quantifiedFor, andF));
2295: quantifiedOr = rec(quantifiedFor, or(quantifiedFor, orF));
2296:
2297: // conjunction or disjunction of literals, without and-or alternation
2298: pureLitConjDisj = or(rec(andF, or(andF, literal)), rec(orF,
2299: or(orF, literal)));
2300: quantifiedPureLitConjDisj = rec(quantifiedFor, or(
2301: quantifiedFor, pureLitConjDisj));
2302:
2303: update = OperatorClassTF.create(IUpdateOperator.class);
2304: program = OperatorClassTF.create(Modality.class);
2305: modalOperator = or(update, program);
2306:
2307: // directCutAllowed = add ( atom, not ( modalOperator ) );
2308: notExecutable = expandQueries() ? add(not(program),
2309: not(query)) : not(program);
2310: notContainsExecutable = rec(any(), notExecutable);
2311:
2312: cutAllowed = add(notContainsExecutable,
2313: tf.notContainsProduct, or(tf.eqF, OperatorClassTF
2314: .create(TermSymbol.class)));
2315: cutAllowedBelowQuantifier = add(not(propJunctor),
2316: notContainsExecutable);
2317: cutPriority = add(ifZero(tf.intInEquation,
2318: longTermConst(0), ifZero(tf.eqF,
2319: longTermConst(100), longTermConst(200))),
2320: rec(any(), longTermConst(1)));
2321: // directCutAllowed = add ( tf.intInEquation, notContainsQuery );
2322: }
2323:
2324: final TermFeature forF;
2325:
2326: final TermFeature orF;
2327: final TermFeature andF;
2328: final TermFeature impF;
2329: final TermFeature notF;
2330: final TermFeature propJunctor;
2331: final TermFeature ifThenElse;
2332: final TermFeature query;
2333: final TermFeature notExecutable;
2334: final TermFeature notContainsExecutable;
2335:
2336: final TermFeature quantifiedFor;
2337: final TermFeature quantifiedOr;
2338: final TermFeature quantifiedAnd;
2339:
2340: final TermFeature atom;
2341: final TermFeature literal;
2342: final TermFeature clause;
2343: final TermFeature clauseSet;
2344: final TermFeature quantifiedClauseSet;
2345:
2346: final TermFeature pureLitConjDisj;
2347: final TermFeature quantifiedPureLitConjDisj;
2348:
2349: final TermFeature update;
2350: final TermFeature program;
2351: final TermFeature modalOperator;
2352:
2353: final TermFeature cutAllowed;
2354: final TermFeature cutAllowedBelowQuantifier;
2355: final TermFeature cutPriority;
2356: }
2357: }
|