Logo Search packages:      
Sourcecode: sat4j version File versions

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

Propagate activity to a constraint

Parameters:
confl a constraint

Implements org::sat4j::minisat::core::ConstrActivityListener.

Definition at line 725 of file Solver.java.

References org::sat4j::minisat::core::Constr::getActivity(), and org::sat4j::minisat::core::Constr::incActivity().

                                                {
            confl.incActivity(claInc);
            if (confl.getActivity() > CLAUSE_RESCALE_BOUND)
                  claRescalActivity();
            // for (int i = 0; i < confl.size(); i++) {
            // varBumpActivity(confl.get(i));
            // }
      }


Generated by  Doxygen 1.6.0   Back to index