public class PredictCostProver
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private class |
PredictCostProver.Clause
A sat() procedure with back searching
|
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<Term> |
assertLiterals
assume that all literal in
assertLiterals are true |
private java.util.Set<PredictCostProver.Clause> |
clauses
clauses from
instance of CNF |
private Term |
falseT |
private Services |
services |
private TermBuilder |
tb |
private Term |
trueT |
Modifier | Constructor and Description |
---|---|
private |
PredictCostProver(Term instance,
ImmutableSet<Term> assertList,
Services services) |
Modifier and Type | Method and Description |
---|---|
static long |
computerInstanceCost(Substitution sub,
Term matrix,
ImmutableSet<Term> assertList,
Services services) |
private long |
cost()
do two step refinement and return the cost
|
private ImmutableSet<ImmutableSet<Term>> |
createClause(ImmutableSet<Term> set) |
private ImmutableSet<ImmutableSet<Term>> |
createClauseHelper(ImmutableSet<ImmutableSet<Term>> res,
Term self,
ImmutableSet<Term> ts) |
private Term |
directConsequenceOrContradictionOfAxiom(Term problem,
Term axiom) |
private long |
firstRefine()
refine every clause, by assume assertList are true and if a clause's cost
is 0 which means it is refined to false, then cost 0 returned.
|
private void |
initClauses(Term instance) |
private Term |
provedByAnother(Term problem,
Term axiom) |
private Term |
provedBySelf(Term problem)
If the given
problem 's operation is equal,or mathmetic
operation(=,>=, <=), this method will try to prove it by finding the
relation between its two subterms. |
private Term |
proveLiteral(Term problem,
java.lang.Iterable<? extends Term> assertLits)
try to prove
problem by know assertLits |
private final TermBuilder tb
private final Term trueT
private final Term falseT
private ImmutableSet<Term> assertLiterals
assertLiterals
are trueprivate java.util.Set<PredictCostProver.Clause> clauses
instance
of CNFprivate final Services services
private PredictCostProver(Term instance, ImmutableSet<Term> assertList, Services services)
public static long computerInstanceCost(Substitution sub, Term matrix, ImmutableSet<Term> assertList, Services services)
private void initClauses(Term instance)
private ImmutableSet<ImmutableSet<Term>> createClause(ImmutableSet<Term> set)
private ImmutableSet<ImmutableSet<Term>> createClauseHelper(ImmutableSet<ImmutableSet<Term>> res, Term self, ImmutableSet<Term> ts)
private Term provedBySelf(Term problem)
problem
's operation is equal,or mathmetic
operation(=,>=, <=), this method will try to prove it by finding the
relation between its two subterms.private Term directConsequenceOrContradictionOfAxiom(Term problem, Term axiom)
private Term provedByAnother(Term problem, Term axiom)
problem
- axiom
- private Term proveLiteral(Term problem, java.lang.Iterable<? extends Term> assertLits)
problem
by know assertLits
problem
- a literal to be provedassertLits
- a set of term assertLiterals in which all literals are truetrueT
if if formu is proved to true,
falseT
if false, and atom
if it cann't
be proved.private long cost()
private long firstRefine()