From 734feaa9fcdcc810ffe3fe10612b90768d966b2c Mon Sep 17 00:00:00 2001 From: danjujan <44864658+danjujan@users.noreply.github.com> Date: Sun, 20 Aug 2023 20:35:25 +0200 Subject: [PATCH 01/11] Create Cofiguration bindings for python --- bindings/python/vara-feature/CMakeLists.txt | 3 +- .../vara-feature/pybind_Configuration.cpp | 52 +++++++++++++++++++ bindings/python/vara-feature/pybind_Init.cpp | 3 ++ 3 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 bindings/python/vara-feature/pybind_Configuration.cpp diff --git a/bindings/python/vara-feature/CMakeLists.txt b/bindings/python/vara-feature/CMakeLists.txt index b8a4ac4aa..5f9fb3bbe 100644 --- a/bindings/python/vara-feature/CMakeLists.txt +++ b/bindings/python/vara-feature/CMakeLists.txt @@ -1,6 +1,7 @@ pybind11_add_module( vara_feature pybind_Init.cpp + pybind_Configuration.cpp pybind_Constraint.cpp pybind_Feature.cpp pybind_FeatureModel.cpp @@ -12,4 +13,4 @@ pybind11_add_module( set(LLVM_LINK_COMPONENTS Core Support) -target_link_libraries(vara_feature LINK_PUBLIC VaRAFeature ${STD_FS_LIB}) +target_link_libraries(vara_feature LINK_PUBLIC VaRAFeature VaRASolver ${STD_FS_LIB}) diff --git a/bindings/python/vara-feature/pybind_Configuration.cpp b/bindings/python/vara-feature/pybind_Configuration.cpp new file mode 100644 index 000000000..45686c9ca --- /dev/null +++ b/bindings/python/vara-feature/pybind_Configuration.cpp @@ -0,0 +1,52 @@ +#include "pybind_common.h" +#include "vara/Configuration/Configuration.h" +#include "vara/Solver/ConfigurationFactory.h" + +#include "pybind11/detail/common.h" +#include "pybind11/pybind11.h" + +#include +#include + +namespace vf = vara::feature; +namespace vs = vara::solver; +namespace py = pybind11; + +void init_configuration_module(py::module &M) { + py::class_(M, "ConfigurationOption") + .def_property_readonly( + "name", [](vf::ConfigurationOption &CO) { return CO.name().str(); }, + R"pbdoc(Returns the name of the ConfigurationOption.)pbdoc") + .def_property_readonly( + "value", &vf::ConfigurationOption::asString, + R"pbdoc(Returns the value of the ConfigurationOption as str.)pbdoc"); + py::class_(M, "Configuration") + .def("__str__", [](vf::Configuration &C) { return C.dumpToString(); }) + /*.def( + "__iter__", + [](vf::Configuration &C) { + return py::make_iterator(C.begin(), C.end()); + }, + py::keep_alive<0, 1>())*/ + .def("getOptions", [](vf::Configuration &C) { + std::vector V; + for (auto &O : C) { + V.push_back(*O.getValue()); + } + + return V; + }); + + M.def( + "getAllConfigs", + [](vf::FeatureModel &FM) { + return vs::ConfigurationFactory::getAllConfigs(FM).extractValue(); + }, + R"pbdoc(Get all configurations of FeatureModel. + +Args: + fm (FeatureModel): the FeatureModel + +Returns: list of all configurations. +)pbdoc"); +} diff --git a/bindings/python/vara-feature/pybind_Init.cpp b/bindings/python/vara-feature/pybind_Init.cpp index 50e00f5f8..141da5f0e 100644 --- a/bindings/python/vara-feature/pybind_Init.cpp +++ b/bindings/python/vara-feature/pybind_Init.cpp @@ -12,6 +12,7 @@ void init_feature_location_module(py::module &M); void init_feature_model_module(py::module &M); void init_feature_model_builder_module(py::module &M); void init_xml_writer(py::module &M); +void init_configuration_module(py::module &M); PYBIND11_MODULE(vara_feature, M) { auto LLVMModule = M.def_submodule("llvm_util"); @@ -27,4 +28,6 @@ PYBIND11_MODULE(vara_feature, M) { init_xml_writer(FMWriterModule); auto FeatureModelBuilderModule = M.def_submodule("feature_model_builder"); init_feature_model_builder_module(FeatureModelBuilderModule); + auto ConfigurationModule = M.def_submodule("configuration"); + init_configuration_module(ConfigurationModule); } From ccd4a5bfe8bf459875b9ebad9dbeed2610c5069e Mon Sep 17 00:00:00 2001 From: danjujan <44864658+danjujan@users.noreply.github.com> Date: Wed, 23 Aug 2023 12:38:57 +0200 Subject: [PATCH 02/11] Cleanup --- bindings/python/vara-feature/pybind_Configuration.cpp | 7 ------- setup.py | 2 +- 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/bindings/python/vara-feature/pybind_Configuration.cpp b/bindings/python/vara-feature/pybind_Configuration.cpp index 45686c9ca..f77430f39 100644 --- a/bindings/python/vara-feature/pybind_Configuration.cpp +++ b/bindings/python/vara-feature/pybind_Configuration.cpp @@ -22,12 +22,6 @@ void init_configuration_module(py::module &M) { R"pbdoc(Returns the value of the ConfigurationOption as str.)pbdoc"); py::class_(M, "Configuration") .def("__str__", [](vf::Configuration &C) { return C.dumpToString(); }) - /*.def( - "__iter__", - [](vf::Configuration &C) { - return py::make_iterator(C.begin(), C.end()); - }, - py::keep_alive<0, 1>())*/ .def("getOptions", [](vf::Configuration &C) { std::vector V; for (auto &O : C) { @@ -36,7 +30,6 @@ void init_configuration_module(py::module &M) { return V; }); - M.def( "getAllConfigs", [](vf::FeatureModel &FM) { diff --git a/setup.py b/setup.py index 805810a6d..f2c7d5e7e 100644 --- a/setup.py +++ b/setup.py @@ -61,7 +61,7 @@ def build_extension(self, ext): build_args += ['--', '/m'] else: cmake_args += ['-DCMAKE_BUILD_TYPE=' + cfg] - build_args += ['--', '-j2'] + build_args += ['--', f'-j{os.cpu_count()}'] env = os.environ.copy() env['CXXFLAGS'] = '{} -DVERSION_INFO=\\"{}\\"'.format( From 09238d6e51a0982a4857b49a80a094c76c35ddad Mon Sep 17 00:00:00 2001 From: danjujan <44864658+danjujan@users.noreply.github.com> Date: Mon, 28 Aug 2023 14:13:07 +0200 Subject: [PATCH 03/11] Do not build z3 if it is installed --- setup.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/setup.py b/setup.py index f2c7d5e7e..63af382ec 100644 --- a/setup.py +++ b/setup.py @@ -47,6 +47,8 @@ def build_extension(self, ext): '-DPYTHON_EXECUTABLE=' + sys.executable, '-DVARA_FEATURE_USE_Z3_SOLVER=True' ] + if os.path.exists('/lib/x86_64-linux-gnu/libz3.so'): + cmake_args.append('-DVARA_FEATURE_BUILD_Z3_SOLVER=False') cfg = 'Debug' if self.debug else 'Release' build_args = ['--config', cfg] From 9725979e56ba22f2611e8f4cd0bbecc04eb78836 Mon Sep 17 00:00:00 2001 From: danjujan <44864658+danjujan@users.noreply.github.com> Date: Fri, 15 Sep 2023 14:12:28 +0200 Subject: [PATCH 04/11] Fix pre-commit --- bindings/python/vara-feature/CMakeLists.txt | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/bindings/python/vara-feature/CMakeLists.txt b/bindings/python/vara-feature/CMakeLists.txt index 5f9fb3bbe..67a5df1c4 100644 --- a/bindings/python/vara-feature/CMakeLists.txt +++ b/bindings/python/vara-feature/CMakeLists.txt @@ -13,4 +13,10 @@ pybind11_add_module( set(LLVM_LINK_COMPONENTS Core Support) -target_link_libraries(vara_feature LINK_PUBLIC VaRAFeature VaRASolver ${STD_FS_LIB}) +target_link_libraries( + vara_feature + LINK_PUBLIC + VaRAFeature + VaRASolver + ${STD_FS_LIB} +) From 0f335341f35462282b3955d4183828edf41c55b4 Mon Sep 17 00:00:00 2001 From: danjujan <44864658+danjujan@users.noreply.github.com> Date: Fri, 6 Oct 2023 17:22:39 +0200 Subject: [PATCH 05/11] Add GetAllConfigurations2 unittest to detect bug --- unittests/Solver/ConfigurationFactory.cpp | 21 ++++++++++++++ unittests/resources/CMakeLists.txt | 1 + .../xml/test_three_optional_features.xml | 29 +++++++++++++++++++ 3 files changed, 51 insertions(+) create mode 100644 unittests/resources/xml/test_three_optional_features.xml diff --git a/unittests/Solver/ConfigurationFactory.cpp b/unittests/Solver/ConfigurationFactory.cpp index 5170271fa..2a095ea34 100644 --- a/unittests/Solver/ConfigurationFactory.cpp +++ b/unittests/Solver/ConfigurationFactory.cpp @@ -2,6 +2,8 @@ #include "vara/Feature/ConstraintBuilder.h" #include "vara/Feature/FeatureModelBuilder.h" + +#include "Utils/UnittestHelper.h" #include "gtest/gtest.h" namespace vara::solver { @@ -51,6 +53,25 @@ TEST(ConfigurationFactory, GetAllConfigurations) { EXPECT_EQ(ConfigResult.extractValue().size(), 6 * 63); } +TEST(ConfigurationFactory, GetAllConfigurations2) { + auto FM = feature::loadFeatureModel( + getTestResource("test_three_optional_features.xml")); + auto ConfigResult = ConfigurationFactory::getAllConfigs(*FM); + EXPECT_TRUE(ConfigResult); + auto Configs = ConfigResult.extractValue(); + + EXPECT_EQ(Configs.size(), 8); + + auto ConfigsStrings = std::vector(); + for (auto &config : Configs) { + ConfigsStrings.push_back(config.get()->dumpToString()); + } + + auto UniqueConfigs = + std::set(ConfigsStrings.begin(), ConfigsStrings.end()); + EXPECT_EQ(Configs.size(), UniqueConfigs.size()); +} + TEST(ConfigurationFactory, GetNConfigurations) { auto FM = getFeatureModel(); auto ConfigResult = ConfigurationFactory::getNConfigs(*FM, 100); diff --git a/unittests/resources/CMakeLists.txt b/unittests/resources/CMakeLists.txt index a243fcb77..5d47f4336 100644 --- a/unittests/resources/CMakeLists.txt +++ b/unittests/resources/CMakeLists.txt @@ -39,6 +39,7 @@ set(FEATURE_LIB_TEST_FILES xml/test_output_string.xml xml/test_revision_range.xml xml/test_step_function.xml + xml/test_three_optional_features.xml xml/test_with_whitespaces.xml yml/dune_configs.yml ) diff --git a/unittests/resources/xml/test_three_optional_features.xml b/unittests/resources/xml/test_three_optional_features.xml new file mode 100644 index 000000000..d18ea984f --- /dev/null +++ b/unittests/resources/xml/test_three_optional_features.xml @@ -0,0 +1,29 @@ + + + + + + root + + False + + + A + A + root + True + + + B + B + root + True + + + C + C + root + True + + + From eb111934f90a998becb07eae9cb684de939928f2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Sebastian=20B=C3=B6hm?= Date: Sun, 22 Oct 2023 14:55:11 +0200 Subject: [PATCH 06/11] Do not exclude the first config. For some reason, this caused other configs to appear multiple times during enumeration. --- lib/Solver/Z3Solver.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index f28c9d4de..06ca079c5 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -177,11 +177,13 @@ Result Z3Solver::hasValidConfigurations() { Result> Z3Solver::getNextConfiguration() { - // Add previous configuration as a constraint + auto CurrentConfig = getCurrentConfiguration(); + + // Add current configuration as a constraint to exclude it for further queries excludeCurrentConfiguration(); // Retrieve the next configuration - return getCurrentConfiguration(); + return CurrentConfig; } Result Z3Solver::getNumberValidConfigurations() { From 67ac14e23bf11d12cadb573eab16d3780dd2a015 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Sebastian=20B=C3=B6hm?= Date: Sun, 22 Oct 2023 14:55:52 +0200 Subject: [PATCH 07/11] Avoid unnecessary solver calls. --- lib/Solver/Z3Solver.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 06ca079c5..ef88d02b0 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -189,8 +189,7 @@ Z3Solver::getNextConfiguration() { Result Z3Solver::getNumberValidConfigurations() { Solver->push(); uint64_t Count = 0; - while (Solver->check() == z3::sat) { - excludeCurrentConfiguration(); + while (getNextConfiguration()) { Count++; } Solver->pop(); @@ -202,10 +201,8 @@ Resultpush(); auto Vector = std::vector>(); - while (Solver->check() == z3::sat) { - auto Config = getCurrentConfiguration().extractValue(); - Vector.insert(Vector.begin(), std::move(Config)); - excludeCurrentConfiguration(); + while (auto Config = getNextConfiguration()) { + Vector.insert(Vector.begin(), Config.extractValue()); } Solver->pop(); return Vector; From b50117dcce9b42d2a1c6deeef27ad39e2f8e99fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Sebastian=20B=C3=B6hm?= Date: Sun, 22 Oct 2023 14:56:10 +0200 Subject: [PATCH 08/11] Use for-each loop to iterate maps. --- lib/Solver/Z3Solver.cpp | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index ef88d02b0..beaad29ed 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -231,18 +231,17 @@ Result Z3Solver::excludeCurrentConfiguration() { } const z3::model M = Solver->get_model(); z3::expr Expr = Context.bool_val(false); - for (auto Iterator = OptionToVariableMapping.begin(); - Iterator != OptionToVariableMapping.end(); Iterator++) { - const z3::expr OptionExpr = *Iterator->getValue(); + for (auto const& Entry : OptionToVariableMapping) { + const z3::expr OptionExpr = *Entry.getValue(); const z3::expr Value = M.eval(OptionExpr, true); if (Value.is_bool()) { if (Value.is_true()) { - Expr = Expr || !*Iterator->getValue(); + Expr = Expr || !OptionExpr; } else { - Expr = Expr || *Iterator->getValue(); + Expr = Expr || OptionExpr; } } else { - Expr = Expr || (*Iterator->getValue() != Value); + Expr = Expr || (OptionExpr != Value); } } Solver->add(Expr); @@ -257,11 +256,10 @@ Z3Solver::getCurrentConfiguration() { const z3::model M = Solver->get_model(); auto Config = std::make_unique(); - for (auto Iterator = OptionToVariableMapping.begin(); - Iterator != OptionToVariableMapping.end(); Iterator++) { - const z3::expr OptionExpr = *Iterator->getValue(); + for (auto const& Entry : OptionToVariableMapping) { + const z3::expr OptionExpr = *Entry.getValue(); const z3::expr Value = M.eval(OptionExpr, true); - Config->setConfigurationOption(Iterator->getKey(), + Config->setConfigurationOption(Entry.getKey(), llvm::StringRef(Value.to_string())); } return Config; From 28bddd7b43e2a05371e94161e106bb0bd304bc59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Sebastian=20B=C3=B6hm?= Date: Sun, 22 Oct 2023 15:51:08 +0200 Subject: [PATCH 09/11] Temporary fix for side effects of getNextConfiguration() This caused 2 issues: - either first config was skipped or getCurrentConfig would always point to the next configuration - getAllValidConfigurations or getNumberValidConfigurations produce incorrect results if called after any call to getNextConfiguration() The last point is an issue with the Solver API and this is a quick-fix for the Z3Solver implementation that returns an error in that case. --- include/vara/Solver/Error.h | 4 ++++ include/vara/Solver/Z3Solver.h | 6 ++++++ lib/Solver/Z3Solver.cpp | 26 ++++++++++++++++++-------- unittests/Solver/Z3Tests.cpp | 2 +- 4 files changed, 29 insertions(+), 9 deletions(-) diff --git a/include/vara/Solver/Error.h b/include/vara/Solver/Error.h index 895f4ca52..60f78aad8 100644 --- a/include/vara/Solver/Error.h +++ b/include/vara/Solver/Error.h @@ -14,6 +14,7 @@ enum SolverErrorCode { ALREADY_PRESENT, NOT_ALL_CONSTRAINTS_PROCESSED, PARENT_NOT_PRESENT, + ILLEGAL_STATE, }; } // namespace solver @@ -52,6 +53,9 @@ class Error { case vara::solver::PARENT_NOT_PRESENT: OS << "Parent feature of a feature is not present."; break; + case vara::solver::ILLEGAL_STATE: + OS << "The solver is in an illegal state for this operation."; + break; } return OS; } diff --git a/include/vara/Solver/Z3Solver.h b/include/vara/Solver/Z3Solver.h index cd43e3a8b..0c29826ad 100644 --- a/include/vara/Solver/Z3Solver.h +++ b/include/vara/Solver/Z3Solver.h @@ -95,6 +95,12 @@ class Z3Solver : public Solver { /// The instance of the Z3 solver needed for caching the constraints and /// variables. std::unique_ptr Solver; + + /// Flag that indicates whether the solver state has been modified by calling + /// \c getNextConfiguration. + /// This is important for functions that want to enumerate all configurations, + /// like \c getAllValidConfigurations or \c getNumberValidConfigurations. + bool Dirty = false; }; /// \brief This class is a visitor to convert the constraints from the diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index beaad29ed..38b29f1da 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -177,34 +177,44 @@ Result Z3Solver::hasValidConfigurations() { Result> Z3Solver::getNextConfiguration() { - auto CurrentConfig = getCurrentConfiguration(); - - // Add current configuration as a constraint to exclude it for further queries - excludeCurrentConfiguration(); + if (!Dirty) { + Dirty = true; + } else { + excludeCurrentConfiguration(); + } - // Retrieve the next configuration - return CurrentConfig; + return getCurrentConfiguration(); } Result Z3Solver::getNumberValidConfigurations() { + if (Dirty) { + return Error(ILLEGAL_STATE); + } + Solver->push(); uint64_t Count = 0; while (getNextConfiguration()) { Count++; } Solver->pop(); + Dirty = false; return Count; } Result>> Z3Solver::getAllValidConfigurations() { + if (Dirty) { + return Error(ILLEGAL_STATE); + } + Solver->push(); auto Vector = std::vector>(); while (auto Config = getNextConfiguration()) { Vector.insert(Vector.begin(), Config.extractValue()); } Solver->pop(); + Dirty = false; return Vector; } @@ -231,7 +241,7 @@ Result Z3Solver::excludeCurrentConfiguration() { } const z3::model M = Solver->get_model(); z3::expr Expr = Context.bool_val(false); - for (auto const& Entry : OptionToVariableMapping) { + for (auto const &Entry : OptionToVariableMapping) { const z3::expr OptionExpr = *Entry.getValue(); const z3::expr Value = M.eval(OptionExpr, true); if (Value.is_bool()) { @@ -256,7 +266,7 @@ Z3Solver::getCurrentConfiguration() { const z3::model M = Solver->get_model(); auto Config = std::make_unique(); - for (auto const& Entry : OptionToVariableMapping) { + for (auto const &Entry : OptionToVariableMapping) { const z3::expr OptionExpr = *Entry.getValue(); const z3::expr Value = M.eval(OptionExpr, true); Config->setConfigurationOption(Entry.getKey(), diff --git a/unittests/Solver/Z3Tests.cpp b/unittests/Solver/Z3Tests.cpp index bd36af3b0..6848f746f 100644 --- a/unittests/Solver/Z3Tests.cpp +++ b/unittests/Solver/Z3Tests.cpp @@ -115,7 +115,7 @@ TEST(Z3Solver, TestGetNextConfiguration) { S->addFeature(*FM->getFeature("Foo")); S->addFeature(*FM->getFeature("Num1")); - for (int Count = 0; Count < 3; Count++) { + for (int Count = 0; Count < 4; Count++) { auto C = S->getNextConfiguration(); EXPECT_TRUE(C); auto Config = C.extractValue(); From 1e5aa2be07a7581996f19f43bf793146f48d6cfd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Sebastian=20B=C3=B6hm?= Date: Mon, 23 Oct 2023 11:56:46 +0200 Subject: [PATCH 10/11] Apply suggested changes. --- lib/Solver/Z3Solver.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 38b29f1da..37d8847a4 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -177,10 +177,10 @@ Result Z3Solver::hasValidConfigurations() { Result> Z3Solver::getNextConfiguration() { - if (!Dirty) { - Dirty = true; - } else { + if (Dirty) { excludeCurrentConfiguration(); + } else { + Dirty = true; } return getCurrentConfiguration(); @@ -241,7 +241,7 @@ Result Z3Solver::excludeCurrentConfiguration() { } const z3::model M = Solver->get_model(); z3::expr Expr = Context.bool_val(false); - for (auto const &Entry : OptionToVariableMapping) { + for (const auto &Entry : OptionToVariableMapping) { const z3::expr OptionExpr = *Entry.getValue(); const z3::expr Value = M.eval(OptionExpr, true); if (Value.is_bool()) { @@ -266,7 +266,7 @@ Z3Solver::getCurrentConfiguration() { const z3::model M = Solver->get_model(); auto Config = std::make_unique(); - for (auto const &Entry : OptionToVariableMapping) { + for (const auto &Entry : OptionToVariableMapping) { const z3::expr OptionExpr = *Entry.getValue(); const z3::expr Value = M.eval(OptionExpr, true); Config->setConfigurationOption(Entry.getKey(), From 67463abaf0e8e3109044bd15da69c5f223f5cde5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Sebastian=20B=C3=B6hm?= Date: Mon, 23 Oct 2023 13:14:48 +0200 Subject: [PATCH 11/11] Quick-fix to make configuration enumeration work. This implementation is quite hacky and requires a redesign of the Solver API to be fixed properly. --- lib/Solver/Z3Solver.cpp | 9 ++--- unittests/Solver/ConfigurationFactory.cpp | 19 +++++++++ unittests/resources/CMakeLists.txt | 1 + unittests/resources/xml/test_msmr.xml | 48 +++++++++++++++++++++++ 4 files changed, 71 insertions(+), 6 deletions(-) create mode 100644 unittests/resources/xml/test_msmr.xml diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 37d8847a4..43128aa0d 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -183,6 +183,9 @@ Z3Solver::getNextConfiguration() { Dirty = true; } + if (Solver->check() == z3::unsat) { + return UNSAT; + } return getCurrentConfiguration(); } @@ -236,9 +239,6 @@ Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature, } Result Z3Solver::excludeCurrentConfiguration() { - if (Solver->check() == z3::unsat) { - return UNSAT; - } const z3::model M = Solver->get_model(); z3::expr Expr = Context.bool_val(false); for (const auto &Entry : OptionToVariableMapping) { @@ -260,9 +260,6 @@ Result Z3Solver::excludeCurrentConfiguration() { Result> Z3Solver::getCurrentConfiguration() { - if (Solver->check() == z3::unsat) { - return UNSAT; - } const z3::model M = Solver->get_model(); auto Config = std::make_unique(); diff --git a/unittests/Solver/ConfigurationFactory.cpp b/unittests/Solver/ConfigurationFactory.cpp index 2a095ea34..84988998f 100644 --- a/unittests/Solver/ConfigurationFactory.cpp +++ b/unittests/Solver/ConfigurationFactory.cpp @@ -72,6 +72,25 @@ TEST(ConfigurationFactory, GetAllConfigurations2) { EXPECT_EQ(Configs.size(), UniqueConfigs.size()); } +TEST(ConfigurationFactory, GetAllConfigurations3) { + auto FM = feature::loadFeatureModel( + getTestResource("test_msmr.xml")); + auto ConfigResult = ConfigurationFactory::getAllConfigs(*FM); + EXPECT_TRUE(ConfigResult); + auto Configs = ConfigResult.extractValue(); + + EXPECT_EQ(Configs.size(), 16); + + auto ConfigsStrings = std::vector(); + for (auto &config : Configs) { + ConfigsStrings.push_back(config.get()->dumpToString()); + } + + auto UniqueConfigs = + std::set(ConfigsStrings.begin(), ConfigsStrings.end()); + EXPECT_EQ(Configs.size(), UniqueConfigs.size()); +} + TEST(ConfigurationFactory, GetNConfigurations) { auto FM = getFeatureModel(); auto ConfigResult = ConfigurationFactory::getNConfigs(*FM, 100); diff --git a/unittests/resources/CMakeLists.txt b/unittests/resources/CMakeLists.txt index 5d47f4336..dbf71e528 100644 --- a/unittests/resources/CMakeLists.txt +++ b/unittests/resources/CMakeLists.txt @@ -32,6 +32,7 @@ set(FEATURE_LIB_TEST_FILES xml/test_hsqldb_num.xml xml/test_member_offset.xml xml/test_mixed_constraints.xml + xml/test_msmr.xml xml/test_numbers.xml xml/test_only_children.xml xml/test_only_parents.xml diff --git a/unittests/resources/xml/test_msmr.xml b/unittests/resources/xml/test_msmr.xml new file mode 100644 index 000000000..20f41419e --- /dev/null +++ b/unittests/resources/xml/test_msmr.xml @@ -0,0 +1,48 @@ + + + + + + root + + False + + + Slow + --slow + root + True + + + Header + --header + root + True + + + Extern + --extern + root + True + + + src/MultiSharedMultipleRegions/FeatureHeader.cpp + + 3 + 6 + + + 3 + 18 + + + + + + Cpp + --cpp + root + True + + + \ No newline at end of file