Skip to content

Commit

Permalink
Merge branch 'vara-dev' into f-FeatureGui
Browse files Browse the repository at this point in the history
  • Loading branch information
Sinerum authored Nov 20, 2023
2 parents 90ff5a8 + 864ff02 commit 4ca982c
Show file tree
Hide file tree
Showing 11 changed files with 199 additions and 123 deletions.
32 changes: 29 additions & 3 deletions include/vara/Solver/ConfigurationFactory.h
Original file line number Diff line number Diff line change
Expand Up @@ -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> *;
Expand Down Expand Up @@ -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.
Expand Down
4 changes: 4 additions & 0 deletions include/vara/Solver/Error.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ enum SolverErrorCode {
ALREADY_PRESENT,
NOT_ALL_CONSTRAINTS_PROCESSED,
PARENT_NOT_PRESENT,
ILLEGAL_STATE,
};

} // namespace solver
Expand Down Expand Up @@ -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;
}
Expand Down
19 changes: 0 additions & 19 deletions include/vara/Solver/Solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
14 changes: 5 additions & 9 deletions include/vara/Solver/Z3Solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand Down
75 changes: 27 additions & 48 deletions lib/Solver/Z3Solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand All @@ -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) {
Expand All @@ -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;
Expand Down
39 changes: 39 additions & 0 deletions unittests/Solver/ConfigurationFactory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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);
Expand Down
13 changes: 7 additions & 6 deletions unittests/Solver/SolverFactory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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
Loading

0 comments on commit 4ca982c

Please sign in to comment.