org.sat4j.minisat.constraints.cnf
Class OriginalHTClause

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.HTClause
      extended by org.sat4j.minisat.constraints.cnf.OriginalHTClause
All Implemented Interfaces:
java.io.Serializable, Constr, Propagatable, IConstr

public class OriginalHTClause
extends HTClause

See Also:
Serialized Form

Field Summary
 
Fields inherited from class org.sat4j.minisat.constraints.cnf.HTClause
head, middleLits, tail, voc
 
Constructor Summary
OriginalHTClause(IVecInt ps, ILits voc)
           
 
Method Summary
static OriginalHTClause brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
 boolean learnt()
           
 void register()
          Register the constraint to the solver.
 void setLearnt()
          Mark a constraint as learnt.
 
Methods inherited from class org.sat4j.minisat.constraints.cnf.HTClause
assertConstraint, calcReason, equals, get, getActivity, getLits, getVocabulary, hashCode, incActivity, locked, propagate, remove, rescaleBy, simplify, size, toString
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Constructor Detail

OriginalHTClause

public OriginalHTClause(IVecInt ps,
                        ILits voc)
Method Detail

register

public void register()
Description copied from interface: Constr
Register the constraint to the solver.


learnt

public boolean learnt()
Returns:
true iff the clause was learnt during the search

setLearnt

public void setLearnt()
Description copied from interface: Constr
Mark a constraint as learnt.


brandNewClause

public static OriginalHTClause brandNewClause(UnitPropagationListener s,
                                              ILits voc,
                                              IVecInt literals)
Creates a brand new clause, presumably from external data.

Parameters:
s - the object responsible for unit propagation
voc - the vocabulary
literals - the literals to store in the clause
Returns:
the created clause or null if the clause should be ignored (tautology for example)


Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.