Quick-fix to make configuration enumeration work.

This implementation is quite hacky and requires a redesign of the Solver API to be fixed properly.
se-sic · Oct 23, 2023 · 67463ab · 67463ab
1 parent 1e5aa2b
commit 67463ab
Show file tree

Hide file tree

Showing 4 changed files with 71 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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>