fix #4901

src/ast/special_relations_decl_plugin.h

@@ -87,6 +87,7 @@ public:
     bool is_special_relation(app* e) const { return is_special_relation(e->get_decl()); }
     sr_property get_property(func_decl* f) const;
     sr_property get_property(app* e) const { return get_property(e->get_decl()); }
+    func_decl* get_relation(func_decl* f) const { SASSERT(is_special_relation(f)); return to_func_decl(f->get_parameter(0).get_ast()); }
 
     func_decl* mk_to_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TO); }
     func_decl* mk_po_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PO); }

src/smt/smt_context.cpp

@@ -34,6 +34,7 @@ Revision History:
 #include "smt/smt_context.h"
 #include "smt/smt_quick_checker.h"
 #include "smt/uses_theory.h"
+#include "smt/theory_special_relations.h"
 #include "smt/smt_for_each_relevant_expr.h"
 #include "smt/smt_model_generator.h"
 #include "smt/smt_model_checker.h"
@@ -1543,6 +1544,13 @@ namespace smt {
         }
     }
 
+    void context::get_specrels(func_decl_set& rels) const {
+        family_id fid = m.get_family_id("specrels");
+        if (th)
+            dynamic_cast<theory_special_relations*>(th)->get_specrels(rels);
+    }
+
+
     void context::relevant_eh(expr * n) {
         if (b_internalized(n)) {
             bool_var v        = get_bool_var(n);

src/smt/smt_context.h

@@ -279,6 +279,9 @@ namespace smt {
             return m_app2enode[n->get_id()];
         }
 
+        void get_specrels(func_decl_set& rels) const;
+
+
         /**
            \brief Similar to get_enode, but returns 0 if n is to e_internalized.
         */

src/smt/smt_model_finder.cpp

@@ -401,6 +401,7 @@ namespace smt {
 
             expr_ref_vector*          m_new_constraints{ nullptr };
             random_gen                m_rand;
+            func_decl_set             m_specrels;
 
 
             void reset_sort2k() {
@@ -470,6 +471,7 @@ namespace smt {
             ast_manager& get_manager() const { return m; }
 
             void reset() {
+                m_specrels.reset();
                 flush_nodes();
                 m_nodes.reset();
                 m_next_node_id = 0;
@@ -479,6 +481,11 @@ namespace smt {
                 reset_sort2k();
             }
 
+            void set_specrels(context& c) {
+                m_specrels.reset();
+                c.get_specrels(m_specrels);
+            }
+
             void set_model(proto_model* m) {
                 reset_eval_cache();
                 m_model = m;
@@ -1049,9 +1056,13 @@ namespace smt {
              */
             void complete_partial_funcs(func_decl_set const& partial_funcs) {
                 for (func_decl* f : partial_funcs) {
+
                     // Complete the current interpretation
                     m_model->complete_partial_func(f, true);
 
+                    if (m_specrels.contains(f))
+                        continue;
+
                     unsigned arity = f->get_arity();
                     func_interp* fi = m_model->get_func_interp(f);
                     if (fi->is_constant())
@@ -2399,9 +2410,11 @@ namespace smt {
         }
     }
 
+
     void model_finder::process_auf(ptr_vector<quantifier> const& qs, proto_model* mdl) {
         m_auf_solver->reset();
         m_auf_solver->set_model(mdl);
+        m_auf_solver->set_specrels(*m_context);
 
         for (quantifier* q : qs) {
             quantifier_info* qi = get_quantifier_info(q);

src/smt/theory_special_relations.cpp

@@ -1146,5 +1146,11 @@ namespace smt {
         expr* e = ctx.bool_var2expr(a.var());
         out << (a.phase() ? "" : "(not ") << mk_pp(e, get_manager()) << (a.phase() ? "" : ")") << "\n";
     }
-    
+
+
+    void theory_special_relations::get_specrels(func_decl_set& rels) const {
+        for (auto [f, r] : m_relations)
+            rels.insert(m_util.get_relation(r->m_decl));
+    }
+
 }

src/smt/theory_special_relations.h

@@ -199,6 +199,8 @@ namespace smt {
         bool can_propagate() override { return m_can_propagate; }
         void propagate() override;
         void display(std::ostream & out) const override;
+
+        void get_specrels(func_decl_set& rels) const;
    
     };
 }