From 629e981e01ad9a6269f4816928a7cd2fdd7f50fd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Sep 2020 12:43:18 -0700 Subject: [PATCH] fix regression in get-consequence on QF_FD Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 16 +++++++------ .../bit_blaster/bit_blaster_rewriter.cpp | 23 ++++++++++++++----- .../bit_blaster/bit_blaster_rewriter.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/tactic/fd_solver/enum2bv_solver.cpp | 7 ++++-- 5 files changed, 33 insertions(+), 16 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 9c9c3d642..d21f7400c 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -79,22 +79,24 @@ extern "C" { } void solver2smt2_pp::check(unsigned n, expr* const* asms) { - for (unsigned i = 0; i < n; ++i) { + for (unsigned i = 0; i < n; ++i) m_pp_util.collect(asms[i]); - } m_pp_util.display_decls(m_out); m_out << "(check-sat"; - for (unsigned i = 0; i < n; ++i) { + for (unsigned i = 0; i < n; ++i) m_pp_util.display_expr(m_out << "\n", asms[i]); - } - for (expr* e : m_tracked) { + for (expr* e : m_tracked) m_pp_util.display_expr(m_out << "\n", e); - } m_out << ")\n"; m_out.flush(); } void solver2smt2_pp::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& variables) { + for (expr* a : assumptions) + m_pp_util.collect(a); + for (expr* v : variables) + m_pp_util.collect(v); + m_pp_util.display_decls(m_out); m_out << "(get-consequences ("; for (expr* f : assumptions) { m_out << "\n"; @@ -105,7 +107,7 @@ extern "C" { m_out << "\n"; m_pp_util.display_expr(m_out, f); } - m_out << ")\n"; + m_out << "))\n"; m_out.flush(); } diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 73c2f979f..aa51c9e47 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -190,18 +190,24 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { } } - unsigned m_keypos; + unsigned m_keypos { 0 }; void start_rewrite() { m_keypos = m_keys.size(); } void end_rewrite(obj_map& const2bits, ptr_vector & newbits) { - for (unsigned i = m_keypos; i < m_keys.size(); ++i) { - const2bits.insert(m_keys[i].get(), m_values[i].get()); - } - for (func_decl* f : m_newbits) newbits.push_back(f); - + for (unsigned i = m_keypos; i < m_keys.size(); ++i) + const2bits.insert(m_keys.get(i), m_values.get(i)); + for (func_decl* f : m_newbits) + newbits.push_back(f); + } + + void get_translation(obj_map& const2bits, ptr_vector & newbits) { + for (unsigned i = 0; i < m_keys.size(); ++i) + const2bits.insert(m_keys.get(i), m_values.get(i)); + for (func_decl* f : m_newbits) + newbits.push_back(f); } template @@ -679,6 +685,7 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl { void pop(unsigned s) { m_cfg.pop(s); } void start_rewrite() { m_cfg.start_rewrite(); } void end_rewrite(obj_map& const2bits, ptr_vector & newbits) { m_cfg.end_rewrite(const2bits, newbits); } + void get_translation(obj_map& const2bits, ptr_vector & newbits) { m_cfg.get_translation(const2bits, newbits); } unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); } }; @@ -734,3 +741,7 @@ void bit_blaster_rewriter::start_rewrite() { void bit_blaster_rewriter::end_rewrite(obj_map& const2bits, ptr_vector & newbits) { m_imp->end_rewrite(const2bits, newbits); } + +void bit_blaster_rewriter::get_translation(obj_map& const2bits, ptr_vector & newbits) { + m_imp->get_translation(const2bits, newbits); +} diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h index 3e575595e..bbe4641f9 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h @@ -34,6 +34,7 @@ public: void cleanup(); void start_rewrite(); void end_rewrite(obj_map& const2bits, ptr_vector & newbits); + void get_translation(obj_map& const2bits, ptr_vector & newbits); void operator()(expr * e, expr_ref & result, proof_ref & result_proof); void push(); void pop(unsigned num_scopes); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index d5de7f619..a7dda80a4 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -718,7 +718,7 @@ private: bool internalize_var(expr* v, sat::bool_var_vector& bvars) { obj_map const2bits; ptr_vector newbits; - m_bb_rewriter->end_rewrite(const2bits, newbits); + m_bb_rewriter->get_translation(const2bits, newbits); expr* bv; bv_util bvutil(m); bool internalized = false; diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index 3410f4062..aa7888b5c 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -146,6 +146,7 @@ public: m_rewriter.flush_side_constraints(bounds); m_solver->assert_expr(bounds); + // translate enumeration constants to bit-vectors. for (expr* v : vars) { func_decl* f = nullptr; @@ -159,12 +160,13 @@ public: lbool r = m_solver->get_consequences(asms, bvars, consequences); // translate bit-vector consequences back to enumeration types - for (unsigned i = 0; i < consequences.size(); ++i) { + unsigned i = 0; + for (expr* c : consequences) { expr* a = nullptr, *b = nullptr, *u = nullptr, *v = nullptr; func_decl* f; rational num; unsigned bvsize; - VERIFY(m.is_implies(consequences[i].get(), a, b)); + VERIFY(m.is_implies(c, a, b)); if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { SASSERT(num.is_unsigned()); expr_ref head(m); @@ -174,6 +176,7 @@ public: consequences[i] = m.mk_implies(a, head); } } + ++i; } return r; }