Logo Search packages:      
Sourcecode: sat4j version File versions

IConstr org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::addClause ( IVecInt  literals  )  throws ContradictionException [inline]

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. (classical Dimacs way of representing literals).

literals a set of literals
a reference to the constraint added in the solver, to use in removeConstr().
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 301 of file Solver.java.

            IVecInt vlits = dimacs2internal(literals);
            return addConstr(dsfactory.createClause(vlits));

Generated by  Doxygen 1.6.0   Back to index