22 #include <spot/twa/twagraph.hh>
50 SPOT_API twa_graph_ptr
52 unsigned target_acc_number,
54 int target_state_number,
55 bool state_based =
false,
56 bool colored =
false);
64 SPOT_API twa_graph_ptr
66 unsigned target_acc_number,
68 bool state_based =
false,
70 bool colored =
false);
78 SPOT_API twa_graph_ptr
80 unsigned target_acc_number,
82 bool state_based =
false,
85 bool colored =
false);
97 SPOT_API twa_graph_ptr
99 unsigned target_acc_number,
101 bool state_based =
false,
103 bool colored =
false,
118 SPOT_API twa_graph_ptr
120 unsigned target_acc_number,
122 bool state_based =
false,
124 bool colored =
false,
145 SPOT_API twa_graph_ptr
146 sat_minimize(twa_graph_ptr aut,
const char* opt,
bool state_based =
false);
Definition: automata.hh:27
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)
Attempt to minimize a deterministic TωA with a SAT solver.
twa_graph_ptr sat_minimize(twa_graph_ptr aut, const char *opt, bool state_based=false)
High-level interface to SAT-based minimization.
twa_graph_ptr 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)
Attempt to synthetize an equivalent deterministic TωA with a SAT solver.
twa_graph_ptr dtwa_sat_minimize_assume(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=6)
Attempt to minimize a deterministic TωA with a SAT solver.
twa_graph_ptr 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)
Attempt to minimize a deterministic TωA with a SAT solver.
twa_graph_ptr 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, bool langmap=false, int max_states=-1, bool colored=false)
Attempt to minimize a deterministic TωA with a SAT solver.
An acceptance formula.
Definition: acc.hh:479