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

twaalgos: Improve data storage in SAT-minimization

Browse source 
* spot/misc/satsolver.hh: Make solver return vector<bool> instead of
vector<int>.
* spot/misc/satsolver.cc: Update code.
* spot/priv/Makefile.am: Add satcommon.*
* spot/priv/satcommon.hh: Declare helper class and factorize some
duplicate code of dt*asat.cc
* spot/priv/satcommon.cc: Implement helper class and factorize some
duplicate code of dt*asat.cc
* spot/twaalgos/dtbasat.cc: Declare helper, implement some functions
in dict struct and update code.
* spot/twaalgos/dtwasat.cc: Declare helper, implement some functions
in dict struct and update code.
* tests/core/readsat.cc: Update tests.
* tests/core/satmin.test: Typo.
* tests/core/satmin2.test: Update an expected result.
This commit is contained in:
Alexandre GBAGUIDI AISSE 2016-10-25 16:29:29 +02:00
parent 79f4c8e0d7
commit 9acd7370b2
10 changed files with 1282 additions and 1004 deletions
Download patch file Download diff file Expand all files Collapse all files

82
spot/misc/satsolver.cc
View file

@ -26,14 +26,15 @@
#include <picosat/picosat.h>
#include <fstream>
#include <limits>
#include <cassert>
#include <sys/wait.h>
namespace spot
{
satsolver::solution
std::vector<int>
satsolver_get_solution(const char* filename)
{
satsolver::solution sol;
std::vector<int> sol;
std::istream* in;
if (filename[0] == '-' && filename[1] == 0)
in = &std::cin;
@ -54,7 +55,7 @@ namespace spot
while (*in >> i)
{
if (i == 0)
goto done;
goto stop;
sol.emplace_back(i);
}
if (!in->eof())
@ -63,7 +64,7 @@ namespace spot
// fail bit so that will loop over.
in->clear();
}
done:
stop:
if (in != &std::cin)
delete in;
return sol;
@ -116,13 +117,13 @@ namespace spot
*cnf_stream_ << '\n';
nclauses_ += 1;
if (nclauses_ < 0)
throw std::runtime_error("too many SAT clauses (more than INT_MAX)");
throw std::runtime_error(": too many SAT clauses (more than INT_MAX).");
}
void satsolver::adjust_nvars(int nvars)
{
if (nvars < 0)
throw std::runtime_error("variable number must be at least 0");
throw std::runtime_error(": total number of lits. must be at least 0.");
if (psat_)
{
@ -133,7 +134,7 @@ namespace spot
if (nvars < nvars_)
{
throw std::runtime_error(
"wrong number of variables, a bigger one was already added");
": wrong number of variables, a bigger one was already added.");
}
nvars_ = nvars;
}
@ -196,19 +197,62 @@ namespace spot
}
satsolver::solution
satsolver::picosat_get_solution(int res)
spot::satsolver::satsolver_get_sol(const char* filename)
{
satsolver::solution sol;
bool empty = true;
std::istream* in;
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 done;
if (i > 0 && empty)
{
empty = false;
sol = satsolver::solution(get_nb_vars(), false);
}
if (i > 0 && !empty)
sol[i - 1] = true;
}
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:
delete in;
if (empty)
{
sol.clear();
assert(sol.empty());
}
return sol;
}
satsolver::solution
satsolver::picosat_get_sol(int res)
{
satsolver::solution sol;
if (res == PICOSAT_SATISFIABLE)
{
int nvars = get_nb_vars();
for (int lit = 1; lit <= nvars; ++lit)
{
if (picosat_deref(psat_, lit) > 0)
sol.push_back(lit);
else
sol.push_back(-lit);
}
sol.push_back(picosat_deref(psat_, lit) > 0);
}
return sol;
}
@ -221,7 +265,7 @@ namespace spot
{
p.first = 0; // A subprocess was not executed so nothing failed.
int res = picosat_sat(psat_, -1); // -1: no limit (number of decisions).
p.second = picosat_get_solution(res);
p.second = picosat_get_sol(res);
}
else
{
@ -230,11 +274,11 @@ namespace spot
*cnf_stream_ << "p cnf " << get_nb_vars() << ' ' << get_nb_clauses();
cnf_stream_->seekp(0, std::ios_base::end);
if (!*cnf_stream_)
throw std::runtime_error("Failed to update cnf header");
throw std::runtime_error(": failed to update cnf header.");
temporary_file* output = create_tmpfile("sat-", ".out");
p.first = cmd_.run(cnf_tmp_, output);
p.second = satsolver_get_solution(output->name());
p.second = satsolver_get_sol(output->name());
delete output;
}
return p;
@ -248,10 +292,10 @@ namespace spot
prime(satsolver);
if (!has('I'))
throw std::runtime_error("SPOT_SATSOLVER should contain %I to "
throw std::runtime_error(": SPOT_SATSOLVER should contain %I to "
"indicate how to use the input filename.");
if (!has('O'))
throw std::runtime_error("SPOT_SATSOLVER should contain %O to "
throw std::runtime_error(": SPOT_SATSOLVER should contain %O to "
"indicate how to use the output filename.");
}

11
spot/misc/satsolver.hh
View file

@ -114,7 +114,7 @@ namespace spot
template<typename T, typename... Args>
void comment(T first, Args... args);
typedef std::vector<int> solution;
typedef std::vector<bool> solution;
typedef std::pair<int, solution> solution_pair;
/// \brief Return std::vector<solving_return_code, solution>.
@ -130,7 +130,11 @@ namespace spot
/// \brief Extract the solution of Picosat output.
/// Must be called only if SPOT_SATSOLVER env variable is not set.
satsolver::solution
picosat_get_solution(int res);
picosat_get_sol(int res);
/// \brief Extract the solution of a SAT solver output.
satsolver::solution
satsolver_get_sol(const char* filename);
private: // variables
/// \brief A satsolver_command. Check if SPOT_SATSOLVER is given.
@ -148,9 +152,8 @@ namespace spot
};
/// \brief Extract the solution of a SAT solver output.
SPOT_API satsolver::solution
SPOT_API std::vector<int>
satsolver_get_solution(const char* filename);
}
namespace spot

2
spot/priv/Makefile.am
View file

@ -27,6 +27,8 @@ libpriv_la_SOURCES = \
bddalloc.hh \
freelist.cc \
freelist.hh \
satcommon.hh\
satcommon.cc\
trim.cc \
trim.hh \
weight.cc \

188
spot/priv/satcommon.cc Normal file
View file

@ -0,0 +1,188 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita.
//
// 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 <fstream>
#include <assert.h>
#include <spot/misc/escape.hh>
#include <spot/priv/satcommon.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/stats.hh>
#if DEBUG_CMN
#define print_debug std::cerr
#else
#define print_debug while (0) std::cout
#endif
namespace spot
{
void
vars_helper::init(unsigned size_src, unsigned size_cond, unsigned size_dst,
unsigned size_nacc, unsigned size_path, bool state_based, bool dtbasat)
{
print_debug << "init(" << size_src << ',' << size_cond << ',' << size_dst
<< ',' << size_nacc << ',' << size_path << ',' << state_based << ")\n";
size_src_ = size_src;
size_cond_ = size_cond;
size_dst_ = size_dst;
size_nacc_ = size_nacc;
size_path_ = size_path;
state_based_ = state_based;
dtbasat_ = dtbasat;
sn_mult_ = size_src * size_nacc;
cd_mult_ = size_cond * size_dst;
dn_mult_ = size_dst * size_nacc;
sd_mult_ = size_src * size_dst;
dr_mult_ = size_dst * 2;
sdr_mult_ = sd_mult_ * 2;
cdn_mult_ = size_cond * size_dst * size_nacc;
scd_mult_ = size_src * size_cond * size_dst;
psd_mult_ = size_path * size_src * size_dst;
scdn_mult_ = scd_mult_ * size_nacc;
scdnp_mult_ = scdn_mult_ * size_path;
assert(scdnp_mult_ != 0);
}
void
vars_helper::declare_all_vars(int& min_t)
{
min_t_ = min_t;
min_ta_ = min_t_ + scd_mult_;
if (!state_based_)
min_p_ = min_ta_ + scdn_mult_;
else
min_p_ = min_ta_ + sn_mult_;
if (!dtbasat_)
max_p_ = min_p_ + psd_mult_ - 1;
else
max_p_ = min_p_ + psd_mult_ * 2 - 1;
print_debug << "declare_all_trans(" << min_t << ") --> min_t_<"
<< min_t_ << ">, min_ta_<" << min_ta_ << ">, min_p<"
<< min_p_ << ">, max_p<" << max_p_ << ">\n";
// Update satdict.nvars.
// max_p_ - 1 was added after noticing that in some cases in dtbasat, the
// last variable is not used and some sat solver can complain about the
// wong number of variable in cnf mode. No worries, if it turns out to be
// used somewhere, it will be taken into account.
min_t = dtbasat_ ? max_p_ - 1 : max_p_;
assert(min_t != min_t_);
}
std::string
vars_helper::format_t(bdd_dict_ptr& debug_dict, unsigned src, bdd& cond,
unsigned dst)
{
std::ostringstream buffer;
buffer << '<' << src << ',' << bdd_format_formula(debug_dict, cond)
<< ',' << dst << '>';
return buffer.str();
}
std::string
vars_helper::format_ta(bdd_dict_ptr& debug_dict,
const acc_cond* debug_cand_acc, unsigned src, bdd& cond, unsigned dst,
const acc_cond::mark_t& acc)
{
std::ostringstream buffer;
buffer << '<' << src << ',' << bdd_format_formula(debug_dict, cond)
<< ',' << debug_cand_acc->format(acc) << ',' << dst << '>';
return buffer.str();
}
std::string
vars_helper::format_p(const acc_cond* debug_cand_acc,
const acc_cond* debug_ref_acc, unsigned src_cand, unsigned src_ref,
unsigned dst_cand, unsigned dst_ref, acc_cond::mark_t acc_cand,
acc_cond::mark_t acc_ref)
{
std::ostringstream buffer;
buffer << '<' << src_cand << ',' << src_ref << ',' << dst_cand << ','
<< dst_ref << ", " << debug_cand_acc->format(acc_cand) << ", "
<< debug_ref_acc->format(acc_ref) << '>';
return buffer.str();
}
std::string
vars_helper::format_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand,
unsigned dst_ref)
{
std::ostringstream buffer;
buffer << '<' << src_cand << ',' << src_ref;
if (src_cand == dst_cand && src_ref == dst_ref)
buffer << '>';
else
buffer << ',' << dst_cand << ',' << dst_ref << '>';
return buffer.str();
}
void
print_log(timer_map& t, int target_state_number,
twa_graph_ptr& res, satsolver& solver)
{
// Always copy the environment variable into a static string,
// so that we (1) look it up once, but (2) won't crash if the
// environment is changed.
static std::string log = []()
{
auto s = getenv("SPOT_SATLOG");
return s ? s : "";
}();
if (!log.empty())
{
std::fstream out(log,
std::ios_base::app | std::ios_base::out);
out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
const timer& te = t.timer("encode");
const timer& ts = t.timer("solve");
out << target_state_number << ',';
if (res)
{
twa_sub_statistics st = sub_stats_reachable(res);
out << st.states << ',' << st.edges << ',' << st.transitions;
}
else
{
out << ",,";
}
std::pair<int, int> s = solver.stats(); // sat_stats
out << ','
<< s.first << ',' << s.second << ','
<< te.utime() + te.cutime() << ','
<< te.stime() + te.cstime() << ','
<< ts.utime() + ts.cutime() << ','
<< ts.stime() + ts.cstime() << ",\"";
if (res)
{
std::ostringstream f;
print_hoa(f, res, "l");
escape_rfc4180(out, f.str());
}
out << "\"\n";
}
}
}

238
spot/priv/satcommon.hh Normal file
View file

@ -0,0 +1,238 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita.
//
// 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/>.
#pragma once
#include <tuple>
#include <sstream>
#include <spot/misc/bddlt.hh>
#include <spot/misc/satsolver.hh>
#include <spot/misc/timer.hh>
#include <spot/twa/twagraph.hh>
#define DEBUG_CMN 0
namespace spot
{
struct src_cond
{
unsigned src;
bdd cond;
src_cond(unsigned src, bdd cond)
: src(src), cond(cond)
{
}
bool operator<(const src_cond& other) const
{
if (this->src < other.src)
return true;
if (this->src > other.src)
return false;
return this->cond.id() < other.cond.id();
}
bool operator==(const src_cond& other) const
{
return (this->src == other.src
&& this->cond.id() == other.cond.id());
}
};
/// \brief Interface with satsolver's litterals.
///
/// This class was created to fill the need to optimize memory storage in
/// SAT-minimization.
///
/// All this relies on the fact that almost everything about the automaton
/// candidate is known in advance and most of the time, litteral's numbers
/// are just incremented continually (they are continuous...).
///
/// This class allows to handle variables by only manipulating indices.
class vars_helper
{
private:
unsigned size_src_;
unsigned size_cond_;
unsigned size_dst_;
unsigned size_nacc_;
unsigned size_path_;
bool state_based_;
bool dtbasat_;
int min_t_;
int min_ta_;
int min_p_;
int max_p_;
// Vars that will be precalculated.
unsigned sn_mult_ = 0; // src * nacc
unsigned cd_mult_ = 0; // cond * dst
unsigned dn_mult_ = 0; // dst * nacc
unsigned sd_mult_ = 0; // src * dst
unsigned dr_mult_ = 0; // dst * 2 --> used only in get_prc(...)
unsigned sdr_mult_ = 0; // src * dst * 2 --> used only in get_prc(...)
unsigned scd_mult_ = 0; // src * cond * dst
unsigned cdn_mult_ = 0; // cond * dst * nacc
unsigned psd_mult_ = 0; // path * src * dst
unsigned scdn_mult_ = 0; // src * cond * dst * nacc
unsigned scdnp_mult_ = 0; // src * cond * dst * nacc * path
public:
vars_helper()
: size_src_(0), size_cond_(0), size_dst_(0), size_nacc_(0), size_path_(0),
state_based_(false), dtbasat_(false), min_t_(0), min_ta_(0), min_p_(0),
max_p_(0)
{
#if DEBUG_CMN
std::cerr << "vars_helper() constructor called\n";
#endif
}
~vars_helper()
{
}
/// \brief Save all different sizes and precompute some values.
void
init(unsigned size_src, unsigned size_cond, unsigned size_dst,
unsigned size_nacc, unsigned size_path, bool state_based,
bool dtbasat);
/// \brief Compute min_t litteral as well as min_ta, min_p and max_p.
/// After this step, all litterals are known.
void
declare_all_vars(int& min_t);
/// \brief Return the transition's litteral corresponding to parameters.
inline int
get_t(unsigned src, unsigned cond, unsigned dst) const
{
#if DEBUG_CMN
if (src >= size_src_ || cond >= size_cond_ || dst >= size_dst_)
{
std::ostringstream buffer;
buffer << "bad arguments get_t(" << src << ',' << cond << ',' << dst
<< ")\n";
throw std::runtime_error(buffer.str());
}
std::cerr << "get_t(" << src << ',' << cond << ',' << dst << ") = "
<< min_t_ + src * cd_mult_ + cond * size_dst_ + dst << '\n';
#endif
return min_t_ + src * cd_mult_ + cond * size_dst_ + dst;
}
/// \brief Return the transition_acc's litteral corresponding to parameters.
/// If (state_based), all outgoing transitions use the same acceptance
/// variable. Therefore, for each combination (src, nacc) there is only one
/// litteral.
/// Note that with Büchi automata, there is only one nacc, thus, only one
/// litteral for each src.
inline int
get_ta(unsigned src, unsigned cond, unsigned dst, unsigned nacc = 0) const
{
#if DEBUG_CMN
if (src >= size_src_ || cond >= size_cond_ || dst >= size_dst_
|| nacc >= size_nacc_)
{
std::stringstream buffer;
buffer << "bad arguments get_ta(" << src << ',' << cond << ',' << dst
<< ',' << nacc << ")\n";
throw std::runtime_error(buffer.str());
}
int res = state_based_ ? min_ta_ + src * size_nacc_ + nacc
: min_ta_ + src * cdn_mult_ + cond * dn_mult_ + (dst * size_nacc_)
+ nacc;
std::cerr << "get_ta(" << src << ',' << cond << ',' << dst << ") = "
<< res << '\n';
#endif
return state_based_ ? min_ta_ + src * size_nacc_ + nacc
: min_ta_ + src * cdn_mult_ + cond * dn_mult_ + dst * size_nacc_ + nacc;
}
/// \brief Return the path's litteral corresponding to parameters.
inline int
get_p(unsigned path, unsigned src, unsigned dst) const
{
#if DEBUG_CMN
if (src >= size_src_ || path >= size_path_ || dst >= size_dst_)
{
std::stringstream buffer;
buffer << "bad arguments get_p(" << path << ',' << src << ',' << dst
<< ")\n";
throw std::runtime_error(buffer.str());
}
std::cerr << "get_p(" << path << ',' << src << ',' << dst << ") = "
<< min_p_ + path * sd_mult_ + src * size_dst_ + dst << '\n';
#endif
assert(!dtbasat_);
return min_p_ + path * sd_mult_ + src * size_dst_ + dst;
}
/// \brief Return the path's litteral corresponding to parameters.
/// Argument ref serves to say whether it is a candidate or a reference
/// litteral. false -> ref | true -> cand
inline int
get_prc(unsigned path, unsigned src, unsigned dst, bool cand) const
{
#if DEBUG_CMN
if (src >= size_src_ || path >= size_path_ || dst >= size_dst_)
{
std::stringstream buffer;
buffer << "bad arguments get_prc(" << path << ',' << src << ',' << dst
<< ',' << cand << ")\n";
throw std::runtime_error(buffer.str());
}
std::cerr << "get_prc(" << path << ',' << src << ',' << dst << ','
<< cand << ") = " << min_p_ + path * sdr_mult_ + src * dr_mult_ +
dst * 2 + cand << '\n';
#endif
assert(dtbasat_);
return min_p_ + path * sdr_mult_ + src * dr_mult_ + dst * 2 + cand;
}
/// \brief Use this function to get a string representation of a transition.
std::string
format_t(bdd_dict_ptr& debug_dict, unsigned src, bdd& cond,
unsigned dst);
/// \brief Use this function to get a string representation of a transition
/// acc.
std::string
format_ta(bdd_dict_ptr& debug_dict, const acc_cond* debug_cand_acc,
unsigned src, bdd& cond, unsigned dst, const acc_cond::mark_t& acc);
/// \brief Use this function to get a string representation of a path var.
std::string
format_p(const acc_cond* debug_cand_acc, const acc_cond* debug_ref_acc,
unsigned src_cand, unsigned src_ref, unsigned dst_cand,
unsigned dst_ref, acc_cond::mark_t acc_cand, acc_cond::mark_t acc_ref);
/// \brief Use this function to get a string representation of a path var.
std::string
format_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand,
unsigned dst_ref);
};
/// \brief Good old function that prints log is SPOT_SATLOG. It has been
/// moved from spot/twaalgos/dt*asat.cc files.
void
print_log(timer_map& t, int target_state_number, twa_graph_ptr& res,
satsolver& solver);
}

822
spot/twaalgos/dtbasat.cc
View file

File diff suppressed because it is too large Load diff

932
spot/twaalgos/dtwasat.cc
View file

File diff suppressed because it is too large Load diff

5
tests/core/readsat.cc
View file

@ -18,12 +18,13 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream>
#include <vector>
#include <spot/misc/satsolver.hh>
int main()
{
spot::satsolver::solution sol = spot::satsolver_get_solution("-");
for (spot::satsolver::solution::const_iterator i = sol.begin();
std::vector<int> sol = spot::satsolver_get_solution("-");
for (std::vector<int>::const_iterator i = sol.begin();
i != sol.end(); ++i)
std::cout << ' ' << *i;
std::cout << '\n';

2
tests/core/satmin.test
View file

@ -37,7 +37,7 @@ ltlcross=ltlcross
# (a U X!a) | XG(!b & XFc)
# XXG(Fa U Xb)
#
# Those one where removed because they were too long in the "expected" file.
# Those ones were removed because they were too long in the "expected" file.
# We can not exceed 80 characters!
#
# p U (q & X(r & F(s & XF(u & XF(v & XFw)))))

4
tests/core/satmin2.test
View file

@ -149,8 +149,8 @@ properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
State: 0
[!0] 0 {0}
[0] 0 {1}
[0] 0 {0}
[!0] 0 {1}
--END--
EOF