...
 
Commits (2)
This diff is collapsed.
......@@ -25,6 +25,7 @@
\usepackage{longtable}
\usepackage{caption}
% \captionsetup[longtable]{skip=0.5\baselineskip}
\usepackage{multirow}
% code
\usepackage{listings}
......@@ -79,6 +80,8 @@
\setlength{\marginparwidth}{2cm}
\usepackage{todonotes}
\setuptodonotes{size=\footnotesize, shadow}
\usepackage{marginnote}
\renewcommand{\marginpar}{\marginnote}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% commands
......
......@@ -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;
}
......