de.uka.ilkd.key.strategy.quantifierHeuristics

Class ClausesSmallerThanFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

de.uka.ilkd.key.strategy.feature.SmallerThanFeature

de.uka.ilkd.key.strategy.quantifierHeuristics.ClausesSmallerThanFeature

All Implemented Interfaces:

Feature

public class ClausesSmallerThanFeature
extends SmallerThanFeature

Ordering used to sort the clauses in a quantified formula. This ordering should only be applied if at least one of the two clauses contains more than one literal (otherwise, use LiteralsSmallerThanFeature).

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	ClausesSmallerThanFeature.ClauseCollector

Nested classes/interfaces inherited from class de.uka.ilkd.key.strategy.feature.SmallerThanFeature

SmallerThanFeature.Collector

Field Summary

Fields

Modifier and Type	Field and Description
private ProjectionToTerm	left
private LiteralsSmallerThanFeature	litComparator
private QuanEliminationAnalyser	quanAnalyser
private ProjectionToTerm	right

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ClausesSmallerThanFeature(ProjectionToTerm left, ProjectionToTerm right, IntegerLDT numbers)

Method Summary

Modifier and Type	Method and Description
static Feature	create(ProjectionToTerm left, ProjectionToTerm right, IntegerLDT numbers)
protected boolean	filter(TacletApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
protected boolean	lessThan(Term t1, Term t2, PosInOccurrence focus, Goal goal) this overwrites the method of SmallerThanFeature

Methods inherited from class de.uka.ilkd.key.strategy.feature.SmallerThanFeature

compare, lessThan

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

filter

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

left

private final ProjectionToTerm left

right

private final ProjectionToTerm right

quanAnalyser

private final QuanEliminationAnalyser quanAnalyser

litComparator

private final LiteralsSmallerThanFeature litComparator

Constructor Detail

ClausesSmallerThanFeature

private ClausesSmallerThanFeature(ProjectionToTerm left,
                                  ProjectionToTerm right,
                                  IntegerLDT numbers)

Method Detail

create

public static Feature create(ProjectionToTerm left,
                             ProjectionToTerm right,
                             IntegerLDT numbers)

filter

protected boolean filter(TacletApp app,
                         PosInOccurrence pos,
                         Goal goal)

Description copied from class: BinaryTacletAppFeature

Compute whether the result of the feature is zero (true) or infinity (false)

Specified by:

filter in class BinaryTacletAppFeature

Parameters:

app - the TacletApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

true iff the the result of the feature is supposed to be zero.

lessThan

protected boolean lessThan(Term t1,
                           Term t2,
                           PosInOccurrence focus,
                           Goal goal)

this overwrites the method of SmallerThanFeature

Overrides:

lessThan in class SmallerThanFeature