From 49f9f4b3b53191e965e7a59dfd3b4868caa719ca Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 30 May 2014 20:52:39 +0530
Subject: [PATCH] fix crash in model construction from finite domain theory

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/dl_decl_plugin.cpp      | 18 +++++++++++++++++-
 src/ast/dl_decl_plugin.h        |  2 ++
 src/smt/smt_model_generator.cpp |  2 ++
 src/smt/theory_dl.cpp           |  7 +++----
 4 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
index 6d0823a24..badf8a59d 100644
--- a/src/ast/dl_decl_plugin.cpp
+++ b/src/ast/dl_decl_plugin.cpp
@@ -599,7 +599,23 @@ namespace datalog {
                         return 0;
                 }
                 result = mk_compare(OP_DL_LT, m_lt_sym, domain);
-                break;                
+                break;   
+
+            case OP_DL_REP: {
+                if (!check_domain(0, 0, num_parameters) ||
+                    !check_domain(1, 1, arity)) return 0;
+                func_decl_info info(m_family_id, k, 0, 0);
+                result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info);
+                break;
+            }
+                
+            case OP_DL_ABS: {
+                if (!check_domain(0, 0, num_parameters) ||
+                    !check_domain(1, 1, arity)) return 0;
+                func_decl_info info(m_family_id, k, 0, 0);
+                result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info);
+                break;
+            }
 
             default:
                 m_manager->raise_exception("operator not recognized");
diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h
index a662de578..65b00235c 100644
--- a/src/ast/dl_decl_plugin.h
+++ b/src/ast/dl_decl_plugin.h
@@ -48,6 +48,8 @@ namespace datalog {
         OP_RA_CLONE,
         OP_DL_CONSTANT,
         OP_DL_LT,
+        OP_DL_REP,
+        OP_DL_ABS,
         LAST_RA_OP
     };
     
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index cf22c3e3a..6c138fd57 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -102,6 +102,7 @@ namespace smt {
                     if (th && th->build_models()) {
                         if (r->get_th_var(th->get_id()) != null_theory_var) {
                             proc = th->mk_value(r, *this);
+                            SASSERT(proc);
                         }
                         else {
                             TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
@@ -110,6 +111,7 @@ namespace smt {
                     }
                     else {
                         proc = mk_model_value(r);
+                        SASSERT(proc);
                     }
                 }
                 SASSERT(proc);
diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp
index 4ef1bd8e0..fc9138bf6 100644
--- a/src/smt/theory_dl.cpp
+++ b/src/smt/theory_dl.cpp
@@ -162,7 +162,7 @@ namespace smt {
             m.register_factory(alloc(dl_factory, m_util, m.get_model()));
         }
         
-        virtual smt::model_value_proc * mk_value(smt::enode * n) {
+        virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) {
             return alloc(dl_value_proc, *this, n);
         }
 
@@ -201,9 +201,8 @@ namespace smt {
             if(!m_reps.find(s, r) || !m_vals.find(s,v)) {
                 SASSERT(!m_reps.contains(s));
                 sort* bv = b().mk_sort(64);
-                // TBD: filter these from model.
-                r = m().mk_fresh_func_decl("rep",1, &s,bv);
-                v = m().mk_fresh_func_decl("val",1, &bv,s);
+                r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv);
+                v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s);
                 m_reps.insert(s, r);
                 m_vals.insert(s, v);
                 add_trail(r);