twaalgos: Implement dt*a_sat_minimize_incr(...) functions

* python/spot/__init__.py: Add 'incr' boolean argument.
* spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_incr(...).
* spot/twaalgos/dtbasat.hh: Declare it.
* spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_incr(...) and
deal with options.
* spot/twaalgos/dtwasat.hh: Declare it.
* spot/twaalgos/postproc.cc: Add option --sat-minimize=incr.
* spot/twaalgos/postproc.hh: Add incr parameter.
* tests/core/satmin.test: Add tests for incremental version.
Update expected result.
* tests/core/satmin2.test: Add tests for incremental version.
* tests/python/satmin.py: Add tests for incremental version.
parent 9acd7370
......@@ -858,7 +858,8 @@ for fun in ['remove_x', 'relabel', 'relabel_bse',
# Better interface to the corresponding C++ function.
def sat_minimize(aut, acc=None, colored=False,
state_based=False, states=0,
max_states=0, dichotomy=False):
max_states=0, dichotomy=False,
param=0, incr=False):
args=''
if acc is not None:
if type(acc) is not str:
......@@ -875,7 +876,11 @@ def sat_minimize(aut, acc=None, colored=False,
raise ValueError("argument 'states' should be a positive integer")
args += ',max-states=' + str(max_states)
if dichotomy:
args += ',dichotomy';
args += ',dichotomy'
if param:
args += ',param=' + str(param)
if incr:
args += ',incr'
from spot.impl import sat_minimize as sm
return sm(aut, args, state_based)
......
......@@ -738,13 +738,96 @@ namespace spot
if (!solution.second.empty())
res = sat_build(solution.second, d, a, state_based);
// Print log if env var SPOT_SATLOG is set.
print_log(t, target_state_number, res, solver);
print_log(t, target_state_number, res, solver); // If SPOT_SATLOG is set.
trace << "dtba_sat_synthetize(...) = " << res << '\n';
return res;
}
twa_graph_ptr
dtba_sat_minimize_incr(const const_twa_graph_ptr& a,
bool state_based, int max_states, int sat_incr_steps)
{
if (!a->acc().is_buchi())
throw std::runtime_error
(": dtba_sat_minimize_incr() can only work with Büchi acceptance.");
const_twa_graph_ptr prev = a;
dict d;
d.cand_size = (max_states < 0) ?
stats_reachable(prev).states - 1 : max_states;
if (d.cand_size == 0)
return nullptr;
trace << "dtba_sat_minimize_incr(..., states = " << d.cand_size
<< ", state_based = " << state_based << ")\n";
bool naive = sat_incr_steps < 0;
trace << "sat_incr_steps: " << sat_incr_steps << '\n';
twa_graph_ptr next = spot::make_twa_graph(spot::make_bdd_dict());
while (next && d.cand_size > 0)
{
// First iteration of classic solving.
satsolver solver;
timer_map t1;
t1.start("encode");
dtba_to_sat(solver, prev, d, state_based);
t1.stop("encode");
t1.start("solve");
satsolver::solution_pair solution = solver.get_solution();
t1.stop("solve");
next = solution.second.empty() ? nullptr :
sat_build(solution.second, d, prev, state_based);
print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set.
trace << "First iteration done\n";
// Compute the AP used.
bdd ap = prev->ap_vars();
// Incremental solving loop.
unsigned orig_cand_size = d.cand_size;
unsigned alpha_size = d.alpha_vect.size();
for (int k = 0; next && d.cand_size > 0 && (naive || k < sat_incr_steps);
++k)
{
t1.start("encode");
prev = next;
int reach_states = stats_reachable(prev).states;
cnf_comment("Next iteration: ", reach_states - 1, "\n");
trace << "Encoding the deletion of state " << reach_states - 1 << '\n';
// Add new constraints.
for (unsigned i = reach_states - 1; i < d.cand_size; ++i)
for (unsigned l = 0; l < alpha_size; ++l)
for (unsigned j = 0; j < orig_cand_size; ++j)
solver.add({-d.transid(j, l, i), 0});
d.cand_size = reach_states - 1;
t1.stop("encode");
t1.start("solve");
satsolver::solution_pair solution = solver.get_solution();
t1.stop("solve");
next = solution.second.empty() ? nullptr :
sat_build(solution.second, d, prev, state_based);
print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set.
}
if (next)
{
trace << "Starting from scratch\n";
prev = next;
d = dict();
d.cand_size = stats_reachable(prev).states - 1;
if (d.cand_size == 0)
next = nullptr;
}
}
return prev == a ? nullptr : std::const_pointer_cast<spot::twa_graph>(prev);
}
twa_graph_ptr
dtba_sat_minimize(const const_twa_graph_ptr& a,
bool state_based, int max_states)
......
......@@ -65,4 +65,20 @@ namespace spot
dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
bool state_based = false,
int max_states = -1);
/// \brief Attempt to minimize a det. TBA with a SAT solver.
///
/// This acts like dtba_sat_synthetize() and obtains a first minimized
/// automaton. Then, incrementally, it encodes the deletion of one state
/// and solves it as many time as param value.
/// If param >= 0, this process is fully repeated until the minimal automaton
/// is found. Otherwise, it continues to delete states one by one
/// incrementally until the minimal automaton is found.
///
/// If no smaller TBA exist, this returns a null pointer.
SPOT_API twa_graph_ptr
dtba_sat_minimize_incr(const const_twa_graph_ptr& a,
bool state_based = false,
int max_states = -1,
int param = 2);
}
......@@ -541,7 +541,7 @@ namespace spot
// Compute the AP used.
bdd ap = ref->ap_vars();
// Count the number of atomic propositions
// Count the number of atomic propositions.
int nap = 0;
{
bdd cur = ap;
......@@ -1015,8 +1015,7 @@ namespace spot
if (!solution.second.empty())
res = sat_build(solution.second, d, a, state_based);
// Print log if env var SPOT_SATLOG is set.
print_log(t, target_state_number, res, solver);
print_log(t, target_state_number, res, solver); // if SPOT_SATLOG is set.
trace << "dtwa_sat_synthetize(...) = " << res << '\n';
return res;
......@@ -1055,6 +1054,97 @@ namespace spot
}
}
twa_graph_ptr
dtwa_sat_minimize_incr(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 sat_incr_steps)
{
const_twa_graph_ptr prev = a;
dict d(prev);
d.cand_size = (max_states < 0) ?
stats_reachable(prev).states - 1 : max_states;
d.cand_nacc = target_acc_number;
d.cand_acc = target_acc;
if (d.cand_size == 0)
return nullptr;
trace << "dtwa_sat_minimize_incr(..., nacc = " << target_acc_number
<< ", acc = \"" << target_acc << "\", states = " << d.cand_size
<< ", state_based = " << state_based << ")\n";
bool naive = sat_incr_steps < 0;
trace << "sat_incr_steps: " << sat_incr_steps << '\n';
twa_graph_ptr next = spot::make_twa_graph(spot::make_bdd_dict());
while (next && d.cand_size > 0)
{
// First iteration of classic solving.
satsolver solver;
timer_map t1;
t1.start("encode");
dtwa_to_sat(solver, prev, d, state_based, colored);
t1.stop("encode");
t1.start("solve");
satsolver::solution_pair solution = solver.get_solution();
t1.stop("solve");
next = solution.second.empty() ? nullptr :
sat_build(solution.second, d, prev, state_based);
print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set.
trace << "First iteraton done\n";
// Compute the AP used.
bdd ap = prev->ap_vars();
// Incremental solving loop.
unsigned orig_cand_size = d.cand_size;
unsigned alpha_size = d.alpha_vect.size();
for (int k = 0; next && d.cand_size > 0 && (naive || k < sat_incr_steps);
++k)
{
t1.start("encode");
prev = next;
int reach_states = stats_reachable(prev).states;
cnf_comment("Next iteration:", reach_states - 1, "\n");
trace << "Encoding the deletion of state " << reach_states - 1 << '\n';
// Add new constraints.
for (unsigned i = reach_states - 1; i < d.cand_size; ++i)
for (unsigned l = 0; l < alpha_size; ++l)
for (unsigned j = 0; j < orig_cand_size; ++j)
solver.add({-d.transid(j, l, i), 0});
d.cand_size = reach_states - 1;
t1.stop("encode");
t1.start("solve");
solution = solver.get_solution();
t1.stop("solve");
next = solution.second.empty() ? nullptr :
sat_build(solution.second, d, prev, state_based);
print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set.
}
if (next)
{
trace << "Starting from scratch\n";
prev = next;
d = dict(prev);
d.cand_size = stats_reachable(prev).states - 1;
d.cand_nacc = target_acc_number;
d.cand_acc = target_acc;
if (d.cand_size == 0)
next = nullptr;
}
};
return prev == a ? nullptr : std::const_pointer_cast<spot::twa_graph>(prev);
}
twa_graph_ptr
dtwa_sat_minimize(const const_twa_graph_ptr& a,
unsigned target_acc_number,
......@@ -1135,6 +1225,8 @@ namespace spot
auto accstr = om.get_str("acc");
bool colored = om.get("colored", 0);
int preproc = om.get("preproc", 3);
bool incr = om.get("incr", 0);
int param = om.get("param", 0);
// No more om.get() below this.
om.report_unused_options();
......@@ -1227,11 +1319,24 @@ namespace spot
{
auto orig = a;
if (!target_is_buchi || !a->acc().is_buchi() || colored)
a = (dicho ? dtwa_sat_minimize_dichotomy : dtwa_sat_minimize)
(a, nacc, target_acc, state_based, max_states, colored);
{
if (incr)
a = dtwa_sat_minimize_incr(a, nacc, target_acc, state_based,
max_states, colored, param);
else
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)
(a, state_based, max_states);
{
if (incr)
a = dtba_sat_minimize_incr(a, state_based, max_states, param);
else
a = (dicho ? dtba_sat_minimize_dichotomy
: dtba_sat_minimize)
(a, state_based, max_states);
}
if (!a && !user_supplied_acc)
a = orig;
......
......@@ -83,6 +83,25 @@ namespace spot
int max_states = -1,
bool colored = false);
/// \brief Attempt to minimize a deterministic TωA with a SAT solver.
///
/// It acts like dtwa_sat_synthetisze() and obtains a first minimized
/// automaton. Then, incrementally, it encodes and solves the deletion of one
/// state as many time as param value.
/// If param >= 0, this process is fully repeated until the minimal automaton
/// is found. Otherwise, it continues to delete states one by one
/// incrementally until the minimal automaton is found.
///
/// If no smaller TGBA exists, this returns a null pointer.
SPOT_API twa_graph_ptr
dtwa_sat_minimize_incr(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,
int param = 2);
/// \brief High-level interface to SAT-based minimization
///
/// Minimize the automaton \a aut, using options \a opt.
......@@ -94,7 +113,10 @@ namespace spot
/// acc = "generalized-Buchi 2"
/// acc = "Rabin 3"
/// acc = "same" /* default */
/// dichotomy = 1 // use dichotomy instead of decreasing loop
/// dichotomy = 1 // use dichotomy
/// incr = 1 // use satsolver incrementally to attempt to delete a
/// fixed number of states before starting from scratch
/// incr < 0 // use satsolver incrementally, never restart
/// colored = 1 // build a colored TωA
///
SPOT_API twa_graph_ptr
......
......@@ -69,6 +69,7 @@ namespace spot
scc_filter_ = opt->get("scc-filter", -1);
ba_simul_ = opt->get("ba-simul", -1);
tba_determinisation_ = opt->get("tba-det", 0);
incr_ = opt->get("incr", 0);
sat_minimize_ = opt->get("sat-minimize", 0);
sat_acc_ = opt->get("sat-acc", 0);
sat_states_ = opt->get("sat-states", 0);
......@@ -427,8 +428,10 @@ namespace spot
res = dtba_sat_synthetize(res, sat_states_, state_based_);
else if (sat_minimize_ == 1 || sat_minimize_ == -1)
res = dtba_sat_minimize(res, state_based_);
else // sat_minimize_ == 2
else if (sat_minimize_ == 2)
res = dtba_sat_minimize_dichotomy(res, state_based_);
else // sat_minimize_ = 3
res = dtba_sat_minimize_incr(res, state_based_, -1, incr_);
}
else
{
......@@ -442,12 +445,17 @@ namespace spot
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_);
else // sat_minimize_ == 2
else if (sat_minimize_ == 2)
res = dtwa_sat_minimize_dichotomy
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_);
}
else // sat_minimize_ = 3
res = dtwa_sat_minimize_incr
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_, -1, false, incr_);
}
if (res)
{
......
......@@ -188,6 +188,7 @@ namespace spot
int scc_filter_ = -1;
int ba_simul_ = -1;
bool tba_determinisation_ = false;
int incr_ = 0;
int sat_minimize_ = 0;
int sat_acc_ = 0;
int sat_states_ = 0;
......
This diff is collapsed.
......@@ -46,22 +46,36 @@ State: 2
[!0] 2
--END--
EOF
cat >expected <<EOF
transitions: 2
edges: 2
states: 1
nondeterministic states: 0
EOF
../ikwiad -RS1 -kt -XH input.hoa > output
diff output expected
# At some point, this formula was correctly minimized, but
# the output was not marked as state-based.
ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,incr=-1' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,incr=0' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,incr=1' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,incr=2' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,incr=50' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
# DRA produced by ltl2dstar for GFp0 -> GFp1
......@@ -96,18 +110,48 @@ State: 3 {1 3}
2
--END--
EOF
# Let's try to find a smaller transition-based Streett automaton We
# easily really check the expected automaton, because different SAT
# solver (even different versions of glucose) can return different
# automata.
$autfilt --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output
test `cat output` = 1
$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=-1' test.hoa \
--stats=%s >output
test `cat output` = 1
$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=0' test.hoa \
--stats=%s >output
test `cat output` = 1
$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=1' test.hoa \
--stats=%s >output
test `cat output` = 1
$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=2' test.hoa \
--stats=%s >output
test `cat output` = 1
$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=50' test.hoa \
--stats=%s >output
test `cat output` = 1
# How about a state-based DSA?
$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa \
--stats=%s > output
test `cat output` = 3
$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=-1' test.hoa \
--stats=%s > output
test `cat output` = 3
$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=0' test.hoa \
--stats=%s > output
test `cat output` = 3
$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=1' test.hoa \
--stats=%s > output
test `cat output` = 3
$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=2' test.hoa \
--stats=%s > output
test `cat output` = 3
$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=50' test.hoa \
--stats=%s > output
test `cat output` = 3
# How about a state-based DPA?
$autfilt -S --sat-minimize='acc="parity max even 3",colored' -H test.hoa \
......@@ -118,6 +162,47 @@ grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=-1' \
-H test.hoa > output
cat output
grep 'properties:.*colored' output
grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=0' \
-H test.hoa > output
cat output
grep 'properties:.*colored' output
grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=1' \
-H test.hoa > output
cat output
grep 'properties:.*colored' output
grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=2' \
-H test.hoa > output
cat output
grep 'properties:.*colored' output
grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=50' \
-H test.hoa > output
cat output
grep 'properties:.*colored' output
grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
# I get headaches whenever I think about this acceptance condition, so
# it should be a good test case.
......@@ -136,9 +221,6 @@ State: 1
[!0] 1 {1}
--END--
EOF
$autfilt -H --sat-minimize special.hoa > output
cat >expected <<EOF
HOA: v1
States: 1
......@@ -153,8 +235,19 @@ State: 0
[!0] 0 {1}
--END--
EOF
$autfilt -H --sat-minimize special.hoa > output
diff output expected
$autfilt -H --sat-minimize='incr=-1' special.hoa > output
diff output expected
$autfilt -H --sat-minimize='incr=0' special.hoa > output
diff output expected
$autfilt -H --sat-minimize='incr=1' special.hoa > output
diff output expected
$autfilt -H --sat-minimize='incr=2' special.hoa > output
diff output expected
$autfilt -H --sat-minimize='incr=50' special.hoa > output
diff output expected
cat >foo.hoa <<EOF
HOA: v1
......@@ -170,15 +263,61 @@ State: 0
0 {2 1} /*{b, a}*/
--END--
EOF
$autfilt --sat-minimize='acc="Streett 1",max-states=2' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=-1' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=0' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=1' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=2' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=50' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Rabin 1",max-states=4' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=-1' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=0' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=1' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=2' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=50' 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
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,incr=-1' \
foo.hoa --stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,incr=0' \
foo.hoa --stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,incr=1' \