From 864ff022ee39ce53234b671887488201cf2d9735 Mon Sep 17 00:00:00 2001 From: danjujan <44864658+danjujan@users.noreply.github.com> Date: Fri, 17 Nov 2023 11:19:01 +0100 Subject: [PATCH] Fixes configuration generation (#126) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit resolves se-sic/VaRA#1043 Co-authored-by: Sebastian Böhm --- include/vara/Solver/ConfigurationFactory.h | 32 +++++++- include/vara/Solver/Error.h | 4 + include/vara/Solver/Solver.h | 19 ----- include/vara/Solver/Z3Solver.h | 14 ++-- lib/Solver/Z3Solver.cpp | 75 +++++++------------ unittests/Solver/ConfigurationFactory.cpp | 39 ++++++++++ unittests/Solver/SolverFactory.cpp | 13 ++-- unittests/Solver/Z3Tests.cpp | 47 +++--------- unittests/resources/CMakeLists.txt | 2 + unittests/resources/xml/test_msmr.xml | 48 ++++++++++++ .../xml/test_three_optional_features.xml | 29 +++++++ 11 files changed, 199 insertions(+), 123 deletions(-) create mode 100644 unittests/resources/xml/test_msmr.xml create mode 100644 unittests/resources/xml/test_three_optional_features.xml diff --git a/include/vara/Solver/ConfigurationFactory.h b/include/vara/Solver/ConfigurationFactory.h index 91e458721..a4b4d2f80 100644 --- a/include/vara/Solver/ConfigurationFactory.h +++ b/include/vara/Solver/ConfigurationFactory.h @@ -17,7 +17,7 @@ class ConfigurationIterable { public: class ConfigurationIterator { public: - using iterator_category = std::forward_iterator_tag; + using iterator_category = std::input_iterator_tag; using difference_type = std::ptrdiff_t; using value_type = std::unique_ptr; using pointer = std::unique_ptr *; @@ -90,8 +90,34 @@ class ConfigurationFactory { std::vector>> getAllConfigs(feature::FeatureModel &Model, const vara::solver::SolverType Type = SolverType::Z3) { - auto S = SolverFactory::initializeSolver(Model, Type); - return S->getAllValidConfigurations(); + auto V = std::vector>(); + for (auto Config : ConfigurationFactory::getConfigIterator(Model, Type)) { + if (!Config) { + return Error(Config.getError()); + } + V.emplace_back(Config.extractValue()); + } + return V; + } + + /// This method returns the number of configurations of the given feature + /// model. + /// Note that this method needs to enumerate all configurations first. + /// If you need to access the configurations afterwards, prefer to call + /// \c getAllConfigs and check the result's size. + /// + /// \param Model the given model containing the features and constraints + /// \param Type the type of solver to use + /// + /// \returns the number of configurations for the given model + static Result + getNumConfigs(feature::FeatureModel &Model, + const vara::solver::SolverType Type = SolverType::Z3) { + auto Configs = getAllConfigs(Model, Type); + if (!Configs) { + return Error(Configs.getError()); + } + return Configs.extractValue().size(); } /// This method returns not all but the specified amount of configurations. 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/Solver.h b/include/vara/Solver/Solver.h index d5a73e3fc..5ef5950b1 100644 --- a/include/vara/Solver/Solver.h +++ b/include/vara/Solver/Solver.h @@ -117,15 +117,6 @@ class Solver { /// the current constraint system is solvable (\c true) or not (\c false). virtual Result hasValidConfigurations() = 0; - /// Returns the number of valid configurations of the current constraint - /// system (i.e., its features and its constraints). In principle, this is a - /// #SAT call (i.e., enumerating all configurations). - /// - /// \returns an error if the number of valid configurations can not be - /// retried. This can be the case if there are still constraints left that - /// were not included into the solver because of missing variables. - virtual Result getNumberValidConfigurations() = 0; - /// Returns the current configuration. /// /// \returns the current configuration found by the solver an error code in @@ -140,16 +131,6 @@ class Solver { /// unsatisfiable). virtual Result> getNextConfiguration() = 0; - - /// Returns all valid configurations. In comparison to \c - /// getNumberValidConfigurations, this method returns the configurations - /// instead of a number of configurations. - /// - /// \returns an error if an error occurs while retrieving the configurations. - /// Otherwise, it will return the configurations. - virtual Result>> - getAllValidConfigurations() = 0; }; } // namespace vara::solver diff --git a/include/vara/Solver/Z3Solver.h b/include/vara/Solver/Z3Solver.h index cd43e3a8b..9a5772b25 100644 --- a/include/vara/Solver/Z3Solver.h +++ b/include/vara/Solver/Z3Solver.h @@ -60,23 +60,16 @@ class Z3Solver : public Solver { Result> getCurrentConfiguration() override; - Result getNumberValidConfigurations() override; - Result> getNextConfiguration() override; - Result>> - getAllValidConfigurations() override; - private: // The Z3SolverConstraintVisitor is a friend class to access the solver and // the context. friend class Z3SolverConstraintVisitor; - /// Exclude the current configuration by adding it as a constraint - /// \return an error code in case of error. - Result excludeCurrentConfiguration(); + /// Exclude the current configuration by adding it as a constraint. + void excludeCurrentConfiguration(); /// Processes the constraints of the binary feature and ignores the 'optional' /// constraint if the feature is in an alternative group. @@ -95,6 +88,9 @@ class Z3Solver : public Solver { /// The instance of the Z3 solver needed for caching the constraints and /// variables. std::unique_ptr Solver; + + /// The current model of the SAT solver. + std::optional CurrentModel; }; /// \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 f28c9d4de..1df128ab2 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -169,6 +169,12 @@ Result Z3Solver::addMixedConstraint( } Result Z3Solver::hasValidConfigurations() { + // If CurrentModel exists, we heave already modified the solver state, thus, + // the result of this function might be wrong. + if (CurrentModel) { + return Error(ILLEGAL_STATE); + } + if (Solver->check() == z3::sat) { return Ok(true); } @@ -177,38 +183,14 @@ Result Z3Solver::hasValidConfigurations() { Result> Z3Solver::getNextConfiguration() { - // Add previous configuration as a constraint + if (Solver->check() == z3::unsat) { + return UNSAT; + } + CurrentModel = Solver->get_model(); excludeCurrentConfiguration(); - - // Retrieve the next configuration return getCurrentConfiguration(); } -Result Z3Solver::getNumberValidConfigurations() { - Solver->push(); - uint64_t Count = 0; - while (Solver->check() == z3::sat) { - excludeCurrentConfiguration(); - Count++; - } - Solver->pop(); - return Count; -} - -Result>> -Z3Solver::getAllValidConfigurations() { - Solver->push(); - auto Vector = std::vector>(); - while (Solver->check() == z3::sat) { - auto Config = getCurrentConfiguration().extractValue(); - Vector.insert(Vector.begin(), std::move(Config)); - excludeCurrentConfiguration(); - } - Solver->pop(); - return Vector; -} - Result Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature, bool IsInAlternativeGroup) { @@ -226,43 +208,40 @@ Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature, return Ok(); } -Result Z3Solver::excludeCurrentConfiguration() { - if (Solver->check() == z3::unsat) { - return UNSAT; +void Z3Solver::excludeCurrentConfiguration() { + if (!CurrentModel) { + return; } - 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(); - const z3::expr Value = M.eval(OptionExpr, true); + for (const auto &Entry : OptionToVariableMapping) { + const z3::expr OptionExpr = *Entry.getValue(); + const z3::expr Value = CurrentModel->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); - return Ok(); } Result> Z3Solver::getCurrentConfiguration() { - if (Solver->check() == z3::unsat) { - return UNSAT; + if (!CurrentModel) { + return getNextConfiguration(); } - 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(); - const z3::expr Value = M.eval(OptionExpr, true); - Config->setConfigurationOption(Iterator->getKey(), + for (const auto &Entry : OptionToVariableMapping) { + const z3::expr OptionExpr = *Entry.getValue(); + const z3::expr Value = CurrentModel->eval(OptionExpr, true); + Config->setConfigurationOption(Entry.getKey(), llvm::StringRef(Value.to_string())); } return Config; diff --git a/unittests/Solver/ConfigurationFactory.cpp b/unittests/Solver/ConfigurationFactory.cpp index 5170271fa..418afed41 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,43 @@ 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->dumpToString()); + } + + auto UniqueConfigs = + std::set(ConfigsStrings.begin(), ConfigsStrings.end()); + 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->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/Solver/SolverFactory.cpp b/unittests/Solver/SolverFactory.cpp index 574ce7a34..5f90e8701 100644 --- a/unittests/Solver/SolverFactory.cpp +++ b/unittests/Solver/SolverFactory.cpp @@ -2,15 +2,16 @@ #include "vara/Feature/ConstraintBuilder.h" #include "vara/Feature/FeatureModelBuilder.h" +#include "vara/Solver/ConfigurationFactory.h" #include "gtest/gtest.h" namespace vara::solver { TEST(SolverFactory, EmptyZ3SolverTest) { auto S = SolverFactory::initializeSolver(SolverType::Z3); - auto E = S->getNumberValidConfigurations(); - EXPECT_TRUE(E); - EXPECT_EQ(E.extractValue(), 1); + auto I = ConfigurationIterable(std::move(S)); + EXPECT_TRUE(*I.begin()); + EXPECT_EQ(std::distance(I.begin(), I.end()), 1); } TEST(SolverFactory, GeneralZ3Test) { @@ -51,9 +52,9 @@ TEST(SolverFactory, GeneralZ3Test) { auto FM = B.buildFeatureModel(); auto S = SolverFactory::initializeSolver(*FM, SolverType::Z3); - auto E = S->getNumberValidConfigurations(); - EXPECT_TRUE(E); - EXPECT_EQ(E.extractValue(), 6 * 63); + auto I = ConfigurationIterable(std::move(S)); + EXPECT_TRUE(*I.begin()); + EXPECT_EQ(std::distance(I.begin(), I.end()), 6 * 63); } } // namespace vara::solver diff --git a/unittests/Solver/Z3Tests.cpp b/unittests/Solver/Z3Tests.cpp index bd36af3b0..ccc4d32dd 100644 --- a/unittests/Solver/Z3Tests.cpp +++ b/unittests/Solver/Z3Tests.cpp @@ -3,6 +3,7 @@ #include "z3++.h" #include "vara/Feature/FeatureModelBuilder.h" +#include "vara/Solver/ConfigurationFactory.h" #include "gtest/gtest.h" namespace vara::solver { @@ -54,10 +55,6 @@ TEST(Z3Solver, AddFeatureObjectTest) { V = S->hasValidConfigurations(); EXPECT_TRUE(V); EXPECT_TRUE(V.extractValue()); - // Enumerate the solutions - auto Enumerate = S->getNumberValidConfigurations(); - EXPECT_TRUE(Enumerate); - EXPECT_EQ(2, Enumerate.extractValue()); E = S->addFeature(*FM->getFeature("B")); EXPECT_TRUE(E); @@ -68,37 +65,10 @@ TEST(Z3Solver, AddFeatureObjectTest) { EXPECT_FALSE(E); EXPECT_EQ(SolverErrorCode::ALREADY_PRESENT, E.getError()); - // Enumerate the solutions - Enumerate = S->getNumberValidConfigurations(); - EXPECT_TRUE(Enumerate); - EXPECT_EQ(6, Enumerate.extractValue()); - E = S->addFeature(*FM->getFeature("C")); EXPECT_TRUE(E); V = S->hasValidConfigurations(); EXPECT_TRUE(V.extractValue()); - Enumerate = S->getNumberValidConfigurations(); - EXPECT_TRUE(Enumerate); - EXPECT_EQ(6, Enumerate.extractValue()); -} - -TEST(Z3Solver, TestAllValidConfigurations) { - std::unique_ptr S = Z3Solver::create(); - vara::feature::FeatureModelBuilder B; - B.makeRoot("root"); - B.makeFeature("Foo", true); - B.addEdge("root", "Foo"); - std::vector Values{0, 1}; - B.makeFeature("Num1", Values); - auto FM = B.buildFeatureModel(); - - S->addFeature(*FM->getFeature("root")); - S->addFeature(*FM->getFeature("Foo")); - S->addFeature(*FM->getFeature("Num1")); - - auto C = S->getAllValidConfigurations(); - EXPECT_TRUE(C); - EXPECT_EQ(C.extractValue().size(), 4); } TEST(Z3Solver, TestGetNextConfiguration) { @@ -115,7 +85,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(); @@ -158,9 +128,9 @@ TEST(Z3Solver, AddImpliesConstraint) { S->addFeature(*FM->getFeature("a")); S->addFeature(*FM->getFeature("b")); S->addConstraint(*C); - auto E = S->getNumberValidConfigurations(); - EXPECT_TRUE(E); - EXPECT_EQ(E.extractValue(), 6); + auto I = ConfigurationIterable(std::move(S)); + EXPECT_TRUE(*I.begin()); + EXPECT_EQ(std::distance(I.begin(), I.end()), 6); } TEST(Z3Solver, AddAlternative) { @@ -203,9 +173,10 @@ TEST(Z3Solver, AddAlternative) { for (const auto &R : FM->relationships()) { S->addRelationship(*R); } - auto E = S->getNumberValidConfigurations(); - EXPECT_TRUE(E); - EXPECT_EQ(E.extractValue(), 63); + + auto I = ConfigurationIterable(std::move(S)); + EXPECT_TRUE(*I.begin()); + EXPECT_EQ(std::distance(I.begin(), I.end()), 63); } } // namespace vara::solver diff --git a/unittests/resources/CMakeLists.txt b/unittests/resources/CMakeLists.txt index a243fcb77..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 @@ -39,6 +40,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_msmr.xml b/unittests/resources/xml/test_msmr.xml new file mode 100644 index 000000000..54d2c13c8 --- /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 + + + 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 + + +