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

sat: rename dtgbasat as dtwasat

* src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Rename as...
* src/twaalgos/dtwasat.cc, src/twaalgos/dtwasat.hh: ... these.
* src/bin/autfilt.cc, src/tests/ikwiad.cc, src/twaalgos/Makefile.am,
src/twaalgos/postproc.cc, wrap/python/spot_impl.i: Adjust.
* NEWS: Mention the renamings.
parent 6237bf4c
......@@ -63,6 +63,8 @@ New in spot 1.99.5a (not yet released)
* Renamings:
is_guarantee_automaton() -> is_terminal_automaton()
tgba_run -> twa_run
dtgba_sat_synthetize() -> dtwa_sat_synthetize()
dtgba_sat_synthetize_dichotomy() -> dtwa_sat_synthetize_dichotomy()
Python:
* Add bindings for is_unambiguous().
......
......@@ -55,7 +55,7 @@
#include "twaalgos/stripacc.hh"
#include "twaalgos/remfin.hh"
#include "twaalgos/cleanacc.hh"
#include "twaalgos/dtgbasat.hh"
#include "twaalgos/dtwasat.hh"
#include "twaalgos/complement.hh"
#include "twaalgos/strength.hh"
......
......@@ -62,7 +62,7 @@
#include "twaalgos/remfin.hh"
#include "twaalgos/complete.hh"
#include "twaalgos/dtbasat.hh"
#include "twaalgos/dtgbasat.hh"
#include "twaalgos/dtwasat.hh"
#include "twaalgos/stutter.hh"
#include "twaalgos/totgba.hh"
......@@ -367,7 +367,7 @@ checked_main(int argc, char** argv)
bool cs_oblig = false;
bool opt_complete = false;
int opt_dtbasat = -1;
int opt_dtgbasat = -1;
int opt_dtwasat = -1;
for (;;)
{
......@@ -679,9 +679,9 @@ checked_main(int argc, char** argv)
else if (!strncmp(argv[formula_index], "-RG", 3))
{
if (argv[formula_index][3] != 0)
opt_dtgbasat = to_int(argv[formula_index] + 3);
opt_dtwasat = to_int(argv[formula_index] + 3);
else
opt_dtgbasat = 0;
opt_dtwasat = 0;
//output = -1;
}
else if (!strcmp(argv[formula_index], "-Rm"))
......@@ -1191,13 +1191,13 @@ checked_main(int argc, char** argv)
if (satminimized)
a = satminimized;
}
else if (opt_dtgbasat >= 0)
else if (opt_dtwasat >= 0)
{
tm.start("dtgbasat");
auto satminimized = dtgba_sat_minimize
(ensure_digraph(a), opt_dtgbasat,
spot::acc_cond::generalized_buchi(opt_dtgbasat));
tm.stop("dtgbasat");
tm.start("dtwasat");
auto satminimized = dtwa_sat_minimize
(ensure_digraph(a), opt_dtwasat,
spot::acc_cond::generalized_buchi(opt_dtwasat));
tm.stop("dtwasat");
if (satminimized)
a = satminimized;
}
......@@ -1210,7 +1210,7 @@ checked_main(int argc, char** argv)
}
if (opt_determinize || opt_dtwacomp || opt_dtbasat >= 0
|| opt_dtgbasat >= 0)
|| opt_dtwasat >= 0)
{
if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
{
......
......@@ -40,7 +40,7 @@ twaalgos_HEADERS = \
degen.hh \
dot.hh \
dtbasat.hh \
dtgbasat.hh \
dtwasat.hh \
emptiness.hh \
emptiness_stats.hh \
gv04.hh \
......@@ -95,7 +95,7 @@ libtwaalgos_la_SOURCES = \
degen.cc \
dot.cc \
dtbasat.cc \
dtgbasat.cc \
dtwasat.cc \
emptiness.cc \
gv04.cc \
hoa.cc \
......
......@@ -20,8 +20,8 @@
#include <iostream>
#include <fstream>
#include <sstream>
#include "dtgbasat.hh"
#include "reachiter.hh"
#include "dtwasat.hh"
#include "dtbasat.hh"
#include <map>
#include <utility>
#include "sccinfo.hh"
......@@ -35,7 +35,6 @@
#include "dot.hh"
#include "complete.hh"
#include "misc/optionmap.hh"
#include "dtbasat.hh"
#include "sccfilter.hh"
#include "sbacc.hh"
#include "postproc.hh"
......@@ -46,7 +45,7 @@
//
// Additionally, if the following DEBUG macro is set to 1, the CNF
// file will be output with a comment before each clause, and an
// additional output file (dtgba-sat.dbg) will be created with a list
// additional output file (dtwa-sat.dbg) will be created with a list
// of all positive variables in the result and their meaning.
#define DEBUG 0
......@@ -602,7 +601,7 @@ namespace spot
typedef std::pair<int, int> sat_stats;
static
sat_stats dtgba_to_sat(std::ostream& out, const_twa_graph_ptr ref,
sat_stats dtwa_to_sat(std::ostream& out, const_twa_graph_ptr ref,
dict& d, bool state_based, bool colored)
{
#if DEBUG
......@@ -1037,7 +1036,7 @@ namespace spot
const transition* last_sat_trans = nullptr;
#if DEBUG
std::fstream out("dtgba-sat.dbg",
std::fstream out("dtwa-sat.dbg",
std::ios_base::trunc | std::ios_base::out);
out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
std::set<int> positive;
......@@ -1119,15 +1118,15 @@ namespace spot
}
twa_graph_ptr
dtgba_sat_synthetize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
int target_state_number,
bool state_based, bool colored)
dtwa_sat_synthetize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
int target_state_number,
bool state_based, bool colored)
{
if (target_state_number == 0)
return nullptr;
trace << "dtgba_sat_synthetize(..., nacc = " << target_acc_number
trace << "dtwa_sat_synthetize(..., nacc = " << target_acc_number
<< ", acc = \"" << target_acc
<< "\", states = " << target_state_number
<< ", state_based = " << state_based << ")\n";
......@@ -1142,7 +1141,7 @@ namespace spot
timer_map t;
t.start("encode");
sat_stats s = dtgba_to_sat(solver(), a, d, state_based, colored);
sat_stats s = dtwa_to_sat(solver(), a, d, state_based, colored);
t.stop("encode");
t.start("solve");
solution = solver.get_solution();
......@@ -1186,16 +1185,16 @@ namespace spot
if (show && res)
print_dot(std::cout, res);
trace << "dtgba_sat_synthetize(...) = " << res << '\n';
trace << "dtwa_sat_synthetize(...) = " << res << '\n';
return res;
}
twa_graph_ptr
dtgba_sat_minimize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based, int max_states,
bool colored)
dtwa_sat_minimize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based, int max_states,
bool colored)
{
int n_states = (max_states < 0) ?
stats_reachable(a).states : max_states + 1;
......@@ -1204,9 +1203,9 @@ namespace spot
for (;;)
{
auto next =
dtgba_sat_synthetize(prev ? prev : a, target_acc_number,
target_acc, --n_states,
state_based, colored);
dtwa_sat_synthetize(prev ? prev : a, target_acc_number,
target_acc, --n_states,
state_based, colored);
if (!next)
return prev;
else
......@@ -1217,11 +1216,11 @@ namespace spot
}
twa_graph_ptr
dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based, int max_states,
bool colored)
dtwa_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based, int max_states,
bool colored)
{
if (max_states < 1)
max_states = stats_reachable(a).states - 1;
......@@ -1232,9 +1231,9 @@ namespace spot
{
int target = (max_states + min_states) / 2;
auto next =
dtgba_sat_synthetize(prev ? prev : a, target_acc_number,
target_acc, target, state_based,
colored);
dtwa_sat_synthetize(prev ? prev : a, target_acc_number,
target_acc, target, state_based,
colored);
if (!next)
{
min_states = target + 1;
......@@ -1358,7 +1357,7 @@ namespace spot
{
auto orig = a;
if (!target_is_buchi || !a->acc().is_buchi() || colored)
a = (dicho ? dtgba_sat_minimize_dichotomy : dtgba_sat_minimize)
a = (dicho ? dtwa_sat_minimize_dichotomy : dtwa_sat_minimize)
(a, nacc, target_acc, state_based, max_states, colored);
else
a = (dicho ? dtba_sat_minimize_dichotomy : dtba_sat_minimize)
......@@ -1370,8 +1369,8 @@ namespace spot
else
{
if (!target_is_buchi || !a->acc().is_buchi() || colored)
a = dtgba_sat_synthetize(a, nacc, target_acc, states,
state_based, colored);
a = dtwa_sat_synthetize(a, nacc, target_acc, states,
state_based, colored);
else
a = dtba_sat_synthetize(a, states, state_based);
}
......
......@@ -23,10 +23,10 @@
namespace spot
{
/// \brief Attempt to synthetize am equivalent deterministic TGBA
/// \brief Attempt to synthetize an equivalent deterministic TωA
/// with a SAT solver.
///
/// \param a the input TGBA. It should be a deterministic TGBA.
/// \param a the input TωA. It should be a deterministic TωA.
///
/// \param target_acc_number is the number of acceptance sets wanted
/// in the result.
......@@ -38,51 +38,50 @@ namespace spot
/// target_state_number reachable states.
///
/// \param state_based set to true to force all outgoing transitions
/// of a state to share the same acceptance conditions, effectively
/// turning the TGBA into a TBA.
/// of a state to share the same acceptance conditions.
///
/// \param colored if true, force all transitions to belong to
/// exactly one acceptance set.
///
/// This functions attempts to find a TGBA with \a target_acc_number
/// This functions attempts to find a TωA with \a target_acc_number
/// acceptance sets and target_state_number states that is
/// equivalent to \a a. If no such TGBA is found, a null pointer is
/// equivalent to \a a. If no such TωA is found, a null pointer is
/// returned.
SPOT_API twa_graph_ptr
dtgba_sat_synthetize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
int target_state_number,
bool state_based = false,
bool colored = false);
dtwa_sat_synthetize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
int target_state_number,
bool state_based = false,
bool colored = false);
/// \brief Attempt to minimize a deterministic TGBA with a SAT solver.
/// \brief Attempt to minimize a deterministic TωA with a SAT solver.
///
/// This calls dtgba_sat_synthetize() in a loop, with a decreasing
/// This calls dtwa_sat_synthetize() in a loop, with a decreasing
/// number of states, and returns the last successfully built TGBA.
///
/// If no smaller TGBA exist, this returns a null pointer.
/// If no smaller TGBA exists, this returns a null pointer.
SPOT_API twa_graph_ptr
dtgba_sat_minimize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based = false,
int max_states = -1,
bool colored = false);
dtwa_sat_minimize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based = false,
int max_states = -1,
bool colored = false);
/// \brief Attempt to minimize a deterministic TGBA with a SAT solver.
/// \brief Attempt to minimize a deterministic TωA with a SAT solver.
///
/// This calls dtgba_sat_synthetize() in a loop, but attempting to
/// This calls dtwa_sat_synthetize() in a loop, but attempting to
/// find the minimum number of states using a binary search.
//
/// If no smaller TBA exist, this returns a null pointer.
SPOT_API twa_graph_ptr
dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based = false,
int max_states = -1,
bool colored = false);
dtwa_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based = false,
int max_states = -1,
bool colored = false);
/// \brief High-level interface to SAT-based minimization
///
......
......@@ -28,7 +28,7 @@
#include "powerset.hh"
#include "isdet.hh"
#include "dtbasat.hh"
#include "dtgbasat.hh"
#include "dtwasat.hh"
#include "complete.hh"
#include "totgba.hh"
#include "sbacc.hh"
......@@ -413,15 +413,15 @@ namespace spot
else
{
if (sat_states_ != -1)
res = dtgba_sat_synthetize
res = dtwa_sat_synthetize
(res, target_acc, acc_cond::generalized_buchi(target_acc),
sat_states_, state_based_);
else if (sat_minimize_ == 1 || sat_minimize_ == -1)
res = dtgba_sat_minimize
res = dtwa_sat_minimize
(res, target_acc, acc_cond::generalized_buchi(target_acc),
state_based_);
else // sat_minimize_ == 2
res = dtgba_sat_minimize_dichotomy
res = dtwa_sat_minimize_dichotomy
(res, target_acc, acc_cond::generalized_buchi(target_acc),
state_based_);
}
......
......@@ -135,7 +135,7 @@
#include "twaalgos/stutter.hh"
#include "twaalgos/translate.hh"
#include "twaalgos/hoa.hh"
#include "twaalgos/dtgbasat.hh"
#include "twaalgos/dtwasat.hh"
#include "twaalgos/relabel.hh"
#include "parseaut/public.hh"
......@@ -315,7 +315,7 @@ namespace std {
%include "twaalgos/stutter.hh"
%include "twaalgos/translate.hh"
%include "twaalgos/hoa.hh"
%include "twaalgos/dtgbasat.hh"
%include "twaalgos/dtwasat.hh"
%include "twaalgos/relabel.hh"
%include "parseaut/public.hh"
......
Markdown is supported
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