Fix configuration generation

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