From 90c106f8a825768838d9adea988adb73bea9e526 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 28 Aug 2013 15:24:16 +0200 Subject: [PATCH] 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. --- src/bin/man/spot-x.x | 3 ++- src/misc/satsolver.cc | 43 ++++++++++++++++++++++++++++++++ src/misc/satsolver.hh | 9 +++++++ src/tgbaalgos/dtbasat.cc | 36 ++++----------------------- src/tgbaalgos/dtgbasat.cc | 38 ++++------------------------ src/tgbatest/Makefile.am | 2 ++ src/tgbatest/readsat.cc | 29 ++++++++++++++++++++++ src/tgbatest/readsat.test | 52 +++++++++++++++++++++++++++++++++++++++ 8 files changed, 147 insertions(+), 65 deletions(-) create mode 100644 src/tgbatest/readsat.cc create mode 100755 src/tgbatest/readsat.test diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x index cbd6e2d03..631846215 100644 --- a/src/bin/man/spot-x.x +++ b/src/bin/man/spot-x.x @@ -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 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). +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 diff --git a/src/misc/satsolver.cc b/src/misc/satsolver.cc index 224881cab..5c17c82eb 100644 --- a/src/misc/satsolver.cc +++ b/src/misc/satsolver.cc @@ -22,6 +22,9 @@ #include #include #include +#include "satsolver.hh" +#include +#include namespace spot { @@ -67,4 +70,44 @@ namespace spot static satsolver_command cmd; 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::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; + } + } diff --git a/src/misc/satsolver.hh b/src/misc/satsolver.hh index fe559919b..0f0b08575 100644 --- a/src/misc/satsolver.hh +++ b/src/misc/satsolver.hh @@ -21,6 +21,7 @@ #define SPOT_MISC_SATSOLVER_HH #include "common.hh" +#include namespace spot { @@ -41,6 +42,14 @@ namespace spot /// printable interface. SPOT_API int satsolver(printable* input, printable* output); + + + typedef std::vector 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 diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index 7d639061e..ba0f2d720 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -595,26 +595,8 @@ namespace spot 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* - 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) { bdd_dict* autdict = aut->get_dict(); @@ -628,7 +610,6 @@ namespace spot for (int s = 1; s < satdict.cand_size; ++s) a->add_state(s); - std::stringstream sol(solution); state_explicit_number::transition* last_aut_trans = 0; const transition* last_sat_trans = 0; @@ -636,20 +617,14 @@ namespace spot std::fstream out("dtba-sat.dbg", std::ios_base::trunc | std::ios_base::out); std::set positive; -#else - // "out" is not used, but it has to exist for the dout() macro to - // compile. - std::ostream& out(std::cout); #endif dout << "--- transition variables ---\n"; std::set acc_states; - for (;;) + for (sat_solution::const_iterator i = solution.begin(); + i != solution.end(); ++i) { - int v; - sol >> v; - if (!sol) - break; + int v = *i; if (v < 0) // FIXME: maybe we can have (v < NNN)? continue; @@ -743,7 +718,6 @@ namespace spot { trace << "dtba_sat_synthetize(..., states = " << target_state_number << ", state_based = " << state_based << ")\n"; - std::string solution; dict* current = 0; temporary_file* cnf = 0; temporary_file* out = 0; @@ -760,7 +734,7 @@ namespace spot out = create_tmpfile("dtba-sat-", ".out"); satsolver(cnf, out); - solution = get_solution(out->name()); + sat_solution solution = satsolver_get_solution(out->name()); tgba_explicit_number* res = 0; if (!solution.empty()) diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 8a120934b..2187aba27 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -800,28 +800,8 @@ namespace spot 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* - 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) { bdd_dict* autdict = aut->get_dict(); @@ -833,7 +813,6 @@ namespace spot for (int s = 1; s < satdict.cand_size; ++s) a->add_state(s); - std::stringstream sol(solution); state_explicit_number::transition* last_aut_trans = 0; const transition* last_sat_trans = 0; @@ -841,20 +820,14 @@ namespace spot std::fstream out("dtgba-sat.dbg", std::ios_base::trunc | std::ios_base::out); std::set positive; -#else - // "out" is not used, but it has to exist for the dout() macro to - // compile. - std::ostream& out(std::cout); #endif dout << "--- transition variables ---\n"; std::map state_acc; - for (;;) + for (sat_solution::const_iterator i = solution.begin(); + i != solution.end(); ++i) { - int v; - sol >> v; - if (!sol) - break; + int v = *i; if (v < 0) // FIXME: maybe we can have (v < NNN)? continue; @@ -946,7 +919,6 @@ namespace spot trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number << ", states = " << target_state_number << ", state_based = " << state_based << ")\n"; - std::string solution; dict* current = 0; temporary_file* cnf = 0; temporary_file* out = 0; @@ -964,7 +936,7 @@ namespace spot out = create_tmpfile("dtgba-sat-", ".out"); satsolver(cnf, out); - solution = get_solution(out->name()); + sat_solution solution = satsolver_get_solution(out->name()); tgba_explicit_number* res = 0; if (!solution.empty()) diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index c38077927..e8154f01f 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -43,6 +43,7 @@ check_PROGRAMS = \ ltlprod \ mixprod \ powerset \ + readsat \ taatgba \ tgbaread \ tripprod @@ -65,6 +66,7 @@ ltlprod_SOURCES = ltlprod.cc mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc randtgba_SOURCES = randtgba.cc +readsat_SOURCES = readsat.cc taatgba_SOURCES = taatgba.cc tgbaread_SOURCES = tgbaread.cc tripprod_SOURCES = tripprod.cc diff --git a/src/tgbatest/readsat.cc b/src/tgbatest/readsat.cc new file mode 100644 index 000000000..61855f0ca --- /dev/null +++ b/src/tgbatest/readsat.cc @@ -0,0 +1,29 @@ +// 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 . + +#include +#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'; +} diff --git a/src/tgbatest/readsat.test b/src/tgbatest/readsat.test new file mode 100755 index 000000000..834ee380a --- /dev/null +++ b/src/tgbatest/readsat.test @@ -0,0 +1,52 @@ +#!/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 . + +# 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 < foo <