argutia.logic.resolution
Class Resolution
java.lang.Object
argutia.logic.resolution.Resolution
public class Resolution
- extends Object
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
affectations
protected final LinkedList<Maillon> affectations
contexte
protected Contexte contexte
resolutionEnclenchee
protected int resolutionEnclenchee
Resolution
public Resolution()
addAffectation
protected void addAffectation(MaillonLitteral mL)
backtrack
public void backtrack(int pointDeBacktrack)
- Rétablit le contexte associé au point de restauration passé en paramètre : O(n*m).
Complexité =
où n est le nombre de .
- Parameters:
pointDeBacktrack
- point de restauration obtenu via la méthode
getPointDeBacktrack()
getNextMLInconnu
protected MaillonLitteral getNextMLInconnu()
- Returns:
- un maillon littéral à l'état INCONNU, ou null s'il n'y en a plus
getPointDeBacktrack
public int getPointDeBacktrack()
- Fournit un point de restauration permettant via un appel à la méthode
backtrack(int)
de
retrouver le contexte présent : O(1).
- See Also:
backtrack(int)
- Returns:
- un point de restauration sous forme d'entier
injecterClause
public void injecterClause(Clause c)
throws IllegalStateException
- On suppose qu'on injecte des clauses uniquement avant un appel à
resoudre()
.
Sinon une exception ResolutionException est levée.
- Parameters:
c
- Clause à injecter
- Throws:
IllegalStateException
- si on tente d'injecter une clause après un appel à resoudre()
.
injecterEnsembleDeFormules
public void injecterEnsembleDeFormules(SetOfFormulas e)
throws IllegalStateException
- Throws:
IllegalStateException
injecterFormule
public void injecterFormule(Formula f)
throws IllegalStateException
- Throws:
IllegalStateException
removeAffectation
protected void removeAffectation()
resoudre
public Resolution.Etat resoudre()
- Davis et Putnam
- Returns:
- l'état de l'ensemble de clauses après résolution
simplifier
public Resolution.EtatApresSimplification simplifier()
memoriser
public void memoriser()
Argutia JavaDoc
23 décembre 2007