additional array handling routines

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

src/muz_qe/pdr_context.cpp

@@ -43,6 +43,7 @@ Notes:
 #include "qe_lite.h"
 #include "ast_ll_pp.h"
 #include "proof_checker.h"
+#include "smt_value_sort.h"
 
 namespace pdr {
 
@@ -1827,14 +1828,14 @@ namespace pdr {
         if (!vars.empty()) {
             // also fresh names for auxiliary variables in body?
             expr_substitution sub(m);
-            expr_ref_vector refs(m);
             expr_ref tmp(m);
             proof_ref pr(m);
             pr = m.mk_asserted(m.mk_true());
-            for (unsigned i = 0; i < vars.size(); ++i) {                
-                VERIFY (M->eval(vars[i].get(), tmp, true));                
-                refs.push_back(tmp);
-                sub.insert(vars[i].get(), tmp, pr);
+            for (unsigned i = 0; i < vars.size(); ++i) {    
+                if (smt::is_value_sort(m, vars[i].get())) {
+                    VERIFY (M->eval(vars[i].get(), tmp, true)); 
+                    sub.insert(vars[i].get(), tmp, pr);
+                }
             }
             if (!rep) rep = mk_expr_simp_replacer(m);
             rep->set_substitution(&sub);

src/muz_qe/pdr_util.cpp

@@ -904,6 +904,7 @@ namespace pdr {
         return !has_x;
     }
 
+
     void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
         ast_manager& m = fml.get_manager();
         expr_ref_vector conjs(m);

src/smt/smt_implied_equalities.cpp

@@ -29,6 +29,7 @@ Revision History:
 #include "array_decl_plugin.h"
 #include "uint_set.h"
 #include "model_v2_pp.h"
+#include "smt_value_sort.h"
 
 
 namespace smt {
@@ -134,44 +135,7 @@ namespace smt {
                     }                    
                 }
             }
-        }        
-        
-        bool is_simple_type(sort* s) {
-            arith_util arith(m);
-            datatype_util data(m);
-            
-            ptr_vector<sort> sorts;
-            ast_mark mark;
-            sorts.push_back(s);
-            
-            while (!sorts.empty()) {
-                s = sorts.back();
-                sorts.pop_back();
-                if (mark.is_marked(s)) {
-                    continue;
-                }
-                mark.mark(s, true);
-                if (arith.is_int_real(s)) {
-                    // simple
-                }
-                else if (m.is_bool(s)) {
-                    // simple
-                }
-                else if (data.is_datatype(s)) {
-                    ptr_vector<func_decl> const& cs = *data.get_datatype_constructors(s);
-                    for (unsigned i = 0; i < cs.size(); ++i) {
-                        func_decl* f = cs[i];
-                        for (unsigned j = 0; j < f->get_arity(); ++j) {
-                            sorts.push_back(f->get_domain(j));
-                        }
-                    }
-                }
-                else {
-                    return false;
-                }
-            }
-            return true;        
-        }
+        }                
         
         /**
            \brief Extract implied equalities for a collection of terms in the current context.
@@ -216,7 +180,7 @@ namespace smt {
 
             uint_set non_values;
             
-            if (!is_simple_type(srt)) {
+            if (!is_value_sort(m, srt)) {
                 for (unsigned i = 0; i < terms.size(); ++i) {
                     non_values.insert(i);
                 }

src/smt/smt_value_sort.cpp

@@ -0,0 +1,74 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    smt_value_sort.cpp
+
+Abstract:
+
+    Determine if elements of a given sort can be values.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-25
+
+Revision History:
+
+
+--*/
+
+#include "smt_value_sort.h"
+#include "bv_decl_plugin.h"
+#include "arith_decl_plugin.h"
+#include "datatype_decl_plugin.h"
+
+namespace smt {
+
+        
+    bool is_value_sort(ast_manager& m, sort* s) {
+        arith_util arith(m);
+        datatype_util data(m);
+        bv_util bv(m);
+        
+        ptr_vector<sort> sorts;
+        ast_mark mark;
+        sorts.push_back(s);
+        
+        while (!sorts.empty()) {
+            s = sorts.back();
+            sorts.pop_back();
+            if (mark.is_marked(s)) {
+                continue;
+            }
+            mark.mark(s, true);
+            if (arith.is_int_real(s)) {
+                // simple
+            }
+            else if (m.is_bool(s)) {
+                // simple
+            }
+            else if (bv.is_bv_sort(s)) {
+                // simple
+            }
+            else if (data.is_datatype(s)) {
+                ptr_vector<func_decl> const& cs = *data.get_datatype_constructors(s);
+                for (unsigned i = 0; i < cs.size(); ++i) {
+                    func_decl* f = cs[i];
+                    for (unsigned j = 0; j < f->get_arity(); ++j) {
+                        sorts.push_back(f->get_domain(j));
+                    }
+                }
+            }
+            else {
+                return false;
+            }
+        }
+        return true;        
+    }
+
+    bool is_value_sort(ast_manager& m, expr* e) {
+        return is_value_sort(m, m.get_sort(e));
+    }
+
+}

src/smt/smt_value_sort.h

@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    smt_value_sort.h
+
+Abstract:
+
+    Determine if elements of a given sort can be values.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-25
+
+Revision History:
+
+
+--*/
+
+
+#ifndef __SMT_VALUE_SORT_H__
+#define __SMT_VALUE_SORT_H__
+
+#include "ast.h"
+
+
+namespace smt {
+        
+    bool is_value_sort(ast_manager& m, sort* s);
+
+    bool is_value_sort(ast_manager& m, expr* e);
+    
+};
+
+
+#endif