mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
make aig/ite extraction conditional
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
afa34a1c12
commit
dddd740846
|
@ -106,6 +106,7 @@ namespace sat {
|
||||||
m_anf_exlin = p.anf_exlin();
|
m_anf_exlin = p.anf_exlin();
|
||||||
m_cut_simplify = p.cut();
|
m_cut_simplify = p.cut();
|
||||||
m_cut_delay = p.cut_delay();
|
m_cut_delay = p.cut_delay();
|
||||||
|
m_cut_aig = p.cut_aig();
|
||||||
m_cut_lut = p.cut_lut();
|
m_cut_lut = p.cut_lut();
|
||||||
m_cut_xor = p.cut_xor();
|
m_cut_xor = p.cut_xor();
|
||||||
m_cut_dont_cares = p.cut_dont_cares();
|
m_cut_dont_cares = p.cut_dont_cares();
|
||||||
|
|
|
@ -123,6 +123,7 @@ namespace sat {
|
||||||
bool m_binspr;
|
bool m_binspr;
|
||||||
bool m_cut_simplify;
|
bool m_cut_simplify;
|
||||||
unsigned m_cut_delay;
|
unsigned m_cut_delay;
|
||||||
|
bool m_cut_aig;
|
||||||
bool m_cut_lut;
|
bool m_cut_lut;
|
||||||
bool m_cut_xor;
|
bool m_cut_xor;
|
||||||
bool m_cut_dont_cares;
|
bool m_cut_dont_cares;
|
||||||
|
|
|
@ -181,6 +181,8 @@ namespace sat {
|
||||||
literal lit = s.trail_literal(m_trail_size);
|
literal lit = s.trail_literal(m_trail_size);
|
||||||
m_aig_cuts.add_node(lit, and_op, 0, 0);
|
m_aig_cuts.add_node(lit, and_op, 0, 0);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
clause_vector clauses(s.clauses());
|
||||||
|
|
||||||
std::function<void (literal head, literal_vector const& ands)> on_and =
|
std::function<void (literal head, literal_vector const& ands)> on_and =
|
||||||
[&,this](literal head, literal_vector const& ands) {
|
[&,this](literal head, literal_vector const& ands) {
|
||||||
|
@ -193,13 +195,13 @@ namespace sat {
|
||||||
m_aig_cuts.add_node(head, ite_op, 3, args);
|
m_aig_cuts.add_node(head, ite_op, 3, args);
|
||||||
m_stats.m_xites++;
|
m_stats.m_xites++;
|
||||||
};
|
};
|
||||||
|
if (s.m_config.m_cut_aig) {
|
||||||
aig_finder af(s);
|
aig_finder af(s);
|
||||||
af.set(on_and);
|
af.set(on_and);
|
||||||
af.set(on_ite);
|
af.set(on_ite);
|
||||||
clause_vector clauses(s.clauses());
|
if (m_config.m_learned2aig) clauses.append(s.learned());
|
||||||
if (m_config.m_learned2aig) clauses.append(s.learned());
|
af(clauses);
|
||||||
af(clauses);
|
}
|
||||||
|
|
||||||
std::function<void (literal_vector const&)> on_xor =
|
std::function<void (literal_vector const&)> on_xor =
|
||||||
[&,this](literal_vector const& xors) {
|
[&,this](literal_vector const& xors) {
|
||||||
|
|
|
@ -76,6 +76,7 @@ def_module_params('sat',
|
||||||
('anf.exlin', BOOL, False, 'enable extended linear simplification'),
|
('anf.exlin', BOOL, False, 'enable extended linear simplification'),
|
||||||
('cut', BOOL, False, 'enable AIG based simplification in-processing'),
|
('cut', BOOL, False, 'enable AIG based simplification in-processing'),
|
||||||
('cut.delay', UINT, 2, 'delay cut simplification by in-processing round'),
|
('cut.delay', UINT, 2, 'delay cut simplification by in-processing round'),
|
||||||
|
('cut.aig', BOOL, False, 'extract aigs (and ites) from cluases for cut simplification'),
|
||||||
('cut.lut', BOOL, False, 'extract luts from clauses for cut simplification'),
|
('cut.lut', BOOL, False, 'extract luts from clauses for cut simplification'),
|
||||||
('cut.xor', BOOL, False, 'extract xors from clauses for cut simplification'),
|
('cut.xor', BOOL, False, 'extract xors from clauses for cut simplification'),
|
||||||
('cut.dont_cares', BOOL, True, 'integrate dont cares with cuts'),
|
('cut.dont_cares', BOOL, True, 'integrate dont cares with cuts'),
|
||||||
|
|
Loading…
Reference in a new issue