mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add cut redundancies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-27 21:11:07 -08:00
parent ff3baffadc
commit 05158b3914
4 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_config.cpp
View file

@ -111,6 +111,7 @@ namespace sat {
m_cut_xor = p.cut_xor(); m_cut_xor = p.cut_xor();
m_cut_npn3 = p.cut_npn3(); m_cut_npn3 = p.cut_npn3();
m_cut_dont_cares = p.cut_dont_cares(); m_cut_dont_cares = p.cut_dont_cares();
m_cut_redundancies = p.cut_redundancies();
m_cut_force = p.cut_force(); m_cut_force = p.cut_force();
m_lookahead_simplify = p.lookahead_simplify(); m_lookahead_simplify = p.lookahead_simplify();
m_lookahead_double = p.lookahead_double(); m_lookahead_double = p.lookahead_double();

1
src/sat/sat_config.h
View file

@ -128,6 +128,7 @@ namespace sat {
bool m_cut_xor; bool m_cut_xor;
bool m_cut_npn3; bool m_cut_npn3;
bool m_cut_dont_cares; bool m_cut_dont_cares;
bool m_cut_redundancies;
bool m_cut_force; bool m_cut_force;
bool m_anf_simplify; bool m_anf_simplify;
unsigned m_anf_delay; unsigned m_anf_delay;

14
src/sat/sat_cut_simplifier.cpp
View file

@ -599,12 +599,14 @@ namespace sat {
} }
void cut_simplifier::add_dont_cares(vector<cut_set> const& cuts) { void cut_simplifier::add_dont_cares(vector<cut_set> const& cuts) {
if (!s.m_config.m_cut_dont_cares) if (s.m_config.m_cut_dont_cares) {
return; cuts2bins(cuts);
cuts2bins(cuts); bins2dont_cares();
bins2dont_cares(); dont_cares2cuts(cuts);
dont_cares2cuts(cuts); }
// m_aig_cuts.simplify(); if (s.m_config.m_cut_redundancies) {
m_aig_cuts.simplify();
}
} }
/** /**

1
src/sat/sat_params.pyg
View file

@ -81,6 +81,7 @@ def_module_params('sat',
('cut.xor', BOOL, False, 'extract xors from clauses for cut simplification'), ('cut.xor', BOOL, False, 'extract xors from clauses for cut simplification'),
('cut.npn3', BOOL, False, 'extract 3 input functions from clauses for cut simplification'), ('cut.npn3', BOOL, False, 'extract 3 input functions 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'),
('cut.redundancies', BOOL, True, 'integrate redundancy checking of cuts'),
('cut.force', BOOL, False, 'force redoing cut-enumeration until a fixed-point'), ('cut.force', BOOL, False, 'force redoing cut-enumeration until a fixed-point'),
('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
# - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth. # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.