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

sat: generalize the code for reading the solution

* src/misc/satsolver.cc, src/misc/satsolver.hh (satsolver_get_solution):
New function, that accepts a solution split on multiple 'v ' lines.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc (get_solution):
Remove, and adjust existing code to use satsolver_get_solution().
* src/tgbatest/readsat.cc, src/tgbatest/readsat.test: New files.
* src/tgbatest/Makefile.am: Add them.
* src/bin/man/spot-x.x: Mention the SAT competition rules for
the expected input/output format.
parent 1ab46b08
...@@ -18,7 +18,8 @@ is used by the sat\-minimize option described above. The default value ...@@ -18,7 +18,8 @@ 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 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 respectively denote the names of the input and output files. These
temporary files are created in the directory specified by \fBSPOT_TMPDIR\fR temporary files are created in the directory specified by \fBSPOT_TMPDIR\fR
or \fBTMPDIR\fR (see below). or \fBTMPDIR\fR (see below). The SAT-solver should follow the convention
of the SAT Competition for its input and output format.
.TP .TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
......
...@@ -22,6 +22,9 @@ ...@@ -22,6 +22,9 @@
#include <cstdlib> #include <cstdlib>
#include <sstream> #include <sstream>
#include <stdexcept> #include <stdexcept>
#include "satsolver.hh"
#include <fstream>
#include <limits>
namespace spot namespace spot
{ {
...@@ -67,4 +70,44 @@ namespace spot ...@@ -67,4 +70,44 @@ namespace spot
static satsolver_command cmd; static satsolver_command cmd;
return cmd.run(input, output); return cmd.run(input, output);
} }
sat_solution
satsolver_get_solution(const char* filename)
{
sat_solution sol;
std::istream* in;
if (filename[0] == '-' && filename[1] == 0)
in = &std::cin;
else
in = new std::fstream(filename, std::ios_base::in);
int c;
while ((c = in->get()) != EOF)
{
// If a line does not start with 'v ', ignore it.
if (c != 'v' || in->get() != ' ')
{
in->ignore(std::numeric_limits<std::streamsize>::max(), '\n');
continue;
}
// Otherwise, read integers one by one.
int i;
while (*in >> i)
{
if (i == 0)
goto done;
sol.push_back(i);
}
if (!in->eof())
// If we haven't reached end-of-file, then we just attempted
// to extract something that wasn't an integer. Clear the
// fail bit so that will loop over.
in->clear();
}
done:
if (in != &std::cin)
delete in;
return sol;
}
} }
...@@ -21,6 +21,7 @@ ...@@ -21,6 +21,7 @@
#define SPOT_MISC_SATSOLVER_HH #define SPOT_MISC_SATSOLVER_HH
#include "common.hh" #include "common.hh"
#include <vector>
namespace spot namespace spot
{ {
...@@ -41,6 +42,14 @@ namespace spot ...@@ -41,6 +42,14 @@ namespace spot
/// printable interface. /// printable interface.
SPOT_API int SPOT_API int
satsolver(printable* input, printable* output); satsolver(printable* input, printable* output);
typedef std::vector<int> sat_solution;
/// \brief Extract the solution of a SAT solver output.
SPOT_API sat_solution
satsolver_get_solution(const char* filename);
} }
#endif // SPOT_MISC_SATSOLVER_HH #endif // SPOT_MISC_SATSOLVER_HH
...@@ -595,26 +595,8 @@ namespace spot ...@@ -595,26 +595,8 @@ namespace spot
out << "p cnf " << d.nvars << " " << nclauses; out << "p cnf " << d.nvars << " " << nclauses;
} }
static std::string
get_solution(const char* filename)
{
std::fstream in(filename, std::ios_base::in);
std::string line;
while (std::getline(in, line))
{
if (line.empty() || line[0] == 'c')
continue;
if (line[0] == 'v')
break;
}
if (line[0] == 'v')
return line.c_str() + 1;
return "";
}
static tgba_explicit_number* static tgba_explicit_number*
sat_build(const std::string& solution, dict& satdict, const tgba* aut, sat_build(const sat_solution& solution, dict& satdict, const tgba* aut,
bool state_based) bool state_based)
{ {
bdd_dict* autdict = aut->get_dict(); bdd_dict* autdict = aut->get_dict();
...@@ -628,7 +610,6 @@ namespace spot ...@@ -628,7 +610,6 @@ namespace spot
for (int s = 1; s < satdict.cand_size; ++s) for (int s = 1; s < satdict.cand_size; ++s)
a->add_state(s); a->add_state(s);
std::stringstream sol(solution);
state_explicit_number::transition* last_aut_trans = 0; state_explicit_number::transition* last_aut_trans = 0;
const transition* last_sat_trans = 0; const transition* last_sat_trans = 0;
...@@ -636,20 +617,14 @@ namespace spot ...@@ -636,20 +617,14 @@ namespace spot
std::fstream out("dtba-sat.dbg", std::fstream out("dtba-sat.dbg",
std::ios_base::trunc | std::ios_base::out); std::ios_base::trunc | std::ios_base::out);
std::set<int> positive; std::set<int> positive;
#else
// "out" is not used, but it has to exist for the dout() macro to
// compile.
std::ostream& out(std::cout);
#endif #endif
dout << "--- transition variables ---\n"; dout << "--- transition variables ---\n";
std::set<int> acc_states; std::set<int> acc_states;
for (;;) for (sat_solution::const_iterator i = solution.begin();
i != solution.end(); ++i)
{ {
int v; int v = *i;
sol >> v;
if (!sol)
break;
if (v < 0) // FIXME: maybe we can have (v < NNN)? if (v < 0) // FIXME: maybe we can have (v < NNN)?
continue; continue;
...@@ -743,7 +718,6 @@ namespace spot ...@@ -743,7 +718,6 @@ namespace spot
{ {
trace << "dtba_sat_synthetize(..., states = " << target_state_number trace << "dtba_sat_synthetize(..., states = " << target_state_number
<< ", state_based = " << state_based << ")\n"; << ", state_based = " << state_based << ")\n";
std::string solution;
dict* current = 0; dict* current = 0;
temporary_file* cnf = 0; temporary_file* cnf = 0;
temporary_file* out = 0; temporary_file* out = 0;
...@@ -760,7 +734,7 @@ namespace spot ...@@ -760,7 +734,7 @@ namespace spot
out = create_tmpfile("dtba-sat-", ".out"); out = create_tmpfile("dtba-sat-", ".out");
satsolver(cnf, out); satsolver(cnf, out);
solution = get_solution(out->name()); sat_solution solution = satsolver_get_solution(out->name());
tgba_explicit_number* res = 0; tgba_explicit_number* res = 0;
if (!solution.empty()) if (!solution.empty())
......
...@@ -800,28 +800,8 @@ namespace spot ...@@ -800,28 +800,8 @@ namespace spot
out << "p cnf " << d.nvars << " " << nclauses; out << "p cnf " << d.nvars << " " << nclauses;
} }
static std::string
get_solution(const char* filename)
{
std::fstream in(filename, std::ios_base::in);
std::string line;
while (std::getline(in, line))
{
if (line.empty() || line[0] == 'c')
continue;
if (line[0] == 'v')
break;
}
if (line[0] == 'v')
return line.c_str() + 1;
return "";
}
static tgba_explicit_number* static tgba_explicit_number*
sat_build(const std::string& solution, dict& satdict, const tgba* aut, sat_build(const sat_solution& solution, dict& satdict, const tgba* aut,
bool state_based) bool state_based)
{ {
bdd_dict* autdict = aut->get_dict(); bdd_dict* autdict = aut->get_dict();
...@@ -833,7 +813,6 @@ namespace spot ...@@ -833,7 +813,6 @@ namespace spot
for (int s = 1; s < satdict.cand_size; ++s) for (int s = 1; s < satdict.cand_size; ++s)
a->add_state(s); a->add_state(s);
std::stringstream sol(solution);
state_explicit_number::transition* last_aut_trans = 0; state_explicit_number::transition* last_aut_trans = 0;
const transition* last_sat_trans = 0; const transition* last_sat_trans = 0;
...@@ -841,20 +820,14 @@ namespace spot ...@@ -841,20 +820,14 @@ namespace spot
std::fstream out("dtgba-sat.dbg", std::fstream out("dtgba-sat.dbg",
std::ios_base::trunc | std::ios_base::out); std::ios_base::trunc | std::ios_base::out);
std::set<int> positive; std::set<int> positive;
#else
// "out" is not used, but it has to exist for the dout() macro to
// compile.
std::ostream& out(std::cout);
#endif #endif
dout << "--- transition variables ---\n"; dout << "--- transition variables ---\n";
std::map<int, bdd> state_acc; std::map<int, bdd> state_acc;
for (;;) for (sat_solution::const_iterator i = solution.begin();
i != solution.end(); ++i)
{ {
int v; int v = *i;
sol >> v;
if (!sol)
break;
if (v < 0) // FIXME: maybe we can have (v < NNN)? if (v < 0) // FIXME: maybe we can have (v < NNN)?
continue; continue;
...@@ -946,7 +919,6 @@ namespace spot ...@@ -946,7 +919,6 @@ namespace spot
trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number
<< ", states = " << target_state_number << ", states = " << target_state_number
<< ", state_based = " << state_based << ")\n"; << ", state_based = " << state_based << ")\n";
std::string solution;
dict* current = 0; dict* current = 0;
temporary_file* cnf = 0; temporary_file* cnf = 0;
temporary_file* out = 0; temporary_file* out = 0;
...@@ -964,7 +936,7 @@ namespace spot ...@@ -964,7 +936,7 @@ namespace spot
out = create_tmpfile("dtgba-sat-", ".out"); out = create_tmpfile("dtgba-sat-", ".out");
satsolver(cnf, out); satsolver(cnf, out);
solution = get_solution(out->name()); sat_solution solution = satsolver_get_solution(out->name());
tgba_explicit_number* res = 0; tgba_explicit_number* res = 0;
if (!solution.empty()) if (!solution.empty())
......
...@@ -43,6 +43,7 @@ check_PROGRAMS = \ ...@@ -43,6 +43,7 @@ check_PROGRAMS = \
ltlprod \ ltlprod \
mixprod \ mixprod \
powerset \ powerset \
readsat \
taatgba \ taatgba \
tgbaread \ tgbaread \
tripprod tripprod
...@@ -65,6 +66,7 @@ ltlprod_SOURCES = ltlprod.cc ...@@ -65,6 +66,7 @@ ltlprod_SOURCES = ltlprod.cc
mixprod_SOURCES = mixprod.cc mixprod_SOURCES = mixprod.cc
powerset_SOURCES = powerset.cc powerset_SOURCES = powerset.cc
randtgba_SOURCES = randtgba.cc randtgba_SOURCES = randtgba.cc
readsat_SOURCES = readsat.cc
taatgba_SOURCES = taatgba.cc taatgba_SOURCES = taatgba.cc
tgbaread_SOURCES = tgbaread.cc tgbaread_SOURCES = tgbaread.cc
tripprod_SOURCES = tripprod.cc tripprod_SOURCES = tripprod.cc
......
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream>
#include "misc/satsolver.hh"
int main()
{
spot::sat_solution sol = spot::satsolver_get_solution("-");
for (spot::sat_solution::const_iterator i = sol.begin();
i != sol.end(); ++i)
std::cout << ' ' << *i;
std::cout << '\n';
}
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
# Do some quick translations to make sure the neverclaims produced by
# spot actually look correct! We do that by parsing them via ltlcross.
# ltl2neverclaim-lbtt.test does the same with LBTT if it is installed.
. ./defs
set -e
cat > foo <<EOF
c some comment
c more comment
v 12 13
cignore
vignore
v 14 -15
signore
v
EOF
test ' 12 13 14 -15' = "`../readsat < foo`"
cat > foo <<EOF
c some comment
c more comment
v12 13
cignore
vignore
v 14 0 -15
signore
v
EOF
test ' 14' = "`../readsat < foo`"
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