de.uka.ilkd.key.strategy.quantifierHeuristics

Class HandleArith

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.HandleArith

public class HandleArith
extends java.lang.Object

This class is used to prove some simple arithmetic problem which are a==b, a>=b, a<=b; Besides it can be used to prove that a>=b or a<=b by knowing that c>=d or c<=d;

Constructor Summary

Constructors

Modifier	Constructor and Description
private	HandleArith()

Method Summary

Modifier and Type	Method and Description
private static Term	formatArithTerm(Term problem, TermBuilder tb, IntegerLDT ig, ServiceCaches caches) Format literal to a form of "geq",linke a>=b;For example, a <=b to b>=a;a>b to a>=b+1;!
private static Term	provedArithEqual(Term problem, TermBuilder tb, Services services)
static Term	provedByArith(Term problem, Services services) try to prove atom by using polynomial
static Term	provedByArith(Term problem, Term axiom, Services services) Try to prove problem by know that axiom is true.
private static void	putInTermCache(LRUCache<Term,Term> provedByArithCache, Term key, Term value)

Methods inherited from class java.lang.Object

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

Constructor Detail

HandleArith

private HandleArith()

Method Detail

provedByArith

public static Term provedByArith(Term problem,
                                 Services services)

try to prove atom by using polynomial

Parameters:

problem -

Returns:

trueT if if formu is proved to true, falseT if false, and problem if it cann't be proved.

putInTermCache

private static void putInTermCache(LRUCache<Term,Term> provedByArithCache,
                                   Term key,
                                   Term value)

provedArithEqual

private static Term provedArithEqual(Term problem,
                                     TermBuilder tb,
                                     Services services)

Parameters:

problem -

Returns:

true if atom.sub(0) is euqual to atom.sub(1), false if not equal, else return atom

provedByArith

public static Term provedByArith(Term problem,
                                 Term axiom,
                                 Services services)

Try to prove problem by know that axiom is true. The idea is that we know a>=b(axiom),we want to prove c>=d(problem). It is enough to prove that c+b>=a+d which means c>=d is true. or we prove that !(c>=d) which is d>=c+1 is true. This means c>= d is false;

Parameters:

problem -

axiom -

Returns:

trueT if true, falseT if false, and atom if can't be prove;

formatArithTerm

private static Term formatArithTerm(Term problem,
                                    TermBuilder tb,
                                    IntegerLDT ig,
                                    ServiceCaches caches)

Format literal to a form of "geq",linke a>=b;For example, a <=b to b>=a;a>b to a>=b+1;!(a>=b) to b>=a+1..

Parameters:

problem -

Returns:

falseT if term's operator is not >= or <=