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

sat: catch cases where nbclause > INT_MAX and report them

* src/misc/satsolver.hh (clause_counter): New class.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Use it.
parent ba5bddec
......@@ -22,11 +22,49 @@
#include "common.hh"
#include <vector>
#include <stdexcept>
namespace spot
{
class printable;
class clause_counter
{
private:
int count_;
public:
clause_counter()
: count_(0)
{
}
void check() const
{
if (count_ < 0)
throw std::runtime_error("too many SAT clauses (more than INT_MAX)");
}
clause_counter& operator++()
{
++count_;
check();
return *this;
}
clause_counter& operator+=(int n)
{
count_ += n;
check();
return *this;
}
int nb_clauses() const
{
return count_;
}
};
/// \brief Run a SAT solver.
///
/// Run a SAT solver using the input in file \a input,
......
......@@ -299,7 +299,7 @@ namespace spot
void dtba_to_sat(std::ostream& out, const tgba* ref, dict& d,
bool state_based)
{
int nclauses = 0;
clause_counter nclauses;
int ref_size = 0;
scc_map sm(ref);
......@@ -359,7 +359,7 @@ namespace spot
}
++j;
}
if (!nclauses)
if (!nclauses.nb_clauses())
dout << "(none)\n";
dout << "(1) the candidate automaton is complete\n";
......@@ -636,7 +636,7 @@ namespace spot
}
}
out.seekp(0);
out << "p cnf " << d.nvars << " " << nclauses;
out << "p cnf " << d.nvars << " " << nclauses.nb_clauses();
}
static tgba_explicit_number*
......@@ -769,11 +769,22 @@ namespace spot
current = new dict;
current->cand_size = target_state_number;
try
{
cnf = create_tmpfile("dtba-sat-", ".cnf");
std::fstream cnfs(cnf->name(),
std::ios_base::trunc | std::ios_base::out);
dtba_to_sat(cnfs, a, *current, state_based);
cnfs.close();
}
catch (...)
{
if (DEBUG)
xrename(cnf->name(), "dtba-sat.cnf");
delete current;
delete cnf;
throw;
}
out = create_tmpfile("dtba-sat-", ".out");
satsolver(cnf, out);
......
......@@ -476,7 +476,7 @@ namespace spot
void dtgba_to_sat(std::ostream& out, const tgba* ref, dict& d,
bool state_based)
{
int nclauses = 0;
clause_counter nclauses;
int ref_size = 0;
scc_map sm(ref);
......@@ -536,7 +536,7 @@ namespace spot
}
++j;
}
if (!nclauses)
if (!nclauses.nb_clauses())
dout << "(none)\n";
dout << "(8) the candidate automaton is complete\n";
......@@ -847,7 +847,7 @@ namespace spot
}
}
out.seekp(0);
out << "p cnf " << d.nvars << " " << nclauses;
out << "p cnf " << d.nvars << " " << nclauses.nb_clauses();
}
static tgba_explicit_number*
......@@ -977,11 +977,22 @@ namespace spot
current->cand_size = target_state_number;
current->cand_nacc = target_acc_number;
try
{
cnf = create_tmpfile("dtgba-sat-", ".cnf");
std::fstream cnfs(cnf->name(),
std::ios_base::trunc | std::ios_base::out);
dtgba_to_sat(cnfs, a, *current, state_based);
cnfs.close();
}
catch (...)
{
if (DEBUG)
xrename(cnf->name(), "dgtba-sat.cnf");
delete current;
delete cnf;
throw;
}
out = create_tmpfile("dtgba-sat-", ".out");
satsolver(cnf, out);
......
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