GitHub-Proxy/PrusaSlicer
1
0
Fork 0
mirror of https://git.mirrors.martin98.com/https://github.com/prusa3d/PrusaSlicer.git synced 2025-09-15 20:53:13 +08:00
Code Issues Actions Packages Projects Releases Wiki Activity

Bug fixes and improvements of progress bar and making test more automated.

Browse Source
This commit is contained in:
surynek 2024-12-01 19:06:25 +01:00 committed by Lukas Matena
parent 3c40a68f16
commit c8769e9b70
9 changed files with 840 additions and 1069 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
src/libseqarrange/src/seq_interface.cpp
View File

@ -379,9 +379,8 @@ void schedule_ObjectsForSequentialPrint(const SolverConfiguration &solver
}
#endif
int progress_objects_done = 0;
int progress_object_phases_done = 0;
int progress_object_phases_total = objects_to_print.size() * SEQ_PROGRESS_PHASES_PER_OBJECT;
int progress_object_phases_total = SEQ_MAKE_EXTRA_PROGRESS((objects_to_print.size() * SEQ_PROGRESS_PHASES_PER_OBJECT));
do
{
@ -398,7 +397,6 @@ void schedule_ObjectsForSequentialPrint(const SolverConfiguration &solver
bool optimized;
printf("Object phases A1: %d, %d\n", progress_object_phases_done, solvable_objects.size());
optimized = optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(solver_configuration,
poly_positions_X,
poly_positions_Y,
@ -409,7 +407,6 @@ void schedule_ObjectsForSequentialPrint(const SolverConfiguration &solver
progress_object_phases_done,
progress_object_phases_total,
progress_callback);
printf("Object phases A2: %d,%d,%d\n", progress_object_phases_done, decided_polygons.size(), remaining_polygons.size());
#ifdef DEBUG
{
@ -457,16 +454,6 @@ void schedule_ObjectsForSequentialPrint(const SolverConfiguration &solver
scheduled_plate.scheduled_objects.push_back(ScheduledObject(original_index->second, X, Y));
}
printf("Object phases B: %d\n", progress_object_phases_done);
/*
if (!decided_polygons.empty())
{
progress_objects_done += decided_polygons.size();
progress_object_phases_done = (progress_object_phases_done % SEQ_PROGRESS_PHASES_PER_OBJECT)
+ progress_objects_done * SEQ_PROGRESS_PHASES_PER_OBJECT;
}
printf("Object phases B1: %d\n", progress_object_phases_done);
*/
}
else
{
@ -508,7 +495,9 @@ void schedule_ObjectsForSequentialPrint(const SolverConfiguration &solver
scheduled_plates.push_back(scheduled_plate);
}
while (!remaining_polygons.empty());
while (!remaining_polygons.empty());
progress_callback(SEQ_PROGRESS_RANGE);
#ifdef PROFILE
{
@ -782,9 +771,8 @@ int schedule_ObjectsForSequentialPrint(const SolverConfiguration &solver_
}
#endif
int progress_objects_done = 0;
int progress_object_phases_done = 0;
int progress_object_phases_total = objects_to_print.size() * SEQ_PROGRESS_PHASES_PER_OBJECT;
int progress_object_phases_total = SEQ_MAKE_EXTRA_PROGRESS((objects_to_print.size() * SEQ_PROGRESS_PHASES_PER_OBJECT));
do
{
@ -858,11 +846,6 @@ int schedule_ObjectsForSequentialPrint(const SolverConfiguration &solver_
scheduled_plate.scheduled_objects.push_back(ScheduledObject(original_index->second, X, Y));
}
if (!decided_polygons.empty())
{
progress_objects_done += decided_polygons.size();
progress_object_phases_done = progress_objects_done * SEQ_PROGRESS_PHASES_PER_OBJECT;
}
}
else
{
@ -902,7 +885,9 @@ int schedule_ObjectsForSequentialPrint(const SolverConfiguration &solver_
scheduled_plates.push_back(scheduled_plate);
}
while (!remaining_polygons.empty());
while (!remaining_polygons.empty());
progress_callback(SEQ_PROGRESS_RANGE);
#ifdef PROFILE
{
@ -1099,8 +1084,8 @@ int schedule_ObjectsForSequentialPrint(const SolverConfiguration
}
#endif
int progress_objects_done = 0;
int progress_objects_total = objects_to_print.size();
int progress_object_phases_done = 0;
int progress_object_phases_total = SEQ_MAKE_EXTRA_PROGRESS((objects_to_print.size() * SEQ_PROGRESS_PHASES_PER_OBJECT));
do
{
@ -1124,8 +1109,8 @@ int schedule_ObjectsForSequentialPrint(const SolverConfiguration
solvable_objects,
decided_polygons,
remaining_polygons,
progress_objects_done,
progress_objects_total,
progress_object_phases_done,
progress_object_phases_total,
progress_callback);
@ -1175,7 +1160,6 @@ int schedule_ObjectsForSequentialPrint(const SolverConfiguration
scheduled_plate.scheduled_objects.push_back(ScheduledObject(original_index->second, X, Y));
}
progress_objects_done += decided_polygons.size();
}
else
{
@ -1215,7 +1199,9 @@ int schedule_ObjectsForSequentialPrint(const SolverConfiguration
scheduled_plates.push_back(scheduled_plate);
}
while (!remaining_polygons.empty());
while (!remaining_polygons.empty());
progress_callback(SEQ_PROGRESS_RANGE);
#ifdef PROFILE
{

69
src/libseqarrange/src/seq_sequential.cpp
View File

@ -8861,7 +8861,12 @@ bool optimize_ConsequentialWeakPolygonNonoverlappingBinaryCentered(z3::solver
std::function<void(int)> progress_callback)
{
z3::set_param("timeout", solver_configuration.optimization_timeout.c_str());
printf("Progress range: %d -- %d\n", progress_range.progress_min, progress_range.progress_max);
#ifdef DEBUG
{
printf("Progress range: %d -- %d\n", progress_range.progress_min, progress_range.progress_max);
}
#endif
coord_t last_solvable_bounding_box_size = -1;
@ -10220,8 +10225,8 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
const std::vector<int> &undecided_polygons,
std::vector<int> &decided_polygons,
std::vector<int> &remaining_polygons,
int objects_done,
int total_objects,
int progress_object_phases_done,
int progress_total_object_phases,
std::function<void(int)> progress_callback)
{
std::vector<std::vector<Slic3r::Polygon> > _unreachable_polygons;
@ -10242,8 +10247,8 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
undecided_polygons,
decided_polygons,
remaining_polygons,
objects_done,
total_objects,
progress_object_phases_done,
progress_total_object_phases,
progress_callback);
}
@ -10420,7 +10425,7 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
}
#endif
progress_callback((SEQ_PROGRESS_RANGE * (decided_polygons.size() + progress_object_phases_done)) / progress_total_object_phases);
progress_callback((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases);
optimized = optimize_ConsequentialWeakPolygonNonoverlappingBinaryCentered(z_solver,
z_context,
@ -10439,8 +10444,10 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
polygons,
unreachable_polygons,
presence_assumptions,
ProgressRange((SEQ_PROGRESS_RANGE * (decided_polygons.size() * SEQ_PROGRESS_PHASES_PER_OBJECT + progress_object_phases_done)) / progress_total_object_phases,
(SEQ_PROGRESS_RANGE * (decided_polygons.size() * SEQ_PROGRESS_PHASES_PER_OBJECT + (progress_object_phases_done + 1))) / progress_total_object_phases),
(progress_object_phases_done < progress_total_object_phases ?
ProgressRange((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases,
(SEQ_PROGRESS_RANGE * (progress_object_phases_done + 1)) / progress_total_object_phases) :
ProgressRange(SEQ_PROGRESS_RANGE, SEQ_PROGRESS_RANGE)),
progress_callback);
if (optimized)
@ -10459,6 +10466,12 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
dec_values_Y[undecided[i]] = local_values_Y[undecided[i]];
dec_values_T[undecided[i]] = local_values_T[undecided[i]];
decided_polygons.push_back(undecided[i]);
if (progress_object_phases_done < progress_total_object_phases)
{
int progress_phase_starter = progress_object_phases_done % SEQ_PROGRESS_PHASES_PER_OBJECT;
progress_object_phases_done += progress_phase_starter > 0 ? SEQ_PROGRESS_PHASES_PER_OBJECT - progress_phase_starter : SEQ_PROGRESS_PHASES_PER_OBJECT;
}
}
augment_TemporalSpread(solver_configuration, dec_values_T, decided_polygons);
@ -10468,10 +10481,10 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
}
else
{
progress_callback((SEQ_PROGRESS_RANGE * (decided_polygons.size() * SEQ_PROGRESS_PHASES_PER_OBJECT + progress_object_phases_done)) / progress_total_object_phases);
progress_callback((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases);
return true;
}
progress_callback((SEQ_PROGRESS_RANGE * (decided_polygons.size() * SEQ_PROGRESS_PHASES_PER_OBJECT + progress_object_phases_done)) / progress_total_object_phases);
progress_callback((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases);
break;
}
else
@ -10481,14 +10494,17 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
printf("Remaining polygon: %d\n", curr_polygon + object_group_size - 1);
}
#endif
++progress_object_phases_done;
if (progress_object_phases_done < progress_total_object_phases)
{
++progress_object_phases_done;
}
remaining_local.push_back(undecided_polygons[curr_polygon + object_group_size - 1]);
}
missing.push_back(undecided.back());
undecided.pop_back();
--object_group_size;
progress_callback((SEQ_PROGRESS_RANGE * (decided_polygons.size() * SEQ_PROGRESS_PHASES_PER_OBJECT + progress_object_phases_done)) / progress_total_object_phases);
progress_callback((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases);
}
std::reverse(remaining_local.begin(), remaining_local.end());
@ -10704,7 +10720,6 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
}
#endif
printf("Top call 1\n");
progress_callback((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases);
optimized = optimize_ConsequentialWeakPolygonNonoverlappingBinaryCentered(z_solver,
@ -10724,14 +10739,14 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
polygons,
unreachable_polygons,
presence_assumptions,
ProgressRange((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases,
(SEQ_PROGRESS_RANGE * (progress_object_phases_done + SEQ_PROGRESS_PHASES_PER_OBJECT / 2)) / progress_total_object_phases),
(progress_object_phases_done < progress_total_object_phases ?
ProgressRange((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases,
(SEQ_PROGRESS_RANGE * (progress_object_phases_done + 1)) / progress_total_object_phases) :
ProgressRange(SEQ_PROGRESS_RANGE, SEQ_PROGRESS_RANGE)),
progress_callback);
printf("Optimo: %d\n", optimized);
if (optimized)
{
printf("alpha 1\n");
/*
printf("Printing solver status:\n");
cout << z_solver << "\n";
@ -10747,8 +10762,11 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
dec_values_T[undecided[i]] = local_values_T[undecided[i]];
decided_polygons.push_back(undecided[i]);
int progress_phase_starter = progress_object_phases_done % SEQ_PROGRESS_PHASES_PER_OBJECT;
progress_object_phases_done += progress_phase_starter > 0 ? SEQ_PROGRESS_PHASES_PER_OBJECT - progress_phase_starter : SEQ_PROGRESS_PHASES_PER_OBJECT;
if (progress_object_phases_done < progress_total_object_phases)
{
int progress_phase_starter = progress_object_phases_done % SEQ_PROGRESS_PHASES_PER_OBJECT;
progress_object_phases_done += progress_phase_starter > 0 ? SEQ_PROGRESS_PHASES_PER_OBJECT - progress_phase_starter : SEQ_PROGRESS_PHASES_PER_OBJECT;
}
}
augment_TemporalSpread(solver_configuration, dec_values_T, decided_polygons);
@ -10758,31 +10776,29 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
}
else
{
printf("Top call 2\n");
progress_callback((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases);
return true;
}
printf("Top call 3\n");
progress_callback((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases);
break;
}
else
{
printf("alpha 2\n");
#ifdef DEBUG
{
printf("Remaining polygon: %d\n", curr_polygon + object_group_size - 1);
}
#endif
printf("Phase increasing\n");
if (progress_object_phases_done < progress_total_object_phases)
{
++progress_object_phases_done;
}
remaining_local.push_back(undecided.back());
}
missing.push_back(undecided.back());
undecided.pop_back();
--object_group_size;
printf("Top call 4\n");
progress_callback((SEQ_PROGRESS_RANGE * progress_object_phases_done) / progress_total_object_phases);
}
@ -10812,15 +10828,12 @@ bool optimize_SubglobalConsequentialPolygonNonoverlappingBinaryCentered(const So
remaining_polygons.push_back(curr_polygon);
}
}
progress_object_phases_done += SEQ_PROGRESS_PHASES_PER_OBJECT / 2;
printf("Complete exit\n");
return true;
}
}
assert(remaining_polygons.empty());
}
assert(remaining_polygons.empty());
printf("Complete exit 2\n");
return true;
}

10
src/libseqarrange/src/seq_sequential.hpp
View File

@ -51,14 +51,18 @@ namespace Sequential
#define SEQ_INTERSECTION_REPULSION_MIN "-0.01"
#define SEQ_INTERSECTION_REPULSION_MAX "1.01"
#define SEQ_TEMPORAL_ABSENCE_THRESHOLD "-16"
#define SEQ_TEMPORAL_PRESENCE_THRESHOLD "16"
#define SEQ_TEMPORAL_PRESENCE_THRESHOLD "16"
#define SEQ_Z3_SOLVER_TIMEOUT "8000"
#define SEQ_Z3_SOLVER_TIMEOUT "8000"
const coord_t SEQ_SVG_SCALE_FACTOR = 50000;
const int SEQ_GROUND_PRESENCE_TIME = 32;
const int SEQ_PROGRESS_RANGE = 100;
const int SEQ_PROGRESS_PHASES_PER_OBJECT = 2;
const int SEQ_PROGRESS_PHASES_PER_OBJECT = 4;
const int SEQ_PROGRESS_EXTRA_PHASES = 4 * SEQ_PROGRESS_PHASES_PER_OBJECT;
const double SEQ_PROGRESS_EXTRA_FACTOR = 1.15;
#define SEQ_MAKE_EXTRA_PROGRESS(x) (((int)((x) * SEQ_PROGRESS_EXTRA_FACTOR / SEQ_PROGRESS_PHASES_PER_OBJECT)) * SEQ_PROGRESS_PHASES_PER_OBJECT)
const int64_t SEQ_RATIONAL_PRECISION = 1000000;
const double SEQ_DECIMATION_TOLERANCE = 400000.0;

2
src/libseqarrange/src/seq_version.hpp
View File

@ -2,6 +2,6 @@
#define __SEQ_VERSION_HPP__
#define SEQ_SEQUENTIAL_BUILD "193"
#define SEQ_SEQUENTIAL_BUILD "200"
#endif /* __SEQ_VERSION_HPP__ */

9
src/libseqarrange/test/seq_test_arrangement.cpp
View File

@ -298,14 +298,12 @@ public:
, high_Obj1_y(space_vars[7])
, high_Obj1_t(time_vars[3])
{
printf("alpha 1\n");
BoolVar low_Obj1_present = expr(*this, low_Obj1_t >= 0);
BoolVar low_Obj2_present = expr(*this, low_Obj2_t >= 0);
BoolVar low_Obj3_present = expr(*this, low_Obj3_t >= 0);
BoolVar high_Obj1_present = expr(*this, high_Obj1_t >= 0);
//BoolVar low_Obj1_above_high_Obj1 = expr(*this, low_Obj1_t >= high_Obj1_t);
printf("alpha 2\n");
BoolVarArgs objects_present(4);
objects_present[0] = low_Obj1_present;
objects_present[1] = low_Obj2_present;
@ -318,7 +316,7 @@ public:
IntVar kine_Obj1_x(kine_vars[0]);
IntVar kine_Obj1_y(kine_vars[1]);
printf("alpha 3\n");
kine_widths[0] = kine_width;
kine_heights[0] = kine_height;
@ -338,7 +336,6 @@ public:
heights[2] = low_Obj3_height;
heights[3] = high_Obj1_height;
//heights[3] = kine_height;
printf("alpha 4\n");
IntVarArgs Xs(4);
Xs[0] = low_Obj1_x;
@ -353,10 +350,8 @@ public:
Ys[2] = low_Obj3_y;
Ys[3] = high_Obj1_y;
//Ys[3] = kine_Obj1_y;
printf("alpha 5\n");
nooverlap(*this, Xs, widths, Ys, heights/*, objects_present*/);
printf("alpha 6\n");
rel(*this, low_Obj1_t >= low_Obj2_t + low_Obj2_duration || low_Obj2_t >= low_Obj1_t + low_Obj1_duration);
rel(*this, low_Obj1_t >= low_Obj3_t + low_Obj3_duration || low_Obj3_t >= low_Obj1_t + low_Obj1_duration);
@ -393,12 +388,10 @@ public:
rel(*this, high_Obj1_t < 10);
rel(*this, high_Obj1_x == 0);
printf("alpha 7\n");
branch(*this, space_vars, INT_VAR_SIZE_MIN(), INT_VAL_MIN());
branch(*this, time_vars, INT_VAR_SIZE_MIN(), INT_VAL_MIN());
branch(*this, kine_vars, INT_VAR_SIZE_MIN(), INT_VAL_MIN());
printf("alpha 8\n");
};
SimpleSequentialProblem(SimpleSequentialProblem &s)

6
src/libseqarrange/test/seq_test_interface.cpp
View File

@ -114,7 +114,7 @@ void save_import_data(const std::string &filename,
/*----------------------------------------------------------------*/
/*
TEST_CASE("Interface test 1", "[Sequential Arrangement Interface]")
{
clock_t start, finish;
@ -246,7 +246,7 @@ TEST_CASE("Interface test 3", "[Sequential Arrangement Interface]")
start = clock();
PrinterGeometry printer_geometry;
int result = load_printer_geometry("printer_geometry.mk4.txt", printer_geometry);
int result = load_printer_geometry("printers/printer_geometry.mk4.txt", printer_geometry);
REQUIRE(result == 0);
if (result != 0)
@ -437,7 +437,7 @@ TEST_CASE("Interface test 5", "[Sequential Arrangement Interface]")
printf("Testing interface 5 ... finished\n");
}
*/
TEST_CASE("Interface test 6", "[Sequential Arrangement Interface]")
{

1022
src/libseqarrange/test/seq_test_polygon.cpp
View File

File diff suppressed because it is too large Load Diff

147
src/libseqarrange/test/seq_test_preprocess.cpp
View File

@ -95,6 +95,7 @@ TEST_CASE("Preprocessing test 1", "[Sequential Arrangement Preprocessing]")
scaleDown_PolygonForSequentialSolver(PRUSA_PART_POLYGONS[i], scale_down_polygon);
test_polygons.push_back(scale_down_polygon);
}
REQUIRE(!test_polygons.empty());
for (unsigned int i = 0; i < test_polygons.size(); ++i)
{
@ -102,10 +103,7 @@ TEST_CASE("Preprocessing test 1", "[Sequential Arrangement Preprocessing]")
Polygon display_polygon = scale_UP(test_polygons[i], 1000, 1000);
preview_svg.draw(display_polygon, "blue");
preview_svg.Close();
getchar();
}
}
finish = clock();
printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC);
@ -164,6 +162,7 @@ TEST_CASE("Preprocessing test 2", "[Sequential Arrangement Preprocessing]")
remaining_polygons);
printf("----> Optimization finished <----\n");
REQUIRE(optimized);
if (optimized)
{
@ -184,21 +183,27 @@ TEST_CASE("Preprocessing test 2", "[Sequential Arrangement Preprocessing]")
{
for (unsigned int i = 0; i < decided_polygons.size(); ++i)
{
/*
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
#ifdef DEBUG
{
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
}
*/
// for (unsigned int j = 0; j < unreachable_polygons[decided_polygons[i]].size(); ++j)
{
/*
for (int k = 0; k < unreachable_polygons[decided_polygons[i]][j].points.size(); ++k)
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
{
printf(" Pxy: %d, %d\n", unreachable_polygons[decided_polygons[i]][j].points[k].x(), unreachable_polygons[decided_polygons[i]][j].points[k].y());
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
}
*/
}
#endif
for (unsigned int j = 0; j < unreachable_polygons[decided_polygons[i]].size(); ++j)
{
#ifdef DEBUG
{
for (int k = 0; k < unreachable_polygons[decided_polygons[i]][j].points.size(); ++k)
{
printf(" Pxy: %d, %d\n", unreachable_polygons[decided_polygons[i]][j].points[k].x(), unreachable_polygons[decided_polygons[i]][j].points[k].y());
}
}
#endif
Polygon display_unreachable_polygon = scale_UP(unreachable_polygons[decided_polygons[i]],
poly_positions_X[decided_polygons[i]].as_double(),
poly_positions_Y[decided_polygons[i]].as_double());
@ -291,10 +296,10 @@ TEST_CASE("Preprocessing test 2", "[Sequential Arrangement Preprocessing]")
else
{
printf("Polygon optimization FAILED.\n");
}
finish = clock();
}
finish = clock();
printf("Intermediate time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC);
getchar();
vector<Polygon> next_polygons;
vector<Polygon> next_unreachable_polygons;
@ -350,14 +355,13 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
nozzle_unreachable_polygons.clear();
extend_PolygonConvexUnreachableZone(solver_configuration,
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_NOZZLE_LEVEL_MK3S,
nozzle_unreachable_polygons);
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_NOZZLE_LEVEL_MK3S,
nozzle_unreachable_polygons);
REQUIRE(nozzle_unreachable_polygons.size() > 0);
SVG preview_svg("preprocess_test_3.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
for (unsigned int j = 0; j < SEQ_UNREACHABLE_POLYGON_NOZZLE_LEVEL_MK3S.size(); ++j)
{
preview_svg.draw(SEQ_UNREACHABLE_POLYGON_NOZZLE_LEVEL_MK3S[j], "lightgrey");
@ -373,7 +377,6 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
preview_svg.Close();
getchar();
}
{
@ -383,12 +386,10 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_NOZZLE_LEVEL_MK3S,
nozzle_unreachable_polygons);
REQUIRE(nozzle_unreachable_polygons.size() > 0);
SVG preview_svg("preprocess_test_3.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
for (unsigned int j = 0; j < SEQ_UNREACHABLE_POLYGON_NOZZLE_LEVEL_MK3S.size(); ++j)
{
preview_svg.draw(SEQ_UNREACHABLE_POLYGON_NOZZLE_LEVEL_MK3S[j], "lightgrey");
@ -404,7 +405,6 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
preview_svg.draw(PRUSA_PART_POLYGONS[p], "red");
preview_svg.Close();
getchar();
}
{
@ -414,11 +414,10 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_EXTRUDER_LEVEL_MK3S,
extruder_unreachable_polygons);
REQUIRE(extruder_unreachable_polygons.size() > 0);
SVG preview_svg("preprocess_test_3.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
for (unsigned int j = 0; j < SEQ_UNREACHABLE_POLYGON_EXTRUDER_LEVEL_MK3S.size(); ++j)
{
preview_svg.draw(SEQ_UNREACHABLE_POLYGON_EXTRUDER_LEVEL_MK3S[j], "lightgrey");
@ -434,7 +433,6 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
preview_svg.draw(PRUSA_PART_POLYGONS[p], "green");
preview_svg.Close();
getchar();
}
{
@ -444,12 +442,10 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_EXTRUDER_LEVEL_MK3S,
extruder_unreachable_polygons);
REQUIRE(extruder_unreachable_polygons.size() > 0);
SVG preview_svg("preprocess_test_3.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
for (unsigned int j = 0; j < SEQ_UNREACHABLE_POLYGON_EXTRUDER_LEVEL_MK3S.size(); ++j)
{
preview_svg.draw(SEQ_UNREACHABLE_POLYGON_EXTRUDER_LEVEL_MK3S[j], "lightgrey");
@ -465,7 +461,6 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
preview_svg.draw(PRUSA_PART_POLYGONS[p], "magenta");
preview_svg.Close();
getchar();
}
{
@ -475,11 +470,10 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_HOSE_LEVEL_MK3S,
hose_unreachable_polygons);
REQUIRE(hose_unreachable_polygons.size() > 0);
SVG preview_svg("preprocess_test_3.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
for (unsigned int j = 0; j < SEQ_UNREACHABLE_POLYGON_HOSE_LEVEL_MK3S.size(); ++j)
{
preview_svg.draw(SEQ_UNREACHABLE_POLYGON_HOSE_LEVEL_MK3S[j], "lightgrey");
@ -495,7 +489,6 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
preview_svg.draw(PRUSA_PART_POLYGONS[p], "yellow");
preview_svg.Close();
getchar();
}
{
@ -505,12 +498,10 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_HOSE_LEVEL_MK3S,
hose_unreachable_polygons);
REQUIRE(hose_unreachable_polygons.size() > 0);
SVG preview_svg("preprocess_test_3.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
for (unsigned int j = 0; j < SEQ_UNREACHABLE_POLYGON_HOSE_LEVEL_MK3S.size(); ++j)
{
preview_svg.draw(SEQ_UNREACHABLE_POLYGON_HOSE_LEVEL_MK3S[j], "lightgrey");
@ -526,7 +517,6 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
preview_svg.draw(PRUSA_PART_POLYGONS[p], "orange");
preview_svg.Close();
getchar();
}
{
@ -536,11 +526,10 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_GANTRY_LEVEL_MK3S,
gantry_unreachable_polygons);
REQUIRE(gantry_unreachable_polygons.size() > 0);
SVG preview_svg("preprocess_test_3.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
for (unsigned int j = 0; j < SEQ_UNREACHABLE_POLYGON_GANTRY_LEVEL_MK3S.size(); ++j)
{
preview_svg.draw(SEQ_UNREACHABLE_POLYGON_GANTRY_LEVEL_MK3S[j], "lightgrey");
@ -556,7 +545,6 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
preview_svg.draw(PRUSA_PART_POLYGONS[p], "grey");
preview_svg.Close();
getchar();
}
{
@ -566,12 +554,10 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
PRUSA_PART_POLYGONS[p],
SEQ_UNREACHABLE_POLYGON_GANTRY_LEVEL_MK3S,
gantry_unreachable_polygons);
REQUIRE(gantry_unreachable_polygons.size() > 0);
SVG preview_svg("preprocess_test_3.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
for (unsigned int j = 0; j < SEQ_UNREACHABLE_POLYGON_GANTRY_LEVEL_MK3S.size(); ++j)
{
preview_svg.draw(SEQ_UNREACHABLE_POLYGON_GANTRY_LEVEL_MK3S[j], "lightgrey");
@ -587,7 +573,6 @@ TEST_CASE("Preprocessing test 3", "[Sequential Arrangement Preprocessing]")
preview_svg.draw(PRUSA_PART_POLYGONS[p], "black");
preview_svg.Close();
getchar();
}
}
@ -611,7 +596,7 @@ TEST_CASE("Preprocessing test 4", "[Sequential Arrangement Preprocessing]")
std::vector<Slic3r::Polygon> polygons;
std::vector<std::vector<Slic3r::Polygon> > unreachable_polygons;
for (int i = 0; i < 12/*PRUSA_PART_POLYGONS.size()*/; ++i)
for (int i = 0; i < 12; ++i)
{
Polygon scale_down_polygon;
scaleDown_PolygonForSequentialSolver(PRUSA_PART_POLYGONS[i], scale_down_polygon);
@ -663,6 +648,7 @@ TEST_CASE("Preprocessing test 4", "[Sequential Arrangement Preprocessing]")
remaining_polygons);
printf("----> Optimization finished <----\n");
REQUIRE(optimized);
if (optimized)
{
@ -683,21 +669,25 @@ TEST_CASE("Preprocessing test 4", "[Sequential Arrangement Preprocessing]")
{
for (unsigned int i = 0; i < decided_polygons.size(); ++i)
{
/*
#ifdef DEBUG
{
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
{
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
}
*/
}
#endif
for (unsigned int j = 0; j < unreachable_polygons[decided_polygons[i]].size(); ++j)
{
/*
#ifdef DEBUG
{
for (int k = 0; k < unreachable_polygons[decided_polygons[i]][j].points.size(); ++k)
{
printf(" Pxy: %d, %d\n", unreachable_polygons[decided_polygons[i]][j].points[k].x(), unreachable_polygons[decided_polygons[i]][j].points[k].y());
}
*/
#endif
Polygon display_unreachable_polygon = scale_UP(unreachable_polygons[decided_polygons[i]][j],
poly_positions_X[decided_polygons[i]].as_double(),
poly_positions_Y[decided_polygons[i]].as_double());
@ -793,7 +783,6 @@ TEST_CASE("Preprocessing test 4", "[Sequential Arrangement Preprocessing]")
}
finish = clock();
printf("Intermediate time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC);
getchar();
vector<Polygon> next_polygons;
vector<vector<Polygon> > next_unreachable_polygons;
@ -844,16 +833,14 @@ TEST_CASE("Preprocessing test 5", "[Sequential Arrangement Preprocessing]")
for (unsigned int i = 0; i < PRUSA_PART_POLYGONS.size(); ++i)
{
Polygon simplified_polygon;
Polygon simplified_polygon, scale_down_polygon;
decimate_PolygonForSequentialSolver(solver_configuration,
PRUSA_PART_POLYGONS[i],
simplified_polygon,
false);
/*
scaleDown_PolygonForSequentialSolver(solver_configuration, PRUSA_PART_POLYGONS[i], scale_down_polygon);
polygons.push_back(scale_down_polygon);
false);
REQUIRE(simplified_polygon.size() > 0);
std::vector<Slic3r::Polygon> convex_level_polygons;
convex_level_polygons.push_back(PRUSA_PART_POLYGONS[i]);
convex_level_polygons.push_back(PRUSA_PART_POLYGONS[i]);
@ -868,17 +855,15 @@ TEST_CASE("Preprocessing test 5", "[Sequential Arrangement Preprocessing]")
SEQ_UNREACHABLE_POLYGON_CONVEX_LEVELS_MK3S,
SEQ_UNREACHABLE_POLYGON_BOX_LEVELS_MK3S,
scale_down_unreachable_polygons);
REQUIRE(scale_down_unreachable_polygons.size() > 0);
unreachable_polygons.push_back(scale_down_unreachable_polygons);
*/
SVG preview_svg("preprocess_test_5.svg");
//preview_svg.draw(PRUSA_PART_POLYGONS[p], "blue");
preview_svg.draw(simplified_polygon, "lightgrey");
preview_svg.draw(PRUSA_PART_POLYGONS[i], "blue");
preview_svg.Close();
getchar();
}
finish = clock();
@ -958,6 +943,7 @@ TEST_CASE("Preprocessing test 6", "[Sequential Arrangement Preprocessing]")
remaining_polygons);
printf("----> Optimization finished <----\n");
REQUIRE(optimized);
if (optimized)
{
@ -978,21 +964,25 @@ TEST_CASE("Preprocessing test 6", "[Sequential Arrangement Preprocessing]")
{
for (unsigned int i = 0; i < decided_polygons.size(); ++i)
{
/*
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
{
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
#ifdef DEBUG
{
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
{
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
}
}
*/
#endif
for (unsigned int j = 0; j < unreachable_polygons[decided_polygons[i]].size(); ++j)
{
/*
for (int k = 0; k < unreachable_polygons[decided_polygons[i]][j].points.size(); ++k)
{
printf(" Pxy: %d, %d\n", unreachable_polygons[decided_polygons[i]][j].points[k].x(), unreachable_polygons[decided_polygons[i]][j].points[k].y());
#ifdef DEBUG
{
for (int k = 0; k < unreachable_polygons[decided_polygons[i]][j].points.size(); ++k)
{
printf(" Pxy: %d, %d\n", unreachable_polygons[decided_polygons[i]][j].points[k].x(), unreachable_polygons[decided_polygons[i]][j].points[k].y());
}
}
*/
#endif
Polygon display_unreachable_polygon = scale_UP(unreachable_polygons[decided_polygons[i]][j],
poly_positions_X[decided_polygons[i]].as_double(),
poly_positions_Y[decided_polygons[i]].as_double());
@ -1088,7 +1078,6 @@ TEST_CASE("Preprocessing test 6", "[Sequential Arrangement Preprocessing]")
}
finish = clock();
printf("Intermediate time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC);
getchar();
vector<Polygon> next_polygons;
vector<vector<Polygon> > next_unreachable_polygons;

600
src/libseqarrange/test/seq_test_sequential.cpp
View File

@ -89,8 +89,6 @@ TEST_CASE("Sequential test 1", "[Sequential Arrangement Core]")
z3::expr c(z_context.real_const("cf"));
z3::expr d(z_context.real_const("df"));
// z3::expr lhs(!x || y);
z3::expr lhs(x || y);
z3::expr rhs(implies(x, y));
z3::expr final(lhs == rhs);
@ -108,7 +106,7 @@ TEST_CASE("Sequential test 1", "[Sequential Arrangement Core]")
z3::expr ef1((c > 3 && d < 6) && c < d);
z3::solver z_solver(z_context);
//z_solver.add(!final);
z_solver.add(final2);
z_solver.add(final5);
z_solver.add(ef1);
@ -119,10 +117,12 @@ TEST_CASE("Sequential test 1", "[Sequential Arrangement Core]")
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
bool sat = false;
switch (z_solver.check())
{
case z3::sat:
{
sat = true;
printf(" SATISFIABLE\n");
break;
}
@ -141,6 +141,7 @@ TEST_CASE("Sequential test 1", "[Sequential Arrangement Core]")
break;
}
}
REQUIRE(sat);
z3::model z_model(z_solver.get_model());
printf("Printing model:\n");
@ -161,28 +162,6 @@ TEST_CASE("Sequential test 1", "[Sequential Arrangement Core]")
{
printf(" value: FALSE\n");
}
/*
case Z3_L_FALSE:
{
printf(" value: FALSE\n");
break;
}
case Z3_L_TRUE:
{
printf(" value: TRUE\n");
break;
}
case Z3_L_UNDEF:
{
printf(" value: UNDEF\n");
break;
}
default:
{
break;
}
}
*/
}
printf("Testing sequential scheduling 1 ... finished\n");
@ -296,16 +275,6 @@ TEST_CASE("Sequential test 2", "[Sequential Arrangement Core]")
gantry_rights.push_back(expr(z_context.real_const(name_R.c_str())));
}
// z3::expr lhs(!x || y);
/*
z3::expr final(lhs == rhs);
z3::expr lhs1(a);
z3::expr rhs1(b);
z3::expr final2(lhs1 == rhs1);
z3::expr ef1((c > 3 && d < 6) && c < d);
*/
z3::solver z_solver(z_context);
for (int i = 0; i < complex_Obj_count; ++i)
@ -370,24 +339,28 @@ TEST_CASE("Sequential test 2", "[Sequential Arrangement Core]")
}
}
printf("Printing solver status:\n");
cout << z_solver << "\n";
#ifdef DEBUG
{
printf("Printing solver status:\n");
cout << z_solver << "\n";
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
}
#endif
bool sat = false;
switch (z_solver.check())
{
case z3::sat:
{
sat = true;
printf(" SATISFIABLE\n");
break;
}
case z3::unsat:
{
printf(" UNSATISFIABLE\n");
return;
break;
}
case z3::unknown:
@ -399,53 +372,65 @@ TEST_CASE("Sequential test 2", "[Sequential Arrangement Core]")
{
break;
}
}
}
REQUIRE(!sat);
z3::model z_model(z_solver.get_model());
printf("Printing model:\n");
cout << z_model << "\n";
#ifdef DEBUG
{
z3::model z_model(z_solver.get_model());
printf("Printing model:\n");
cout << z_model << "\n";
}
#endif
finish = clock();
for (unsigned int i = 0; i < z_model.size(); ++i)
{
printf("Variable:%s\n", z_model[i].name().str().c_str());
printf("Printing interpretation:\n");
cout << z_model.get_const_interp(z_model[i]) << "\n";
//cout << float(z_model[i]) << "\n";
/*
switch (z_model.get_const_interp(z_model[i]).bool_value())
{
case Z3_L_FALSE:
{
printf(" value: FALSE\n");
break;
}
case Z3_L_TRUE:
{
printf(" value: TRUE\n");
break;
}
case Z3_L_UNDEF:
{
printf(" value: UNDEF\n");
break;
}
default:
{
break;
}
}
*/
}
for (int i = 0; i < complex_Obj_count; ++i)
#ifdef DEBUG
{
//double val;
//printf("%s\n", z_model.get_const_interp(z_model[i]).get_string().c_str());
}
for (unsigned int i = 0; i < z_model.size(); ++i)
{
printf("Variable:%s\n", z_model[i].name().str().c_str());
printf("Printing interpretation:\n");
cout << z_model.get_const_interp(z_model[i]) << "\n";
cout << float(z_model[i]) << "\n";
switch (z_model.get_const_interp(z_model[i]).bool_value())
{
case Z3_L_FALSE:
{
printf(" value: FALSE\n");
break;
}
case Z3_L_TRUE:
{
printf(" value: TRUE\n");
break;
}
case Z3_L_UNDEF:
{
printf(" value: UNDEF\n");
break;
}
default:
{
break;
}
}
}
}
#endif
#ifdef DEBUG
{
for (int i = 0; i < complex_Obj_count; ++i)
{
double val;
printf("%s\n", z_model.get_const_interp(z_model[i]).get_string().c_str());
}
}
#endif
printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC);
printf("Testing sequential scheduling 2 ... finished\n");
@ -648,23 +633,28 @@ TEST_CASE("Sequential test 3", "[Sequential Arrangement Core]")
}
}
printf("Printing solver status:\n");
cout << z_solver << "\n";
#ifdef DEBUG
{
printf("Printing solver status:\n");
cout << z_solver << "\n";
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
}
#endif
bool sat = false;
switch (z_solver.check())
{
case z3::sat:
{
sat = true;
printf(" SATISFIABLE\n");
break;
}
case z3::unsat:
{
printf(" UNSATISFIABLE\n");
return;
break;
}
case z3::unknown:
@ -676,53 +666,65 @@ TEST_CASE("Sequential test 3", "[Sequential Arrangement Core]")
{
break;
}
}
}
REQUIRE(sat);
z3::model z_model(z_solver.get_model());
printf("Printing model:\n");
cout << z_model << "\n";
#ifdef DEBUG
{
z3::model z_model(z_solver.get_model());
printf("Printing model:\n");
cout << z_model << "\n";
}
#endif
finish = clock();
for (unsigned int i = 0; i < z_model.size(); ++i)
{
printf("Variable:%s\n", z_model[i].name().str().c_str());
printf("Printing interpretation:\n");
cout << z_model.get_const_interp(z_model[i]) << "\n";
//cout << float(z_model[i]) << "\n";
/*
switch (z_model.get_const_interp(z_model[i]).bool_value())
{
case Z3_L_FALSE:
{
printf(" value: FALSE\n");
break;
}
case Z3_L_TRUE:
{
printf(" value: TRUE\n");
break;
}
case Z3_L_UNDEF:
{
printf(" value: UNDEF\n");
break;
}
default:
{
break;
}
}
*/
}
for (int i = 0; i < complex_Obj_count; ++i)
#ifdef DEBUG
{
//double val;
//printf("%s\n", z_model.get_const_interp(z_model[i]).get_string().c_str());
}
for (unsigned int i = 0; i < z_model.size(); ++i)
{
printf("Variable:%s\n", z_model[i].name().str().c_str());
printf("Printing interpretation:\n");
cout << z_model.get_const_interp(z_model[i]) << "\n";
cout << float(z_model[i]) << "\n";
switch (z_model.get_const_interp(z_model[i]).bool_value())
{
case Z3_L_FALSE:
{
printf(" value: FALSE\n");
break;
}
case Z3_L_TRUE:
{
printf(" value: TRUE\n");
break;
}
case Z3_L_UNDEF:
{
printf(" value: UNDEF\n");
break;
}
default:
{
break;
}
}
}
}
#endif
#ifdef DEBUG
{
for (int i = 0; i < complex_Obj_count; ++i)
{
double val;
printf("%s\n", z_model.get_const_interp(z_model[i]).get_string().c_str());
}
}
#endif
printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC);
printf("Testing sequential scheduling 3 ... finished\n");
@ -810,7 +812,6 @@ TEST_CASE("Sequential test 4", "[Sequential Arrangement Core]")
}
z3::set_param("parallel.enable", "true");
//Z3_global_param_set("threads", "4");
z3::solver z_solver(z_context);
vector<Polygon> polygons;
@ -833,14 +834,16 @@ TEST_CASE("Sequential test 4", "[Sequential Arrangement Core]")
polygons,
unreachable_polygons);
introduce_TemporalOrdering(z_solver, z_context, T_times, 16, polygons);
printf("Printing solver status:\n");
cout << z_solver << "\n";
/*
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
*/
#ifdef DEBUG
{
printf("Printing solver status:\n");
cout << z_solver << "\n";
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
}
#endif
int last_solvable_bounding_box_size = -1;
double poly_1_pos_x, poly_1_pos_y, poly_2_pos_x, poly_2_pos_y, poly_3_pos_x, poly_3_pos_y, poly_4_pos_x, poly_4_pos_y;
@ -894,10 +897,13 @@ TEST_CASE("Sequential test 4", "[Sequential Arrangement Core]")
if (sat)
{
z3::model z_model(z_solver.get_model());
/*
printf("Printing model:\n");
cout << z_model << "\n";
*/
#ifdef DEBUG
{
printf("Printing model:\n");
cout << z_model << "\n";
}
#endif
printf("Printing interpretation:\n");
for (unsigned int i = 0; i < z_model.size(); ++i)
@ -1013,7 +1019,6 @@ TEST_CASE("Sequential test 4", "[Sequential Arrangement Core]")
if (refined)
{
printf("alpha 1\n");
switch (z_solver.check(bounding_box_assumptions))
{
case z3::sat:
@ -1038,19 +1043,25 @@ TEST_CASE("Sequential test 4", "[Sequential Arrangement Core]")
break;
}
}
printf("alpha 2: %d\n", (int)refined_sat);
if (refined_sat)
{
z3::model z_model(z_solver.get_model());
/*
printf("Printing model:\n");
cout << z_model << "\n";
*/
#ifdef DEBUG
{
printf("Printing model:\n");
cout << z_model << "\n";
}
#endif
for (unsigned int i = 0; i < z_model.size(); ++i)
{
//printf("Variable:%s ", z_model[i].name().str().c_str());
#ifdef DEBUG
{
printf("Variable:%s ", z_model[i].name().str().c_str());
}
#endif
double value = z_model.get_const_interp(z_model[i]).as_double();
if (z_model[i].name().str() == "x_pos-0")
@ -1147,35 +1158,11 @@ TEST_CASE("Sequential test 4", "[Sequential Arrangement Core]")
{
break;
}
//cout << float(z_model[i]) << "\n";
/*
switch (z_model.get_const_interp(z_model[i]).bool_value())
{
case Z3_L_FALSE:
{
printf(" value: FALSE\n");
break;
}
case Z3_L_TRUE:
{
printf(" value: TRUE\n");
break;
}
case Z3_L_UNDEF:
{
printf(" value: UNDEF\n");
break;
}
default:
{
break;
}
}
*/
}
finish = clock();
REQUIRE(last_solvable_bounding_box_size > 0);
printf("Solvable bounding box: %d\n", last_solvable_bounding_box_size);
printf("Final spatio-temporal positions: %.3f, %.3f [%.3f], %.3f, %.3f [%.3f], %.3f, %.3f [%.3f], %.3f, %.3f [%.3f]\n",
@ -1192,16 +1179,18 @@ TEST_CASE("Sequential test 4", "[Sequential Arrangement Core]")
_poly_4_pos_y,
_time_4_t);
/*
for (int i = 0; i < 2; ++i)
{
double value = X_positions[i];
printf("Orig X: %.3f\n", value);
#ifdef DEBUG
{
for (int i = 0; i < 2; ++i)
{
double value = X_positions[i];
printf("Orig X: %.3f\n", value);
value = Y_positions[i];
printf("Orig Y: %.3f\n", value);
value = Y_positions[i];
printf("Orig Y: %.3f\n", value);
}
}
*/
#endif
SVG preview_svg("sequential_test_4.svg");
@ -1270,10 +1259,8 @@ TEST_CASE("Sequential test 5", "[Sequential Arrangement Core]")
T_times.push_back(expr(z_context.real_const(name.c_str())));
}
z3::solver z_solver(z_context);
z3::solver z_solver(z_context);
Z3_global_param_set("parallel.enable", "false");
//Z3_global_param_set("threads", "4");
vector<Polygon> polygons;
polygons.push_back(polygon_1);
@ -1304,10 +1291,12 @@ TEST_CASE("Sequential test 5", "[Sequential Arrangement Core]")
printf("Printing solver status:\n");
cout << z_solver << "\n";
/*
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
*/
#ifdef DEBUG
{
printf("Printing smt status:\n");
cout << z_solver.to_smt2() << "\n";
}
#endif
int last_solvable_bounding_box_size = -1;
Rational poly_1_pos_x, poly_1_pos_y, poly_2_pos_x, poly_2_pos_y, poly_3_pos_x, poly_3_pos_y, poly_4_pos_x, poly_4_pos_y;
@ -1357,10 +1346,13 @@ TEST_CASE("Sequential test 5", "[Sequential Arrangement Core]")
{
z3::model z_model(z_solver.get_model());
/*
printf("Printing model:\n");
cout << z_model << "\n";
*/
#ifdef DEBUG
{
printf("Printing model:\n");
cout << z_model << "\n";
}
#endif
printf("Printing interpretation:\n");
for (unsigned int i = 0; i < z_model.size(); ++i)
{
@ -1422,21 +1414,6 @@ TEST_CASE("Sequential test 5", "[Sequential Arrangement Core]")
}
}
/*
_poly_1_pos_x = poly_1_pos_x;
_poly_1_pos_y = poly_1_pos_y;
_time_1_t = time_1_t;
_poly_2_pos_x = poly_2_pos_x;
_poly_2_pos_y = poly_2_pos_y;
_time_2_t = time_2_t;
_poly_3_pos_x = poly_3_pos_x;
_poly_3_pos_y = poly_3_pos_y;
_time_3_t = time_3_t;
_poly_4_pos_x = poly_4_pos_x;
_poly_4_pos_y = poly_4_pos_y;
_time_4_t = time_4_t;
*/
printf("Times: %.3f, %.3f, %.3f, %3f\n",
time_1_t.as_double(),
time_2_t.as_double(),
@ -1492,7 +1469,6 @@ TEST_CASE("Sequential test 5", "[Sequential Arrangement Core]")
if (refined)
{
printf("alpha 1\n");
switch (z_solver.check(bounding_box_assumptions))
{
case z3::sat:
@ -1517,15 +1493,17 @@ TEST_CASE("Sequential test 5", "[Sequential Arrangement Core]")
break;
}
}
printf("alpha 2: %d\n", (int)refined_sat);
if (refined_sat)
{
z3::model z_model(z_solver.get_model());
/*
printf("Printing model:\n");
cout << z_model << "\n";
*/
#ifdef DEBUG
{
printf("Printing model:\n");
cout << z_model << "\n";
}
#endif
for (unsigned int i = 0; i < z_model.size(); ++i)
{
@ -1629,35 +1607,10 @@ TEST_CASE("Sequential test 5", "[Sequential Arrangement Core]")
{
break;
}
//cout << float(z_model[i]) << "\n";
/*
switch (z_model.get_const_interp(z_model[i]).bool_value())
{
case Z3_L_FALSE:
{
printf(" value: FALSE\n");
break;
}
case Z3_L_TRUE:
{
printf(" value: TRUE\n");
break;
}
case Z3_L_UNDEF:
{
printf(" value: UNDEF\n");
break;
}
default:
{
break;
}
}
*/
}
finish = clock();
REQUIRE(last_solvable_bounding_box_size > 0);
printf("Solvable bounding box: %d\n", last_solvable_bounding_box_size);
printf("Final spatio-temporal positions: %.3f, %.3f [%.3f], %.3f, %.3f [%.3f], %.3f, %.3f [%.3f], %.3f, %.3f [%.3f]\n",
@ -1674,16 +1627,20 @@ TEST_CASE("Sequential test 5", "[Sequential Arrangement Core]")
_poly_4_pos_y.as_double(),
_time_4_t.as_double());
/*
for (int i = 0; i < 2; ++i)
{
double value = X_positions[i].as_double();
printf("Orig X: %.3f\n", value);
value = Y_positions[i].as_double();
printf("Orig Y: %.3f\n", value);
#ifdef DEBUG
{
for (int i = 0; i < 2; ++i)
{
double value = X_positions[i].as_double();
printf("Orig X: %.3f\n", value);
value = Y_positions[i].as_double();
printf("Orig Y: %.3f\n", value);
}
}
*/
#endif
SVG preview_svg("sequential_test_5.svg");
@ -1745,28 +1702,6 @@ TEST_CASE("Sequential test 6", "[Sequential Arrangement Core]")
vector<int> polygon_index_map;
vector<int> decided_polygons;
/*
polygons.push_back(polygon_1);
unreachable_polygons.push_back(unreachable_polygon_1);
polygons.push_back(polygon_2);
unreachable_polygons.push_back(unreachable_polygon_2);
polygons.push_back(polygon_3);
unreachable_polygons.push_back(unreachable_polygon_3);
polygons.push_back(polygon_4);
unreachable_polygons.push_back(unreachable_polygon_4);
*/
/*
polygons.push_back(polygon_1);
unreachable_polygons.push_back(polygon_1);
polygons.push_back(polygon_2);
unreachable_polygons.push_back(polygon_2);
polygons.push_back(polygon_3);
unreachable_polygons.push_back(polygon_3);
polygons.push_back(polygon_4);
unreachable_polygons.push_back(polygon_4);
*/
polygons.push_back(polygon_1);
unreachable_polygons.push_back(unreachable_polygon_1);
polygons.push_back(polygon_2);
@ -1812,15 +1747,17 @@ TEST_CASE("Sequential test 6", "[Sequential Arrangement Core]")
polygons.push_back(polygon_4);
unreachable_polygons.push_back(unreachable_polygon_4);
/*
for (int j = 0; j < unreachable_polygons_1.size(); ++j)
#ifdef DEBUG
{
for (int k = 0; k < unreachable_polygons_1[j].points.size(); ++k)
for (int j = 0; j < unreachable_polygons_1.size(); ++j)
{
printf(" Ppxy: %d, %d\n", unreachable_polygons_1[j].points[k].x(), unreachable_polygons_1[j].points[k].y());
for (int k = 0; k < unreachable_polygons_1[j].points.size(); ++k)
{
printf(" Ppxy: %d, %d\n", unreachable_polygons_1[j].points[k].x(), unreachable_polygons_1[j].points[k].y());
}
}
}
*/
#endif
for (unsigned int index = 0; index < polygons.size(); ++index)
{
@ -1831,11 +1768,6 @@ TEST_CASE("Sequential test 6", "[Sequential Arrangement Core]")
vector<Rational> poly_positions_Y;
vector<Rational> times_T;
/*
poly_positions_X.resize(polygons.size());
poly_positions_Y.resize(polygons.size());
*/
do
{
decided_polygons.clear();
@ -1850,16 +1782,8 @@ TEST_CASE("Sequential test 6", "[Sequential Arrangement Core]")
polygon_index_map,
decided_polygons,
remaining_polygons);
REQUIRE(optimized);
/*
bool optimized = optimize_SubglobalPolygonNonoverlapping(solver_configuration,
poly_positions_X,
poly_positions_Y,
polygons,
polygon_index_map,
decided_polygons,
remaining_polygons);
*/
printf("----> Optimization finished <----\n");
if (optimized)
@ -1867,7 +1791,6 @@ TEST_CASE("Sequential test 6", "[Sequential Arrangement Core]")
printf("Polygon positions:\n");
for (unsigned int i = 0; i < decided_polygons.size(); ++i)
{
// printf(" [%d] %.3f, %.3f (%.3f)\n", decided_polygons[i], poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double(), times_T[decided_polygons[i]].as_double());
printf(" [%d] %.3f, %.3f (%.3f)\n", decided_polygons[i], poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double(), times_T[decided_polygons[i]].as_double());
}
printf("Remaining polygons: %ld\n", remaining_polygons.size());
@ -1882,17 +1805,19 @@ TEST_CASE("Sequential test 6", "[Sequential Arrangement Core]")
{
for (unsigned int i = 0; i < decided_polygons.size(); ++i)
{
/*
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
#ifdef DEBUG
{
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
{
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
}
}
*/
#endif
Polygon display_unreachable_polygon = scale_UP(unreachable_polygons[decided_polygons[i]],
poly_positions_X[decided_polygons[i]].as_double(),
poly_positions_Y[decided_polygons[i]].as_double());
//if (decided_polygons[i] != 2)
{
preview_svg.draw(display_unreachable_polygon, "lightgrey");
}
@ -1984,7 +1909,6 @@ TEST_CASE("Sequential test 6", "[Sequential Arrangement Core]")
{
printf("Polygon optimization FAILED.\n");
}
getchar();
vector<Polygon> next_polygons;
vector<Polygon> next_unreachable_polygons;
@ -2053,11 +1977,6 @@ TEST_CASE("Sequential test 7", "[Sequential Arrangement Core]")
polygons.push_back(polygon_3);
unreachable_polygons.push_back(unreachable_polygons_3);
/*
polygons.push_back(polygon_4);
unreachable_polygons.push_back(unreachable_polygons_4);
*/
polygons.push_back(polygon_1);
unreachable_polygons.push_back(unreachable_polygons_1);
polygons.push_back(polygon_2);
@ -2067,43 +1986,17 @@ TEST_CASE("Sequential test 7", "[Sequential Arrangement Core]")
polygons.push_back(polygon_4);
unreachable_polygons.push_back(unreachable_polygons_4);
/*
polygons.push_back(polygon_1);
unreachable_polygons.push_back(unreachable_polygons_1);
polygons.push_back(polygon_2);
unreachable_polygons.push_back(unreachable_polygons_2);
polygons.push_back(polygon_3);
unreachable_polygons.push_back(unreachable_polygons_3);
polygons.push_back(polygon_4);
unreachable_polygons.push_back(unreachable_polygons_4);
polygons.push_back(polygon_1);
unreachable_polygons.push_back(unreachable_polygons_1);
polygons.push_back(polygon_2);
unreachable_polygons.push_back(unreachable_polygons_2);
polygons.push_back(polygon_3);
unreachable_polygons.push_back(unreachable_polygons_3);
polygons.push_back(polygon_4);
unreachable_polygons.push_back(unreachable_polygons_4);
polygons.push_back(polygon_1);
unreachable_polygons.push_back(unreachable_polygons_1);
polygons.push_back(polygon_2);
unreachable_polygons.push_back(unreachable_polygons_2);
polygons.push_back(polygon_3);
unreachable_polygons.push_back(unreachable_polygons_3);
polygons.push_back(polygon_4);
unreachable_polygons.push_back(unreachable_polygons_4);
*/
/*
for (int j = 0; j < unreachable_polygons_1.size(); ++j)
#ifdef DEBUG
{
for (int k = 0; k < unreachable_polygons_1[j].points.size(); ++k)
for (int j = 0; j < unreachable_polygons_1.size(); ++j)
{
printf(" Ppxy: %d, %d\n", unreachable_polygons_1[j].points[k].x(), unreachable_polygons_1[j].points[k].y());
for (int k = 0; k < unreachable_polygons_1[j].points.size(); ++k)
{
printf(" Ppxy: %d, %d\n", unreachable_polygons_1[j].points[k].x(), unreachable_polygons_1[j].points[k].y());
}
}
}
*/
#endif
for (unsigned int index = 0; index < polygons.size(); ++index)
{
@ -2114,11 +2007,6 @@ TEST_CASE("Sequential test 7", "[Sequential Arrangement Core]")
vector<Rational> poly_positions_Y;
vector<Rational> times_T;
/*
poly_positions_X.resize(polygons.size());
poly_positions_Y.resize(polygons.size());
*/
do
{
decided_polygons.clear();
@ -2133,6 +2021,7 @@ TEST_CASE("Sequential test 7", "[Sequential Arrangement Core]")
polygon_index_map,
decided_polygons,
remaining_polygons);
REQUIRE(optimized);
printf("----> Optimization finished <----\n");
@ -2155,21 +2044,27 @@ TEST_CASE("Sequential test 7", "[Sequential Arrangement Core]")
{
for (unsigned int i = 0; i < decided_polygons.size(); ++i)
{
/*
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
#ifdef DEBUG
{
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
printf("----> %.3f,%.3f\n", poly_positions_X[decided_polygons[i]].as_double(), poly_positions_Y[decided_polygons[i]].as_double());
for (int k = 0; k < polygons[decided_polygons[i]].points.size(); ++k)
{
printf(" xy: %d, %d\n", polygons[decided_polygons[i]].points[k].x(), polygons[decided_polygons[i]].points[k].y());
}
}
*/
#endif
for (unsigned int j = 0; j < unreachable_polygons[decided_polygons[i]].size(); ++j)
{
/*
for (int k = 0; k < unreachable_polygons[decided_polygons[i]][j].points.size(); ++k)
#ifdef DEBUG
{
printf(" Pxy: %d, %d\n", unreachable_polygons[decided_polygons[i]][j].points[k].x(), unreachable_polygons[decided_polygons[i]][j].points[k].y());
for (int k = 0; k < unreachable_polygons[decided_polygons[i]][j].points.size(); ++k)
{
printf(" Pxy: %d, %d\n", unreachable_polygons[decided_polygons[i]][j].points[k].x(), unreachable_polygons[decided_polygons[i]][j].points[k].y());
}
}
*/
#endif
Polygon display_unreachable_polygon = scale_UP(unreachable_polygons[decided_polygons[i]][j],
poly_positions_X[decided_polygons[i]].as_double(),
poly_positions_Y[decided_polygons[i]].as_double());
@ -2263,7 +2158,6 @@ TEST_CASE("Sequential test 7", "[Sequential Arrangement Core]")
{
printf("Polygon optimization FAILED.\n");
}
getchar();
vector<Polygon> next_polygons;
vector<vector<Polygon> > next_unreachable_polygons;
@ -2299,5 +2193,5 @@ TEST_CASE("Sequential test 7", "[Sequential Arrangement Core]")
}
/*----------------------------------------------------------------*/
/*----------------------------------------------------------------*/