Robust redef context #249

Restore context-unaware redef of !=, fixing redef in int_ne_05.mod

Fix context check after redef

Author: glebbelov

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());
     }

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

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);
+      }
     }
   }
 

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,

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;

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": {