org.sat4j.minisat.constraints.cnf
Class OriginalWLClause

java.lang.Object
  org.sat4j.minisat.constraints.cnf.WLClause
      org.sat4j.minisat.constraints.cnf.OriginalWLClause

All Implemented Interfaces:

java.io.Serializable, Constr, Propagatable, IConstr

public class OriginalWLClause
extends WLClause

See Also:

Serialized Form

Constructor Summary

OriginalWLClause(IVecInt ps, ILits voc)

Method Summary

static OriginalWLClause	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.WLClause

assertConstraint, calcReason, equals, get, getActivity, getLits, getVocabulary, hashCode, incActivity, locked, propagate, remove, rescaleBy, sanityCheck, simplify, size, toString

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

OriginalWLClause

public OriginalWLClause(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 OriginalWLClause 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)