Logo Search packages:      
Sourcecode: sat4j version File versions

org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> Member List

This is the complete list of members for org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>, including all inherited members.

__dimacs_out (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
addAllClauses(IVec< IVecInt > clauses)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
addAtLeast(IVecInt literals, int degree)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
addAtMost(IVecInt literals, int degree)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
addClause(IVecInt literals)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
addConstr(Constr constr)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
analysisResult (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
analyze(Constr confl, Pair results) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
analyzeAtRootLevel(Constr conflict) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
analyzer (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [protected]
analyzeRemovable(int p) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, private]
analyzestack (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
analyzetoclear (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
assume(int p)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
cancel()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, private]
cancelLearntLiterals()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, private]
cancelUntil(int level)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
claBumpActivity(Constr confl)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, virtual]
claDecayorg::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
claDecayActivity() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, private]
claIncorg::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
claRescalActivity() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, private]
CLAUSE_RESCALE_BOUND (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private, static]
CLAUSE_RESCALE_FACTOR (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private, static]
clearLearntClauses()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
comparator (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
conflictCount (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
constrsorg::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
constrTypes (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
decayActivities() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
decisionLevel() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
decode2dimacs(int p)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, static]
dimacs2internal(IVecInt in) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
dsfactory (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [protected]
enqueue(int p)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, virtual]
enqueue(int p, Constr from)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, virtual]
EXPENSIVE_SIMPLIFICATION (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>
expensiveSimplification(IVecInt outLearnt) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, private]
expireTimeout()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
findModel()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
findModel(IVecInt assumps)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
fullmodel (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
getDSFactory() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
getIthConstr(int i)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
getOrder() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
getOutLearnt() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
getStat()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
getStats() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
getTimeout()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
getVocabulary() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
isDBSimplificationAllowed (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
isDBSimplificationAllowed()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
isSatisfiable()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
isSatisfiable(boolean global)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
isSatisfiable(IVecInt assumps)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
isSatisfiable(IVecInt assumps, boolean global)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
learn(Constr c) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
learnedLiterals (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
learner (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
learntsorg::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
model (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
model()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
model(int var)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
modelFound() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, package]
mseen (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
nAssigns() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
nConstraints()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
needToReduceDB (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
newVar()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
newVar(int howmany)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
NO_SIMPLIFICATION (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [static]
nVars()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
order (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
outLearnt (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
params (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
preason (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
printInfos(PrintWriter out, String prefix)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
printStat(PrintStream out, String prefix)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
printStat(PrintWriter out, String prefix)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
propagate()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
qheadorg::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
record(Constr constr) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, package]
reduceDB() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
reduceDB(double lim) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
removeConstr(IConstr co)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
reset()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
restarter (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
rootLevelorg::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [protected]
search(long nofConflicts) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, package]
serialVersionUID (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private, static]
setDataStructureFactory(D dsf)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setDBSimplificationAllowed(boolean status)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setExpectedNumberOfClauses(int nb)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setOrder(IOrder< L > h) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setRestartStrategy(RestartStrategy restarter) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setSearchListener(SearchListener sl) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setSearchParams(SearchParams sp) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setSimplifier(String simp)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setSimplifier(ISimplifier simp)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setTimeout(int t)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setTimeoutMs(long t)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
setTimeoutOnConflicts(int count)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
SIMPLE_SIMPLIFICATION (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>
simpleSimplification(IVecInt outLearnt) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, private]
simplifier (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
simplifyDB() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
slistener (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
Solver(AssertingClauseGenerator acg, LearningStrategy< L, D > learner, D dsf, IOrder< L > order, RestartStrategy restarter)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
Solver(AssertingClauseGenerator acg, LearningStrategy< L, D > learner, D dsf, SearchParams params, IOrder< L > order, RestartStrategy restarter) (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
sortOnActivity()org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, private]
stats (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
timeBasedTimeout (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
timebegin (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
timeout (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
timer (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
toString(String prefix)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
toString() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline]
trailorg::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [protected]
trailLimorg::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [protected]
undertimeout (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [private]
undoOne() (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, protected]
varBumpActivity(int p)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [inline, virtual]
voc (defined in org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>)org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >> [protected]


Generated by  Doxygen 1.6.0   Back to index