|
||||||||||
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 contraints. |
org.sat4j.minisat.core | Implementation of the MiniSAT solver skeleton. |
org.sat4j.pb | |
org.sat4j.pb.constraints | |
org.sat4j.pb.constraints.pb | Implementations of pseudo boolean contraints. |
org.sat4j.pb.core | |
org.sat4j.pb.reader | |
org.sat4j.pb.tools | |
org.sat4j.specs | Those classes are intented for users dealing with SAT solvers as blackboxes. |
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 |
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)
|
void |
Supports.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
Supports.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 |
BinarySupportEncoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
DirectEncoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
GeneralizedSupportEncoding.onInit(ISolver solver,
IVec<Var> scope)
|
void |
BinarySupportEncoding.onInit(ISolver solver,
IVec<Var> scope)
|
void |
DirectEncoding.onInit(ISolver solver,
IVec<Var> scope)
|
void |
GeneralizedSupportEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
BinarySupportEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
DirectEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
GeneralizedSupportEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
BinarySupportEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
DirectEncoding.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 |
---|
Methods in org.sat4j.minisat.core that return IVec | |
---|---|
IVec<Propagatable> |
DataStructureFactory.getWatchesFor(int p)
|
IVec<Undoable> |
ILits.undos(int lit)
|
IVec<Propagatable> |
ILits.watches(int lit)
|
Methods in org.sat4j.minisat.core with parameters of type IVec | |
---|---|
void |
Solver.addAllClauses(IVec<IVecInt> 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 |
PseudoBitsAdderDecorator.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.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 |
PseudoBitsAdderDecorator.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.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 |
PseudoBitsAdderDecorator.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.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 |
PseudoBitsAdderDecorator.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" |
IConstr |
UserFriendlyPBStringSolver.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)
|
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.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 |
PBSolver.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
|
IConstr |
PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
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 |
ClausalConstraintsDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
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.addAtMost(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)
|
void |
LexicoDecoratorPB.addCriterion(IVecInt literals,
IVec<BigInteger> coefs)
|
IConstr |
ClausalConstraintsDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
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.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
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)
|
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<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 |
AbstractOutputSolver.addAllClauses(IVec<IVecInt> clauses)
|
void |
ManyCore.addAllClauses(IVec<IVecInt> clauses)
|
void |
SolverDecorator.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 |