Bug fix in scheduling of object instances (for HT90)

This commit is contained in:
surynek 2025-02-26 01:28:11 +01:00 committed by Lukas Matena
parent 302a662a50
commit 243101f20f
2 changed files with 47 additions and 20 deletions

View File

@ -86,6 +86,7 @@ bool PrinterGeometry::convert_Geometry2PlateBounds(Slic3r::BoundingBox &plate_bo
plate_bounding_polygon.points.insert(plate_bounding_polygon.points.begin() + i, Point(plate.points[i].x() / SEQ_SLICER_SCALE_FACTOR, plate_bounding_polygon.points.insert(plate_bounding_polygon.points.begin() + i, Point(plate.points[i].x() / SEQ_SLICER_SCALE_FACTOR,
plate.points[i].y() / SEQ_SLICER_SCALE_FACTOR)); plate.points[i].y() / SEQ_SLICER_SCALE_FACTOR));
} }
plate_bounding_polygon.make_counter_clockwise();
return false; return false;
} }
else else

View File

@ -148,6 +148,19 @@ void assume_BedBoundingPolygon(z3::context &Context,
{ {
BoundingBox box = get_extents(polygon); BoundingBox box = get_extents(polygon);
#ifdef DEBUG
{
printf("Polygon box: [%d,%d] [%d,%d]\n", box.min.x(), box.min.y(), box.max.x(), box.max.y());
printf("Bed bounding polygon: %ld\n", bed_bounding_polygon.points.size());
for (unsigned int i = 0; i < bed_bounding_polygon.points.size(); ++i)
{
printf("[%d,%d] ", bed_bounding_polygon.points[i].x(), bed_bounding_polygon.points[i].y());
}
printf("\n");
}
#endif
assume_PointInsidePolygon(Context, assume_PointInsidePolygon(Context,
dec_var_X + box.min.x(), dec_var_X + box.min.x(),
dec_var_Y + box.min.y(), dec_var_Y + box.min.y(),
@ -470,7 +483,8 @@ void introduce_ConsequentialTemporalLepoxAgainstFixed(z3::solver
#endif #endif
for (unsigned int j = 1; j < undecided.size(); ++j) for (unsigned int j = 1; j < undecided.size(); ++j)
{ {
Solver.add(dec_vars_T[0] + temporal_spread < dec_vars_T[undecided[j]]); //Solver.add(dec_vars_T[0] + temporal_spread < dec_vars_T[undecided[j]]);
Solver.add(dec_vars_T[undecided[j]] < 0 || dec_vars_T[0] + temporal_spread < dec_vars_T[undecided[j]]);
} }
} }
else if (is_fixed(0, fixed)) else if (is_fixed(0, fixed))
@ -481,8 +495,9 @@ void introduce_ConsequentialTemporalLepoxAgainstFixed(z3::solver
} }
#endif #endif
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[0].numerator, dec_values_T[0].denominator) + temporal_spread < dec_vars_T[undecided[j]]); //Solver.add(Context.real_val(dec_values_T[0].numerator, dec_values_T[0].denominator) + temporal_spread < dec_vars_T[undecided[j]]);
Solver.add(dec_vars_T[undecided[j]] < 0 || Context.real_val(dec_values_T[0].numerator, dec_values_T[0].denominator) + temporal_spread < dec_vars_T[undecided[j]]);
} }
} }
else else
@ -506,7 +521,8 @@ void introduce_ConsequentialTemporalLepoxAgainstFixed(z3::solver
printf("Undecided --> Undecided: %d --> %d standard\n", undecided[i], next_i); printf("Undecided --> Undecided: %d --> %d standard\n", undecided[i], next_i);
} }
#endif #endif
Solver.add(dec_vars_T[undecided[i]] + temporal_spread < dec_vars_T[next_i] && dec_vars_T[undecided[i]] + temporal_spread + temporal_spread / 2 > dec_vars_T[next_i]); //Solver.add(dec_vars_T[undecided[i]] + temporal_spread < dec_vars_T[next_i] && dec_vars_T[undecided[i]] + temporal_spread + temporal_spread / 2 > dec_vars_T[next_i]);
Solver.add((dec_vars_T[undecided[i]] < 0 || dec_vars_T[next_i] < 0) || dec_vars_T[undecided[i]] + temporal_spread < dec_vars_T[next_i] && dec_vars_T[undecided[i]] + temporal_spread + temporal_spread / 2 > dec_vars_T[next_i]);
} }
/* Undecided --> missing */ /* Undecided --> missing */
else else
@ -520,12 +536,14 @@ void introduce_ConsequentialTemporalLepoxAgainstFixed(z3::solver
{ {
if (i != j) if (i != j)
{ {
Solver.add(dec_vars_T[undecided[j]] + temporal_spread < dec_vars_T[undecided[i]]); //Solver.add(dec_vars_T[undecided[j]] + temporal_spread < dec_vars_T[undecided[i]]);
Solver.add(dec_vars_T[undecided[j]] < 0 || dec_vars_T[undecided[j]] + temporal_spread < dec_vars_T[undecided[i]]);
} }
} }
for (unsigned int j = 0; j < fixed.size(); ++j) for (unsigned int j = 0; j < fixed.size(); ++j)
{ {
Solver.add(Context.real_val(dec_values_T[fixed[j]].numerator, dec_values_T[fixed[j]].denominator) + temporal_spread < dec_vars_T[undecided[i]]); //Solver.add(Context.real_val(dec_values_T[fixed[j]].numerator, dec_values_T[fixed[j]].denominator) + temporal_spread < dec_vars_T[undecided[i]]);
Solver.add(dec_vars_T[undecided[i]] < 0 || Context.real_val(dec_values_T[fixed[j]].numerator, dec_values_T[fixed[j]].denominator) + temporal_spread < dec_vars_T[undecided[i]]);
} }
} }
} }
@ -544,8 +562,12 @@ void introduce_ConsequentialTemporalLepoxAgainstFixed(z3::solver
printf("Fixed --> Undecided: %d --> %d standard\n", fixed[i], next_i); printf("Fixed --> Undecided: %d --> %d standard\n", fixed[i], next_i);
} }
#endif #endif
/*
Solver.add( Context.real_val(dec_values_T[fixed[i]].numerator, dec_values_T[fixed[i]].denominator) + temporal_spread < dec_vars_T[next_i] Solver.add( Context.real_val(dec_values_T[fixed[i]].numerator, dec_values_T[fixed[i]].denominator) + temporal_spread < dec_vars_T[next_i]
&& Context.real_val(dec_values_T[fixed[i]].numerator, dec_values_T[fixed[i]].denominator) + temporal_spread + temporal_spread / 2 > dec_vars_T[next_i]); && Context.real_val(dec_values_T[fixed[i]].numerator, dec_values_T[fixed[i]].denominator) + temporal_spread + temporal_spread / 2 > dec_vars_T[next_i]);
*/
Solver.add(dec_vars_T[next_i] < 0 || ( Context.real_val(dec_values_T[fixed[i]].numerator, dec_values_T[fixed[i]].denominator) + temporal_spread < dec_vars_T[next_i]
&& Context.real_val(dec_values_T[fixed[i]].numerator, dec_values_T[fixed[i]].denominator) + temporal_spread + temporal_spread / 2 > dec_vars_T[next_i]));
} }
/* Fixed --> Fixed */ /* Fixed --> Fixed */
else if (is_fixed(next_i, fixed)) else if (is_fixed(next_i, fixed))
@ -557,8 +579,12 @@ void introduce_ConsequentialTemporalLepoxAgainstFixed(z3::solver
#endif #endif
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) + temporal_spread < dec_vars_T[undecided[j]]); || Context.real_val(dec_values_T[next_i].numerator, dec_values_T[next_i].denominator) + temporal_spread < dec_vars_T[undecided[j]]);
*/
Solver.add(dec_vars_T[undecided[j]] < 0 || ( 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) + temporal_spread < dec_vars_T[undecided[j]]));
} }
} }
} }
@ -1431,7 +1457,7 @@ void assume_PointInsidePolygon(z3::context &Context,
z3::expr inside_half_plane( (normal.x() * dec_var_X) z3::expr inside_half_plane( (normal.x() * dec_var_X)
+ (normal.y() * dec_var_Y) + (normal.y() * dec_var_Y)
- (normal.x() * line.a.x()) - (normal.x() * line.a.x())
- (normal.y() * line.a.y()) < 0); - (normal.y() * line.a.y()) < 0);
if (point == polygon.points.begin()) if (point == polygon.points.begin())
{ {
@ -1442,7 +1468,6 @@ void assume_PointInsidePolygon(z3::context &Context,
in_conjunction = in_conjunction && inside_half_plane; in_conjunction = in_conjunction && inside_half_plane;
} }
} }
constraints.push_back(in_conjunction); constraints.push_back(in_conjunction);
} }
} }
@ -9488,8 +9513,6 @@ bool optimize_ConsequentialWeakPolygonNonoverlappingBinaryCentered(z3::solver
bool size_solvable = false; bool size_solvable = false;
z3::expr_vector bounding_box_assumptions(Context);
coord_t box_min_x = (_outer_half_box.min.x() + _inner_half_box.min.x()) / 2; coord_t box_min_x = (_outer_half_box.min.x() + _inner_half_box.min.x()) / 2;
coord_t box_max_x = (_outer_half_box.max.x() + _inner_half_box.max.x()) / 2; coord_t box_max_x = (_outer_half_box.max.x() + _inner_half_box.max.x()) / 2;
@ -9770,6 +9793,8 @@ bool optimize_ConsequentialWeakPolygonNonoverlappingBinaryCentered(z3::solver
std::vector<Rational> local_dec_values_Y = dec_values_Y; std::vector<Rational> local_dec_values_Y = dec_values_Y;
std::vector<Rational> local_dec_values_T = dec_values_T; std::vector<Rational> local_dec_values_T = dec_values_T;
assert(inner_half_polygon.points.size() == solver_configuration.plate_bounding_polygon.points.size());
Polygon _inner_half_polygon = inner_half_polygon; Polygon _inner_half_polygon = inner_half_polygon;
Polygon _outer_half_polygon = solver_configuration.plate_bounding_polygon; Polygon _outer_half_polygon = solver_configuration.plate_bounding_polygon;
@ -9839,7 +9864,6 @@ bool optimize_ConsequentialWeakPolygonNonoverlappingBinaryCentered(z3::solver
bool size_solvable = false; bool size_solvable = false;
z3::expr_vector bounding_box_assumptions(Context);
Polygon bounding_polygon; Polygon bounding_polygon;
for (unsigned int i = 0; i < _outer_half_polygon.points.size(); ++i) for (unsigned int i = 0; i < _outer_half_polygon.points.size(); ++i)
@ -9883,7 +9907,7 @@ bool optimize_ConsequentialWeakPolygonNonoverlappingBinaryCentered(z3::solver
undecided, undecided,
polygons, polygons,
unreachable_polygons)) unreachable_polygons))
{ {
switch (Solver.check(complete_assumptions)) switch (Solver.check(complete_assumptions))
{ {
case z3::sat: case z3::sat:
@ -11102,7 +11126,7 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
BoundingBox inner_half_box({box_center_x, box_center_y}, {box_center_x, box_center_y}); BoundingBox inner_half_box({box_center_x, box_center_y}, {box_center_x, box_center_y});
for (unsigned int curr_polygon = 0; curr_polygon < polygons.size(); /* nothing */) for (unsigned int curr_polygon = 0; curr_polygon < polygons.size(); /* nothing */)
{ {
bool optimized = false; bool optimized = false;
z3::set_param("timeout", solver_configuration.optimization_timeout.c_str()); z3::set_param("timeout", solver_configuration.optimization_timeout.c_str());
@ -11311,7 +11335,7 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
if (!optimized) if (!optimized)
{ {
if (curr_polygon <= 0) if (curr_polygon <= 0)
{ {
return false; return false;
} }
else else
@ -11328,7 +11352,6 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
return true; return true;
} }
} }
assert(remaining_polygons.empty());
} }
assert(remaining_polygons.empty()); assert(remaining_polygons.empty());
@ -11398,7 +11421,7 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
} }
for (unsigned int curr_polygon = 0; curr_polygon < solvable_objects.size(); /* nothing */) for (unsigned int curr_polygon = 0; curr_polygon < solvable_objects.size(); /* nothing */)
{ {
bool optimized = false; bool optimized = false;
z3::set_param("timeout", solver_configuration.optimization_timeout.c_str()); z3::set_param("timeout", solver_configuration.optimization_timeout.c_str());
@ -11477,12 +11500,11 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
polygons, polygons,
lepox_to_next, lepox_to_next,
trans_bed_lepox); trans_bed_lepox);
std::vector<int> missing; std::vector<int> missing;
std::vector<int> remaining_local; std::vector<int> remaining_local;
while(object_group_size > 0) while(object_group_size > 0)
{ {
z3::expr_vector presence_assumptions(z_context); z3::expr_vector presence_assumptions(z_context);
assume_ConsequentialObjectPresence(z_context, local_dec_vars_T, undecided, missing, presence_assumptions); assume_ConsequentialObjectPresence(z_context, local_dec_vars_T, undecided, missing, presence_assumptions);
@ -11493,6 +11515,11 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
{ {
printf(" %d\n", undecided[j]); printf(" %d\n", undecided[j]);
} }
printf("Missing\n");
for (unsigned int j = 0; j < missing.size(); ++j)
{
printf(" %d\n", missing[j]);
}
printf("Decided\n"); printf("Decided\n");
for (unsigned int j = 0; j < decided_polygons.size(); ++j) for (unsigned int j = 0; j < decided_polygons.size(); ++j)
{ {
@ -11579,7 +11606,7 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
} }
if (optimized) if (optimized)
{ {
for (unsigned int i = 0; i < undecided.size(); ++i) for (unsigned int i = 0; i < undecided.size(); ++i)
{ {
dec_values_X[undecided[i]] = local_values_X[undecided[i]]; dec_values_X[undecided[i]] = local_values_X[undecided[i]];
@ -11650,7 +11677,6 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
return true; return true;
} }
} }
assert(remaining_polygons.empty());
} }
assert(remaining_polygons.empty()); assert(remaining_polygons.empty());