|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use IVecInt | |
---|---|
org.sat4j.core | Implementation of the data structures available in org.sat4j.specs. |
org.sat4j.minisat.constraints | Implementations of various constraints for MiniSAT. |
org.sat4j.minisat.constraints.card | Implementations of cardinality contraints. |
org.sat4j.minisat.constraints.cnf | Implementations of clausal contraints. |
org.sat4j.minisat.constraints.pb | Implementations of pseudo boolean contraints. |
org.sat4j.minisat.core | Implementation of the MiniSAT solver skeleton. |
org.sat4j.opt | Optimization extensions. |
org.sat4j.reader | Some utility classes to read problems from plain text files. |
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 IVecInt in org.sat4j.core |
---|
Classes in org.sat4j.core that implement IVecInt | |
---|---|
class |
VecInt
A vector specific for primitive integers, widely used in the solver. |
Fields in org.sat4j.core declared as IVecInt | |
---|---|
static IVecInt |
VecInt.EMPTY
|
Methods in org.sat4j.core that return IVecInt | |
---|---|
IVecInt |
VecInt.pop()
d�pile le dernier �l�ment du vecteur. |
IVecInt |
VecInt.push(int elem)
|
Methods in org.sat4j.core with parameters of type IVecInt | |
---|---|
void |
VecInt.copyTo(IVecInt copy)
C'est op�rations devraient se faire en temps constant. |
boolean |
VecInt.isSubsetOf(IVecInt vec)
|
void |
VecInt.moveTo(IVecInt dest)
|
void |
VecInt.moveTo2(IVecInt dest)
|
void |
VecInt.pushAll(IVecInt vec)
|
Uses of IVecInt in org.sat4j.minisat.constraints |
---|
Methods in org.sat4j.minisat.constraints with parameters of type IVecInt | |
---|---|
Constr |
MixedDataStructureDaniel.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructure.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureWithBinaryAndTernary.createClause(IVecInt literals)
|
Constr |
MixedDataStructureWithBinary.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureWL.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureCBWL.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureCB.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMin.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMax.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructure.createClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
Constr |
AbstractDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
Constr |
AbstractCardinalityDataStructure.createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
Constr |
ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
|
Constr |
ClausalDataStructureCBWL.createUnregisteredClause(IVecInt literals)
|
Constr |
ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMax.createUnregisteredClause(IVecInt literals)
|
Constr |
CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createUnregisteredClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree)
|
Constr |
AbstractDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree)
|
IConstr |
AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
Uses of IVecInt in org.sat4j.minisat.constraints.card |
---|
Methods in org.sat4j.minisat.constraints.card with parameters of type IVecInt | |
---|---|
static AtLeast |
AtLeast.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
void |
MinWatchCard.calcReason(int p,
IVecInt outReason)
computes the reason for a literal |
void |
MaxWatchCard.calcReason(int p,
IVecInt outReason)
Calcule la cause de l'affection d'un litt? |
void |
AtLeast.calcReason(int p,
IVecInt outReason)
|
static MaxWatchCard |
MaxWatchCard.maxWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr? |
static MinWatchCard |
MinWatchCard.minWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Constructs a cardinality constraint with a minimal set of watched literals Permet la cr? |
Constructors in org.sat4j.minisat.constraints.card with parameters of type IVecInt | |
---|---|
MinWatchCard(ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Constructs and normalizes a cardinality constraint. |
Uses of IVecInt in org.sat4j.minisat.constraints.cnf |
---|
Methods in org.sat4j.minisat.constraints.cnf that return IVecInt | |
---|---|
IVecInt |
MarkableLits.getMarkedLiterals()
|
IVecInt |
MarkableLits.getMarkedLiterals(int mark)
|
IVecInt |
MarkableLits.getMarkedVariables()
|
IVecInt |
MarkableLits.getMarkedVariables(int mark)
|
static IVecInt |
WLClause.sanityCheck(IVecInt ps,
ILits voc,
UnitPropagationListener s)
Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation |
Methods in org.sat4j.minisat.constraints.cnf with parameters of type IVecInt | |
---|---|
static WLClause |
WLClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data. |
static CBClause |
MixableCBClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
|
static CBClause |
CBClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
|
void |
WLClause.calcReason(int p,
IVecInt outReason)
|
void |
TernaryClauses.calcReason(int p,
IVecInt outReason)
|
void |
CBClause.calcReason(int p,
IVecInt outReason)
|
void |
BinaryClauses.calcReason(int p,
IVecInt outReason)
|
static IVecInt |
WLClause.sanityCheck(IVecInt ps,
ILits voc,
UnitPropagationListener s)
Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation |
Constructors in org.sat4j.minisat.constraints.cnf with parameters of type IVecInt | |
---|---|
CBClause(IVecInt ps,
ILits voc)
|
|
CBClause(IVecInt ps,
ILits voc,
boolean learnt)
|
|
MixableCBClause(IVecInt ps,
ILits voc)
|
|
MixableCBClause(IVecInt ps,
ILits voc,
boolean learnt)
|
|
WLClause(IVecInt ps,
ILits voc)
Creates a new basic clause |
Uses of IVecInt in org.sat4j.minisat.constraints.pb |
---|
Methods in org.sat4j.minisat.constraints.pb that return IVecInt | |
---|---|
IVecInt |
WLClausePB.computeAnImpliedClause()
|
IVecInt |
MixableCBClausePB.computeAnImpliedClause()
|
IVecInt |
MinWatchCardPB.computeAnImpliedClause()
|
IVecInt |
AtLeastPB.computeAnImpliedClause()
|
IVecInt |
WatchPb.computeAnImpliedClause()
compute an implied clause on the literals with the greater coefficients |
IVecInt |
PBConstr.computeAnImpliedClause()
|
Methods in org.sat4j.minisat.constraints.pb with parameters of type IVecInt | |
---|---|
IConstr |
PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger degree)
|
static AtLeastPB |
AtLeastPB.atLeastNew(ILits voc,
IVecInt ps,
int n)
|
static AtLeastPB |
AtLeastPB.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
static WLClausePB |
WLClausePB.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data. |
static MixableCBClausePB |
MixableCBClausePB.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
|
void |
MapPb.buildConstraintFromConflict(IVecInt resLits,
IVec<java.math.BigInteger> resCoefs)
|
void |
ArrayPb.buildConstraintFromConflict(IVecInt resLits,
IVec<java.math.BigInteger> resCoefs)
|
void |
IDataStructurePB.buildConstraintFromConflict(IVecInt resLits,
IVec<java.math.BigInteger> resCoefs)
|
void |
WatchPb.calcReason(int p,
IVecInt outReason)
Calcule la cause de l'affectation d'un litt??? |
IConstr |
IInternalPBConstraintCreator.createUnregisteredPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree)
|
static MaxWatchPb |
MaxWatchPb.maxWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static MaxWatchPb |
MaxWatchPb.maxWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
static MinWatchCardPB |
MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr? |
static PuebloMinWatchPb |
PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static MinWatchPb |
MinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static PuebloMinWatchPb |
PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
static MinWatchPb |
MinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
static IDataStructurePB |
WatchPb.niceCheckedParameters(IVecInt ps,
IVec<java.math.BigInteger> bigCoefs,
boolean moreThan,
java.math.BigInteger bigDeg,
ILits voc)
|
static IDataStructurePB |
WatchPb.niceParameters(IVecInt ps,
IVec<java.math.BigInteger> bigCoefs,
boolean moreThan,
java.math.BigInteger bigDeg,
ILits voc)
|
static MinWatchCardPB |
MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int degree)
Permet la cr? |
static IVec<java.math.BigInteger> |
WatchPb.toVecBigInt(IVecInt vec)
|
static WatchPb |
PuebloMinWatchPb.watchPbNew(ILits voc,
IVecInt lits,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static WatchPb |
MinWatchPb.watchPbNew(ILits voc,
IVecInt lits,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static WatchPb |
MaxWatchPb.watchPbNew(ILits voc,
IVecInt lits,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static WatchPb |
PuebloMinWatchPb.watchPbNew(ILits voc,
IVecInt lits,
IVecInt coefs,
boolean moreThan,
int degree)
|
static WatchPb |
MinWatchPb.watchPbNew(ILits voc,
IVecInt lits,
IVecInt coefs,
boolean moreThan,
int degree)
|
static WatchPb |
MaxWatchPb.watchPbNew(ILits voc,
IVecInt lits,
IVecInt coefs,
boolean moreThan,
int degree)
|
Constructors in org.sat4j.minisat.constraints.pb with parameters of type IVecInt | |
---|---|
MinWatchCardPB(ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
|
|
MinWatchCardPB(ILits voc,
IVecInt ps,
int degree)
|
|
MixableCBClausePB(IVecInt ps,
ILits voc)
|
|
MixableCBClausePB(IVecInt ps,
ILits voc,
boolean learnt)
|
|
WLClausePB(IVecInt ps,
ILits voc)
|
Uses of IVecInt in org.sat4j.minisat.core |
---|
Methods in org.sat4j.minisat.core that return IVecInt | |
---|---|
IVecInt |
IMarkableLits.getMarkedLiterals()
Returns the set of all marked literals. |
IVecInt |
IMarkableLits.getMarkedLiterals(int mark)
Returns that set of all the literals having a specific mark. |
IVecInt |
IMarkableLits.getMarkedVariables()
Returns the set of all marked variables. |
IVecInt |
IMarkableLits.getMarkedVariables(int mark)
Returns the set of all variables having a specific mark. |
IVecInt |
Solver.getOutLearnt()
|
Methods in org.sat4j.minisat.core with parameters of type IVecInt | |
---|---|
IConstr |
Solver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
Solver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
Solver.addClause(IVecInt literals)
|
IConstr |
Solver.addPseudoBoolean(IVecInt literals,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger degree)
|
void |
Constr.calcReason(int p,
IVecInt outReason)
Calcule la cause de l'affection d'un litt? |
Constr |
DataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
DataStructureFactory.createClause(IVecInt literals)
|
Constr |
DataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
Constr |
DataStructureFactory.createUnregisteredClause(IVecInt literals)
|
Constr |
DataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
java.math.BigInteger degree)
|
boolean |
Solver.isSatisfiable(IVecInt assumps)
|
Method parameters in org.sat4j.minisat.core with type arguments of type IVecInt | |
---|---|
void |
Solver.addAllClauses(IVec<IVecInt> clauses)
|
Uses of IVecInt in org.sat4j.opt |
---|
Methods in org.sat4j.opt with parameters of type IVecInt | |
---|---|
IConstr |
WeightedMaxSatDecorator.addClause(IVecInt literals)
|
IConstr |
MaxSatDecorator.addClause(IVecInt literals)
|
Uses of IVecInt in org.sat4j.reader |
---|
Methods in org.sat4j.reader that return IVecInt | |
---|---|
IVecInt |
OPBReader2005.getVars()
|
IVecInt |
ObjectiveFunction.getVars()
|
Constructors in org.sat4j.reader with parameters of type IVecInt | |
---|---|
ObjectiveFunction(IVecInt vars,
IVec<java.math.BigInteger> coeffs)
|
Uses of IVecInt in org.sat4j.specs |
---|
Methods in org.sat4j.specs that return IVecInt | |
---|---|
IVecInt |
IVecInt.pop()
d�pile le dernier �l�ment du vecteur. |
IVecInt |
IVecInt.push(int elem)
|
Methods in org.sat4j.specs with parameters of type IVecInt | |
---|---|
IConstr |
ISolver.addAtLeast(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at least n of those literals must be satisfied" |
IConstr |
ISolver.addAtMost(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at most n of those literals must be satisfied" |
IConstr |
ISolver.addClause(IVecInt literals)
Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. |
IConstr |
ISolver.addPseudoBoolean(IVecInt lits,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger d)
Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied" |
void |
IVecInt.copyTo(IVecInt copy)
C'est op�rations devraient se faire en temps constant. |
boolean |
IProblem.isSatisfiable(IVecInt assumps)
Check the satisfiability of the set of constraints contained inside the solver. |
void |
IVecInt.moveTo(IVecInt dest)
|
void |
IVecInt.moveTo2(IVecInt dest)
|
Method parameters in org.sat4j.specs with type arguments of type IVecInt | |
---|---|
void |
ISolver.addAllClauses(IVec<IVecInt> clauses)
Create clauses from a set of set of literals. |
Uses of IVecInt in org.sat4j.tools |
---|
Methods in org.sat4j.tools that return IVecInt | |
---|---|
static IVecInt |
RemiUtils.backbone(ISolver s)
Compute the set of literals common to all models of the formula. |
Methods in org.sat4j.tools with parameters of type IVecInt | |
---|---|
IConstr |
SolverDecorator.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
SolverDecorator.addAtMost(IVecInt literals,
int degree)
|
IConstr |
SolverDecorator.addClause(IVecInt literals)
|
IConstr |
SolverDecorator.addPseudoBoolean(IVecInt literals,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger degree)
|
boolean |
SingleSolutionDetector.hasASingleSolution(IVecInt assumptions)
Please use that method only after a positive answer from isSatisfiable(assumptions) (else a runtime exception will be launched). |
boolean |
ModelIterator.isSatisfiable(IVecInt assumps)
|
boolean |
SolverDecorator.isSatisfiable(IVecInt assumps)
|
Method parameters in org.sat4j.tools with type arguments of type IVecInt | |
---|---|
void |
SolverDecorator.addAllClauses(IVec<IVecInt> clauses)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |