From 354c16454a6704f2176573eed418c87a28b4d355 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Feb 2018 22:19:25 -0800 Subject: [PATCH] fix bug in translation of pbeq into sat Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.cpp | 3 +++ src/ast/rewriter/pb2bv_rewriter.cpp | 5 ----- src/ast/rewriter/pb_rewriter.cpp | 2 +- src/cmd_context/basic_cmds.cpp | 2 ++ src/sat/tactic/goal2sat.cpp | 5 ++++- 5 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index d36c4ba89..b189eabf7 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -162,6 +162,9 @@ app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const * if (!m_k.is_int()) { return m.mk_false(); } + if (num_args == 0) { + return m_k.is_zero() ? m.mk_true() : m.mk_false(); + } m_params.reset(); m_params.push_back(parameter(m_k)); for (unsigned i = 0; i < num_args; ++i) { diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index d4aa5ad3e..3b657f1a3 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -94,12 +94,7 @@ struct pb2bv_rewriter::imp { for (unsigned i = 0; i < m_args.size(); ++i) { cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args[i].get(), m))); } - //for (ca const& ca : cas) std::cout << ca.first << " "; - //std::cout << "\n"; std::sort(cas.begin(), cas.end(), compare_coeffs()); - //std::cout << "post-sort\n"; - //for (ca const& ca : cas) std::cout << ca.first << " "; - //std::cout << "\n"; m_coeffs.reset(); m_args.reset(); for (ca const& ca : cas) { diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 004f0d592..8bf7f2078 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -329,7 +329,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons tout << tmp << "\n"; tout << result << "\n"; ); - + TRACE("pb_validate", validate_rewrite(f, num_args, args, result);); diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 88c5cb257..d5e295b37 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -110,6 +110,8 @@ public: virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } virtual void execute(cmd_context & ctx) { model_ref m; + if (ctx.ignore_check()) + return; if (!ctx.is_model_available(m) || ctx.get_check_sat_result() == 0) throw cmd_exception("model is not available"); if (m_index > 0 && ctx.get_opt()) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index a7b2eb582..b84a64651 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -571,6 +571,8 @@ struct goal2sat::imp { l.neg(); } m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned()); + + if (root) { m_result_stack.reset(); } @@ -582,7 +584,8 @@ struct goal2sat::imp { mk_clause(~l, l2); mk_clause(~l1, ~l2, l); m_result_stack.shrink(m_result_stack.size() - t->get_num_args()); - m_result_stack.push_back(l); + m_result_stack.push_back(sign ? ~l : l); + } }