From f96133f4d93a70e08fe1030c23289437f404e442 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Jul 2018 07:17:08 -0700 Subject: [PATCH] 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; }