sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

remove outdated parts in highlevel counterexamplse

tempestpy_adaptions
Sebastian Junges 7 years ago
parent
e29e6c7cd2
commit
d1ab260068
1 changed files with 0 additions and 106 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 106
      src/storm/counterexamples/SMTMinimalLabelSetGenerator.h

106
src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
View File

@ -1162,112 +1162,6 @@ namespace storm {
return relaxingVariable;
}
/*!
* Asserts that the input vector encodes a decimal smaller or equal to one.
*
* @param context The Z3 context in which to build the expressions.
* @param solver The solver to use for the satisfiability evaluation.
* @param input The binary encoded input number.
*/
static void assertLessOrEqualOne(z3::context& context, z3::solver& solver, std::vector<z3::expr> input) {
std::transform(input.begin(), input.end(), input.begin(), [](z3::expr e) -> z3::expr { return !e; });
assertConjunction(context, solver, input);
}
/*!
* Asserts that at most one of given literals may be true at any time.
*
* @param context The Z3 context in which to build the expressions.
* @param solver The solver to use for the satisfiability evaluation.
* @param blockingVariables A vector of variables out of which only one may be true.
*/
static void assertAtMostOne(z3::context& context, z3::solver& solver, std::vector<z3::expr> const& literals) {
std::vector<z3::expr> counter = createCounterCircuit(context, literals);
assertLessOrEqualOne(context, solver, counter);
}
/*!
* Performs one Fu-Malik-Maxsat step.
*
* @param context The Z3 context in which to build the expressions.
* @param solver The solver to use for the satisfiability evaluation.
* @param variableInformation A structure with information about the variables for the labels.
* @return True iff the constraint system was satisfiable.
*/
static bool fuMalikMaxsatStep(z3::context& context, z3::solver& solver, std::vector<z3::expr>& auxiliaryVariables, std::vector<z3::expr>& softConstraints, uint_fast64_t& nextFreeVariableIndex) {
z3::expr_vector assumptions(context);
for (auto const& auxiliaryVariable : auxiliaryVariables) {
assumptions.push_back(!auxiliaryVariable);
}
// Check whether the assumptions are satisfiable.
STORM_LOG_DEBUG("Invoking satisfiability checking.");
z3::check_result result = solver.check(assumptions);
STORM_LOG_DEBUG("Done invoking satisfiability checking.");
if (result == z3::sat) {
return true;
} else {
STORM_LOG_DEBUG("Computing unsat core.");
z3::expr_vector unsatCore = solver.unsat_core();
STORM_LOG_DEBUG("Computed unsat core.");
std::vector<z3::expr> blockingVariables;
blockingVariables.reserve(unsatCore.size());
// Create stringstream to build expression names.
std::stringstream variableName;
for (uint_fast64_t softConstraintIndex = 0; softConstraintIndex < softConstraints.size(); ++softConstraintIndex) {
for (uint_fast64_t coreIndex = 0; coreIndex < unsatCore.size(); ++coreIndex) {
bool isContainedInCore = false;
if (softConstraints[softConstraintIndex] == unsatCore[coreIndex]) {
isContainedInCore = true;
}
if (isContainedInCore) {
variableName.clear();
variableName.str("");
variableName << "b" << nextFreeVariableIndex;
blockingVariables.push_back(context.bool_const(variableName.str().c_str()));
variableName.clear();
variableName.str("");
variableName << "a" << nextFreeVariableIndex;
++nextFreeVariableIndex;
auxiliaryVariables[softConstraintIndex] = context.bool_const(variableName.str().c_str());
softConstraints[softConstraintIndex] = softConstraints[softConstraintIndex] || blockingVariables.back();
solver.add(softConstraints[softConstraintIndex] || auxiliaryVariables[softConstraintIndex]);
}
}
}
assertAtMostOne(context, solver, blockingVariables);
}
return false;
}
/*!
* Rules out the given command set for the given solver.
*
* @param context The Z3 context in which to build the expressions.
* @param solver The solver to use for the satisfiability evaluation.
* @param commandSet The command set to rule out as a solution.
* @param variableInformation A structure with information about the variables for the labels.
*/
static void ruleOutSolution(z3::context& context, z3::solver& solver, boost::container::flat_set<uint_fast64_t> const& commandSet, VariableInformation const& variableInformation) {
z3::expr blockSolutionExpression = context.bool_val(false);
for (auto labelIndexPair : variableInformation.labelToIndexMap) {
if (commandSet.find(labelIndexPair.first) != commandSet.end()) {
blockSolutionExpression = blockSolutionExpression || variableInformation.labelVariables[labelIndexPair.second];
}
}
solver.add(blockSolutionExpression);
}
/*!
* Determines the set of labels that was chosen by the given model.

Write Preview
Loading…
Cancel
Save