alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

test the SPOT_SATSOLVER envvar

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2017-11-02 11:11:55 +01:00
parent 161bb0675f
commit f84ca9995c
6 changed files with 104 additions and 137 deletions
Download patch file Download diff file Expand all files Collapse all files

49
spot/misc/satsolver.cc
View file

@ -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<int>
satsolver_get_solution(const char* filename)
{
std::vector<int> 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<std::streamsize>::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

9
spot/misc/satsolver.hh
View file

@ -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<int>
satsolver_get_solution(const char* filename);
}
namespace spot
{
template<typename T>
void
satsolver::comment_rec(T single)