org.sat4j.pb.constraints.pb
Class HTClausePB
java.lang.Object
org.sat4j.minisat.constraints.cnf.HTClause
org.sat4j.pb.constraints.pb.HTClausePB
- All Implemented Interfaces:
- java.io.Serializable, Constr, Propagatable, PBConstr, IConstr
public class HTClausePB
- extends HTClause
- implements PBConstr
- See Also:
- Serialized Form
Methods inherited from class org.sat4j.minisat.constraints.cnf.HTClause |
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 |
HTClausePB
public HTClausePB(IVecInt ps,
ILits voc)
getCoef
public java.math.BigInteger getCoef(int literal)
- Specified by:
getCoef
in interface PBConstr
getDegree
public java.math.BigInteger getDegree()
- Specified by:
getDegree
in interface PBConstr
getCoefs
public java.math.BigInteger[] getCoefs()
- Specified by:
getCoefs
in interface PBConstr
brandNewClause
public static HTClausePB brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
- Creates a brand new clause, presumably from external data. Performs all
sanity checks.
- Parameters:
s
- the object responsible for unit propagationvoc
- the vocabularyliterals
- the literals to store in the clause
- Returns:
- the created clause or null if the clause should be ignored
(tautology for example)
assertConstraint
public void assertConstraint(UnitPropagationListener s)
- Specified by:
assertConstraint
in interface Constr
- Overrides:
assertConstraint
in class HTClause
computeAnImpliedClause
public IVecInt computeAnImpliedClause()
- Specified by:
computeAnImpliedClause
in interface PBConstr
setLearnt
public void setLearnt()
- declares this clause as learnt
- Specified by:
setLearnt
in interface Constr
learnt
public boolean learnt()
- Specified by:
learnt
in interface IConstr
register
public void register()
- Register this clause which means watching the necessary literals If the
clause is learnt, setLearnt() must be called before a call to register()
- Specified by:
register
in interface Constr
- See Also:
setLearnt()
Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.