Merge branch 'fix-configuration-generation' into jan-dev

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/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<z3::solver> 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

lib/Solver/Z3Solver.cpp

@@ -177,35 +177,44 @@ Result<SolverErrorCode, bool> Z3Solver::hasValidConfigurations() {
 
 Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
 Z3Solver::getNextConfiguration() {
-  // Add previous configuration as a constraint
-  excludeCurrentConfiguration();
+  if (!Dirty) {
+    Dirty = true;
+  } else {
+    excludeCurrentConfiguration();
+  }
 
-  // Retrieve the next configuration
   return getCurrentConfiguration();
 }
 
 Result<SolverErrorCode, uint64_t> Z3Solver::getNumberValidConfigurations() {
+  if (Dirty) {
+    return Error(ILLEGAL_STATE);
+  }
+
   Solver->push();
   uint64_t Count = 0;
-  while (Solver->check() == z3::sat) {
-    excludeCurrentConfiguration();
+  while (getNextConfiguration()) {
     Count++;
   }
   Solver->pop();
+  Dirty = false;
   return Count;
 }
 
 Result<SolverErrorCode,
        std::vector<std::unique_ptr<vara::feature::Configuration>>>
 Z3Solver::getAllValidConfigurations() {
+  if (Dirty) {
+    return Error(ILLEGAL_STATE);
+  }
+
   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();
+  while (auto Config = getNextConfiguration()) {
+    Vector.insert(Vector.begin(), Config.extractValue());
   }
   Solver->pop();
+  Dirty = false;
   return Vector;
 }
 
@@ -232,18 +241,17 @@ Result<SolverErrorCode> 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);
@@ -258,11 +266,10 @@ Z3Solver::getCurrentConfiguration() {
   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();
+  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;

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();