From f84ca9995c2f475f840ac0cc69b8b1eaffdf720f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 2 Nov 2017 11:11:55 +0100 Subject: [PATCH] test the SPOT_SATSOLVER envvar * tests/core/satmin3.test: New file. * tests/Makefile.am: Add it. * spot/misc/satsolver.cc: Cleanup error messages. * spot/misc/satsolver.hh (satsolver_get_solution): Remove this unused function. * tests/core/readsat.cc, tests/core/readsat.test: Delete (unused). * tests/Makefile.am: Adjust. --- spot/misc/satsolver.cc | 49 +++------------------ spot/misc/satsolver.hh | 9 +--- tests/Makefile.am | 3 +- tests/core/readsat.cc | 31 ------------- tests/core/readsat.test | 52 ---------------------- tests/core/satmin3.test | 97 +++++++++++++++++++++++++++++++++++++++++ 6 files changed, 104 insertions(+), 137 deletions(-) delete mode 100644 tests/core/readsat.cc delete mode 100755 tests/core/readsat.test create mode 100755 tests/core/satmin3.test diff --git a/spot/misc/satsolver.cc b/spot/misc/satsolver.cc index 3350597b0..fd61b76b1 100644 --- a/spot/misc/satsolver.cc +++ b/spot/misc/satsolver.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -31,45 +31,6 @@ namespace spot { - std::vector - satsolver_get_solution(const char* filename) - { - std::vector sol; - std::istream* in; - if (filename[0] == '-' && filename[1] == 0) - in = &std::cin; - else - in = new std::ifstream(filename); - - 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 stop; - sol.emplace_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(); - } - stop: - if (in != &std::cin) - delete in; - return sol; - } - // In other functions, command_given() won't be called anymore as it is more // easy to check if psat_ was initialized or not. satsolver::satsolver() @@ -379,11 +340,11 @@ namespace spot prime(satsolver); if (!has('I')) - throw std::runtime_error(": SPOT_SATSOLVER should contain %I to " - "indicate how to use the input filename."); + throw std::runtime_error("SPOT_SATSOLVER should use %I as " + "input filename."); if (!has('O')) - throw std::runtime_error(": SPOT_SATSOLVER should contain %O to " - "indicate how to use the output filename."); + throw std::runtime_error("SPOT_SATSOLVER should use %O as " + "output filename."); } bool diff --git a/spot/misc/satsolver.hh b/spot/misc/satsolver.hh index ece0a2dc1..4a850d30b 100644 --- a/spot/misc/satsolver.hh +++ b/spot/misc/satsolver.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2017 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -173,13 +173,6 @@ namespace spot std::string path_; }; - /// \brief Extract the solution of a SAT solver output. - SPOT_API std::vector - satsolver_get_solution(const char* filename); -} - -namespace spot -{ template void satsolver::comment_rec(T single) diff --git a/tests/Makefile.am b/tests/Makefile.am index afa1a3d6a..a219c431d 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -84,7 +84,6 @@ check_PROGRAMS = \ core/ngraph \ core/parity \ core/randtgba \ - core/readsat \ core/reduc \ core/reduccmp \ core/reduceu \ @@ -112,7 +111,6 @@ core_intvcmp2_SOURCES = core/intvcmp2.cc core_kripkecat_SOURCES = core/kripkecat.cc core_ngraph_SOURCES = core/ngraph.cc core_randtgba_SOURCES = core/randtgba.cc -core_readsat_SOURCES = core/readsat.cc core_taatgba_SOURCES = core/taatgba.cc core_tgbagraph_SOURCES = core/twagraph.cc core_consterm_SOURCES = core/consterm.cc @@ -294,6 +292,7 @@ TESTS_twa = \ core/basimul.test \ core/satmin.test \ core/satmin2.test \ + core/satmin3.test \ core/spotlbtt.test \ core/ltlcross.test \ core/spotlbtt2.test \ diff --git a/tests/core/readsat.cc b/tests/core/readsat.cc deleted file mode 100644 index 3301f9b21..000000000 --- a/tests/core/readsat.cc +++ /dev/null @@ -1,31 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015 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 -#include - -int main() -{ - std::vector sol = spot::satsolver_get_solution("-"); - for (std::vector::const_iterator i = sol.begin(); - i != sol.end(); ++i) - std::cout << ' ' << *i; - std::cout << '\n'; -} diff --git a/tests/core/readsat.test b/tests/core/readsat.test deleted file mode 100755 index 90672caf1..000000000 --- a/tests/core/readsat.test +++ /dev/null @@ -1,52 +0,0 @@ -#!/bin/sh -# -*- coding: utf-8 -*- -# Copyright (C) 2013, 2015 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 <. + +. ./defs +set -e + + +# Make sure the SPOT_SATSOLVER envar works. + +# DRA produced by ltl2dstar for GFp0 -> GFp1 +cat >test.hoa <err && exit 1 +grep 'autfilt: SPOT_SATSOLVER should use %I' err + +SPOT_SATSOLVER='false %I' \ + autfilt --sat-minimize test.hoa --stats=%s 2>err && exit 1 +grep 'autfilt: SPOT_SATSOLVER should use %O' err + +SPOT_SATSOLVER='false %I %O' \ + autfilt --sat-minimize test.hoa --stats=%s >output +test `cat output` = 4 + +SPOT_SATSOLVER='this-does-not-exist %I %O' \ + autfilt --sat-minimize test.hoa --stats=%s 2>err && exit +grep 'this-does-not-exist.*failed' err + +# Now use some real one if we can find one. + +if (picosat -h >/dev/null) 2>/dev/null; then + SPOT_SATSOLVER='picosat %I >%O' +elif (glucose --help >/dev/null) 2>/dev/null; then + SPOT_SATSOLVER='glucose -model -verb=0 %I >%O' +else + exit 77 +fi + +export SPOT_SATSOLVER + +# Let's try to find a smaller transition-based Streett automaton We +# easily really check the expected automaton, because different SAT +# solver (even different versions of glucose) can return different +# automata. +autfilt --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output +test `cat output` = 1 + +autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output +test `cat output` = 3