de.uka.ilkd.key.strategy.quantifierHeuristics

Class PredictCostProver.Clause

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.PredictCostProver.Clause

All Implemented Interfaces:

java.lang.Iterable<Term>

Enclosing class:

PredictCostProver

private class PredictCostProver.Clause
extends java.lang.Object
implements java.lang.Iterable<Term>

A sat() procedure with back searching

Field Summary

Fields

Modifier and Type	Field and Description
ImmutableSet<Term>	literals all literals contains in this clause

Constructor Summary

Constructors

Constructor and Description
Clause(ImmutableSet<Term> lits)

Method Summary

Modifier and Type	Method and Description
long	cost()
boolean	equals(java.lang.Object o)
void	firstRefine() Refine this clause in two process, first try to refined by itself, @see selfRefine.
int	hashCode()
java.util.Iterator<Term>	iterator()
ImmutableSet<Term>	refine(java.lang.Iterable<? extends Term> assertLits) Refine literals in this clause, but it does not change literlas, only return literals that can't be removed by refining
boolean	selfRefine(ImmutableSet<Term> lits) This method is used for detect where a clause can be simply refined to to true.
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

literals

public ImmutableSet<Term> literals

all literals contains in this clause

Constructor Detail

Clause

public Clause(ImmutableSet<Term> lits)

Method Detail

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

iterator

public java.util.Iterator<Term> iterator()

Specified by:

iterator in interface java.lang.Iterable<Term>

cost

public long cost()

Returns:

0 if this clause is refine to false. 1 if true. Otherwise,return the number of literals it left.

firstRefine

public void firstRefine()

Refine this clause in two process, first try to refined by itself, @see selfRefine. Second refine this clause by assuming assertLiteras are true

refine

public ImmutableSet<Term> refine(java.lang.Iterable<? extends Term> assertLits)

Refine literals in this clause, but it does not change literlas, only return literals that can't be removed by refining

selfRefine

public boolean selfRefine(ImmutableSet<Term> lits)

This method is used for detect where a clause can be simply refined to to true. And it is implemented like this. Assume that the clause contains two literals Li and Lj. If (!Li->Lj) which is acturally (Li|Lj), is true, and the clasue is true. provedByAnthoer(Lj,!Li) is used to proved (!Li->Lj). Some examples are (!a|a) which is (!!a->a) and (a>=1|a<=0) which is !a>=1->a<=0

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object