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.

p the literal.
from the reason to propagate that literal, else null
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.setLevel(p, decisionLevel());
            voc.setReason(p, from);
            return true;

Generated by  Doxygen 1.6.0   Back to index