Logo Search packages:      
Sourcecode: sat4j version File versions

boolean org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::removeConstr ( IConstr  c  )  [inline]

Remove a constraint returned by one of the add method from the solver. All learned clauses will be cleared.

Current implementation does not handle properly the case of unit clauses.

Parameters:
c a constraint returned by one of the add method.
Returns:
true if the constraint was successfully removed.

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

Definition at line 306 of file Solver.java.

References org::sat4j::minisat::core::Constr::remove().

                                              {
            if (co == null) {
                  throw new IllegalArgumentException(
                              "Reference to the constraint to remove needed!"); //$NON-NLS-1$
            }
            Constr c = (Constr) co;
            c.remove();
            constrs.remove(c);
            clearLearntClauses();
            cancelLearntLiterals();
            return true;
      }


Generated by  Doxygen 1.6.0   Back to index