Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237

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

src/model/model_evaluator.cpp

@@ -101,31 +101,21 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
         family_id fid = f->get_family_id();
-        if (fid == null_family_id) {
+        if (fid == null_family_id && num == 0) {
-            if (num == 0) {
+            expr * val = m_model.get_const_interp(f);
-                expr * val = m_model.get_const_interp(f);
+            if (val != 0) {
-                if (val != 0) {
+                result = val;
-                    result = val;
-                    return BR_DONE;
-                }
-                
-                if (m_model_completion) {
-                    sort * s   = f->get_range();
-                    expr * val = m_model.get_some_value(s);
-                    m_model.register_decl(f, val);
-                    result = val;
-                    return BR_DONE;
-                }
-                return BR_FAILED;
-            }
-            SASSERT(num > 0);
-            func_interp * fi = m_model.get_func_interp(f);
-            if (fi != 0 && eval_fi(fi, num, args, result)) {
-                TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
-                      for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
-                      tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";);
                 return BR_DONE;
             }
+            
+            if (m_model_completion) {
+                sort * s   = f->get_range();
+                expr * val = m_model.get_some_value(s);
+                m_model.register_decl(f, val);
+                result = val;
+                return BR_DONE;
+            }
+            return BR_FAILED;
         }
 
         if (fid == m_b_rw.get_fid()) {
@@ -160,42 +150,50 @@ struct evaluator_cfg : public default_rewriter_cfg {
             return m_pb_rw.mk_app_core(f, num, args, result);
         if (fid == m_f_rw.get_fid())
             return m_f_rw.mk_app_core(f, num, args, result);
+
+        func_interp * fi = m_model.get_func_interp(f);
+        if (fi != 0 && eval_fi(fi, num, args, result)) {
+            TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
+                  for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
+                  tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";);
+            return BR_DONE;
+        }
+        TRACE("model_evaluator", tout << f->get_name() << "\n";);
+
         return BR_FAILED;
     }
 
     bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { 
-        if (f->get_family_id() == null_family_id) {
+
-            func_interp * fi = m_model.get_func_interp(f);
+        func_interp * fi = m_model.get_func_interp(f);        
-            
+        if (fi != 0) {
-            if (fi != 0) {
+            if (fi->is_partial()) {
-                if (fi->is_partial()) {
+                if (m_model_completion) {
-                    if (m_model_completion) {
+                    sort * s   = f->get_range();
-                        sort * s   = f->get_range();
+                    expr * val = m_model.get_some_value(s);
-                        expr * val = m_model.get_some_value(s);
+                    fi->set_else(val);
-                        fi->set_else(val);
-                    }
-                    else {
-                        return false;
-                    }
                 }
-                
+                else {
-                def    = fi->get_interp();
+                    return false;
-                SASSERT(def != 0);
+                }
-                return true;
+            }            
-            }
+            def    = fi->get_interp();
-            
+            SASSERT(def != 0);
-            if (m_model_completion) {
+            return true;
-                sort * s   = f->get_range();
+        }
-                expr * val = m_model.get_some_value(s);
+
-                func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
+        if (f->get_family_id() == null_family_id && m_model_completion) {
-                new_fi->set_else(val);
+            sort * s   = f->get_range();
-                m_model.register_decl(f, new_fi);
+            expr * val = m_model.get_some_value(s);
-                def = val;
+            func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
-                return true;
+            new_fi->set_else(val);
-            }
+            m_model.register_decl(f, new_fi);
+            def = val;
+            return true;
         }
         return false;
     }
+
     
     bool max_steps_exceeded(unsigned num_steps) const { 
         cooperate("model evaluator");

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