mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add stubs for npn3

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

1
src/sat/sat_config.cpp
View file

@ -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();

1
src/sat/sat_config.h
View file

@ -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;

21
src/sat/sat_cut_simplifier.cpp
View file

@ -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<void (literal head, literal_vector const& ands)> 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<void (literal_vector const&)> 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);

49
src/sat/sat_npn3_finder.cpp
View file

@ -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<literal_vector> const& clauses) {
solver vs(s.params(), s.rlimit());
for (unsigned i = 0; i < s.num_vars(); ++i) {
vs.mk_var();
}
svector<solver::bin_clause> 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<literal_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<literal_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);
}
}

3
src/sat/sat_npn3_finder.h
View file

@ -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<bool(binary_hash_table_t const&, ternary_hash_table_t const&, literal, literal, literal, clause&)> 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<literal_vector> const& clauses);
void validate_clause(literal_vector const& clause, vector<literal_vector> const& clauses);
public:

1
src/sat/sat_params.pyg
View file

@ -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'),