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

Removed debug output from Z3 adapter. Put new backward cuts in actions. 

Former-commit-id: a26787f613
main
dehnert 12 years ago
parent
e24c64e41e
commit
0329899304
2 changed files with 23 additions and 33 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 5
      src/adapters/Z3ExpressionAdapter.h
  2. 49
      src/counterexamples/SMTMinimalCommandSetGenerator.h

5
src/adapters/Z3ExpressionAdapter.h
View File

@ -39,12 +39,10 @@ namespace storm {
expression->accept(this); expression->accept(this);
z3::expr result = stack.top(); z3::expr result = stack.top();
stack.pop(); stack.pop();
LOG4CPLUS_DEBUG(logger, "Returning " << result << ".");
return result; return result;
} }
virtual void visit(ir::expressions::BinaryBooleanFunctionExpression* expression) { virtual void visit(ir::expressions::BinaryBooleanFunctionExpression* expression) {
LOG4CPLUS_DEBUG(logger, "Binary boolean function expression " << expression->toString() << ".");
expression->getLeft()->accept(this); expression->getLeft()->accept(this);
expression->getRight()->accept(this); expression->getRight()->accept(this);
@ -100,7 +98,6 @@ namespace storm {
} }
virtual void visit(ir::expressions::BinaryRelationExpression* expression) { virtual void visit(ir::expressions::BinaryRelationExpression* expression) {
LOG4CPLUS_DEBUG(logger, "Binary boolean relation expression " << expression->toString() << ".");
expression->getLeft()->accept(this); expression->getLeft()->accept(this);
expression->getRight()->accept(this); expression->getRight()->accept(this);
@ -173,7 +170,6 @@ namespace storm {
} }
virtual void visit(ir::expressions::IntegerLiteralExpression* expression) { virtual void visit(ir::expressions::IntegerLiteralExpression* expression) {
LOG4CPLUS_DEBUG(logger, "IntegerLiteralExpression " << expression->toString() << ".");
stack.push(context.int_val(expression->getValueAsInt(nullptr))); stack.push(context.int_val(expression->getValueAsInt(nullptr)));
} }
@ -208,7 +204,6 @@ namespace storm {
} }
virtual void visit(ir::expressions::VariableExpression* expression) { virtual void visit(ir::expressions::VariableExpression* expression) {
LOG4CPLUS_DEBUG(logger, "Variable " << expression->toString() << ".");
stack.push(variableToExpressionMap.at(expression->getVariableName())); stack.push(variableToExpressionMap.at(expression->getVariableName()));
} }

49
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -525,7 +525,6 @@ namespace storm {
} else { } else {
guardExpression = guardExpression | !expressionAdapter.translateExpression(command.get().getGuard()); guardExpression = guardExpression | !expressionAdapter.translateExpression(command.get().getGuard());
} }
std::cout << command.get().getGuard()->toString() << std::endl;
} }
localSolver.add(guardExpression); localSolver.add(guardExpression);
LOG4CPLUS_DEBUG(logger, "Asserted disjunction of negated guards."); LOG4CPLUS_DEBUG(logger, "Asserted disjunction of negated guards.");
@ -607,34 +606,30 @@ namespace storm {
// Popping the disjunction of negated guards from the solver stack. // Popping the disjunction of negated guards from the solver stack.
localSolver.pop(); localSolver.pop();
} }
for (auto const& labelSetImplicationsPair : backwardImplications) {
std::vector<z3::expr> implicationExpression;
// Create the first part of the implication.
for (auto label : labelSetImplicationsPair.first) {
if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
implicationExpression.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
}
} }
std::vector<z3::expr> formulae;
std::cout << "got " << backwardImplications.size() << " backward implications." << std::endl;
// for (auto const& labelSetImplicationSetsPair : backwardImplications) {
// // We only need to make this an implication if the label is not already known. If it is known,
// // we can directly assert the disjunction of the implications.
// if (relevancyInformation.knownLabels.find(labelImplicationsPair.first) == relevancyInformation.knownLabels.end()) {
// formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelImplicationsPair.first)));
// }
//
// std::set<uint_fast64_t> actualImplications;
// std::set_intersection(labelImplicationsPair.second.begin(), labelImplicationsPair.second.end(), precedingLabels.at(labelImplicationsPair.first).begin(), precedingLabels.at(labelImplicationsPair.first).end(), std::inserter(actualImplications, actualImplications.begin()));
//
// // We should assert the implications if they are not already known to be true anyway.
// std::set<uint_fast64_t> knownImplications;
// std::set_intersection(actualImplications.begin(), actualImplications.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(knownImplications, knownImplications.begin()));
//
// if (knownImplications.empty()) {
// for (auto label : actualImplications) {
// formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
// }
//
// std::cout << "actually asserting a backward implication." << std::endl;
// assertDisjunction(context, solver, formulae);
// formulae.clear();
// }
// }
// Create the disjunction of conjuncts that represent the possible implications.
for (auto const& implicationSet : labelSetImplicationsPair.second) {
implicationExpression.push_back(context.bool_val(true));
for (auto label : implicationSet) {
if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
implicationExpression.back() = implicationExpression.back() && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
}
}
}
assertDisjunction(context, solver, implicationExpression);
}
}
} }
/*! /*!

Write Preview
Loading…
Cancel
Save