From f96133f4d93a70e08fe1030c23289437f404e442 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Jul 2018 07:17:08 -0700 Subject: [PATCH 1/5] fix #1729 Signed-off-by: Nikolaj Bjorner --- src/api/api_goal.cpp | 4 +-- src/api/z3_api.h | 5 ++++ .../bit_blaster/bit_blaster_rewriter.cpp | 25 ++++++++++++++++--- src/tactic/goal.cpp | 6 +++-- 4 files changed, 33 insertions(+), 7 deletions(-) diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index 090553df5..cb3bb7478 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -199,8 +199,8 @@ extern "C" { RESET_ERROR_CODE(); std::ostringstream buffer; if (!to_goal_ref(g)->is_cnf()) { - warning_msg("goal is not in CNF. This will produce a propositional abstraction. " - "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf"); + SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf"); + RETURN_Z3(nullptr); } to_goal_ref(g)->display_dimacs(buffer); // Hack for removing the trailing '\n' diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9af548af0..2657e558d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5525,6 +5525,11 @@ extern "C" { /** \brief Convert a goal into a DIMACS formatted string. + The goal must be in CNF. You can convert a goal to CNF + by applying the tseitin-cnf tactic. Bit-vectors are not automatically + converted to Booleans either, so the caller intends to + preserve satisfiability, it should apply bit-blasting tactics. + Quantifiers and theory atoms will not be encoded. def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL))) */ diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 862d1cdab..fe750acdd 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -89,6 +89,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { expr_ref_vector m_out; obj_map m_const2bits; expr_ref_vector m_bindings; + unsigned_vector m_shifts; func_decl_ref_vector m_keys; expr_ref_vector m_values; unsigned_vector m_keyval_lim; @@ -579,19 +580,36 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); } SASSERT(new_bindings.size() == q->get_num_decls()); i = q->get_num_decls(); + unsigned shift = j; + if (!m_shifts.empty()) shift += m_shifts.back(); while (i > 0) { i--; m_bindings.push_back(new_bindings[i]); + m_shifts.push_back(shift); } } return true; } bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { - if (m_blast_quant) { - if (t->get_idx() >= m_bindings.size()) + if (m_blast_quant) { + if (m_bindings.empty()) return false; - result = m_bindings.get(m_bindings.size() - t->get_idx() - 1); + unsigned shift = m_shifts.back(); + if (t->get_idx() >= m_bindings.size()) { + if (shift == 0) + return false; + result = m_manager.mk_var(t->get_idx() + shift, t->get_sort()); + } + else { + unsigned offset = m_bindings.size() - t->get_idx() - 1; + result = m_bindings.get(offset); + shift = shift - m_shifts[offset]; + if (shift > 0) { + var_shifter vs(m_manager); + vs(result, shift, result); + } + } result_pr = nullptr; return true; } @@ -641,6 +659,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); result_pr = nullptr; m_bindings.shrink(old_sz); + m_shifts.shrink(old_sz); return true; } }; diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 203ca2ca0..f00f0e77e 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -733,7 +733,9 @@ bool goal::is_cnf() const { bool goal::is_literal(expr* f) const { m_manager.is_not(f, f); if (!is_app(f)) return false; - if (to_app(f)->get_family_id() == m_manager.get_basic_family_id() && - !m_manager.is_false(f) && !m_manager.is_true(f)) return false; + if (to_app(f)->get_family_id() == m_manager.get_basic_family_id()) { + for (expr* arg : *to_app(f)) + if (m_manager.is_bool(arg)) return false; + } return true; } From eceb92f5ef03a92446761a92b4af34ef40369e89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Jul 2018 09:50:39 -0700 Subject: [PATCH 2/5] add utilities for purification Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbi.cpp | 42 +++++++++++++++++++++++- src/qe/qe_term_graph.cpp | 70 +++++++++++++++++++++++++++++++++------- src/qe/qe_term_graph.h | 13 ++++++++ 3 files changed, 113 insertions(+), 12 deletions(-) diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 7dfa35003..b7f0d0d49 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -346,10 +346,50 @@ namespace qe { func_decl_ref_vector no_shared(m); tg1.set_vars(no_shared, false); tg1.add_lits(lits); + arith_util a(m); + expr_ref_vector foreign = tg1.shared_occurrences(a.get_family_id()); + obj_hashtable _foreign; + for (expr* e : foreign) _foreign.insert(e); + vector partition = tg1.get_partition(*mdl); expr_ref_vector diseq = tg1.get_ackerman_disequalities(); lits.append(diseq); - TRACE("qe", tout << "diseq: " << diseq << "\n";); + TRACE("qe", tout << "diseq: " << diseq << "\n"; + tout << "foreign: " << foreign << "\n"; + for (auto const& v : partition) { + tout << "partition: {"; + bool first = true; + for (expr* e : v) { + if (first) first = false; else tout << ", "; + tout << expr_ref(e, m); + } + tout << "}\n"; + } + ); + vector refined_partition; + for (auto & p : partition) { + unsigned j = 0; + for (expr* e : p) { + if (_foreign.contains(e) || + (is_app(e) && m_shared.contains(to_app(e)->get_decl()))) { + p[j++] = e; + } + } + p.shrink(j); + if (!p.empty()) refined_partition.push_back(p); + } + TRACE("qe", + for (auto const& v : refined_partition) { + tout << "partition: {"; + bool first = true; + for (expr* e : v) { + if (first) first = false; else tout << ", "; + tout << expr_ref(e, m); + } + tout << "}\n"; + }); + + arith_project_plugin ap(m); ap.set_check_purified(false); diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 2e81454a0..faa9cfed8 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -99,7 +99,7 @@ namespace qe { m_mark(false), m_mark2(false), m_interpreted(false) { - if (!is_app()) return; + if (!is_app(m_expr)) return; for (expr* e : *to_app(m_expr)) { term* t = app2term[e->get_id()]; t->get_root().m_parents.push_back(this); @@ -151,7 +151,7 @@ namespace qe { unsigned get_id() const { return m_expr->get_id();} - unsigned get_decl_id() const { return is_app() ? get_app()->get_decl()->get_id() : m_expr->get_id(); } + unsigned get_decl_id() const { return is_app(m_expr) ? to_app(m_expr)->get_decl()->get_id() : m_expr->get_id(); } bool is_marked() const {return m_mark;} void set_mark(bool v){m_mark = v;} @@ -159,12 +159,10 @@ namespace qe { void set_mark2(bool v){m_mark2 = v;} // NSB: where is this used? bool is_interpreted() const {return m_interpreted;} - bool is_theory() const { return !is_app() || get_app()->get_family_id() != null_family_id; } + bool is_theory() const { return !is_app(m_expr) || to_app(m_expr)->get_family_id() != null_family_id; } void mark_as_interpreted() {m_interpreted=true;} expr* get_expr() const {return m_expr;} - bool is_app() const {return ::is_app(m_expr);} - app *get_app() const {return is_app() ? to_app(m_expr) : nullptr;} - unsigned get_num_args() const { return is_app() ? get_app()->get_num_args() : 0; } + unsigned get_num_args() const { return is_app(m_expr) ? to_app(m_expr)->get_num_args() : 0; } term &get_root() const {return *m_root;} bool is_root() const {return m_root == this;} @@ -226,7 +224,7 @@ namespace qe { } bool term_graph::is_variable_proc::operator()(const term &t) const { - return (*this)(t.get_app()); + return (*this)(t.get_expr()); } void term_graph::is_variable_proc::set_decls(const func_decl_ref_vector &decls, bool exclude) { @@ -444,7 +442,7 @@ namespace qe { return expr_ref(res, m); } - res = mk_app_core (r.get_app()); + res = mk_app_core (r.get_expr()); m_term2app.insert(r.get_id(), res); return expr_ref(res, m); @@ -463,7 +461,7 @@ namespace qe { SASSERT(t.is_root()); expr_ref rep(mk_app(t), m); for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { - expr* mem = mk_app_core(it->get_app()); + expr* mem = mk_app_core(it->get_expr()); out.push_back (m.mk_eq (rep, mem)); } } @@ -472,9 +470,9 @@ namespace qe { mk_equalities(t, out); for (term *it = &t.get_next(); it != &t; it = &it->get_next ()) { - expr* a1 = mk_app_core (it->get_app()); + expr* a1 = mk_app_core (it->get_expr()); for (term *it2 = &it->get_next(); it2 != &t; it2 = &it2->get_next()) { - expr* a2 = mk_app_core(it2->get_app()); + expr* a2 = mk_app_core(it2->get_expr()); out.push_back (m.mk_eq (a1, a2)); } } @@ -1000,6 +998,47 @@ namespace qe { reset(); return res; } + + vector get_partition(model& mdl) { + vector result; + expr_ref_vector pinned(m); + obj_map pid; + model::scoped_model_completion _smc(mdl, true); + for (term *t : m_tg.m_terms) { + expr* a = t->get_expr(); + if (!is_app(a)) continue; + if (m.is_bool(a)) continue; + expr_ref val = mdl(a); + unsigned p = 0; + // NB. works for simple domains Integers, Rationals, + // but not for algebraic numerals. + if (!pid.find(val, p)) { + p = pid.size(); + pid.insert(val, p); + pinned.push_back(val); + result.push_back(expr_ref_vector(m)); + } + result[p].push_back(a); + } + return result; + } + + expr_ref_vector shared_occurrences(family_id fid) { + expr_ref_vector result(m); + for (term *t : m_tg.m_terms) { + expr* e = t->get_expr(); + if (m.get_sort(e)->get_family_id() != fid) continue; + for (term * p : term::parents(t->get_root())) { + expr* pe = p->get_expr(); + if (!is_app(pe)) continue; + if (to_app(pe)->get_family_id() == fid) continue; + if (to_app(pe)->get_family_id() == m.get_basic_family_id()) continue; + result.push_back(e); + break; + } + } + return result; + } }; void term_graph::set_vars(func_decl_ref_vector const& decls, bool exclude) { @@ -1033,5 +1072,14 @@ namespace qe { return p.get_ackerman_disequalities(); } + vector term_graph::get_partition(model& mdl) { + term_graph::projector p(*this); + return p.get_partition(mdl); + } + + expr_ref_vector term_graph::shared_occurrences(family_id fid) { + term_graph::projector p(*this); + return p.shared_occurrences(fid); + } } diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 8c02163ab..855a0f2bc 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -122,6 +122,19 @@ namespace qe { */ expr_ref_vector get_ackerman_disequalities(); + /** + * Produce a model-based partition. + */ + vector get_partition(model& mdl); + + /** + * Extract shared occurrences of terms whose sort are + * fid, but appear in a context that is not fid. + * for example f(x + y) produces the shared occurrence + * x + y when f is uninterpreted and x + y has sort Int or Real. + */ + expr_ref_vector shared_occurrences(family_id fid); + }; } From 1918395f0eabad5038d8a97f2fe16855a27c4fa9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Jul 2018 12:19:03 -0700 Subject: [PATCH 3/5] fix bug in sat-solver where frozen clauses get re-attached Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 12 ++++++++---- src/sat/sat_solver.h | 4 ++-- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a59dd2b46..04a0274c4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -17,6 +17,7 @@ Revision History: --*/ + #include #include "sat/sat_solver.h" #include "sat/sat_integrity_checker.h" @@ -298,6 +299,9 @@ namespace sat { if (!c.is_learned()) { m_stats.m_non_learned_generation++; } + if (c.frozen()) { + --m_num_frozen; + } if (m_config.m_drat && !m_drat.is_cleaned(c)) { m_drat.del(c); } @@ -481,9 +485,10 @@ namespace sat { } unsigned some_idx = c.size() >> 1; literal block_lit = c[some_idx]; - DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off);); - DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off);); - VERIFY(c[0] != c[1]); + VERIFY(!c.frozen()); + DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off);); + DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off);); + SASSERT(c[0] != c[1]); m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off)); m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off)); return reinit; @@ -2139,7 +2144,6 @@ namespace sat { else { c.inc_inact_rounds(); if (c.inact_rounds() > m_config.m_gc_k) { - m_num_frozen--; del_clause(c); m_stats.m_gc_clause++; deleted++; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index b44c04604..ad972b2af 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -682,10 +682,10 @@ namespace sat { bool m_deleted; public: scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) { - s.detach_clause(c); + if (!c.frozen()) s.detach_clause(c); } ~scoped_detach() { - if (!m_deleted) s.attach_clause(c); + if (!m_deleted && !c.frozen()) s.attach_clause(c); } void del_clause() { From 905282ffe4ec675d96d80a059ede62815b2a790a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 5 Jul 2018 14:47:05 -0700 Subject: [PATCH 4/5] fix in theory_lra.cpp get_value Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6b8d7a47d..b4415264b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1168,7 +1168,9 @@ public: if (m_variable_values.count(vi) > 0) return m_variable_values[vi]; - SASSERT (m_solver->is_term(vi)); + if(!m_solver->is_term(vi)) + return rational::zero(); + m_todo_terms.push_back(std::make_pair(vi, rational::one())); rational result(0); while (!m_todo_terms.empty()) { From 852df6f7d9cec0fc138eadfbada3dec87e97b96c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 5 Jul 2018 16:35:05 -0700 Subject: [PATCH 5/5] reshufle var_register to faster access Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 5 ----- src/util/lp/lar_solver.h | 2 -- src/util/lp/var_register.h | 46 ++++++++++++++++++-------------------- 3 files changed, 22 insertions(+), 31 deletions(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 8b5d8814a..6fec5b329 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1507,11 +1507,6 @@ bool lar_solver::column_is_fixed(unsigned j) const { return m_mpq_lar_core_solver.column_is_fixed(j); } - -bool lar_solver::ext_var_is_int(var_index ext_var) const { - return m_var_register.external_is_int(ext_var); -} - // below is the initialization functionality of lar_solver bool lar_solver::strategy_is_undecided() const { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 9f79ff835..f17aa4a0d 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -155,8 +155,6 @@ public: bool var_is_int(var_index v) const; - bool ext_var_is_int(var_index ext_var) const; - void add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int); void add_new_var_to_core_fields_for_doubles(bool register_in_basis); diff --git a/src/util/lp/var_register.h b/src/util/lp/var_register.h index 86c238e12..93404bf91 100644 --- a/src/util/lp/var_register.h +++ b/src/util/lp/var_register.h @@ -19,19 +19,19 @@ Revision History: #pragma once namespace lp { class ext_var_info { - unsigned m_internal_j; // the internal index + unsigned m_external_j; // the internal index bool m_is_integer; public: ext_var_info() {} ext_var_info(unsigned j): ext_var_info(j, true) {} - ext_var_info(unsigned j , bool is_int) : m_internal_j(j), m_is_integer(is_int) {} - unsigned internal_j() const { return m_internal_j;} + ext_var_info(unsigned j , bool is_int) : m_external_j(j), m_is_integer(is_int) {} + unsigned external_j() const { return m_external_j;} bool is_integer() const {return m_is_integer;} }; class var_register { - svector m_local_to_external; - std::unordered_map m_external_to_local; + svector m_local_to_external; + std::unordered_map m_external_to_local; public: unsigned add_var(unsigned user_var) { return add_var(user_var, true); @@ -39,19 +39,23 @@ public: unsigned add_var(unsigned user_var, bool is_int) { auto t = m_external_to_local.find(user_var); if (t != m_external_to_local.end()) { - return t->second.internal_j(); + return t->second; } - unsigned j = size(); - m_external_to_local[user_var] = ext_var_info(j, is_int); - m_local_to_external.push_back(user_var); - return j; + m_local_to_external.push_back(ext_var_info(user_var, is_int)); + return m_external_to_local[user_var] = size() - 1; } - const svector & vars() const { return m_local_to_external; } + svector vars() const { + svector ret; + for (const auto& p : m_local_to_external) { + ret.push_back(p.external_j()); + } + return ret; + } unsigned local_to_external(unsigned local_var) const { - return m_local_to_external[local_var]; + return m_local_to_external[local_var].external_j(); } unsigned size() const { return m_local_to_external.size(); @@ -64,13 +68,7 @@ public: unsigned external_to_local(unsigned j) const { auto it = m_external_to_local.find(j); lp_assert(it != m_external_to_local.end()); - return it->second.internal_j(); - } - - bool external_is_int(unsigned j) const { - auto it = m_external_to_local.find(j); - lp_assert(it != m_external_to_local.end()); - return it->second.is_integer(); + return it->second; } bool external_is_used(unsigned ext_j) const { @@ -82,7 +80,7 @@ public: auto it = m_external_to_local.find(ext_j); if ( it == m_external_to_local.end()) return false; - local_j = it->second.internal_j(); + local_j = it->second; return true; } @@ -90,19 +88,19 @@ public: auto it = m_external_to_local.find(ext_j); if ( it == m_external_to_local.end()) return false; - local_j = it->second.internal_j(); - is_int = it->second.is_integer(); + local_j = it->second; + is_int = m_local_to_external[local_j].is_integer(); return true; } bool local_is_int(unsigned j) const { - return external_is_int(m_local_to_external[j]); + return m_local_to_external[j].is_integer(); } void shrink(unsigned shrunk_size) { for (unsigned j = size(); j-- > shrunk_size;) { - m_external_to_local.erase(m_local_to_external[j]); + m_external_to_local.erase(m_local_to_external[j].external_j()); } m_local_to_external.resize(shrunk_size); }