| java.lang.Object
 de.uka.ilkd.key.strategy.quantifierHeuristics.HandleArith
| HandleArith | | class HandleArith (Code) | | 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;
|
| provedArithEqual | | public static Term provedArithEqual(Term problem, Services services)(Code) | |
Parameters:
problem - true if atom.sub(0) is euqual to atom.sub(1), false if notequal, else return atom |
| provedByArith | | public static Term provedByArith(Term problem, Services services)(Code) | | try to prove atom by using polynomial
Parameters:
problem - trueT if if formu is proved to true,falseT if false, and problem if itcann't be proved. |
| provedByArith | | public static Term provedByArith(Term problem, Term axiom, Services services)(Code) | | 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 -
Parameters:
axiom - trueT if true, falseT if false, and atom if can't be prove; |
|
|