From c8769e9b7024f949e5a6ef880ee2b45033a834c9 Mon Sep 17 00:00:00 2001 From: surynek Date: Sun, 1 Dec 2024 19:06:25 +0100 Subject: [PATCH] Bug fixes and improvements of progress bar and making test more automated. --- src/libseqarrange/src/seq_interface.cpp | 44 +- src/libseqarrange/src/seq_sequential.cpp | 69 +- src/libseqarrange/src/seq_sequential.hpp | 10 +- src/libseqarrange/src/seq_version.hpp | 2 +- .../test/seq_test_arrangement.cpp | 9 +- src/libseqarrange/test/seq_test_interface.cpp | 6 +- src/libseqarrange/test/seq_test_polygon.cpp | 1022 ++++++++--------- .../test/seq_test_preprocess.cpp | 147 ++- .../test/seq_test_sequential.cpp | 600 ++++------ 9 files changed, 840 insertions(+), 1069 deletions(-) diff --git a/src/libseqarrange/src/seq_interface.cpp b/src/libseqarrange/src/seq_interface.cpp index 2c5c38de57..120ec293af 100644 --- a/src/libseqarrange/src/seq_interface.cpp +++ b/src/libseqarrange/src/seq_interface.cpp @@ -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 { diff --git a/src/libseqarrange/src/seq_sequential.cpp b/src/libseqarrange/src/seq_sequential.cpp index dd0d685864..92907ab452 100644 --- a/src/libseqarrange/src/seq_sequential.cpp +++ b/src/libseqarrange/src/seq_sequential.cpp @@ -8861,7 +8861,12 @@ bool optimize_ConsequentialWeakPolygonNonoverlappingBinaryCentered(z3::solver std::function 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 &undecided_polygons, std::vector &decided_polygons, std::vector &remaining_polygons, - int objects_done, - int total_objects, + int progress_object_phases_done, + int progress_total_object_phases, std::function progress_callback) { std::vector > _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; } diff --git a/src/libseqarrange/src/seq_sequential.hpp b/src/libseqarrange/src/seq_sequential.hpp index 052f0b2dfd..07d4da5cd9 100644 --- a/src/libseqarrange/src/seq_sequential.hpp +++ b/src/libseqarrange/src/seq_sequential.hpp @@ -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; diff --git a/src/libseqarrange/src/seq_version.hpp b/src/libseqarrange/src/seq_version.hpp index 2cb62d53a9..e8bc06c6ee 100644 --- a/src/libseqarrange/src/seq_version.hpp +++ b/src/libseqarrange/src/seq_version.hpp @@ -2,6 +2,6 @@ #define __SEQ_VERSION_HPP__ -#define SEQ_SEQUENTIAL_BUILD "193" +#define SEQ_SEQUENTIAL_BUILD "200" #endif /* __SEQ_VERSION_HPP__ */ diff --git a/src/libseqarrange/test/seq_test_arrangement.cpp b/src/libseqarrange/test/seq_test_arrangement.cpp index acb022d6ae..a297f95cf3 100644 --- a/src/libseqarrange/test/seq_test_arrangement.cpp +++ b/src/libseqarrange/test/seq_test_arrangement.cpp @@ -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) diff --git a/src/libseqarrange/test/seq_test_interface.cpp b/src/libseqarrange/test/seq_test_interface.cpp index 574e5ac74c..c148c76907 100644 --- a/src/libseqarrange/test/seq_test_interface.cpp +++ b/src/libseqarrange/test/seq_test_interface.cpp @@ -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]") { diff --git a/src/libseqarrange/test/seq_test_polygon.cpp b/src/libseqarrange/test/seq_test_polygon.cpp index 56f0e10d6e..10b39fd294 100644 --- a/src/libseqarrange/test/seq_test_polygon.cpp +++ b/src/libseqarrange/test/seq_test_polygon.cpp @@ -48,7 +48,6 @@ using namespace Sequential; /*----------------------------------------------------------------*/ - TEST_CASE("Polygon test 1", "[Polygon]") { printf("Testing polygon 1 ...\n"); @@ -60,6 +59,7 @@ TEST_CASE("Polygon test 1", "[Polygon]") Point point = polygon_1[i]; printf("%d,%d\n", point.x(), point.y()); } + REQUIRE(polygon_1.size() > 0); printf("Testing polygon 1 ... finished\n"); } @@ -89,6 +89,8 @@ TEST_CASE("Polygon test 2", "[Polygon]") printf("hull %d: %d,%d\n", i, point.x(), point.y()); } + REQUIRE(hull_1.size() > 0); + if (hull_1.size() >= 2) { const Point &point_1 = hull_1[0]; @@ -125,14 +127,19 @@ TEST_CASE("Polygon test 2", "[Polygon]") } }; - bool ins1 = is_inside(point_1); + bool ins1 = is_inside(point_1); printf("%s\n", ins1 ? "yes" : "no"); + REQUIRE(ins1); + bool ins2 = is_inside(point_2); - printf("%s\n", ins2 ? "yes" : "no"); + printf("%s\n", ins2 ? "yes" : "no"); + REQUIRE(ins2); + bool ins3 = is_inside(point_1 + point_2); - printf("%s\n", ins3 ? "yes" : "no"); + printf("%s\n", ins3 ? "yes" : "no"); + bool ins4 = is_inside(point_1 - point_2); - printf("%s\n", ins4 ? "yes" : "no"); + printf("%s\n", ins4 ? "yes" : "no"); } } @@ -205,16 +212,22 @@ TEST_CASE("Polygon test 3", "[Polygon]") T_parameters[3], lines[3]); - 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; } @@ -233,11 +246,17 @@ TEST_CASE("Polygon test 3", "[Polygon]") { break; } - } + } + REQUIRE(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 finish = clock(); @@ -246,36 +265,39 @@ TEST_CASE("Polygon test 3", "[Polygon]") { printf("Variable:%s ", z_model[i].name().str().c_str()); - cout << z_model.get_const_interp(z_model[i]).as_double() << "\n"; - double value = z_model.get_const_interp(z_model[i]).as_double(); + #ifdef DEBUG + { + cout << z_model.get_const_interp(z_model[i]).as_double() << "\n"; + double value = z_model.get_const_interp(z_model[i]).as_double(); + + printf("value: %.3f\n", value); - printf("value: %.3f\n", value); - - //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"); + 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; - } - default: - { + } + case Z3_L_TRUE: + { + printf(" value: TRUE\n"); break; - } - } - */ + } + case Z3_L_UNDEF: + { + printf(" value: UNDEF\n"); + break; + } + default: + { + break; + } + } + } + #endif } printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC); @@ -351,10 +373,13 @@ TEST_CASE("Polygon test 4", "[Polygon]") 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; } @@ -373,7 +398,8 @@ TEST_CASE("Polygon test 4", "[Polygon]") { break; } - } + } + REQUIRE(sat); z3::model z_model(z_solver.get_model()); printf("Printing model:\n"); @@ -391,8 +417,8 @@ TEST_CASE("Polygon test 4", "[Polygon]") printf("value: %.3f\n", value); - //cout << float(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: @@ -415,7 +441,6 @@ TEST_CASE("Polygon test 4", "[Polygon]") break; } } - */ } printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC); @@ -486,16 +511,22 @@ TEST_CASE("Polygon test 5", "[Polygon]") Y_positions[1], poly_lines[3]); - 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; } @@ -514,11 +545,16 @@ TEST_CASE("Polygon test 5", "[Polygon]") { break; } - } + } + REQUIRE(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 finish = clock(); @@ -527,36 +563,39 @@ TEST_CASE("Polygon test 5", "[Polygon]") { printf("Variable:%s ", z_model[i].name().str().c_str()); - cout << z_model.get_const_interp(z_model[i]).as_double() << "\n"; - double value = z_model.get_const_interp(z_model[i]).as_double(); + #ifdef DEBUG + { + cout << z_model.get_const_interp(z_model[i]).as_double() << "\n"; + double value = z_model.get_const_interp(z_model[i]).as_double(); + + printf("value: %.3f\n", value); - printf("value: %.3f\n", value); - - //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"); + 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; - } - default: - { + } + case Z3_L_TRUE: + { + printf(" value: TRUE\n"); break; + } + case Z3_L_UNDEF: + { + printf(" value: UNDEF\n"); + break; + } + default: + { + break; + } + } } - } - */ + #endif } printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC); @@ -607,16 +646,22 @@ TEST_CASE("Polygon test 6", "[Polygon]") Y_positions[1], polygon_1); - 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; } @@ -635,54 +680,61 @@ TEST_CASE("Polygon test 6", "[Polygon]") { break; } - } + } + REQUIRE(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 finish = clock(); printf("Printing interpretation:\n"); for (unsigned int i = 0; i < z_model.size(); ++i) { - printf("Variable:%s ", z_model[i].name().str().c_str()); - + printf("Variable:%s ", z_model[i].name().str().c_str()); cout << z_model.get_const_interp(z_model[i]).as_double() << "\n"; - double value = z_model.get_const_interp(z_model[i]).as_double(); z3::expr valo_1 = z_model.get_const_interp(z_model[i]); z3::expr deco_1 = expr(z_context.real_const("deco_1")); z3::expr lino_1 = (valo_1 * deco_1 == 0); + + #ifdef DEBUG + { + printf("value: %.3f\n", value); - printf("value: %.3f\n", value); - - //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"); + 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; - } - default: - { + } + case Z3_L_TRUE: + { + printf(" value: TRUE\n"); break; + } + case Z3_L_UNDEF: + { + printf(" value: UNDEF\n"); + break; + } + default: + { + break; + } + } } - } - */ + #endif } printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC); @@ -755,16 +807,22 @@ TEST_CASE("Polygon test 7", "[Polygon]") Y_positions[1], polygon_2); - 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; } @@ -783,11 +841,17 @@ TEST_CASE("Polygon test 7", "[Polygon]") { break; } - } + } + REQUIRE(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 finish = clock(); @@ -820,51 +884,60 @@ TEST_CASE("Polygon test 7", "[Polygon]") poly_2_pos_y = value; } + #ifdef DEBUG + { + 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 - //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; - } - } - */ } printf("Positions: %.3f, %.3f, %.3f, %.3f\n", poly_1_pos_x, poly_1_pos_y, poly_2_pos_x, poly_2_pos_y); - /* - for (int i = 0; i < 2; ++i) - { - double value = X_positions[i].as_double(); - printf("Orig X: %.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); + value = Y_positi ons[i].as_double(); + printf("Orig Y: %.3f\n", value); + } } - */ + #endif SVG preview_svg("polygon_test_7.svg"); -// preview_svg.draw(polygon_1); -// preview_svg.draw(polygon_2); + #ifdef DEBUG + { + preview_svg.draw(polygon_1); + preview_svg.draw(polygon_2); + } + #endif preview_svg.Close(); @@ -960,11 +1033,6 @@ TEST_CASE("Polygon test 8", "[Polygon]") z3::solver z_solver(z_context); - /* - introduce_DecisionBox(z_solver, X_positions[0], Y_positions[0], 200, 200); - introduce_DecisionBox(z_solver, X_positions[1], Y_positions[1], 200, 200); - */ - introduce_PolygonOutsidePolygon(z_solver, z_context, X_positions[0], @@ -974,17 +1042,6 @@ TEST_CASE("Polygon test 8", "[Polygon]") Y_positions[1], polygon_2); - /* - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[1], - Y_positions[1], - polygon_2, - X_positions[0], - Y_positions[0], - polygon_1); - */ - introduce_PolygonLineNonIntersection(z_solver, z_context, X_positions[0], @@ -1003,17 +1060,6 @@ TEST_CASE("Polygon test 8", "[Polygon]") Y_positions[2], polygon_3); - /* - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[2], - Y_positions[2], - polygon_3, - X_positions[1], - Y_positions[1], - polygon_2); - */ - introduce_PolygonLineNonIntersection(z_solver, z_context, X_positions[1], @@ -1032,17 +1078,6 @@ TEST_CASE("Polygon test 8", "[Polygon]") Y_positions[2], polygon_3); -/* - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[2], - Y_positions[2], - polygon_3, - X_positions[0], - Y_positions[0], - polygon_1); -*/ - introduce_PolygonLineNonIntersection(z_solver, z_context, X_positions[0], @@ -1052,12 +1087,16 @@ TEST_CASE("Polygon test 8", "[Polygon]") Y_positions[2], polygon_3); - - 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 int last_solvable_decision_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; @@ -1072,7 +1111,7 @@ TEST_CASE("Polygon test 8", "[Polygon]") assume_DecisionBox(X_positions[2], Y_positions[2], decision_box_size, decision_box_size, decision_box_assumptions); bool sat = false; - + switch (z_solver.check(decision_box_assumptions)) { case z3::sat: @@ -1102,8 +1141,13 @@ TEST_CASE("Polygon test 8", "[Polygon]") 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) @@ -1144,48 +1188,55 @@ TEST_CASE("Polygon test 8", "[Polygon]") { break; } - - //cout << float(z_model[i]) << "\n"; - /* - switch (z_model.get_const_interp(z_model[i]).bool_value()) + + #ifdef DEBUG { - 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"); + 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; - } - default: - { + } + case Z3_L_TRUE: + { + printf(" value: TRUE\n"); break; + } + case Z3_L_UNDEF: + { + printf(" value: UNDEF\n"); + break; + } + default: + { + break; + } + } } - } - */ + #endif + } finish = clock(); + REQUIRE(last_solvable_decision_box_size > 0); + printf("Solvable decision box: %d\n", last_solvable_decision_box_size); printf("Positions: %.3f, %.3f, %.3f, %.3f, %.3f, %.3f\n", poly_1_pos_x, poly_1_pos_y, poly_2_pos_x, poly_2_pos_y, poly_3_pos_x, poly_3_pos_y); - /* - for (int i = 0; i < 2; ++i) - { - double value = X_positions[i].as_double(); - printf("Orig X: %.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); + value = Y_positions[i].as_double(); + printf("Orig Y: %.3f\n", value); } - */ + #endif SVG preview_svg("polygon_test_8.svg"); @@ -1262,11 +1313,6 @@ TEST_CASE("Polygon test 9", "[Polygon]") z3::solver z_solver(z_context); - /* - introduce_DecisionBox(z_solver, X_positions[0], Y_positions[0], 200, 200); - introduce_DecisionBox(z_solver, X_positions[1], Y_positions[1], 200, 200); - */ - introduce_PolygonOutsidePolygon(z_solver, z_context, X_positions[0], @@ -1275,16 +1321,6 @@ TEST_CASE("Polygon test 9", "[Polygon]") X_positions[1], Y_positions[1], polygon_2); -/* - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[1], - Y_positions[1], - polygon_2, - X_positions[0], - Y_positions[0], - polygon_1); -*/ introduce_PolygonLineNonIntersection(z_solver, z_context, @@ -1303,16 +1339,7 @@ TEST_CASE("Polygon test 9", "[Polygon]") X_positions[2], Y_positions[2], polygon_3); -/* - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[2], - Y_positions[2], - polygon_3, - X_positions[1], - Y_positions[1], - polygon_2); -*/ + introduce_PolygonLineNonIntersection(z_solver, z_context, X_positions[1], @@ -1330,16 +1357,6 @@ TEST_CASE("Polygon test 9", "[Polygon]") X_positions[2], Y_positions[2], polygon_3); -/* - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[2], - Y_positions[2], - polygon_3, - X_positions[0], - Y_positions[0], - polygon_1); -*/ introduce_PolygonLineNonIntersection(z_solver, z_context, @@ -1350,12 +1367,16 @@ TEST_CASE("Polygon test 9", "[Polygon]") Y_positions[2], polygon_3); - - 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 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; @@ -1400,8 +1421,13 @@ TEST_CASE("Polygon test 9", "[Polygon]") 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) @@ -1442,48 +1468,54 @@ TEST_CASE("Polygon test 9", "[Polygon]") { break; } - - //cout << float(z_model[i]) << "\n"; - /* - switch (z_model.get_const_interp(z_model[i]).bool_value()) + + #ifdef DEBUG { - 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"); + 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; - } - default: - { + } + case Z3_L_TRUE: + { + printf(" value: TRUE\n"); break; + } + case Z3_L_UNDEF: + { + printf(" value: UNDEF\n"); + break; + } + default: + { + break; + } + } } - } - */ + #endif } finish = clock(); + REQUIRE(last_solvable_bounding_box_size > 0); printf("Solvable bounding box: %d\n", last_solvable_bounding_box_size); printf("Positions: %.3f, %.3f, %.3f, %.3f, %.3f, %.3f\n", poly_1_pos_x, poly_1_pos_y, poly_2_pos_x, poly_2_pos_y, poly_3_pos_x, poly_3_pos_y); - /* - for (int i = 0; i < 2; ++i) - { - double value = X_positions[i].as_double(); - printf("Orig X: %.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); + value = Y_positions[i].as_double(); + printf("Orig Y: %.3f\n", value); + } } - */ + #endif SVG preview_svg("polygon_test_9.svg"); @@ -1577,103 +1609,21 @@ TEST_CASE("Polygon test 10", "[Polygon]") polygons.push_back(polygon_3); polygons.push_back(polygon_4); - /* - introduce_DecisionBox(z_solver, X_positions[0], Y_positions[0], 200, 200); - introduce_DecisionBox(z_solver, X_positions[1], Y_positions[1], 200, 200); - */ - - /* - for (int i = 0; i < 3; ++i) - { - for (int j = i + 1; j < 4; ++j) - { - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[i], - Y_positions[i], - polygons[i], - X_positions[j], - Y_positions[j], - polygons[j]); - } - } - */ - -/* - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[0], - Y_positions[0], - polygons[0], - X_positions[2], - Y_positions[2], - polygons[2]); - - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[0], - Y_positions[0], - polygons[0], - X_positions[1], - Y_positions[1], - polygons[1]); - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[0], - Y_positions[0], - polygons[0], - X_positions[3], - Y_positions[3], - polygons[3]); - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[1], - Y_positions[1], - polygons[1], - X_positions[3], - Y_positions[3], - polygons[3]); - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[1], - Y_positions[1], - polygons[1], - X_positions[2], - Y_positions[2], - polygons[2]); - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[2], - Y_positions[2], - polygons[2], - X_positions[3], - Y_positions[3], - polygons[3]); -*/ - -/* - introduce_PolygonWeakNonoverlapping(z_solver, - z_context, - X_positions, - Y_positions, - polygons); -*/ introduce_PolygonStrongNonoverlapping(z_solver, z_context, X_positions, Y_positions, polygons); - - 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 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; @@ -1683,7 +1633,6 @@ TEST_CASE("Polygon test 10", "[Polygon]") { z3::expr_vector bounding_box_assumptions(z_context); - //assume_BedBoundingBox(X_positions, Y_positions, polygons, bounding_box_size, bounding_box_size, bounding_box_assumptions); assume_BedBoundingBox(X_positions[0], Y_positions[0], polygons[0], bounding_box_size, bounding_box_size, bounding_box_assumptions); assume_BedBoundingBox(X_positions[1], Y_positions[1], polygons[1], bounding_box_size, bounding_box_size, bounding_box_assumptions); assume_BedBoundingBox(X_positions[2], Y_positions[2], polygons[2], bounding_box_size, bounding_box_size, bounding_box_assumptions); @@ -1720,8 +1669,13 @@ TEST_CASE("Polygon test 10", "[Polygon]") 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) @@ -1770,35 +1724,41 @@ TEST_CASE("Polygon test 10", "[Polygon]") { break; } - - //cout << float(z_model[i]) << "\n"; - /* - switch (z_model.get_const_interp(z_model[i]).bool_value()) + + #ifdef DEBUG { - 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"); + 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; - } - default: - { + } + case Z3_L_TRUE: + { + printf(" value: TRUE\n"); break; + } + case Z3_L_UNDEF: + { + printf(" value: UNDEF\n"); + break; + } + default: + { + break; + } + } } - } - */ + #endif + } finish = clock(); + REQUIRE(last_solvable_bounding_box_size > 0); + printf("Solvable bounding box: %d\n", last_solvable_bounding_box_size); printf("Positions: %.3f, %.3f, %.3f, %.3f, %.3f, %.3f, %.3f, %.3f\n", poly_1_pos_x, poly_1_pos_y, @@ -1809,16 +1769,18 @@ TEST_CASE("Polygon test 10", "[Polygon]") poly_4_pos_x, poly_4_pos_y); - /* - for (int i = 0; i < 2; ++i) - { - double value = X_positions[i].as_double(); - printf("Orig X: %.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); + value = Y_positions[i].as_double(); + printf("Orig Y: %.3f\n", value); + } } - */ + #endif SVG preview_svg("polygon_test_10.svg"); @@ -1912,96 +1874,21 @@ TEST_CASE("Polygon test 11", "[Polygon]") polygons.push_back(polygon_3); polygons.push_back(polygon_4); - /* - introduce_DecisionBox(z_solver, X_positions[0], Y_positions[0], 200, 200); - introduce_DecisionBox(z_solver, X_positions[1], Y_positions[1], 200, 200); - */ - - /* - for (int i = 0; i < 3; ++i) - { - for (int j = i + 1; j < 4; ++j) - { - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[i], - Y_positions[i], - polygons[i], - X_positions[j], - Y_positions[j], - polygons[j]); - } - } - */ - -/* - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[0], - Y_positions[0], - polygons[0], - X_positions[2], - Y_positions[2], - polygons[2]); - - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[0], - Y_positions[0], - polygons[0], - X_positions[1], - Y_positions[1], - polygons[1]); - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[0], - Y_positions[0], - polygons[0], - X_positions[3], - Y_positions[3], - polygons[3]); - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[1], - Y_positions[1], - polygons[1], - X_positions[3], - Y_positions[3], - polygons[3]); - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[1], - Y_positions[1], - polygons[1], - X_positions[2], - Y_positions[2], - polygons[2]); - - introduce_PolygonOutsidePolygon(z_solver, - z_context, - X_positions[2], - Y_positions[2], - polygons[2], - X_positions[3], - Y_positions[3], - polygons[3]); -*/ - introduce_PolygonWeakNonoverlapping(z_solver, z_context, X_positions, Y_positions, polygons); - - 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 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; @@ -2012,7 +1899,6 @@ TEST_CASE("Polygon test 11", "[Polygon]") printf("BB: %d\n", bounding_box_size); z3::expr_vector bounding_box_assumptions(z_context); - //assume_BedBoundingBox(X_positions, Y_positions, polygons, bounding_box_size, bounding_box_size, bounding_box_assumptions); assume_BedBoundingBox(X_positions[0], Y_positions[0], polygons[0], bounding_box_size, bounding_box_size, bounding_box_assumptions); assume_BedBoundingBox(X_positions[1], Y_positions[1], polygons[1], bounding_box_size, bounding_box_size, bounding_box_assumptions); assume_BedBoundingBox(X_positions[2], Y_positions[2], polygons[2], bounding_box_size, bounding_box_size, bounding_box_assumptions); @@ -2048,8 +1934,13 @@ TEST_CASE("Polygon test 11", "[Polygon]") 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) @@ -2156,13 +2047,17 @@ TEST_CASE("Polygon test 11", "[Polygon]") if (refined_sat) { - z3::model z_model(z_solver.get_model()); - printf("Printing model:\n"); - cout << z_model << "\n"; + z3::model z_model(z_solver.get_model()); + + #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()); double value = z_model.get_const_interp(z_model[i]).as_double(); if (z_model[i].name().str() == "x_pos-0") @@ -2223,35 +2118,41 @@ TEST_CASE("Polygon test 11", "[Polygon]") { break; } - - //cout << float(z_model[i]) << "\n"; - /* - switch (z_model.get_const_interp(z_model[i]).bool_value()) + + #ifdef DEBUG { - 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"); + 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; - } - default: - { + } + case Z3_L_TRUE: + { + printf(" value: TRUE\n"); break; + } + case Z3_L_UNDEF: + { + printf(" value: UNDEF\n"); + break; + } + default: + { + break; + } + } } - } - */ + #endif + } finish = clock(); + REQUIRE(last_solvable_bounding_box_size > 0); + printf("Solvable bounding box: %d\n", last_solvable_bounding_box_size); printf("Positions: %.3f, %.3f, %.3f, %.3f, %.3f, %.3f, %.3f, %.3f\n", poly_1_pos_x, poly_1_pos_y, @@ -2262,16 +2163,18 @@ TEST_CASE("Polygon test 11", "[Polygon]") poly_4_pos_x, poly_4_pos_y); - /* - for (int i = 0; i < 2; ++i) - { - double value = X_positions[i].as_double(); - printf("Orig X: %.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); + value = Y_positions[i].as_double(); + printf("Orig Y: %.3f\n", value); + } } - */ + #endif SVG preview_svg("polygon_test_11.svg"); @@ -2332,6 +2235,7 @@ TEST_CASE("Polygon test 12", "[Polygon]") polygons); finish = clock(); + REQUIRE(optimized); if (optimized) { @@ -2421,10 +2325,6 @@ TEST_CASE("Polygon test 13", "[Polygon]") string_map dec_var_names_map; - /* - z3::params z_parameters(z_context); - z_parameters.set("timeout", 1000); - */ Z3_global_param_set("timeout", "8000"); z3::solver z_solver(z_context); @@ -2458,6 +2358,7 @@ TEST_CASE("Polygon test 13", "[Polygon]") polygons); finish = clock(); + REQUIRE(optimized); if (optimized) { @@ -2601,11 +2502,7 @@ TEST_CASE("Polygon test 14", "[Polygon]") vector X_values; vector Y_values; - string_map dec_var_names_map; - - /* - Z3_global_param_set("timeout", "8000"); - */ + string_map dec_var_names_map; z3::solver z_solver(z_context); @@ -2805,6 +2702,8 @@ TEST_CASE("Polygon test 14", "[Polygon]") { printf("Polygon optimization FAILED.\n"); } + + REQUIRE(optimized); } printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC); @@ -2856,10 +2755,6 @@ TEST_CASE("Polygon test 15", "[Polygon]") polygons.push_back(polygon_1); polygons.push_back(polygon_2); - /* - polygons.push_back(polygon_3); - polygons.push_back(polygon_4); - */ for (unsigned int index = 0; index < polygons.size(); ++index) { polygon_index_map.push_back(index); @@ -2867,11 +2762,6 @@ TEST_CASE("Polygon test 15", "[Polygon]") vector poly_positions_X; vector poly_positions_Y; - - /* - poly_positions_X.resize(polygons.size()); - poly_positions_Y.resize(polygons.size()); - */ do { @@ -2986,7 +2876,7 @@ TEST_CASE("Polygon test 15", "[Polygon]") { printf("Polygon optimization FAILED.\n"); } - getchar(); + REQUIRE(optimized); vector next_polygons; @@ -3026,13 +2916,15 @@ TEST_CASE("Polygon test 16", "[Polygon]") polygons.push_back(polygon_4); double area = calc_PolygonUnreachableZoneArea(polygon_1, polygons); + REQUIRE(area > 0.0); printf("Polygons area: %.3f\n", area); finish = clock(); printf("Time: %.3f\n", (finish - start) / (double)CLOCKS_PER_SEC); printf("Testing polygon 16 ... finished\n"); -} +} + /*----------------------------------------------------------------*/ diff --git a/src/libseqarrange/test/seq_test_preprocess.cpp b/src/libseqarrange/test/seq_test_preprocess.cpp index 04b7830fe5..f119ff69f9 100644 --- a/src/libseqarrange/test/seq_test_preprocess.cpp +++ b/src/libseqarrange/test/seq_test_preprocess.cpp @@ -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 next_polygons; vector 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 polygons; std::vector > 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 next_polygons; vector > 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 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 next_polygons; vector > next_unreachable_polygons; diff --git a/src/libseqarrange/test/seq_test_sequential.cpp b/src/libseqarrange/test/seq_test_sequential.cpp index a58f4e7908..53fa2bf531 100644 --- a/src/libseqarrange/test/seq_test_sequential.cpp +++ b/src/libseqarrange/test/seq_test_sequential.cpp @@ -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 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 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 polygon_index_map; vector 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 poly_positions_Y; vector 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 next_polygons; vector 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 poly_positions_Y; vector 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 next_polygons; vector > next_unreachable_polygons; @@ -2299,5 +2193,5 @@ TEST_CASE("Sequential test 7", "[Sequential Arrangement Core]") } -/*----------------------------------------------------------------*/ +/*----------------------------------------------------------------*/