From e8f7a082897a5a32f4b4c000521624fff006193c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 21:19:02 -0800 Subject: [PATCH] add stubs for npn3 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_config.cpp | 1 + src/sat/sat_config.h | 1 + src/sat/sat_cut_simplifier.cpp | 21 ++++++++++++++- src/sat/sat_npn3_finder.cpp | 49 ---------------------------------- src/sat/sat_npn3_finder.h | 3 --- src/sat/sat_params.pyg | 1 + 6 files changed, 23 insertions(+), 53 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index f5ff21521..5772e1030 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -109,6 +109,7 @@ namespace sat { m_cut_aig = p.cut_aig(); m_cut_lut = p.cut_lut(); m_cut_xor = p.cut_xor(); + m_cut_npn3 = p.cut_npn3(); m_cut_dont_cares = p.cut_dont_cares(); m_cut_force = p.cut_force(); m_lookahead_simplify = p.lookahead_simplify(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 8bc609246..bd47171f8 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -126,6 +126,7 @@ namespace sat { bool m_cut_aig; bool m_cut_lut; bool m_cut_xor; + bool m_cut_npn3; bool m_cut_dont_cares; bool m_cut_force; bool m_anf_simplify; diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp index 4091a9cc9..9ed5976cf 100644 --- a/src/sat/sat_cut_simplifier.cpp +++ b/src/sat/sat_cut_simplifier.cpp @@ -19,6 +19,7 @@ #include "sat/sat_cut_simplifier.h" #include "sat/sat_xor_finder.h" #include "sat/sat_lut_finder.h" +#include "sat/sat_npn3_finder.h" #include "sat/sat_elim_eqs.h" namespace sat { @@ -183,6 +184,7 @@ namespace sat { } clause_vector clauses(s.clauses()); + if (m_config.m_learned2aig) clauses.append(s.learned()); std::function on_and = [&,this](literal head, literal_vector const& ands) { @@ -199,10 +201,10 @@ namespace sat { aig_finder af(s); af.set(on_and); af.set(on_ite); - if (m_config.m_learned2aig) clauses.append(s.learned()); af(clauses); } + std::function on_xor = [&,this](literal_vector const& xors) { SASSERT(xors.size() > 1); @@ -243,6 +245,23 @@ namespace sat { m_aig_cuts.add_node(v, lut, vars.size(), vars.c_ptr()); }; + if (s.m_config.m_cut_npn3) { + npn3_finder nf(s); + // TBD: stubs for npn3 + // question: perhaps just use a LUT interface? + // nf.set_on_mux + // nf.set_on_maj + // nf.set_on_orand + // nf.set_on_and + // nf.set_on_xor + // nf.set_on_andxor + // nf.set_on_xorand + // nf.set_on_gamble + // nf.set_on_onehot + // nf.set_on_dot + // nf(clauses); + } + if (s.m_config.m_cut_lut) { lut_finder lf(s); lf.set(on_lut); diff --git a/src/sat/sat_npn3_finder.cpp b/src/sat/sat_npn3_finder.cpp index a5319e811..d67a39bd3 100644 --- a/src/sat/sat_npn3_finder.cpp +++ b/src/sat/sat_npn3_finder.cpp @@ -226,7 +226,6 @@ namespace sat { if (c1) c1->mark_used(); if (c2) c2->mark_used(); if (c3) c3->mark_used(); - // DEBUG_CODE(validate_if(~x, ~y, z, u, c, c1, c2, c3);); m_on_mux(~x, ~y, z, u); return true; } @@ -271,7 +270,6 @@ namespace sat { if (c4) c4->mark_used(); if (c5) c5->mark_used(); if (c6) c6->mark_used(); - // DEBUG_CODE(validate_if(~x, ~y, z, u, c, c1, c2, c3);); m_on_maj(~x, y, z, u); return true; } @@ -614,51 +612,4 @@ namespace sat { filter(clauses); } - void npn3_finder::validate_clause(literal_vector const& clause, vector const& clauses) { - solver vs(s.params(), s.rlimit()); - for (unsigned i = 0; i < s.num_vars(); ++i) { - vs.mk_var(); - } - svector bins; - s.collect_bin_clauses(bins, true, false); - for (auto b : bins) { - vs.mk_clause(b.first, b.second); - } - for (auto const& cl : clauses) { - vs.mk_clause(cl); - } - for (literal l : clause) { - literal nl = ~l; - vs.mk_clause(1, &nl); - } - lbool r = vs.check(); - if (r != l_false) { - vs.display(verbose_stream()); - UNREACHABLE(); - } - } - - void npn3_finder::validate_clause(literal x, literal y, literal z, vector const& clauses) { - literal_vector clause; - clause.push_back(x); - clause.push_back(y); - clause.push_back(z); - validate_clause(clause, clauses); - } - - void npn3_finder::validate_if(literal x, literal c, literal t, literal e, clause const& c0, clause const* c1, clause const* c2, clause const* c3) { - IF_VERBOSE(2, verbose_stream() << "validate if: " << x << " == " << c << " ? " << t << " : " << e << "\n"); - vector clauses; - clauses.push_back(literal_vector(c0.size(), c0.begin())); - if (c1) clauses.push_back(literal_vector(c1->size(), c1->begin())); - if (c2) clauses.push_back(literal_vector(c2->size(), c2->begin())); - if (c3) clauses.push_back(literal_vector(c3->size(), c3->begin())); - literal_vector clause; - validate_clause(~x, ~c, t, clauses); - validate_clause(~x, c, e, clauses); - validate_clause(~t, ~c, x, clauses); - validate_clause(~e, c, x, clauses); - } - - } diff --git a/src/sat/sat_npn3_finder.h b/src/sat/sat_npn3_finder.h index 4d8288904..f3285e4e9 100644 --- a/src/sat/sat_npn3_finder.h +++ b/src/sat/sat_npn3_finder.h @@ -102,7 +102,6 @@ namespace sat { void filter(clause_vector& clauses) const; void find_npn3(clause_vector& clauses, on_function_t const& on_function, std::function const& checker); void find_mux(clause_vector& clauses); - void validate_if(literal x, literal c, literal t, literal e, clause const& c0, clause const* c1, clause const* c2, clause const* c3); void find_maj(clause_vector& clauses); void find_orand(clause_vector& clauses); void find_and(clause_vector& clauses); @@ -112,8 +111,6 @@ namespace sat { void find_gamble(clause_vector& clauses); void find_onehot(clause_vector& clauses); void find_dot(clause_vector& clauses); - void validate_clause(literal x, literal y, literal z, vector const& clauses); - void validate_clause(literal_vector const& clause, vector const& clauses); public: diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index c32c4335f..d36cc1256 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -79,6 +79,7 @@ def_module_params('sat', ('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.xor', BOOL, False, 'extract xors 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.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'),