Commit e5874ee4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Call glucose with -verb=0.

* src/misc/satsolver.cc: Call glucose with -verb=0.
* src/bin/man/spot-x.x: Document it.
parent 977a6dfa
......@@ -14,12 +14,13 @@ spot-x \- Common fine-tuning options.
.TP
\fBSPOT_SATSOLVER\fR
If set, this variable should indicate how to call a SAT\-solver. This
is used by the sat\-minimize option described above. The default value
is \f(CW"glucose %I >%O"\fR. The escape sequences \f(CW%I\fR and \f(CW%O\fR
respectively denote the names of the input and output files. These
temporary files are created in the directory specified by \fBSPOT_TMPDIR\fR
or \fBTMPDIR\fR (see below). The SAT-solver should follow the convention
of the SAT Competition for its input and output format.
is used by the sat\-minimize option described above. The default
value is \f(CW"glucose -verb=0 %I >%O"\fR. The escape sequences
\f(CW%I\fR and \f(CW%O\fR respectively denote the names of the input
and output files. These temporary files are created in the directory
specified by \fBSPOT_TMPDIR\fR or \fBTMPDIR\fR (see below). The
SAT-solver should follow the convention of the SAT Competition for its
input and output format.
.TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
......
......@@ -40,7 +40,7 @@ namespace spot
satsolver = getenv("SPOT_SATSOLVER");
if (!satsolver)
{
satsolver = "glucose %I >%O";
satsolver = "glucose -verb=0 %I >%O";
return;
}
prime(satsolver);
......
Supports Markdown
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