From 200f47369dd1dc36087513e0660a2880a090106c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Feb 2020 16:58:25 -0800 Subject: [PATCH] some micro tuning Signed-off-by: Nikolaj Bjorner --- src/sat/sat_aig_cuts.cpp | 44 +++++++++++++++++++++++++++++++++++ src/sat/sat_aig_cuts.h | 14 ++++++++++- src/smt/asserted_formulas.cpp | 3 +++ src/smt/smt_context.cpp | 6 +++-- src/smt/smt_context.h | 2 ++ src/smt/theory_lra.cpp | 24 ++++++++++++------- 6 files changed, 81 insertions(+), 12 deletions(-) diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp index bb99ab116..7c2968145 100644 --- a/src/sat/sat_aig_cuts.cpp +++ b/src/sat/sat_aig_cuts.cpp @@ -61,6 +61,9 @@ namespace sat { else if (n.is_var()) { SASSERT(!n.sign()); } + else if (n.is_lut()) { + augment_lut(id, n, cs); + } else if (n.is_ite()) { augment_ite(id, n, cs); } @@ -97,6 +100,47 @@ namespace sat { return true; } + void aig_cuts::augment_lut(unsigned v, node const& n, cut_set& cs) { + IF_VERBOSE(4, display(verbose_stream() << "augment_lut " << v << " ", n) << "\n"); + literal l1 = child(n, 0); + for (auto const& a : m_cuts[l1.var()]) { + m_tables[0] = &a; + cut b(a); + augment_lut_rec(v, n, b, 1, cs); + } + } + + void aig_cuts::augment_lut_rec(unsigned v, node const& n, cut& a, unsigned idx, cut_set& cs) { + if (idx < n.size()) { + for (auto const& b : m_cuts[child(n, idx).var()]) { + cut ab; + if (ab.merge(a, b)) { + m_tables[idx] = &b; + augment_lut_rec(v, n, ab, idx + 1, cs); + } + } + return; + } + for (unsigned i = 0; i < n.size(); ++i) { + m_luts[i] = m_tables[i]->shift_table(a); + } + uint64_t r = 0; + SASSERT(a.size() <= 6); + SASSERT(n.size() <= 6); + for (unsigned j = (1u << a.size()); j-- > 0; ) { + unsigned w = 0; + // when computing the output at position j, + // the i'th bit to index into n.lut() is + // based on the j'th output bit in lut[i] + for (unsigned i = n.size(); i-- > 0; ) { + w |= ((m_luts[i] >> j) & 0x1) << i; + } + r |= ((n.lut() >> w) & 0x1) << j; + } + a.set_table(r); + insert_cut(v, a, cs); + } + void aig_cuts::augment_ite(unsigned v, node const& n, cut_set& cs) { IF_VERBOSE(4, display(verbose_stream() << "augment_ite " << v << " ", n) << "\n"); literal l1 = child(n, 0); diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h index 530367bce..9587230cf 100644 --- a/src/sat/sat_aig_cuts.h +++ b/src/sat/sat_aig_cuts.h @@ -39,6 +39,7 @@ namespace sat { and_op, ite_op, xor_op, + lut_op, no_op }; @@ -48,6 +49,7 @@ namespace sat { case and_op: return out << "&"; case ite_op: return out << "?"; case xor_op: return out << "^"; + case lut_op: return out << "#"; default: return out << ""; } } @@ -69,6 +71,7 @@ namespace sat { class node { bool m_sign; bool_op m_op; + uint64_t m_lut; unsigned m_size; unsigned m_offset; public: @@ -78,17 +81,21 @@ namespace sat { m_sign(false), m_op(var_op), m_size(0), m_offset(v) {} explicit node(bool sign, bool_op op, unsigned nc, unsigned o) : m_sign(sign), m_op(op), m_size(nc), m_offset(o) {} + explicit node(uint64_t lut, unsigned nc, unsigned o): + m_sign(false), m_op(lut_op), m_size(nc), m_offset(o) {} bool is_valid() const { return m_offset != UINT_MAX; } bool_op op() const { return m_op; } bool is_var() const { return m_op == var_op; } bool is_and() const { return m_op == and_op; } bool is_xor() const { return m_op == xor_op; } bool is_ite() const { return m_op == ite_op; } + bool is_lut() const { return m_op == lut_op; } bool is_const() const { return is_and() && size() == 0; } unsigned var() const { SASSERT(is_var()); return m_offset; } bool sign() const { return m_sign; } unsigned size() const { return m_size; } unsigned offset() const { return m_offset; } + uint64_t lut() const { return m_lut; } }; random_gen m_rand; config m_config; @@ -106,6 +113,8 @@ namespace sat { on_clause_t m_on_clause_add, m_on_clause_del; cut_set::on_update_t m_on_cut_add, m_on_cut_del; literal_vector m_clause; + cut const* m_tables[6]; + uint64_t m_luts[6]; bool is_touched(bool_var v, node const& n); bool is_touched(literal lit) const { return is_touched(lit.var()); } @@ -119,12 +128,15 @@ namespace sat { unsigned_vector filter_valid_nodes() const; void augment(unsigned_vector const& ids); void augment(unsigned id, node const& n); - void augment_ite(unsigned v, node const& n, cut_set& cs); + void augment_ite(unsigned v, node const& n, cut_set& cs); void augment_aig0(unsigned v, node const& n, cut_set& cs); void augment_aig1(unsigned v, node const& n, cut_set& cs); void augment_aig2(unsigned v, node const& n, cut_set& cs); void augment_aigN(unsigned v, node const& n, cut_set& cs); + void augment_lut(unsigned v, node const& n, cut_set& cs); + void augment_lut_rec(unsigned v, node const& n, cut& a, unsigned idx, cut_set& cs); + bool insert_cut(unsigned v, cut const& c, cut_set& cs); void flush_roots(); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6120caf68..65690f7eb 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -277,6 +277,9 @@ void asserted_formulas::reduce() { TRACE("macros", m_macro_manager.display(tout);); flush_cache(); CASSERT("well_sorted",check_well_sorted()); + +// display(std::cout); +// exit(0); } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5f71bd4e5..88a34ed2d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2003,12 +2003,14 @@ namespace smt { */ void context::add_lit_occs(clause const& cls) { + if (!track_occs()) return; for (literal l : cls) { inc_ref(l); } } void context::remove_lit_occs(clause const& cls, unsigned nbv) { + if (!track_occs()) return; for (literal l : cls) { if (l.var() < static_cast(nbv)) dec_ref(l); @@ -2016,9 +2018,9 @@ namespace smt { } // TBD: enable as assertion when ready to re-check - void context::dec_ref(literal l) { if (m_lit_occs[l.index()] > 0) m_lit_occs[l.index()]--; } + void context::dec_ref(literal l) { if (track_occs() && m_lit_occs[l.index()] > 0) m_lit_occs[l.index()]--; } - void context::inc_ref(literal l) { m_lit_occs[l.index()]++; } + void context::inc_ref(literal l) { if (track_occs()) m_lit_occs[l.index()]++; } /** \brief Delete the given clause. diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 73a091181..41bd2c3a7 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -839,6 +839,8 @@ namespace smt { void mk_ite_cnstr(app * n); + bool track_occs() const { return m_fparams.m_phase_selection == PS_THEORY; } + void dec_ref(literal l); void inc_ref(literal l); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index fb6cb42a6..dfdcc61fc 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -357,7 +357,8 @@ class theory_lra::imp { scoped_ptr m_solver; resource_limit m_resource_limit; lp_bounds m_new_bounds; - switcher m_switcher; + switcher m_switcher; + symbol m_farkas; context& ctx() const { return th.get_context(); } theory_id get_id() const { return th.get_id(); } @@ -1001,7 +1002,8 @@ public: m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)), m_solver(nullptr), m_resource_limit(*this), - m_switcher(*this) { + m_switcher(*this), + m_farkas("farkas") { } ~imp() { @@ -1911,17 +1913,19 @@ public: if (m_idiv_terms.empty()) { return true; } - init_variable_values(); + // init_variable_values(); bool all_divs_valid = true; for (expr* n : m_idiv_terms) { expr* p = nullptr, *q = nullptr; VERIFY(a.is_idiv(n, p, q)); theory_var v = mk_var(n); theory_var v1 = mk_var(p); - rational r1 = get_value(v1); + lp::impq r1 = get_ivalue(v1); + SASSERT(r1.y.is_zero()); + SASSERT(r1.x.is_int()); rational r2; - if (!r1.is_int() || r1.is_neg()) { + if (!r1.x.is_int() || r1.x.is_neg()) { // TBD // r1 = 223/4, r2 = 2, r = 219/8 // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0 @@ -1932,15 +1936,17 @@ public: } if (a.is_numeral(q, r2) && r2.is_pos()) { - rational val_v = get_value(v); - if (val_v == div(r1, r2)) continue; if (!is_bounded(n)) { TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";); continue; } + lp::impq val_v = get_ivalue(v); + SASSERT(val_v.y.is_zero()); + SASSERT(val_v.x.is_int()); + if (val_v.x == div(r1.x, r2)) continue; TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";); - rational div_r = div(r1, r2); + rational div_r = div(r1.x, r2); // p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2) // p >= q * div(r1, q) => div(r1, q) <= div(p, q) rational mul(1); @@ -2842,7 +2848,7 @@ public: m_core.reset(); m_eqs.reset(); m_core.push_back(lit1); - m_params.push_back(parameter(symbol("farkas"))); + m_params.push_back(parameter(m_farkas)); m_params.push_back(parameter(rational(1))); m_params.push_back(parameter(rational(1))); assign(lit2);