@Test(groups="1s", timeOut=60000) public void testVariableBound3() throws Exception{ vars[0].instantiateTo(1, Cause.Null); try { PNG.VariableBound(0, true); Assert.fail(); }catch (ContradictionException cew){ } }
void VariableBound(int index, boolean sign) throws ContradictionException { try { if (sat_trail_.get() < sat_.trailMarker()) { sat_.cancelUntil(sat_trail_.get()); assert (sat_trail_.get() == sat_.trailMarker()); } int lit = makeLiteral(index, sign); if (!sat_.propagateOneLiteral(lit)) { doReduce(negated(lit)); } else { sat_trail_.set(sat_.trailMarker()); for (int i = 0; i < sat_.touched_variables_.size(); ++i) { lit = sat_.touched_variables_.get(i); doReduce(lit); } } } finally { sat_.touched_variables_.resetQuick(); } }
PropNogoods extends Propagator<Variable> { void VariableBound(int index, boolean sign) throws ContradictionException { try { if (sat_trail_.get() < sat_.trailMarker()) { sat_.cancelUntil(sat_trail_.get()); assert (sat_trail_.get() == sat_.trailMarker()); } int lit = makeLiteral(index, sign); if (!sat_.propagateOneLiteral(lit)) { doReduce(negated(lit)); } else { sat_trail_.set(sat_.trailMarker()); for (int i = 0; i < sat_.touched_variables_.size(); ++i) { lit = sat_.touched_variables_.get(i); doReduce(lit); } } } finally { sat_.touched_variables_.resetQuick(); } } }
PropNogoods extends Propagator<Variable> { void VariableBound(int index, boolean sign) throws ContradictionException { try { if (sat_trail_.get() < sat_.trailMarker()) { sat_.cancelUntil(sat_trail_.get()); assert (sat_trail_.get() == sat_.trailMarker()); } int lit = makeLiteral(index, sign); if (!sat_.propagateOneLiteral(lit)) { doReduce(negated(lit)); } else { sat_trail_.set(sat_.trailMarker()); for (int i = 0; i < sat_.touched_variables_.size(); ++i) { lit = sat_.touched_variables_.get(i); doReduce(lit); } } } finally { sat_.touched_variables_.resetQuick(); } } PropNogoods(Model model); }
PropNogoods extends Propagator<Variable> { void VariableBound(int index, boolean sign) throws ContradictionException { try { if (sat_trail_.get() < sat_.trailMarker()) { sat_.cancelUntil(sat_trail_.get()); assert (sat_trail_.get() == sat_.trailMarker()); } int lit = makeLiteral(index, sign); if (!sat_.propagateOneLiteral(lit)) { doReduce(negated(lit)); } else { sat_trail_.set(sat_.trailMarker()); for (int i = 0; i < sat_.touched_variables_.size(); ++i) { lit = sat_.touched_variables_.get(i); doReduce(lit); } } } finally { sat_.touched_variables_.resetQuick(); } } PropNogoods(Model model); @Override void propagate(int evtmask); @Override void propagate(int idxVarInProp, int mask); @Override ESat isEntailed(); void initialize(); int Literal(IntVar ivar, int value, boolean eq); int Literal(SetVar svar, int value, boolean in); @SuppressWarnings("unused") boolean addNogood(int p); @SuppressWarnings("unused") boolean addNogood(TIntList lits); void addLearnt(int... lits); }
PropNogoods extends Propagator<Variable> { void VariableBound(int index, boolean sign) throws ContradictionException { try { if (sat_trail_.get() < sat_.trailMarker()) { sat_.cancelUntil(sat_trail_.get()); assert (sat_trail_.get() == sat_.trailMarker()); } int lit = makeLiteral(index, sign); if (!sat_.propagateOneLiteral(lit)) { doReduce(negated(lit)); } else { sat_trail_.set(sat_.trailMarker()); for (int i = 0; i < sat_.touched_variables_.size(); ++i) { lit = sat_.touched_variables_.get(i); doReduce(lit); } } } finally { sat_.touched_variables_.resetQuick(); } } PropNogoods(Model model); @Override void propagate(int evtmask); @Override void propagate(int idxVarInProp, int mask); @Override ESat isEntailed(); void initialize(); int Literal(IntVar ivar, int value, boolean eq); int Literal(SetVar svar, int value, boolean in); @SuppressWarnings("unused") boolean addNogood(int p); @SuppressWarnings("unused") boolean addNogood(TIntList lits); void addLearnt(int... lits);  }