public class HandleArith
extends java.lang.Object
Modifier | Constructor and Description |
---|---|
private |
HandleArith() |
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) |
public static Term provedByArith(Term problem, Services services)
problem
- trueT
if if formu is proved to true,
falseT
if false, and problem
if it
cann't be proved.private static void putInTermCache(LRUCache<Term,Term> provedByArithCache, Term key, Term value)
private static Term provedArithEqual(Term problem, TermBuilder tb, Services services)
problem
- public static Term provedByArith(Term problem, Term axiom, Services services)
problem
- axiom
- private static Term formatArithTerm(Term problem, TermBuilder tb, IntegerLDT ig, ServiceCaches caches)
problem
- term
's operator is not >= or <=