Uses of Interface
org.sat4j.specs.IVec

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.
 



Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.