From 753b9dd734305bd6211bc8f90e8b558d1775bae2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 May 2018 08:56:13 -0700 Subject: [PATCH] fix #1650 fix #1648 Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 3 ++- src/ast/rewriter/pb2bv_rewriter.cpp | 16 +++++++++------- src/ast/rewriter/pb2bv_rewriter.h | 2 +- src/tactic/arith/card2bv_tactic.cpp | 2 +- src/tactic/portfolio/pb2bv_solver.cpp | 2 +- src/test/pb2bv.cpp | 13 ++++++++++--- 6 files changed, 24 insertions(+), 14 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 87d766e55..d51735255 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2460,7 +2460,7 @@ def mk_config(): check_ar() CXX = find_cxx_compiler() CC = find_c_compiler() - SLIBEXTRAFLAGS = '-Wl,-soname,libz3.so' + SLIBEXTRAFLAGS = '' EXE_EXT = '' LIB_EXT = '.a' if GPROF: @@ -2511,6 +2511,7 @@ def mk_config(): LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS + SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS elif sysname == 'FreeBSD': CXXFLAGS = '%s -D_FREEBSD_' % CXXFLAGS OS_DEFINES = '-D_FREEBSD_' diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 7da8b2d3f..e4a34fc93 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -726,9 +726,9 @@ struct pb2bv_rewriter::imp { } } - bool mk_app(expr* e, expr_ref& r) { + bool mk_app(bool full, expr* e, expr_ref& r) { app* a; - return (is_app(e) && (a = to_app(e), mk_app(false, a->get_decl(), a->get_num_args(), a->get_args(), r))); + return (is_app(e) && (a = to_app(e), mk_app(full, a->get_decl(), a->get_num_args(), a->get_args(), r))); } bool is_pb(expr* x, expr* y) { @@ -844,6 +844,8 @@ struct pb2bv_rewriter::imp { else { result = mk_bv(f, sz, args); } + TRACE("pb", tout << "full: " << full << " " << expr_ref(m.mk_app(f, sz, args), m) << " " << result << "\n"; + ); return true; } @@ -915,9 +917,9 @@ struct pb2bv_rewriter::imp { void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); } void set_pb_solver(symbol const& s) { m_cfg.set_pb_solver(s); } void set_at_most1(sorting_network_encoding e) { m_cfg.set_at_most1(e); } - void rewrite(expr* e, expr_ref& r, proof_ref& p) { + void rewrite(bool full, expr* e, expr_ref& r, proof_ref& p) { expr_ref ee(e, m()); - if (m_cfg.m_r.mk_app(e, r)) { + if (m_cfg.m_r.mk_app(full, e, r)) { ee = r; // mp proof? } @@ -980,9 +982,9 @@ struct pb2bv_rewriter::imp { unsigned get_num_steps() const { return m_rw.get_num_steps(); } void cleanup() { m_rw.cleanup(); } - void operator()(expr * e, expr_ref & result, proof_ref & result_proof) { + void operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof) { // m_rw(e, result, result_proof); - m_rw.rewrite(e, result, result_proof); + m_rw.rewrite(full, e, result, result_proof); } void push() { m_fresh_lim.push_back(m_fresh.size()); @@ -1023,7 +1025,7 @@ ast_manager & pb2bv_rewriter::m() const { return m_imp->m; } unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; } -void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); } +void pb2bv_rewriter::operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(full, e, result, result_proof); } void pb2bv_rewriter::push() { m_imp->push(); } void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } diff --git a/src/ast/rewriter/pb2bv_rewriter.h b/src/ast/rewriter/pb2bv_rewriter.h index 9e3785649..3460f08ab 100644 --- a/src/ast/rewriter/pb2bv_rewriter.h +++ b/src/ast/rewriter/pb2bv_rewriter.h @@ -36,7 +36,7 @@ public: unsigned get_num_steps() const; void cleanup(); func_decl_ref_vector const& fresh_constants() const; - void operator()(expr * e, expr_ref & result, proof_ref & result_proof); + void operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof); void push(); void pop(unsigned num_scopes); void flush_side_constraints(expr_ref_vector& side_constraints); diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 63d034374..97649cc2f 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -71,7 +71,7 @@ public: for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) { rw1(g->form(idx), new_f1, new_pr1); TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;); - rw2(new_f1, new_f2, new_pr2); + rw2(false, new_f1, new_f2, new_pr2); if (m.proofs_enabled()) { new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1); new_pr1 = m.mk_modus_ponens(new_pr1, new_pr2); diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 0f2311233..f8794ca41 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -147,7 +147,7 @@ private: expr_ref_vector fmls(m); for (expr* a : m_assertions) { m_th_rewriter(a, fml1, proof); - m_rewriter(fml1, fml, proof); + m_rewriter(false, fml1, fml, proof); m_solver->assert_expr(fml); } m_rewriter.flush_side_constraints(fmls); diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp index 35c444bae..d58bf61ee 100644 --- a/src/test/pb2bv.cpp +++ b/src/test/pb2bv.cpp @@ -37,7 +37,7 @@ static void test1() { expr_ref fml(m), result(m); proof_ref proof(m); fml = pb.mk_at_least_k(vars.size(), vars.c_ptr(), k); - rw(fml, result, proof); + rw(true, fml, result, proof); std::cout << fml << " |-> " << result << "\n"; } expr_ref_vector lemmas(m); @@ -60,9 +60,10 @@ static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector(1 << N); ++values) { smt_params fp; smt::kernel solver(m, fp); @@ -86,6 +87,12 @@ static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector