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().

Parameters:
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.
Exceptions:
ContradictionException iff the vector of literals is empty or if it contains only falsified literals after unit propagation
See also:
addClause(IVecInt)

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

Definition at line 319 of file Solver.java.

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


Generated by  Doxygen 1.6.0   Back to index