Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master

src/smt/smt_model_generator.cpp

@@ -400,7 +400,12 @@ namespace smt {
        \brief Return true if the interpretation of the function should be included in the model.
     */
     bool model_generator::include_func_interp(func_decl * f) const {
-        return f->get_family_id() == null_family_id;
+        family_id fid = f->get_family_id();
+        if (fid == null_family_id) return true;
+        if (fid == m_manager.get_basic_family_id()) return false;
+        theory * th   = m_context->get_theory(fid);
+        if (!th) return true;
+        return th->include_func_interp(f);
     }
     
     /**

src/smt/smt_theory.h

@@ -412,6 +412,10 @@ namespace smt {
             return 0;
         }
 
+        virtual bool include_func_interp(func_decl* f) {
+            return false;
+        }
+
         // -----------------------------------
         //
         // Model checker

src/smt/theory_arith_aux.h

@@ -1346,7 +1346,7 @@ namespace smt {
                 empty_column ||
                 (unbounded_gain(max_gain) == (x_i == null_theory_var)));
         
-        return !empty_column && safe_gain(min_gain, max_gain);
+        return safe_gain(min_gain, max_gain);
     }
 
     template<typename Ext>
@@ -1557,14 +1557,12 @@ namespace smt {
                     // variable cannot be used for max/min.
                     continue; 
                 }
-                bool picked_var = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, 
+                bool safe_to_leave = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, 
                                                     curr_min_gain, curr_max_gain, 
                                                     has_shared, curr_x_i);
 
-
-                SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain));
                 
-                if (!safe_gain(curr_min_gain, curr_max_gain)) {
+                if (!safe_to_leave) {
                     TRACE("opt", tout << "no variable picked\n";);
                     has_bound = true;
                     best_efforts++;

src/smt/theory_bv.cpp

@@ -1283,6 +1283,21 @@ namespace smt {
         theory::reset_eh();
     }
 
+    bool theory_bv::include_func_interp(func_decl* f) {
+        SASSERT(f->get_family_id() == get_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_BSDIV0:
+        case OP_BUDIV0:
+        case OP_BSREM0:
+        case OP_BUREM0:       
+        case OP_BSMOD0:        
+            return true;
+        default:
+            return false;
+        }
+        return false;
+    }
+
     theory_bv::theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params):
         theory(m.mk_family_id("bv")),
         m_params(params),

src/smt/theory_bv.h

@@ -236,6 +236,7 @@ namespace smt {
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual final_check_status final_check_eh();
         virtual void reset_eh();
+        virtual bool include_func_interp(func_decl* f);
         svector<theory_var>   m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
         bool merge_zero_one_bits(theory_var r1, theory_var r2);
 

src/smt/theory_fpa.cpp

@@ -555,26 +555,11 @@ namespace smt {
         literal l(ctx.mk_bool_var(atom));
         ctx.set_var_theory(l.var(), get_id());
 
-        expr_ref bv_atom(m);
-        bv_atom = convert_atom(atom);
-        SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
-        bv_atom = m.mk_and(bv_atom, mk_side_conditions());
-
-        // CMW: Do not use assert_cnstr here; the internalizer expects normalized expressions.
-        // See GitHub issue #227
-        // assert_cnstr(m.mk_iff(atom, bv_atom));
-
-        ctx.internalize(atom, false);
-        ctx.internalize(bv_atom, false);
-        literal lit1(ctx.get_literal(atom));
-        literal lit2(ctx.get_literal(bv_atom));
-        ctx.mark_as_relevant(lit1);
-        ctx.mark_as_relevant(lit2);
-        literal lits1[2] = { lit1, ~lit2 };
-        literal lits2[2] = { ~lit1, lit2 };
-        ctx.mk_th_axiom(get_id(), 2, lits1);
-        ctx.mk_th_axiom(get_id(), 2, lits2);
-
+        expr_ref bv_atom(convert_atom(atom));
+        expr_ref bv_atom_w_side_c(m);
+        bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions());
+        m_th_rw(bv_atom_w_side_c);
+        assert_cnstr(m.mk_eq(atom, bv_atom_w_side_c));
         return true;
     }
 
@@ -752,10 +737,11 @@ namespace smt {
 
         expr_ref converted(m);
         converted = m.mk_and(convert(e), mk_side_conditions());
-        if (is_true)
-            assert_cnstr(m.mk_implies(e, converted));
-        else
-            assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
+
+        expr_ref cnstr(m);
+        cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e);
+        m_th_rw(cnstr);
+        assert_cnstr(cnstr);
     }
 
     void theory_fpa::relevant_eh(app * n) {