Logo Search packages:      
Sourcecode: sat4j version File versions

boolean org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::enqueue ( int  p,
Constr  from 
) [inline, virtual]

Put the literal on the queue of assignments to be done.

Parameters:
p the literal.
from the reason to propagate that literal, else null
Returns:
true if the asignment can be made, false if a conflict is detected.

Implements org::sat4j::minisat::core::UnitPropagationListener.

Definition at line 405 of file Solver.java.

                                                 {
            assert p > 1;
            if (voc.isSatisfied(p)) {
                  // literal is already satisfied. Skipping.
                  return true;
            }
            if (voc.isFalsified(p)) {
                  // conflicting enqueued assignment
                  return false;
            }
            // new fact, store it
            voc.satisfies(p);
            voc.setLevel(p, decisionLevel());
            voc.setReason(p, from);
            trail.push(p);
            return true;
      }


Generated by  Doxygen 1.6.0   Back to index