|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||
| Packages that use IVec | |
|---|---|
| org.sat4j.core | Implementation of the data structures available in org.sat4j.specs. |
| org.sat4j.csp | Classes needed for CSP to SAT translation. |
| org.sat4j.csp.constraints | Classes needed for CSP to SAT translation. |
| org.sat4j.csp.encodings | |
| org.sat4j.maxsat | MAXSAT and Weighted Max SAT framework. |
| org.sat4j.minisat.constraints | Implementations of various constraints for MiniSAT. |
| org.sat4j.minisat.constraints.cnf | Implementations of clausal constraints. |
| org.sat4j.minisat.core | Implementation of the MiniSAT solver skeleton. |
| org.sat4j.pb | Implementations of pseudo boolean solvers |
| org.sat4j.pb.constraints | Implementation of data structures for pseudo boolean constraints. |
| org.sat4j.pb.constraints.pb | Implementations of pseudo boolean constraints. |
| org.sat4j.pb.core | Implementations of pseudo boolean solvers |
| org.sat4j.pb.reader | Readers for opb instances. |
| org.sat4j.pb.tools | Implementation of different tools for pseudo boolean solvers |
| org.sat4j.specs | Those classes are intended for users dealing with SAT solvers as black boxes. |
| org.sat4j.tools | Tools to be used on top of an ISolver. |
| Uses of IVec in org.sat4j.core |
|---|
| Classes in org.sat4j.core that implement IVec | |
|---|---|
class |
ReadOnlyVec<T>
Utility class to allow Read Only access to an IVec |
class |
Vec<T>
Simple but efficient vector implementation, based on the vector implementation available in MiniSAT. |
| Methods in org.sat4j.core that return IVec | |
|---|---|
IVec<T> |
Vec.push(T elem)
|
IVec<T> |
ReadOnlyVec.push(T elem)
|
| Methods in org.sat4j.core with parameters of type IVec | |
|---|---|
void |
Vec.copyTo(IVec<T> copy)
Ces operations devraient se faire en temps constant. |
void |
ReadOnlyVec.copyTo(IVec<T> copy)
|
void |
Vec.moveTo(IVec<T> dest)
|
void |
ReadOnlyVec.moveTo(IVec<T> dest)
|
| Constructors in org.sat4j.core with parameters of type IVec | |
|---|---|
ReadOnlyVec(IVec<T> vec)
|
|
| Uses of IVec in org.sat4j.csp |
|---|
| Methods in org.sat4j.csp with parameters of type IVec | |
|---|---|
void |
Encoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
Encoding.onInit(ISolver solver,
IVec<Var> scope)
|
void |
Encoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
Encoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
Predicate.toClause(ISolver solver,
IVec<Var> vscope,
IVec<Evaluable> vars)
|
void |
Predicate.toClause(ISolver solver,
IVec<Var> vscope,
IVec<Evaluable> vars)
|
void |
Clausifiable.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
Clausifiable.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
| Uses of IVec in org.sat4j.csp.constraints |
|---|
| Methods in org.sat4j.csp.constraints with parameters of type IVec | |
|---|---|
protected Encoding |
WalshSupports.chooseEncoding(IVec<Var> scope)
|
protected abstract Encoding |
Supports.chooseEncoding(IVec<Var> scope)
|
protected Encoding |
GentSupports.chooseEncoding(IVec<Var> scope)
|
protected Encoding |
BessiereSupports.chooseEncoding(IVec<Var> scope)
|
void |
Supports.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
Supports.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
Nogoods.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
Nogoods.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
AllDiff.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
AllDiff.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
| Uses of IVec in org.sat4j.csp.encodings |
|---|
| Methods in org.sat4j.csp.encodings with parameters of type IVec | |
|---|---|
void |
GeneralizedSupportEncoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
DirectEncoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
BinarySupportEncoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
GeneralizedSupportEncoding.onInit(ISolver solver,
IVec<Var> scope)
|
void |
DirectEncoding.onInit(ISolver solver,
IVec<Var> scope)
|
void |
BinarySupportEncoding.onInit(ISolver solver,
IVec<Var> scope)
|
void |
GeneralizedSupportEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
DirectEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
BinarySupportEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
GeneralizedSupportEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
DirectEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
BinarySupportEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
| Uses of IVec in org.sat4j.maxsat |
|---|
| Methods in org.sat4j.maxsat with parameters of type IVec | |
|---|---|
void |
WeightedMaxSatDecorator.addWeightedLiteralsToMinimize(IVecInt literals,
IVec<BigInteger> coefficients)
Set some literals whose sum must be minimized. |
| Uses of IVec in org.sat4j.minisat.constraints |
|---|
| Methods in org.sat4j.minisat.constraints that return IVec | |
|---|---|
IVec<Propagatable> |
AbstractDataStructureFactory.getWatchesFor(int p)
|
| Uses of IVec in org.sat4j.minisat.constraints.cnf |
|---|
| Methods in org.sat4j.minisat.constraints.cnf that return IVec | |
|---|---|
IVec<Undoable> |
Lits.undos(int lit)
|
IVec<Propagatable> |
Lits.watches(int lit)
|
| Uses of IVec in org.sat4j.minisat.core |
|---|
| Fields in org.sat4j.minisat.core declared as IVec | |
|---|---|
protected IVec<Constr> |
Solver.constrs
Set of original constraints. |
protected IVec<Constr> |
Solver.learnts
Set of learned constraints. |
| Methods in org.sat4j.minisat.core that return IVec | |
|---|---|
IVec<Constr> |
Solver.getLearnedConstraints()
|
IVec<Propagatable> |
DataStructureFactory.getWatchesFor(int p)
|
IVec<Undoable> |
ILits.undos(int lit)
Retrieve the methods to call when the solver backtracks. |
IVec<Propagatable> |
ILits.watches(int lit)
|
| Methods in org.sat4j.minisat.core with parameters of type IVec | |
|---|---|
void |
Solver.addAllClauses(IVec<IVecInt> clauses)
|
void |
LearnedConstraintsDeletionStrategy.reduce(IVec<Constr> learnedConstrs)
Hook method called when the solver wants to reduce the set of learned clauses. |
| Uses of IVec in org.sat4j.pb |
|---|
| Methods in org.sat4j.pb that return IVec | |
|---|---|
IVec<BigInteger> |
ObjectiveFunction.getCoeffs()
|
| Methods in org.sat4j.pb with parameters of type IVec | |
|---|---|
IConstr |
UserFriendlyPBStringSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PseudoBitsAdderDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PBSolverDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
OPBStringSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
LPStringSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
IPBSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
Create a pseudo-boolean constraint of the type "at least". |
IConstr |
UserFriendlyPBStringSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PseudoBitsAdderDecorator.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PBSolverDecorator.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
OPBStringSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
LPStringSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
IPBSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
Create a pseudo boolean constraint of the type "at most". |
IConstr |
UserFriendlyPBStringSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
PseudoBitsAdderDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
PBSolverDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
OPBStringSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
LPStringSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
IPBSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
Create a pseudo-boolean constraint of the type "subset sum". |
IConstr |
UserFriendlyPBStringSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
PseudoBitsAdderDecorator.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
PBSolverDecorator.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
OPBStringSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
LPStringSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
IPBSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied" |
| Constructors in org.sat4j.pb with parameters of type IVec | |
|---|---|
ObjectiveFunction(IVecInt vars,
IVec<BigInteger> coeffs)
|
|
| Uses of IVec in org.sat4j.pb.constraints |
|---|
| Methods in org.sat4j.pb.constraints with parameters of type IVec | |
|---|---|
Constr |
AbstractPBDataStructureFactory.createAtLeastPBConstraint(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree)
|
Constr |
AbstractPBDataStructureFactory.createAtMostPBConstraint(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree)
|
Constr |
AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<BigInteger> coefs,
boolean moreThan,
BigInteger degree)
|
| Uses of IVec in org.sat4j.pb.constraints.pb |
|---|
| Methods in org.sat4j.pb.constraints.pb that return IVec | |
|---|---|
static IVec<BigInteger> |
Pseudos.toVecBigInt(IVecInt vec)
|
| Methods in org.sat4j.pb.constraints.pb with parameters of type IVec | |
|---|---|
void |
MapPb.buildConstraintFromConflict(IVecInt resLits,
IVec<BigInteger> resCoefs)
|
void |
IDataStructurePB.buildConstraintFromConflict(IVecInt resLits,
IVec<BigInteger> resCoefs)
|
static IDataStructurePB |
Pseudos.niceCheckedParameters(IVecInt ps,
IVec<BigInteger> bigCoefs,
boolean moreThan,
BigInteger bigDeg,
ILits voc)
|
static IDataStructurePB |
Pseudos.niceParameters(IVecInt ps,
IVec<BigInteger> bigCoefs,
boolean moreThan,
BigInteger bigDeg,
ILits voc)
|
| Uses of IVec in org.sat4j.pb.core |
|---|
| Methods in org.sat4j.pb.core with parameters of type IVec | |
|---|---|
IConstr |
PBSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PBSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PBSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
|
IConstr |
PBSolver.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
|
Constr |
PBDataStructureFactory.createAtLeastPBConstraint(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree)
|
Constr |
PBDataStructureFactory.createAtMostPBConstraint(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree)
|
Constr |
PBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<BigInteger> coefs,
boolean moreThan,
BigInteger degree)
|
| Uses of IVec in org.sat4j.pb.reader |
|---|
| Fields in org.sat4j.pb.reader declared as IVec | |
|---|---|
protected IVec<BigInteger> |
OPBReader2005.coeffs
|
| Methods in org.sat4j.pb.reader that return IVec | |
|---|---|
IVec<BigInteger> |
OPBReader2005.getCoeffs()
|
| Uses of IVec in org.sat4j.pb.tools |
|---|
| Methods in org.sat4j.pb.tools that return IVec | |
|---|---|
IVec<T> |
DependencyHelper.getSolution()
Retrieve the solution found. |
| Methods in org.sat4j.pb.tools with parameters of type IVec | |
|---|---|
IConstr |
XplainPB.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
ManyCorePB.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
LexicoDecoratorPB.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
ClausalConstraintsDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
XplainPB.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
ManyCorePB.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
LexicoDecoratorPB.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
ClausalConstraintsDecorator.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
void |
LexicoDecoratorPB.addCriterion(IVecInt literals,
IVec<BigInteger> coefs)
|
IConstr |
XplainPB.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
ManyCorePB.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
LexicoDecoratorPB.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
ClausalConstraintsDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
XplainPB.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
ManyCorePB.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
LexicoDecoratorPB.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
ClausalConstraintsDecorator.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
void |
DependencyHelper.discard(IVec<T> things)
|
boolean |
DependencyHelper.hasASolution(IVec<T> assumps)
|
| Constructors in org.sat4j.pb.tools with parameters of type IVec | |
|---|---|
ImplicationNamer(DependencyHelper<T,C> helper,
IVec<IConstr> toName)
|
|
| Uses of IVec in org.sat4j.specs |
|---|
| Methods in org.sat4j.specs that return IVec | |
|---|---|
IVec<? extends IConstr> |
ISolverService.getLearnedConstraints()
Read-Only access to the list of constraints learned and not deleted so far in the solver. |
IVec<T> |
IVec.push(T elem)
|
| Methods in org.sat4j.specs with parameters of type IVec | |
|---|---|
void |
ISolver.addAllClauses(IVec<IVecInt> clauses)
Create clauses from a set of set of literals. |
void |
IVec.copyTo(IVec<T> copy)
Ces operations devraient se faire en temps constant. |
void |
IVec.moveTo(IVec<T> dest)
Move the content of the vector into dest. |
| Uses of IVec in org.sat4j.tools |
|---|
| Methods in org.sat4j.tools with parameters of type IVec | |
|---|---|
void |
SolverDecorator.addAllClauses(IVec<IVecInt> clauses)
|
void |
ManyCore.addAllClauses(IVec<IVecInt> clauses)
|
void |
AbstractOutputSolver.addAllClauses(IVec<IVecInt> clauses)
|
void |
GateTranslator.optimisationFunction(IVecInt literals,
IVec<BigInteger> coefs,
IVecInt result)
Translate an optimization function into constraints and provides the binary literals in results. |
|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||