Uses of Interface
org.sat4j.specs.IVec

Packages that use IVec

Package	Description
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

Modifier and Type	Class and Description
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

Modifier and Type	Method and Description
IVec<T>	Vec.push(T elem)
IVec<T>	ReadOnlyVec.push(T elem)

Methods in org.sat4j.core with parameters of type IVec

Modifier and Type	Method and Description
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

Constructor and Description
ReadOnlyVec(IVec<T> vec)

Uses of IVec in org.sat4j.csp

Methods in org.sat4j.csp with parameters of type IVec

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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	AllDiffCard.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
void	AllDiffCard.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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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

Modifier and Type	Field and Description
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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
IVec<BigInteger>	ObjectiveFunction.getCoeffs()

Methods in org.sat4j.pb with parameters of type IVec

Modifier and Type	Method and Description
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	LPStringSolver.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	LPStringSolver.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	IPBSolverService.addAtMostOnTheFly(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	LPStringSolver.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	LPStringSolver.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

Constructor and Description
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

Modifier and Type	Method and Description
protected Constr	AbstractPBClauseCardConstrDataStructure.constructLearntCard(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructLearntPB(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
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)
Constr	AbstractPBDataStructureFactory.createUnregisteredAtLeastConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	AbstractPBDataStructureFactory.createUnregisteredAtMostConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected abstract Constr	AbstractPBDataStructureFactory.learntAtLeastConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.learntAtLeastConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	PuebloPBMinDataStructure.learntAtLeastConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	PBMinDataStructure.learntAtLeastConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	PBMaxDataStructure.learntAtLeastConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected abstract Constr	AbstractPBDataStructureFactory.learntAtMostConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.learntAtMostConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	PuebloPBMinDataStructure.learntAtMostConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	PBMinDataStructure.learntAtMostConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected Constr	PBMaxDataStructure.learntAtMostConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)

Uses of IVec in org.sat4j.pb.constraints.pb

Methods in org.sat4j.pb.constraints.pb that return IVec

Modifier and Type	Method and Description
static IVec<BigInteger>	Pseudos.toVecBigInt(IVecInt vec)

Methods in org.sat4j.pb.constraints.pb with parameters of type IVec

Modifier and Type	Method and Description
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)

Constructors in org.sat4j.pb.constraints.pb with parameters of type IVec

Constructor and Description
MapPb(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)

Uses of IVec in org.sat4j.pb.core

Methods in org.sat4j.pb.core with parameters of type IVec

Modifier and Type	Method and Description
void	ObjectiveReducerPBSolverDecorator.addAllClauses(IVec<IVecInt> clauses)
IConstr	PBSolver.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ObjectiveReducerPBSolverDecorator.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ObjectiveReducerPBSolverDecorator.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolver.addAtMostOnTheFly(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
IConstr	PBSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	ObjectiveReducerPBSolverDecorator.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)
IConstr	ObjectiveReducerPBSolverDecorator.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
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)
Constr	PBDataStructureFactory.createUnregisteredAtLeastConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	PBDataStructureFactory.createUnregisteredAtMostConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)

Uses of IVec in org.sat4j.pb.reader

Fields in org.sat4j.pb.reader declared as IVec

Modifier and Type	Field and Description
protected IVec<BigInteger>	OPBReader2005.coeffs

Methods in org.sat4j.pb.reader that return IVec

Modifier and Type	Method and Description
IVec<BigInteger>	OPBReader2005.getCoeffs()

Uses of IVec in org.sat4j.pb.tools

Methods in org.sat4j.pb.tools that return IVec

Modifier and Type	Method and Description
IVec<T>	DependencyHelper.getSolution() Retrieve the solution found.

Methods in org.sat4j.pb.tools with parameters of type IVec

Modifier and Type	Method and Description
IConstr	PBAdapter.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
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	PBAdapter.addAtMost(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	PBAdapter.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
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	PBAdapter.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
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	AbstractLexicoHelper.hasASolution(IVec<T> assumps)
boolean	DependencyHelper.hasASolution(IVec<T> assumps)
static boolean	ClausalConstraintsDecorator.isCardinality(IVec<BigInteger> coeffs)

Constructors in org.sat4j.pb.tools with parameters of type IVec

Constructor and Description
ImplicationNamer(DependencyHelper<T,C> helper, IVec<IConstr> toName)

Uses of IVec in org.sat4j.specs

Methods in org.sat4j.specs that return IVec

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
void	AbstractOutputSolver.addAllClauses(IVec<IVecInt> clauses)
void	ManyCore.addAllClauses(IVec<IVecInt> clauses)
void	StatisticsSolver.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.