public class AbstractMinimalModel extends SolverDecorator<ISolver>
Modifier and Type | Field and Description |
---|---|
protected SolutionFoundListener |
modelListener |
protected SortedSet<Integer> |
pLiterals |
Constructor and Description |
---|
AbstractMinimalModel(ISolver solver) |
AbstractMinimalModel(ISolver solver,
IVecInt p) |
AbstractMinimalModel(ISolver solver,
IVecInt p,
SolutionFoundListener modelListener) |
AbstractMinimalModel(ISolver solver,
SolutionFoundListener modelListener) |
Modifier and Type | Method and Description |
---|---|
static IVecInt |
negativeLiterals(ISolver solver) |
static IVecInt |
positiveLiterals(ISolver solver) |
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, setVerbose, toString, toString, unsatExplanation
protected final SolutionFoundListener modelListener
public AbstractMinimalModel(ISolver solver)
public AbstractMinimalModel(ISolver solver, SolutionFoundListener modelListener)
public AbstractMinimalModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.