fix #1650 fix #1648

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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_'

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); } 

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);

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);

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);

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<r
     case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
     default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
     }
-    rw(fml1, result1, proof);
+    rw(true, fml1, result1, proof);
     rw.flush_side_constraints(lemmas);
-    std::cout << lemmas << "\n";
+    std::cout << "lemmas: " << lemmas << "\n";
+    std::cout << "simplified: " << result1 << "\n";
     for (unsigned values = 0; values < static_cast<unsigned>(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<r
         VERIFY(res == l_true);
         solver.assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
         res = solver.check();
+        if (res != l_false) {
+            IF_VERBOSE(0, solver.display(verbose_stream());
+                       verbose_stream() << vars << " k: " << k << " kind: " << kind << "\n";
+                       for (auto const& c : coeffs) verbose_stream() << c << "\n";
+                       );
+        }
         VERIFY(res == l_false);
     }
 }