|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.minisat.core.Solver org.sat4j.minisat.constraints.pb.PBSolver
public class PBSolver
Field Summary |
---|
Fields inherited from class org.sat4j.minisat.core.Solver |
---|
NO_SIMPLIFICATION, SIMPLE_SIMPLIFICATION |
Constructor Summary | |
---|---|
PBSolver(AssertingClauseGenerator acg,
LearningStrategy learner,
DataStructureFactory dsf,
IOrder order)
|
Method Summary | |
---|---|
int |
analyze(Constr myconfl,
Handle<Constr> outLearntRef)
|
java.lang.String |
toString(java.lang.String prefix)
Display a textual representation of the solver configuration. |
Methods inherited from class org.sat4j.minisat.core.Solver |
---|
addAllClauses, addAtLeast, addAtMost, addClause, addPseudoBoolean, assume, claBumpActivity, decisionLevel, decode2dimacs, enqueue, enqueue, getDSFactory, getIthConstr, getOrder, getOutLearnt, getStat, getStats, getTimeout, getVocabulary, isSatisfiable, isSatisfiable, learn, model, model, nConstraints, newVar, newVar, nVars, printStat, printStat, propagate, removeConstr, reset, setDataStructureFactory, setExpectedNumberOfClauses, setOrder, setSearchListener, setSimplifier, setTimeout, simplifyDB, toString, varBumpActivity |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Constructor Detail |
---|
public PBSolver(AssertingClauseGenerator acg, LearningStrategy learner, DataStructureFactory dsf, IOrder order)
acg
- learner
- dsf
- Method Detail |
---|
public int analyze(Constr myconfl, Handle<Constr> outLearntRef)
analyze
in class Solver
public java.lang.String toString(java.lang.String prefix)
ISolver
toString
in interface ISolver
toString
in class Solver
prefix
- the prefix to use on each line.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |