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

Parameters:
literals a set of literals
Returns:
a reference to the constraint added in the solver, to use in removeConstr().
Exceptions:
ContradictionException iff the vector of literals is empty or if it contains only falsified literals after unit propagation
See also:
removeConstr(IConstr)

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