de.uka.ilkd.key.strategy.quantifierHeuristics

Class PredictCostProver

java.lang.Object

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

public class PredictCostProver
extends java.lang.Object

TODO: rewrite, this seems pretty inefficient ...

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	PredictCostProver.Clause A sat() procedure with back searching

Field Summary

Fields

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

Constructor Summary

Constructors

Modifier	Constructor and Description
private	PredictCostProver(Term instance, ImmutableSet<Term> assertList, Services services)

Method Summary

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

Methods inherited from class java.lang.Object

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

Field Detail

tb

private final TermBuilder tb

trueT

private final Term trueT

falseT

private final Term falseT

assertLiterals

private ImmutableSet<Term> assertLiterals

assume that all literal in assertLiterals are true

clauses

private java.util.Set<PredictCostProver.Clause> clauses

clauses from instance of CNF

services

private final Services services

Constructor Detail

PredictCostProver

private PredictCostProver(Term instance,
                          ImmutableSet<Term> assertList,
                          Services services)

Method Detail

computerInstanceCost

public static long computerInstanceCost(Substitution sub,
                                        Term matrix,
                                        ImmutableSet<Term> assertList,
                                        Services services)

initClauses

private void initClauses(Term instance)

createClause

private ImmutableSet<ImmutableSet<Term>> createClause(ImmutableSet<Term> set)

createClauseHelper

private ImmutableSet<ImmutableSet<Term>> createClauseHelper(ImmutableSet<ImmutableSet<Term>> res,
                                                            Term self,
                                                            ImmutableSet<Term> ts)

provedBySelf

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.

directConsequenceOrContradictionOfAxiom

private Term directConsequenceOrContradictionOfAxiom(Term problem,
                                                     Term axiom)

Returns:

trueT if problem is equal axiom, false if problem's negation is equal axiom. Otherwise retrun problem.

provedByAnother

private Term provedByAnother(Term problem,
                             Term axiom)

Parameters:

problem -

axiom -

Returns:

if axiom conduct problem then return trueT. If axiom conduct negation of problem return fastT. Otherwise, return problem

proveLiteral

private Term proveLiteral(Term problem,
                          java.lang.Iterable<? extends Term> assertLits)

try to prove problem by know assertLits

Parameters:

problem - a literal to be proved

assertLits - a set of term assertLiterals in which all literals are true

Returns:

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

cost

private long cost()

do two step refinement and return the cost

firstRefine

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. If every clause's cost is -1 which means every clause is refined to true, cost -1 returned. Otherwise, multiply of every cost is return. Beside, if a clause is refined to a situation that only one literal is left, the literal will be add to assertLiterals.