Commit 7880b25a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

sat-minimize: add a max-states option

* src/twaalgos/dtbasat.cc, src/twaalgos/dtbasat.hh,
src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Add it.
* src/tests/satmin2.test: Add couple of tests.
parent 91f68ab1
......@@ -149,3 +149,30 @@ State: 0
EOF
diff output expected
cat >foo.hoa <<EOF
HOA: v1
States: 1
Start: 0
Acceptance: 4 (Fin(0)&Inf(1)) | (Fin(2)&Inf(3))
AP: 2 "b" "a"
--BODY--
State: 0
0 {3} /*{}*/
0 {1 3} /*{b}*/
0 {2} /*{a}*/
0 {2 1} /*{b, a}*/
--END--
EOF
$autfilt --sat-minimize='acc="Inf(0)|Fin(1)",max-states=2' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)",max-states=4' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
......@@ -806,9 +806,11 @@ namespace spot
}
twa_graph_ptr
dtba_sat_minimize(const const_twa_graph_ptr& a, bool state_based)
dtba_sat_minimize(const const_twa_graph_ptr& a,
bool state_based, int max_states)
{
int n_states = stats_reachable(a).states;
int n_states = (max_states < 0) ?
stats_reachable(a).states : max_states + 1;
twa_graph_ptr prev = nullptr;
for (;;)
......@@ -826,9 +828,10 @@ namespace spot
twa_graph_ptr
dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
bool state_based)
bool state_based, int max_states)
{
int max_states = stats_reachable(a).states - 1;
if (max_states < 0)
max_states = stats_reachable(a).states - 1;
int min_states = 1;
twa_graph_ptr prev = nullptr;
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita.
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
......@@ -52,7 +52,8 @@ namespace spot
/// If no smaller TBA exist, this returns a null pointer.
SPOT_API twa_graph_ptr
dtba_sat_minimize(const const_twa_graph_ptr& a,
bool state_based = false);
bool state_based = false,
int max_states = -1);
/// \brief Attempt to minimize a deterministic TBA with a SAT solver.
///
......@@ -62,5 +63,6 @@ namespace spot
/// If no smaller TBA exist, this returns a null pointer.
SPOT_API twa_graph_ptr
dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
bool state_based = false);
bool state_based = false,
int max_states = -1);
}
......@@ -1156,9 +1156,11 @@ namespace spot
dtgba_sat_minimize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based)
bool state_based,
int max_states)
{
int n_states = stats_reachable(a).states;
int n_states = (max_states < 0) ?
stats_reachable(a).states : max_states + 1;
twa_graph_ptr prev = nullptr;
for (;;)
......@@ -1179,9 +1181,11 @@ namespace spot
dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based)
bool state_based,
int max_states)
{
int max_states = stats_reachable(a).states - 1;
if (max_states < 1)
max_states = stats_reachable(a).states - 1;
int min_states = 1;
twa_graph_ptr prev = nullptr;
......@@ -1223,6 +1227,7 @@ namespace spot
bool sb = om.get("state-based", 0);
bool dicho = om.get("dichotomy", 0);
int states = om.get("states", -1);
int max_states = om.get("max-states", -1);
int nacc = om.get("gba", -1);
auto accstr = om.get_str("acc");
......@@ -1260,17 +1265,17 @@ namespace spot
tgba_complete_here(a);
if (sb)
a = sbacc(a);
if (sb && states == -1 && max_states == -1)
max_states = sbacc(a)->num_states();
if (states == -1)
{
if (!target_is_buchi || !a->acc().is_buchi())
a = (dicho ? dtgba_sat_minimize_dichotomy : dtgba_sat_minimize)
(a, nacc, target_acc, sb);
(a, nacc, target_acc, sb, max_states);
else
a = (dicho ? dtba_sat_minimize_dichotomy : dtba_sat_minimize)
(a, sb);
(a, sb, max_states);
}
else
{
......
......@@ -62,7 +62,8 @@ namespace spot
dtgba_sat_minimize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based = false);
bool state_based = false,
int max_states = -1);
/// \brief Attempt to minimize a deterministic TGBA with a SAT solver.
///
......@@ -74,7 +75,8 @@ namespace spot
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);
bool state_based = false,
int max_states = -1);
/// \brief High-level interface to SAT-based minimization
///
......
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