22#include <boost/algorithm/string.hpp>
32 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"functionality not (yet) implemented");
36 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"functionality not (yet) implemented");
40 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"functionality not (yet) implemented");
44 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"functionality not (yet) implemented");
48 :
SmtSolver(manager), isCommandFileOpen(false), expressionAdapter(nullptr), useCarlExpressions(useCarlExpressions) {
49#ifndef STORM_HAVE_CARL
50 STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalArgumentException,
"Tried to use carl expressions but storm is not linked with CARL");
53 processIdOfSolver = 0;
54 this->expressionAdapter =
60 writeCommand(
"( exit )",
63 if (processIdOfSolver != 0) {
67 kill(processIdOfSolver, SIGTERM);
68 waitpid(processIdOfSolver,
nullptr, 0);
73 expressionAdapter->increaseScope();
74 writeCommand(
"( push 1 ) ",
true);
78 expressionAdapter->decreaseScope();
79 writeCommand(
"( pop 1 ) ",
true);
83 expressionAdapter->decreaseScope(n);
84 writeCommand(
"( pop " + std::to_string(n) +
" ) ",
true);
88 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"functionality not (yet) implemented");
92 STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalFunctionCallException,
"This solver was initialized without allowing carl expressions");
93 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"functionality not (yet) implemented");
98 STORM_LOG_THROW(useCarlExpressions, storm::exceptions::IllegalFunctionCallException,
"This solver was initialized without allowing carl expressions");
100 std::set<storm::RationalFunctionVariable> variables;
101 leftHandSide.gatherVariables(variables);
102 rightHandSide.gatherVariables(variables);
103 std::vector<std::string>
const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
104 for (
auto declaration : varDeclarations) {
105 writeCommand(declaration,
true);
107 writeCommand(
"( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) +
" )",
true);
111 STORM_LOG_THROW((variable.type() == carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException,
112 "Tried to add a constraint that consists of a non-boolean variable.");
113 std::set<storm::RationalFunctionVariable> variableSet;
114 variableSet.insert(variable);
115 std::vector<std::string>
const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variableSet);
116 for (
auto declaration : varDeclarations) {
117 writeCommand(declaration,
true);
119 std::string varName = carl::VariablePool::getInstance().getName(variable, this->useReadableVarNames);
121 writeCommand(
"( assert " + varName +
" )",
true);
123 writeCommand(
"( assert (not " + varName +
") )",
true);
130 writeCommand(
"( check-sat )",
false);
132 if (processIdOfSolver != 0) {
133 auto solverOutput = readSolverOutput();
135 solverOutput.size() == 1, storm::exceptions::UnexpectedException,
136 "expected a single line of output after smt2 command ( check-sat ). Got " + std::to_string(solverOutput.size()) +
" lines of output instead.");
137 solverOutput[0].erase(std::remove_if(solverOutput[0].begin(), solverOutput[0].end(), ::isspace), solverOutput[0].end());
138 if (solverOutput[0] ==
"sat")
140 if (solverOutput[0] ==
"unsat")
142 if (solverOutput[0] ==
"unknown")
145 STORM_LOG_DEBUG(
"unexpected solver output: " << solverOutput[0] <<
". Returning result 'unknown'");
148 STORM_LOG_WARN(
"No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving is done... Assume that the result is \"unknown\"");
154 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"functionality not (yet) implemented");
158 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"functionality not (yet) implemented");
161void SmtlibSmtSolver::init() {
162 if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isSolverCommandSet()) {
163 signal(SIGPIPE, SIG_IGN);
164 this->needsRestart =
false;
168 const std::string cmdString = storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getSolverCommand();
169 std::vector<std::string> solverCommandVec;
170 boost::split(solverCommandVec, cmdString, boost::is_any_of(
"\t "));
171 char** solverArgs =
new char*[solverCommandVec.size() + 1];
172 solverArgs[0] =
const_cast<char*
>(solverCommandVec[0].substr(0, cmdString.rfind(
'/') + 1).c_str());
173 for (uint_fast64_t argumentIndex = 1; argumentIndex < solverCommandVec.size(); ++argumentIndex) {
174 solverArgs[argumentIndex] =
const_cast<char*
>(solverCommandVec[argumentIndex].c_str());
176 solverArgs[solverCommandVec.size()] = NULL;
183 STORM_LOG_THROW(pipe(pipeIn) == 0 && pipe(pipeOut) == 0, storm::exceptions::UnexpectedException,
"Could not open pipe to new process");
187 STORM_LOG_THROW(pid >= 0, storm::exceptions::UnexpectedException,
"Could not start new process for the smt solver");
191 dup2(pipeIn[READ], STDIN_FILENO);
192 dup2(pipeOut[WRITE], STDOUT_FILENO);
193 dup2(pipeOut[WRITE], STDERR_FILENO);
196 close(pipeIn[WRITE]);
197 close(pipeOut[READ]);
198 close(pipeOut[WRITE]);
200 execv(solverCommandVec[0].c_str(), solverArgs);
202 STORM_LOG_THROW(
false, storm::exceptions::UnexpectedException,
"Could not execute the solver correctly");
205 toSolver = pipeIn[WRITE];
206 fromSolver = pipeOut[READ];
207 close(pipeOut[WRITE]);
209 processIdOfSolver = pid;
212 STORM_LOG_WARN(
"No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving can be done");
215 if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isExportSmtLibScriptSet()) {
216 STORM_LOG_DEBUG(
"The SMT-LIBv2 commands are exportet to the given file");
217 storm::io::openFile(storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getExportSmtLibScriptPath(), commandFile);
218 isCommandFileOpen =
true;
223 writeCommand(
"( set-option :print-success true )",
true);
224 writeCommand(
"( set-logic QF_NRA )",
true);
229 return this->needsRestart;
232void SmtlibSmtSolver::writeCommand(std::string smt2Command,
bool expectSuccess) {
233 if (isCommandFileOpen) {
234 commandFile << smt2Command <<
'\n';
237 if (processIdOfSolver != 0) {
238 if (write(toSolver, (smt2Command +
"\n").c_str(), smt2Command.length() + 1) < 0) {
239 STORM_LOG_DEBUG(
"Was not able to write " << smt2Command <<
"to the solver.");
242 auto output = readSolverOutput();
243 STORM_LOG_THROW(output.size() == 1, storm::exceptions::UnexpectedException,
244 "expected a single success response after smt2 command " + smt2Command +
". Got " + std::to_string(output.size()) +
245 " lines of output instead.");
246 output[0].erase(std::remove_if(output[0].begin(), output[0].end(), ::isspace), output[0].end());
247 STORM_LOG_THROW(output[0] ==
"success", storm::exceptions::UnexpectedException,
248 "expected <<success>> response after smt2 command " + smt2Command +
". Got <<" + output[0] +
">> instead");
253std::vector<std::string> SmtlibSmtSolver::readSolverOutput(
bool waitForOutput) {
254 if (processIdOfSolver == 0) {
255 STORM_LOG_DEBUG(
"failed to read solver output as the solver is not running");
256 return std::vector<std::string>();
261 }
else if (ioctl(fromSolver, FIONREAD, &bytesReadable) < 0) {
263 return std::vector<std::string>();
265 std::string solverOutput =
"";
266 const ssize_t MAX_CHUNK_SIZE = 256;
267 char chunk[MAX_CHUNK_SIZE];
268 while (bytesReadable > 0) {
269 ssize_t chunkSize = read(fromSolver, chunk, MAX_CHUNK_SIZE);
270 STORM_LOG_THROW(chunkSize >= 0, storm::exceptions::UnexpectedException,
"failed to read solver output");
271 solverOutput += std::string(chunk, chunkSize);
272 if (ioctl(fromSolver, FIONREAD, &bytesReadable) < 0) {
274 return std::vector<std::string>();
276 if (bytesReadable == 0 && solverOutput.back() !=
'\n') {
280 <<
"' did not end with newline symbol (\\n). Since we assume that this should be the case, we will wait for more output from the solver");
283 if (bytesReadable > 0) {
284 pid_t w = waitpid(processIdOfSolver,
nullptr, WNOHANG);
286 STORM_LOG_WARN_COND(w > 0,
"Error when checking whether the solver is still running. Will assume that solver has terminated.");
287 STORM_LOG_WARN(
"The solver exited unexpectedly when reading output: " << solverOutput);
288 solverOutput +=
"terminated";
289 this->needsRestart =
true;
290 this->processIdOfSolver = 0;
295 checkForErrorMessage(solverOutput);
296 std::vector<std::string> solverOutputAsVector;
297 if (solverOutput.length() > 0) {
298 solverOutput = solverOutput.substr(0, solverOutput.length() - 1);
299 boost::split(solverOutputAsVector, solverOutput, boost::is_any_of(
"\n"));
302 return solverOutputAsVector;
305void SmtlibSmtSolver::checkForErrorMessage(
const std::string message) {
306 size_t errorOccurrance = message.find(
"error");
308 if (message.find(
"timeout") != std::string::npos) {
309 STORM_LOG_INFO(
"SMT solver answered: '" << message <<
"' and I am interpreting this as timeout ");
310 this->needsRestart =
true;
311 this->processIdOfSolver = 0;
312 }
else if (message.find(
"memory") != std::string::npos) {
313 STORM_LOG_INFO(
"SMT solver answered: '" << message <<
"' and I am interpreting this as out of memory ");
314 this->needsRestart =
true;
315 this->processIdOfSolver = 0;
316 }
else if (errorOccurrance != std::string::npos) {
317 this->needsRestart =
true;
318 std::string errorMsg =
"An error was detected while checking the solver output. ";
319 STORM_LOG_DEBUG(
"Detected an error message in the solver response:\n" + message);
320 size_t firstQuoteSign = message.find(
'\"', errorOccurrance);
321 if (firstQuoteSign != std::string::npos && message.find(
"\\\"", firstQuoteSign - 1) != firstQuoteSign - 1) {
322 size_t secondQuoteSign = message.find(
'\"', firstQuoteSign + 1);
323 while (secondQuoteSign != std::string::npos && message.find(
"\\\"", secondQuoteSign - 1) == secondQuoteSign - 1) {
324 secondQuoteSign = message.find(
'\"', secondQuoteSign + 1);
326 if (secondQuoteSign != std::string::npos) {
327 errorMsg +=
"The error message was: <<" + message.substr(errorOccurrance, secondQuoteSign - errorOccurrance + 1) +
">>.";
328 STORM_LOG_THROW(
false, storm::exceptions::UnexpectedException, errorMsg);
332 errorMsg +=
"The error message could not be parsed correctly. Snippet:\n" + message.substr(errorOccurrance, 200);
333 STORM_LOG_THROW(
false, storm::exceptions::UnexpectedException, errorMsg);
This class is responsible for managing a set of typed variables and all expressions using these varia...
The base class for all model references.
An interface that captures the functionality of an SMT solver.
storm::expressions::ExpressionManager const & getManager() const
Retrieves the expression manager associated with the solver.
CheckResult
possible check results
virtual bool getBooleanValue(storm::expressions::Variable const &variable) const override
SmtlibModelReference(storm::expressions::ExpressionManager const &manager)
virtual std::string toString() const override
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const &variable) const override
virtual double getRationalValue(storm::expressions::Variable const &variable) const override
virtual ~SmtlibSmtSolver()
virtual CheckResult check() override
Checks whether the conjunction of assertions that are currently on the solver's stack is satisfiable.
virtual void push() override
Pushes a backtracking point on the solver's stack.
virtual void reset() override
Removes all assertions from the solver's stack.
virtual void add(storm::expressions::Expression const &assertion) override
Adds an assertion to the solver's stack.
virtual CheckResult checkWithAssumptions(std::set< storm::expressions::Expression > const &assumptions) override
Checks whether the conjunction of assertions that are currently on the solver's stack together with t...
bool isNeedsRestart() const
SmtlibSmtSolver(storm::expressions::ExpressionManager &manager, bool useCarlExpressions=false)
Creates a new solver with the given manager.
virtual void pop() override
Pops a backtracking point from the solver's stack.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN(message)
#define STORM_LOG_DEBUG(message)
#define STORM_LOG_ERROR(message)
#define STORM_LOG_WARN_COND(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
void openFile(std::string const &filepath, std::ofstream &filestream, bool append=false, bool silent=false)
Open the given file for writing.
carl::Relation CompareRelation
carl::Variable RationalFunctionVariable