Commit 5bbdf7fa authored by phlo's avatar phlo

improved solver parsing error handling

parent 35963b19
......@@ -119,11 +119,17 @@ Output run (const std::vector<std::string> & command, const std::string & input)
close(std_err[WRITE]);
close(exec_err[WRITE]);
// ignore SIGPIPE raised by parser errors
signal(SIGPIPE, SIG_IGN);
// write given input to stdin of child
if (!input.empty())
if (write(std_in[WRITE], input.c_str(), input.length()) < 0)
throw std::runtime_error(errmsg("writing to stdin pipe"));
// restore default SIGPIPE handler
signal(SIGPIPE, SIG_DFL);
// close stdin pipe file descriptor
close(std_in[WRITE]);
......
......@@ -31,12 +31,18 @@ std::string Solver::formula (Encoder & encoder) const
bool External::sat (const std::string & input)
{
shell::Output out;
const auto & cmd = command();
time = runtime::measure([this, &input, &cmd] {
stdout = std::move(shell::run(cmd, input).stdout);
time = runtime::measure([&input, &cmd, &out] {
out = shell::run(cmd, input);
});
if (out.stderr.rdbuf()->in_avail())
throw std::runtime_error(out.stderr.str());
stdout = std::move(out.stdout);
std::string sat;
return (stdout >> sat) && sat == "sat";
}
......
......@@ -44,10 +44,14 @@ bool Z3::sat (const std::string & formula)
z3::context c;
z3::solver s = c;
time = runtime::measure([&formula, &sat, &s] {
s.from_string(formula.c_str());
sat = s.check() == z3::sat;
});
try
{
time = runtime::measure([&formula, &sat, &s] {
s.from_string(formula.c_str());
sat = s.check() == z3::sat;
});
}
catch (const z3::exception & e) { throw std::runtime_error(e.msg()); }
return sat;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment