Logo Search packages:      
Sourcecode: sat4j version File versions

Constr org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::propagate (  )  [inline]

Returns:
null if not conflict is found, else a conflicting constraint.

Definition at line 748 of file Solver.java.

                                {
            while (qhead < trail.size()) {
                  stats.propagations++;
                  int p = trail.get(qhead++);
                  slistener.propagating(decode2dimacs(p));
                  order.assignLiteral(p);
                  // p is the literal to propagate
                  // Moved original MiniSAT code to dsfactory to avoid
                  // watches manipulation in counter Based clauses for instance.
                  assert p > 1;
                  IVec<Propagatable> constrs = dsfactory.getWatchesFor(p);

                  final int size = constrs.size();
                  for (int i = 0; i < size; i++) {
                        stats.inspects++;
                        if (!constrs.get(i).propagate(this, p)) {
                              // Constraint is conflicting: copy remaining watches to
                              // watches[p]
                              // and return constraint
                              dsfactory.conflictDetectedInWatchesFor(p, i);
                              qhead = trail.size(); // propQ.clear();
                              // FIXME enlever le transtypage
                              return (Constr) constrs.get(i);
                        }
                  }
            }
            return null;
      }


Generated by  Doxygen 1.6.0   Back to index