twaalgos: Set 'dicho' algo as default for SAT-based minimization

* python/spot/__init__.py: Handle options.
* spot/twaalgos/dtwasat.cc: Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Handle options.
* tests/core/satmin.test: Update tests.
Now use 'sat-minimize=4' to use the naive algo.
* tests/core/satmin2.test: Update tests.
Now use --sat-minimize='naive' to use the naive algo.
* tests/python/satmin.py: Update tests.
Now use 'naive=True' to use the naive algo.
parent 67e3a4f2
......@@ -858,8 +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, dicho=False,
param=0, incr=False, assume=False):
max_states=0, sat_naive=False, sat_langmap=False,
sat_incr=0, sat_incr_steps=0):
args=''
if acc is not None:
if type(acc) is not str:
......@@ -875,14 +875,14 @@ def sat_minimize(aut, acc=None, colored=False,
if type(max_states) is not int or max_states < 0:
raise ValueError("argument 'states' should be a positive integer")
args += ',max-states=' + str(max_states)
if dicho:
args += ',dicho';
if param:
args += ',param=' + str(param)
if incr:
args += ',incr'
if assume:
args += ',assume'
if sat_naive:
args += ',sat-naive'
if sat_langmap:
args += ',sat-langmap'
if sat_incr:
args += ',sat-incr=' + str(sat_incr)
args += ',sat-incr-steps=' + str(sat_incr_steps)
from spot.impl import sat_minimize as sm
return sm(aut, args, state_based)
......
......@@ -1391,17 +1391,23 @@ namespace spot
throw std::runtime_error
("SAT-based minimization only works with deterministic automata");
bool incr = om.get("incr", 0);
bool assume = om.get("assume", 0);
int param = om.get("param", 0);
bool dicho = om.get("dicho", 0);
bool dicho_langmap = om.get("langmap", 0);
int sat_incr = om.get("sat-incr", 0);
int sat_incr_steps = om.get("sat-incr-steps", 0);
bool sat_naive = om.get("sat-naive", 0);
bool sat_langmap = om.get("sat-langmap", 0);
int states = om.get("states", -1);
int max_states = om.get("max-states", -1);
auto accstr = om.get_str("acc");
bool colored = om.get("colored", 0);
int preproc = om.get("preproc", 3);
// Set default sat-incr-steps value if not provided and used.
if (sat_incr == 1 && !sat_incr_steps) // Assume
sat_incr_steps = 6;
else if (sat_incr == 2 && !sat_incr_steps) // Incremental
sat_incr_steps = 2;
// No more om.get() below this.
om.report_unused_options();
......@@ -1494,36 +1500,39 @@ namespace spot
auto orig = a;
if (!target_is_buchi || !a->acc().is_buchi() || colored)
{
if (incr)
a = dtwa_sat_minimize_incr(a, nacc, target_acc, state_based,
max_states, colored, param);
if (sat_naive)
a = dtwa_sat_minimize
(a, nacc, target_acc, state_based, max_states, colored);
else if (assume)
else if (sat_incr == 1)
a = dtwa_sat_minimize_assume(a, nacc, target_acc, state_based,
max_states, colored, param);
max_states, colored, sat_incr_steps);
else if (sat_incr == 2)
a = dtwa_sat_minimize_incr(a, nacc, target_acc, state_based,
max_states, colored, sat_incr_steps);
else if (dicho)
else
a = dtwa_sat_minimize_dichotomy
(a, nacc, target_acc, state_based, dicho_langmap, max_states,
(a, nacc, target_acc, state_based, sat_langmap, max_states,
colored);
else
a = dtwa_sat_minimize
(a, nacc, target_acc, state_based, max_states, colored);
}
else
{
if (incr)
a = dtba_sat_minimize_incr(a, state_based, max_states, param);
if (sat_naive)
a = dtba_sat_minimize(a, state_based, max_states);
else if (assume)
a = dtba_sat_minimize_assume(a, state_based, max_states, assume);
else if (sat_incr == 1)
a = dtba_sat_minimize_assume(a, state_based, max_states,
sat_incr_steps);
else if (dicho)
a = dtba_sat_minimize_dichotomy
(a, state_based, dicho_langmap, max_states);
else if (sat_incr == 2)
a = dtba_sat_minimize_incr(a, state_based, max_states,
sat_incr_steps);
else
a = dtba_sat_minimize(a, state_based, max_states);
a = dtba_sat_minimize_dichotomy
(a, state_based, sat_langmap, max_states);
}
if (!a && !user_supplied_acc)
......
......@@ -70,15 +70,15 @@ namespace spot
ba_simul_ = opt->get("ba-simul", -1);
tba_determinisation_ = opt->get("tba-det", 0);
sat_minimize_ = opt->get("sat-minimize", 0);
param_ = opt->get("param", 0);
dicho_langmap_ = opt->get("langmap", 0);
sat_incr_steps_ = opt->get("sat-incr-steps", -2); // -2 or any num < -1
sat_langmap_ = opt->get("sat-langmap", 0);
sat_acc_ = opt->get("sat-acc", 0);
sat_states_ = opt->get("sat-states", 0);
state_based_ = opt->get("state-based", 0);
wdba_minimize_ = opt->get("wdba-minimize", 1);
if (sat_acc_ && sat_minimize_ == 0)
sat_minimize_ = 1; // 2?
sat_minimize_ = 1; // Dicho.
if (sat_states_ && sat_minimize_ == 0)
sat_minimize_ = 1;
if (sat_minimize_)
......@@ -89,6 +89,12 @@ namespace spot
if (sat_states_ <= 0)
sat_states_ = -1;
}
// Set default param value if not provided and used.
if (sat_minimize_ == 2 && sat_incr_steps_ < 0) // Assume algorithm.
sat_incr_steps_ = 6;
else if (sat_minimize_ == 3 && sat_incr_steps_ < -1) // Incr algorithm.
sat_incr_steps_ = 2;
}
}
......@@ -427,15 +433,17 @@ namespace spot
{
if (sat_states_ != -1)
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 if (sat_minimize_ == 2)
else if (sat_minimize_ == 1)
res = dtba_sat_minimize_dichotomy
(res, state_based_, dicho_langmap_);
(res, state_based_, sat_langmap_);
else if (sat_minimize_ == 2)
res = dtba_sat_minimize_assume(res, state_based_, -1,
sat_incr_steps_);
else if (sat_minimize_ == 3)
res = dtba_sat_minimize_incr(res, state_based_, -1, param_);
else // if (sat_minimize == 4)
res = dtba_sat_minimize_assume(res, state_based_, -1, param_);
res = dtba_sat_minimize_incr(res, state_based_, -1,
sat_incr_steps_);
else // if (sat_minimize == 4 || sat_minimize == -1)
res = dtba_sat_minimize(res, state_based_);
}
else
{
......@@ -444,26 +452,26 @@ namespace spot
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
sat_states_, state_based_);
else if (sat_minimize_ == 1 || sat_minimize_ == -1)
res = dtwa_sat_minimize
else if (sat_minimize_ == 1)
res = dtwa_sat_minimize_dichotomy
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_);
state_based_, sat_langmap_);
else if (sat_minimize_ == 2)
res = dtwa_sat_minimize_dichotomy
res = dtwa_sat_minimize_assume
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_, dicho_langmap_);
state_based_, -1, false, sat_incr_steps_);
else if (sat_minimize_ == 3)
res = dtwa_sat_minimize_incr
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_, -1, false, param_);
else // if (sat_minimize_ == 4)
res = dtwa_sat_minimize_assume
state_based_, -1, false, sat_incr_steps_);
else // if (sat_minimize_ == 4 || sat_minimize_ == -1)
res = dtwa_sat_minimize
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_, -1, false, param_);
state_based_);
}
if (res)
......
......@@ -189,8 +189,8 @@ namespace spot
int ba_simul_ = -1;
bool tba_determinisation_ = false;
int sat_minimize_ = 0;
int param_ = 0;
bool dicho_langmap_ = false;
int sat_incr_steps_ = 0;
bool sat_langmap_ = false;
int sat_acc_ = 0;
int sat_states_ = 0;
bool state_based_ = false;
......
This diff is collapsed.
This diff is collapsed.
......@@ -29,177 +29,211 @@ assert aut.is_deterministic()
min1 = spot.sat_minimize(aut, acc='Rabin 1')
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', dicho=True)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_langmap=True)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', assume=True)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', assume=True, param=0)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=0)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', assume=True, param=1)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=1)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', assume=True, param=2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=2)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', assume=True, param=50)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=50)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=-1)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=-1)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=0)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=0)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=1)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=1)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=2)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=50)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=50)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_naive=True)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min2 = spot.sat_minimize(aut, acc='Streett 2', dicho=True)
min2 = spot.sat_minimize(aut, acc='Streett 2')
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', assume=True)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_langmap=True)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', assume=True, param=0)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', assume=True, param=1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=0)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', assume=True, param=2)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=1)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', assume=True, param=50)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=2)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=50)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=-1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=0)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=-1)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=0)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=2)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=1)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=50)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=2)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=50)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_naive=True)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, dicho=True)
state_based=True, max_states=5)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_langmap=True)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, assume=True)
state_based=True, max_states=5, sat_incr=1)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, assume=True, param=0)
state_based=True, max_states=5, sat_incr=1,
sat_incr_steps=0)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, assume=True, param=1)
state_based=True, max_states=5, sat_incr=1,
sat_incr_steps=1)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, assume=True, param=2)
state_based=True, max_states=5, sat_incr=1,
sat_incr_steps=2)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, assume=True, param=50)
state_based=True, max_states=5, sat_incr=1,
sat_incr_steps=50)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, incr=True)
state_based=True, max_states=5, sat_incr=2)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, incr=True, param=-1)
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=-1)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, incr=True, param=0)
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=0)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, incr=True, param=1)
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=1)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, incr=True, param=2)
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=2)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, incr=True, param=50)
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=50)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_naive=True)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, dicho=True)
colored=True)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_langmap=True)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=1)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, assume=True)
colored=True, sat_incr=1, sat_incr_steps=0)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, assume=True, param=0)
colored=True, sat_incr=1, sat_incr_steps=1)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, assume=True, param=1)
colored=True, sat_incr=1, sat_incr_steps=2)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, assume=True, param=2)
colored=True, sat_incr=1, sat_incr_steps=50)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, assume=True, param=50)
colored=True, sat_incr=2)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, incr=True)
colored=True, sat_incr=2, sat_incr_steps=-1)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, incr=True, param=-1)
colored=True, sat_incr=2, sat_incr_steps=0)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, incr=True, param=0)
colored=True, sat_incr=2, sat_incr_steps=1)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, incr=True, param=1)
colored=True, sat_incr=2, sat_incr_steps=2)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, incr=True, param=2)
colored=True, sat_incr=2, sat_incr_steps=50)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, incr=True, param=50)
colored=True, sat_naive=True)
assert min4.num_sets() == 3
assert min4.num_states() == 2
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