Bug fix in temporal scheduling constraint for object instances (object gluing).

This commit is contained in:
surynek 2025-02-12 17:59:34 +01:00 committed by Lukas Matena
parent 242c1a0415
commit f2d0bc1f4f

View File

@ -558,7 +558,7 @@ void introduce_ConsequentialTemporalLepoxAgainstFixed(z3::solver
for (unsigned int j = 0; j < undecided.size(); ++j) for (unsigned int j = 0; j < undecided.size(); ++j)
{ {
Solver.add( Context.real_val(dec_values_T[fixed[i]].numerator, dec_values_T[fixed[i]].denominator) > dec_vars_T[undecided[j]] + temporal_spread Solver.add( Context.real_val(dec_values_T[fixed[i]].numerator, dec_values_T[fixed[i]].denominator) > dec_vars_T[undecided[j]] + temporal_spread
|| Context.real_val(dec_values_T[next_i].numerator, dec_values_T[next_i].denominator) < dec_vars_T[undecided[j]] + temporal_spread); || Context.real_val(dec_values_T[next_i].numerator, dec_values_T[next_i].denominator) + temporal_spread < dec_vars_T[undecided[j]]);
} }
} }
} }