Logo Search packages:      
Sourcecode: sat4j version File versions

void org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::addAllClauses ( IVec< IVecInt clauses  )  throws ContradictionException [inline]

Create clauses from a set of set of literals. This is convenient to create in a single call all the clauses (mandatory for the distributed version of the solver). It is mainly a loop to addClause().

clauses a vector of set (VecInt) of literals in the dimacs format. The vector can be reused since the solver is not supposed to keep a reference to that vector.
ContradictionException iff the vector of literals is empty or if it contains only falsified literals after unit propagation
See also:

Implements org::sat4j::specs::ISolver.

Definition at line 319 of file Solver.java.

            for (Iterator<IVecInt> iterator = clauses.iterator(); iterator
                        .hasNext();) {

Generated by  Doxygen 1.6.0   Back to index