Fixes configuration generation (#126)

resolves se-sic/VaRA#1043

Co-authored-by: Sebastian Böhm <boehmseb@cs.uni-saarland.de>

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<vara::feature::Configuration>;
     using pointer = std::unique_ptr<vara::feature::Configuration> *;
@@ -90,8 +90,34 @@ class ConfigurationFactory {
                 std::vector<std::unique_ptr<vara::feature::Configuration>>>
   getAllConfigs(feature::FeatureModel &Model,
                 const vara::solver::SolverType Type = SolverType::Z3) {
-    auto S = SolverFactory::initializeSolver(Model, Type);
-    return S->getAllValidConfigurations();
+    auto V = std::vector<std::unique_ptr<vara::feature::Configuration>>();
+    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<SolverErrorCode, uint64_t>
+  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.

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<vara::solver::SolverErrorCode> {
     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;
   }

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<SolverErrorCode, bool> 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<SolverErrorCode, uint64_t> 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<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
   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<SolverErrorCode,
-                 std::vector<std::unique_ptr<vara::feature::Configuration>>>
-  getAllValidConfigurations() = 0;
 };
 
 } // namespace vara::solver

include/vara/Solver/Z3Solver.h

@@ -60,23 +60,16 @@ class Z3Solver : public Solver {
   Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
   getCurrentConfiguration() override;
 
-  Result<SolverErrorCode, uint64_t> getNumberValidConfigurations() override;
-
   Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
   getNextConfiguration() override;
 
-  Result<SolverErrorCode,
-         std::vector<std::unique_ptr<vara::feature::Configuration>>>
-  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<SolverErrorCode> 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<z3::solver> Solver;
+
+  /// The current model of the SAT solver.
+  std::optional<z3::model> CurrentModel;
 };
 
 /// \brief This class is a visitor to convert the constraints from the

lib/Solver/Z3Solver.cpp

@@ -169,6 +169,12 @@ Result<SolverErrorCode> Z3Solver::addMixedConstraint(
 }
 
 Result<SolverErrorCode, bool> 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<SolverErrorCode, bool> Z3Solver::hasValidConfigurations() {
 
 Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
 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<SolverErrorCode, uint64_t> Z3Solver::getNumberValidConfigurations() {
-  Solver->push();
-  uint64_t Count = 0;
-  while (Solver->check() == z3::sat) {
-    excludeCurrentConfiguration();
-    Count++;
-  }
-  Solver->pop();
-  return Count;
-}
-
-Result<SolverErrorCode,
-       std::vector<std::unique_ptr<vara::feature::Configuration>>>
-Z3Solver::getAllValidConfigurations() {
-  Solver->push();
-  auto Vector = std::vector<std::unique_ptr<vara::feature::Configuration>>();
-  while (Solver->check() == z3::sat) {
-    auto Config = getCurrentConfiguration().extractValue();
-    Vector.insert(Vector.begin(), std::move(Config));
-    excludeCurrentConfiguration();
-  }
-  Solver->pop();
-  return Vector;
-}
-
 Result<SolverErrorCode>
 Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature,
                                       bool IsInAlternativeGroup) {
@@ -226,43 +208,40 @@ Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature,
   return Ok();
 }
 
-Result<SolverErrorCode> 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<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
 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<vara::feature::Configuration>();
 
-  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;

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<string>();
+  for (auto &Config : Configs) {
+    ConfigsStrings.push_back(Config->dumpToString());
+  }
+
+  auto UniqueConfigs =
+      std::set<string>(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<string>();
+  for (auto &Config : Configs) {
+    ConfigsStrings.push_back(Config->dumpToString());
+  }
+
+  auto UniqueConfigs =
+      std::set<string>(ConfigsStrings.begin(), ConfigsStrings.end());
+  EXPECT_EQ(Configs.size(), UniqueConfigs.size());
+}
+
 TEST(ConfigurationFactory, GetNConfigurations) {
   auto FM = getFeatureModel();
   auto ConfigResult = ConfigurationFactory::getNConfigs(*FM, 100);

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