diff --git a/include/mp/flat/constr_keeper.h b/include/mp/flat/constr_keeper.h index 42781ac60..b72e3dab4 100644 --- a/include/mp/flat/constr_keeper.h +++ b/include/mp/flat/constr_keeper.h @@ -87,15 +87,15 @@ class ConstraintKeeper final int GetConstraintDepth(int i) const { assert(check_index(i)); return cons_[i].GetDepth(); } - /// Get context of contraint \a i + /// Get context of constraint \a i Context GetContext(int i) const override { assert(check_index(i)); return cons_[i].GetCon().GetContext(); } - /// Add context of contraint \a i + /// Add context of constraint \a i void AddContext(int i, Context ctx) override { assert(check_index(i)); cons_[i].GetCon().AddContext(ctx); } - /// Set context of contraint \a i + /// Set context of constraint \a i void SetContext(int i, Context ctx) override { assert(check_index(i)); cons_[i].GetCon().SetContext(ctx); } @@ -116,7 +116,7 @@ class ConstraintKeeper final try { // Too strong: instead, differentiate context // in which the redefinition happened #248. - // MP_ASSERT_ALWAYS(!GetContext(i).IsProperSubsetOf(ctx) + // MP_ASSERT_ALWAYS(ctx.IsSubsetOf(GetContext()) // || IsBridgingToBeConsidered(i), auto ctx_redef = cons_[i].GetRedefContext(); MP_ASSERT_ALWAYS(ctx_redef.IsNone() @@ -129,7 +129,7 @@ class ConstraintKeeper final } catch (const std::exception& exc) { MP_RAISE(Converter::GetTypeName() + std::string(": propagating result for constraint ") + - std::to_string(i) + " of type '" + + std::to_string(i) + "\nof type '" + Constraint::GetTypeName() + "':\n" + exc.what()); } diff --git a/include/mp/flat/constr_prop_down.h b/include/mp/flat/constr_prop_down.h index aaade6171..5113eba42 100644 --- a/include/mp/flat/constr_prop_down.h +++ b/include/mp/flat/constr_prop_down.h @@ -141,7 +141,7 @@ class ConstraintPropagatorsDown { void PropagateResult(OrConstraint& con, double lb, double ub, Context ctx) { MPD( NarrowVarBounds(con.GetResultVar(), lb, ub) ); con.AddContext(ctx); - if (ub<=0.5 && ctx.HasNegative()) { // Remove, arguments are fixed + if (ub<0.5 && ctx.HasNegative()) { // Remove, arguments are fixed MPD( PropagateResult2Vars(con.GetArguments(), 0.0, ub, +ctx) ); MPD( DecrementVarUsage(con.GetResultVar()) ); } else diff --git a/include/mp/flat/converter.h b/include/mp/flat/converter.h index ed5a4a3a1..ecae05db5 100644 --- a/include/mp/flat/converter.h +++ b/include/mp/flat/converter.h @@ -99,8 +99,10 @@ class FlatConverter : if (HasInitExpression(var)) { const auto& ckid = GetInitExpression(var); const auto ctx_old = ckid.GetCK()->GetContext(ckid.GetIndex()); - if (tighterBounds || ctx_old.IsProperSubsetOf(ctx)) + if (tighterBounds + || !ctx.IsSubsetOf(ctx_old)) { // new context ckid.GetCK()->PropagateResult(*this, ckid.GetIndex(), lb, ub, ctx); + } } } diff --git a/include/mp/flat/redef/MIP/cond_eq.h b/include/mp/flat/redef/MIP/cond_eq.h index f4234e375..c8e281f35 100644 --- a/include/mp/flat/redef/MIP/cond_eq.h +++ b/include/mp/flat/redef/MIP/cond_eq.h @@ -76,10 +76,16 @@ class CondEQConverter_MIP : } else if ( !GetMC().is_fixed(res) || // not fixed, or !GetMC().fixed_value(res) ) // fixed to 0 { -#ifndef USE_FLAT_ALGEBRA auto bNt = GetMC().ComputeBoundsAndType(con.GetBody()); double cmpEps = GetMC().ComparisonEps( bNt.get_result_type() ); - /// res3 <==> (res || body <= rhs-eps || body >= rhs+eps) +#define COND_LIN_EQ__USE_FLAT_ALGEBRA +#ifndef COND_LIN_EQ__USE_FLAT_ALGEBRA + // Not doing this. + // Reason: the below OR propagates CTX+ into res, + // which is the expression we are redefining, + // but this is not necessary. See #248. + // Happens on eqVarConst01.mod. + /// res3 ==> (res || body <= rhs-eps || body >= rhs+eps) auto res3 = GetMC().AssignResultVar2Args( OrConstraint{ { res, @@ -91,16 +97,19 @@ class CondEQConverter_MIP : { { con.GetBody(), con.rhs() + cmpEps } }) } }); GetMC().FixAsTrue(res3); -#else // USE_FLAT_ALGEBRA - // Old way: straight to algebra and indicators - auto con = eq0c.GetArguments(); +#else // COND_LIN_EQ__USE_FLAT_ALGEBRA + // Old way: straight to algebra and indicators. + // This could duplicate the below indicators, + // but simpler as of now: + // the indicators redefine conditional inequalities + // which, in the above variant, could have been redefined + // in CTX- before, see int_ne_05_redef_ctx.mod, + // thus losing the CTX+ redefinition, see #248. auto newvars = GetMC().AddVars_returnIds(2, 0.0, 1.0, var::INTEGER); newvars.push_back( res ); GetMC().AddConstraint( LinConGE( // b1+b2+resvar >= 1 {{1.0, 1.0, 1.0}, newvars}, 1.0 ) ); - auto bNt = GetMC().ComputeBoundsAndType(con.GetBody()); - double cmpEps = GetMC().ComparisonEps( bNt.get_result_type() ); { GetMC().AddConstraint(IndicatorConstraint< AlgCon<-1> >( newvars[0], 1, diff --git a/test/end2end/cases/categorized/fast/logical/int_ne_05_ctx_redef.mod b/test/end2end/cases/categorized/fast/logical/int_ne_05_ctx_redef.mod new file mode 100644 index 000000000..d374151f5 --- /dev/null +++ b/test/end2end/cases/categorized/fast/logical/int_ne_05_ctx_redef.mod @@ -0,0 +1,14 @@ +# int_ne_05_ctx_redef.mod +# +# Test that x<=5 is redefined after all +# its contexts are known + +var x >=-3 <=11 integer; +var b binary; +var b1: binary; + +minimize Obj: -10*b - 10*b1 + if x<=5 then 1; + +s.t. ConNE_01: x != 6 <==> b; + +s.t. ConImpl_01: b1 ==> x <= 6; \ No newline at end of file diff --git a/test/end2end/cases/categorized/fast/logical/modellist.json b/test/end2end/cases/categorized/fast/logical/modellist.json index 9df1ef60b..b138cf06d 100644 --- a/test/end2end/cases/categorized/fast/logical/modellist.json +++ b/test/end2end/cases/categorized/fast/logical/modellist.json @@ -192,6 +192,14 @@ "objective" : 1, "tags" : ["logical"] }, + { + "name" : "int_ne_05_ctx_redef", + "objective" : -19, + "tags" : ["logical"], + "values": { + "if x<5.5 then 1": 1 + } + }, { "name" : "float_ne_01__vnec cvt:mip:eps", "options": {