From 67463abaf0e8e3109044bd15da69c5f223f5cde5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Sebastian=20B=C3=B6hm?= <boehmseb@cs.uni-saarland.de>
Date: Mon, 23 Oct 2023 13:14:48 +0200
Subject: [PATCH] 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 37d8847a..43128aa0 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<SolverErrorCode> 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<SolverErrorCode> Z3Solver::excludeCurrentConfiguration() {
 
 Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
 Z3Solver::getCurrentConfiguration() {
-  if (Solver->check() == z3::unsat) {
-    return UNSAT;
-  }
   const z3::model M = Solver->get_model();
   auto Config = std::make_unique<vara::feature::Configuration>();
 
diff --git a/unittests/Solver/ConfigurationFactory.cpp b/unittests/Solver/ConfigurationFactory.cpp
index 2a095ea3..84988998 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<string>();
+  for (auto &config : Configs) {
+    ConfigsStrings.push_back(config.get()->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);
diff --git a/unittests/resources/CMakeLists.txt b/unittests/resources/CMakeLists.txt
index 5d47f433..dbf71e52 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 00000000..20f41419
--- /dev/null
+++ b/unittests/resources/xml/test_msmr.xml
@@ -0,0 +1,48 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE vm SYSTEM "vm.dtd">
+<vm name="SingleLocalSingle" root="root">
+    <binaryOptions>
+        <configurationOption>
+            <name>root</name>
+            <parent></parent>
+            <optional>False</optional>
+        </configurationOption>
+        <configurationOption>
+            <name>Slow</name>
+            <outputString>--slow</outputString>
+            <parent>root</parent>
+            <optional>True</optional>
+        </configurationOption>
+        <configurationOption>
+            <name>Header</name>
+            <outputString>--header</outputString>
+            <parent>root</parent>
+            <optional>True</optional>
+        </configurationOption>
+        <configurationOption>
+            <name>Extern</name>
+            <outputString>--extern</outputString>
+            <parent>root</parent>
+            <optional>True</optional>
+            <locations>
+                <sourceRange category="necessary">
+                    <path>src/MultiSharedMultipleRegions/FeatureHeader.cpp</path>
+                    <start>
+                        <line>3</line>
+                        <column>6</column>
+                    </start>
+                    <end>
+                        <line>3</line>
+                        <column>18</column>
+                    </end>
+                </sourceRange>
+            </locations>
+        </configurationOption>
+        <configurationOption>
+            <name>Cpp</name>
+            <outputString>--cpp</outputString>
+            <parent>root</parent>
+            <optional>True</optional>
+        </configurationOption>
+    </binaryOptions>
+</vm>
\ No newline at end of file