From a07b459fdf4562288816d947315469da81447f27 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Dec 2012 12:53:51 -0800
Subject: [PATCH] Added is_unique_value. Its semantics is equal to the old
 is_value method. The contract for is_value changed. See comments at ast.h for
 more information.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/ast/arith_decl_plugin.cpp                 | 46 +++++++++++++-----
 src/ast/arith_decl_plugin.h                   | 12 +++--
 src/ast/ast.cpp                               | 29 ++++++++++++
 src/ast/ast.h                                 | 47 +++++++++++++++++--
 src/ast/bv_decl_plugin.h                      |  4 +-
 src/ast/datatype_decl_plugin.h                |  3 ++
 src/ast/dl_decl_plugin.h                      |  3 +-
 src/ast/float_decl_plugin.h                   |  1 +
 src/ast/rewriter/bool_rewriter.cpp            |  2 +-
 src/ast/rewriter/th_rewriter.cpp              |  7 ++-
 src/ast/seq_decl_plugin.h                     |  5 +-
 .../simplifier/array_simplifier_plugin.cpp    | 20 ++++----
 src/model/func_interp.cpp                     |  8 ++--
 src/model/func_interp.h                       |  4 +-
 src/smt/proto_model/proto_model.cpp           |  2 +-
 src/smt/smt_internalizer.cpp                  |  2 +-
 src/smt/user_plugin/user_decl_plugin.h        |  2 +
 src/tactic/core/cofactor_elim_term_ite.cpp    |  4 +-
 src/tactic/core/reduce_args_tactic.cpp        |  6 +--
 19 files changed, 157 insertions(+), 50 deletions(-)

diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 4aadafae2..a89cc18d0 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -38,13 +38,6 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
     
     unsigned mk_id(algebraic_numbers::anum const & val) {
         SASSERT(!m_amanager.is_rational(val));
-        // TODO: avoid linear scan. Use hashtable based on the floor of val
-        unsigned sz = m_nums.size();
-        for (unsigned i = 0; i < sz; i++) {
-            algebraic_numbers::anum const & other = m_nums.get(i);
-            if (m_amanager.eq(val, other))
-                return i;
-        }
         unsigned new_id = m_id_gen.mk();
         m_nums.reserve(new_id+1);
         m_amanager.set(m_nums[new_id], val);
@@ -71,13 +64,13 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
 
 };
 
-arith_decl_plugin::algebraic_numbers_wrapper & arith_decl_plugin::aw() {
+arith_decl_plugin::algebraic_numbers_wrapper & arith_decl_plugin::aw() const {
     if (m_aw == 0)
-        m_aw = alloc(algebraic_numbers_wrapper);
+        const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper);
     return *m_aw;
 }
 
-algebraic_numbers::manager & arith_decl_plugin::am() {
+algebraic_numbers::manager & arith_decl_plugin::am() const {
     return aw().m_amanager;
 }
 
@@ -509,16 +502,43 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
     }
 }
 
-bool arith_decl_plugin::is_value(app* e) const {
-    return is_app_of(e, m_family_id, OP_NUM);
+bool arith_decl_plugin::is_value(app * e) const {
+    return 
+        is_app_of(e, m_family_id, OP_NUM) || 
+        is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) ||
+        is_app_of(e, m_family_id, OP_PI) ||
+        is_app_of(e, m_family_id, OP_E);
 }
 
-bool arith_decl_plugin::are_distinct(app* a, app* b) const {
+bool arith_decl_plugin::is_unique_value(app * e) const {
+    return 
+        is_app_of(e, m_family_id, OP_NUM) || 
+        is_app_of(e, m_family_id, OP_PI) ||
+        is_app_of(e, m_family_id, OP_E);
+}
+
+bool arith_decl_plugin::are_equal(app * a, app * b) const {
+    if (decl_plugin::are_equal(a, b)) {
+        return true;
+    }
+
+    if (is_app_of(a, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) && is_app_of(b, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM)) {
+        return am().eq(aw().to_anum(a->get_decl()), aw().to_anum(b->get_decl()));
+    }
+
+    return false;
+}
+
+bool arith_decl_plugin::are_distinct(app * a, app * b) const {
     TRACE("are_distinct_bug", tout << mk_ismt2_pp(a, *m_manager) << "\n" << mk_ismt2_pp(b, *m_manager) << "\n";);
     if (decl_plugin::are_distinct(a,b)) {
         return true;
     }
 
+    if (is_app_of(a, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) && is_app_of(b, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM)) {
+        return am().neq(aw().to_anum(a->get_decl()), aw().to_anum(b->get_decl()));
+    }
+
 #define is_non_zero(e) is_app_of(e,m_family_id, OP_NUM) && !to_app(e)->get_decl()->get_parameter(0).get_rational().is_zero()
 
     if (is_app_of(a, m_family_id, OP_ADD) &&
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 6a377c577..b8ad11506 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -141,8 +141,8 @@ public:
     virtual ~arith_decl_plugin();
     virtual void finalize();
 
-    algebraic_numbers::manager & am();
-    algebraic_numbers_wrapper & aw();
+    algebraic_numbers::manager & am() const;
+    algebraic_numbers_wrapper & aw() const;
 
     virtual void del(parameter const & p);
     virtual parameter translate(parameter const & p, decl_plugin & target);
@@ -159,9 +159,13 @@ public:
     virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                      unsigned num_args, expr * const * args, sort * range);
 
-    virtual bool is_value(app* e) const;
+    virtual bool is_value(app * e) const;
 
-    virtual bool are_distinct(app* a, app* b) const;
+    virtual bool is_unique_value(app * e) const;
+
+    virtual bool are_equal(app * a, app * b) const;
+
+    virtual bool are_distinct(app * a, app * b) const;
 
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
 
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index ae82dcadf..bd5ffaf35 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -872,6 +872,10 @@ bool basic_decl_plugin::is_value(app* a) const {
     return a->get_decl() == m_true_decl || a->get_decl() == m_false_decl;
 }
 
+bool basic_decl_plugin::is_unique_value(app* a) const {
+    return is_value(a);
+}
+
 void basic_decl_plugin::finalize() {
 #define DEC_REF(FIELD) if (FIELD) { m_manager->dec_ref(FIELD); }
 #define DEC_ARRAY_REF(FIELD) m_manager->dec_array_ref(FIELD.size(), FIELD.begin())
@@ -1151,6 +1155,10 @@ bool model_value_decl_plugin::is_value(app* n) const {
     return is_app_of(n, m_family_id, OP_MODEL_VALUE);
 }
 
+bool model_value_decl_plugin::is_unique_value(app* n) const {
+    return is_value(n);
+}
+
 // -----------------------------------
 //
 // user_sort_plugin
@@ -1442,6 +1450,27 @@ bool ast_manager::is_value(expr* e) const {
     return false;
 }
 
+bool ast_manager::is_unique_value(expr* e) const {
+    decl_plugin const * p = 0;
+    if (is_app(e)) {
+        p = get_plugin(to_app(e)->get_family_id());
+        return p && p->is_unique_value(to_app(e));
+    }
+    return false;
+}
+
+bool ast_manager::are_equal(expr * a, expr * b) const {
+    if (is_app(a) && is_app(b)) {
+        app* ap = to_app(a), *bp = to_app(b);
+        decl_plugin const * p = get_plugin(ap->get_family_id());
+        if (!p) {
+            p = get_plugin(bp->get_family_id());
+        }
+        return p && p->are_equal(ap, bp);
+    }
+    return false;
+}
+
 bool ast_manager::are_distinct(expr* a, expr* b) const {
     if (is_app(a) && is_app(b)) {
         app* ap = to_app(a), *bp = to_app(b);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 2a0872721..0ca47ccec 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -933,9 +933,39 @@ public:
     virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters, 
                                      unsigned num_args, expr * const * args, sort * range);
 
-    virtual bool is_value(app*) const { return false; }
+    /**
+       \brief Return true if the plugin can decide whether two
+       interpreted constants are equal or not.
+       
+       For all a, b:
+          If is_value(a) and is_value(b)
+          Then,
+               are_equal(a, b) != are_distinct(a, b)
+          
+       The may be much more expensive than checking a pointer.
 
-    virtual bool are_distinct(app* a, app* b) const { return a != b && is_value(a) && is_value(b); }
+       We need this because some plugin values are too expensive too canonize.
+    */
+    virtual bool is_value(app * a) const { return false; }
+
+    /**
+       \brief Return true if \c a is a unique plugin value.
+       The following property should hold for unique theory values:
+       
+       For all a, b:
+          If is_unique_value(a) and is_unique_value(b)
+          Then,
+              a == b (pointer equality)
+              IFF
+              the interpretations of these theory terms are equal.
+
+       \remark This is a stronger version of is_value.
+    */
+    virtual bool is_unique_value(app * a) const { return false; }
+
+    virtual bool are_equal(app * a, app * b) const { return a == b && is_unique_value(a) && is_unique_value(b); }
+    
+    virtual bool are_distinct(app * a, app * b) const { return a != b && is_unique_value(a) && is_unique_value(b); }
     
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic = symbol()) {}
     
@@ -1080,6 +1110,8 @@ public:
     virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
 
     virtual bool is_value(app* a) const; 
+
+    virtual bool is_unique_value(app* a) const; 
     
     sort * mk_bool_sort() const { return m_bool_sort; }
     sort * mk_proof_sort() const { return m_proof_sort; } 
@@ -1116,7 +1148,6 @@ public:
 
     virtual decl_plugin * mk_fresh() { return alloc(label_decl_plugin); }
 
-
     virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
 
     /**
@@ -1198,6 +1229,8 @@ public:
                                      unsigned arity, sort * const * domain, sort * range);
 
     virtual bool is_value(app* n) const;
+
+    virtual bool is_unique_value(app* a) const; 
 };
 
 // -----------------------------------
@@ -1442,9 +1475,13 @@ public:
     */
     void set_next_expr_id(unsigned id);
     
-    bool is_value(expr* e) const; 
+    bool is_value(expr * e) const; 
+    
+    bool is_unique_value(expr * e) const;
 
-    bool are_distinct(expr* a, expr* b) const;
+    bool are_equal(expr * a, expr * b) const;
+    
+    bool are_distinct(expr * a, expr * b) const;
     
     bool contains(ast * a) const { return m_ast_table.contains(a); }
     
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index a98f39323..34f2baf6b 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -260,8 +260,10 @@ public:
     virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                      unsigned num_args, expr * const * args, sort * range);
 
-    virtual bool is_value(app* e) const;
+    virtual bool is_value(app * e) const;
     
+    virtual bool is_unique_value(app * e) const { return is_value(e); }
+
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
 
     virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index a8bd28d8e..96b678fb2 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -146,6 +146,9 @@ public:
     virtual bool is_fully_interp(sort const * s) const;
 
     virtual bool is_value(app* e) const;
+
+    virtual bool is_unique_value(app * e) const { return is_value(e); }
+
 private:
     bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
 };
diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h
index 32e3c6da9..559aff7bd 100644
--- a/src/ast/dl_decl_plugin.h
+++ b/src/ast/dl_decl_plugin.h
@@ -130,7 +130,8 @@ namespace datalog {
         
         virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
 
-        virtual bool is_value(app* e) const { return is_app_of(e, m_family_id, OP_DL_CONSTANT); }
+        virtual bool is_value(app * e) const { return is_app_of(e, m_family_id, OP_DL_CONSTANT); }
+        virtual bool is_unique_value(app * e) const { return is_value(e); }
 
     };
 
diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h
index c4503349b..6f1ef5ec2 100644
--- a/src/ast/float_decl_plugin.h
+++ b/src/ast/float_decl_plugin.h
@@ -141,6 +141,7 @@ public:
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
     virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
     virtual bool is_value(app* e) const;
+    virtual bool is_unique_value(app* e) const { return is_value(e); }
     
     mpf_manager & fm() { return m_fm; }
     func_decl * mk_value_decl(mpf const & v);
diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 4fcaf02fe..b5f18a461 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -732,7 +732,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
             return BR_DONE;
         }
         visited.mark(arg);
-        if (!m().is_value(arg))
+        if (!m().is_unique_value(arg))
             all_value = false;
     }
     if (all_value) {
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 29034d396..966544b78 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -200,7 +200,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     expr * mk_eq_value(expr * lhs, expr * value) {
         SASSERT(m().is_value(value));
         if (m().is_value(lhs)) {
-            return lhs == value ? m().mk_true() : m().mk_false();
+            if (m().are_equal(lhs, value)) {
+                return m().mk_true();
+            }
+            else if (m().are_distinct(lhs, value)) {
+                return m().mk_false();
+            }
         }
         return m().mk_eq(lhs, value);
     }
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index c055694eb..1bb3f3581 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -112,7 +112,10 @@ public:
     
     virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
     
-    virtual bool is_value(app* e) const;
+    virtual bool is_value(app * e) const;
+
+    virtual bool is_unique_value(app * e) const { return is_value(e); }
+
     
 };
 
diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp
index 75c3cdbce..bf9ca8ffe 100644
--- a/src/ast/simplifier/array_simplifier_plugin.cpp
+++ b/src/ast/simplifier/array_simplifier_plugin.cpp
@@ -293,7 +293,7 @@ bool array_simplifier_plugin::all_const_array(unsigned num_args, expr* const* ar
 
 bool array_simplifier_plugin::all_values(unsigned num_args, expr* const* args) const {
     for (unsigned i = 0; i < num_args; ++i) {
-        if (!m_manager.is_value(args[i])) {
+        if (!m_manager.is_unique_value(args[i])) {
             return false;
         }
     }
@@ -331,7 +331,7 @@ lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned nu
         if (st[i][arity] == def) {
             continue;
         }
-        if (m_manager.is_value(st[i][arity]) && m_manager.is_value(def)) {
+        if (m_manager.is_unique_value(st[i][arity]) && m_manager.is_unique_value(def)) {
             return l_false;
         }
         return l_undef;
@@ -342,7 +342,7 @@ lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned nu
 bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) {
     for (unsigned i = 0; i < num_st; ++i ) {
         for (unsigned j = 0; j < arity; ++j) {
-            if (!m_manager.is_value(st[i][j])) {
+            if (!m_manager.is_unique_value(st[i][j])) {
                 return false;
             }
         }
@@ -380,12 +380,12 @@ lbool array_simplifier_plugin::eq_stores(expr* def, unsigned arity, unsigned num
                 table2.erase(e1);
                 continue;
             }
-            if (m_manager.is_value(v1) && m_manager.is_value(v2)) {
+            if (m_manager.is_unique_value(v1) && m_manager.is_unique_value(v2)) {
                 return l_false;
             }
             return l_undef;
         }
-        else if (m_manager.is_value(v1) && m_manager.is_value(def) && v1 != def) {
+        else if (m_manager.is_unique_value(v1) && m_manager.is_unique_value(def) && v1 != def) {
             return l_false;
         }
     }
@@ -394,7 +394,7 @@ lbool array_simplifier_plugin::eq_stores(expr* def, unsigned arity, unsigned num
     for (; it != end; ++it) {
         args_entry const & e = *it;
         expr* v = e.m_args[arity];
-        if (m_manager.is_value(v) && m_manager.is_value(def) && v != def) {
+        if (m_manager.is_unique_value(v) && m_manager.is_unique_value(def) && v != def) {
             return l_false;
         }
     }
@@ -431,7 +431,7 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul
                 return false;
             }
         }
-        else if (m_manager.is_value(c1) && m_manager.is_value(c2)) {
+        else if (m_manager.is_unique_value(c1) && m_manager.is_unique_value(c2)) {
             result = m_manager.mk_false();
             return true;
         }
@@ -464,7 +464,7 @@ array_simplifier_plugin::mk_select_const(expr* m, app* index, expr_ref& result)
     // 
     // Unfold and cache the store while searching for value of index.
     //     
-    while (is_store(a) && m_manager.is_value(to_app(a)->get_arg(1))) {
+    while (is_store(a) && m_manager.is_unique_value(to_app(a)->get_arg(1))) {
         app* b = to_app(a);
         app* c = to_app(b->get_arg(1));
         
@@ -728,7 +728,7 @@ void array_simplifier_plugin::mk_select(unsigned num_args, expr * const * args,
         return;
     }
 
-    bool is_const_select = num_args == 2 && m_manager.is_value(args[1]);
+    bool is_const_select = num_args == 2 && m_manager.is_unique_value(args[1]);
     app* const_index = is_const_select?to_app(args[1]):0;
     unsigned num_const_stores = 0;
     expr_ref tmp(m_manager);
@@ -766,7 +766,7 @@ void array_simplifier_plugin::mk_select(unsigned num_args, expr * const * args,
             expr * else_branch  = 0;
             entry[0] = nested_array;
             if (is_const_select) {
-                if (m_manager.is_value(to_app(m)->get_arg(1))) {
+                if (m_manager.is_unique_value(to_app(m)->get_arg(1))) {
                     app* const_index2 = to_app(to_app(m)->get_arg(1));
                     //
                     // we found the value, all other stores are different.
diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index 678d95c86..ae4c657bd 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -49,10 +49,10 @@ void func_entry::set_result(ast_manager & m, expr * r) {
     m_result = r;
 }
 
-bool func_entry::eq_args(unsigned arity, expr * const * args) const {
+bool func_entry::eq_args(ast_manager & m, unsigned arity, expr * const * args) const {
     unsigned i = 0;
     for (; i < arity; i++) {
-        if (m_args[i] != args[i])
+        if (!m.are_equal(m_args[i], args[i]))
             return false;
     }
     return true;
@@ -131,7 +131,7 @@ bool func_interp::is_constant() const {
 }
 
 /**
-   \brief Return a func_entry e such that e.m_args[i] == args[i] for all i in [0, m_arity).
+   \brief Return a func_entry e such that m().are_equal(e.m_args[i], args[i]) for all i in [0, m_arity).
    If such entry does not exist then return 0, and store set
    args_are_values to true if for all entries e e.args_are_values() is true.
 */
@@ -140,7 +140,7 @@ func_entry * func_interp::get_entry(expr * const * args) const {
     ptr_vector<func_entry>::const_iterator end = m_entries.end();
     for (; it != end; ++it) {
         func_entry * curr = *it;
-        if (curr->eq_args(m_arity, args))
+        if (curr->eq_args(m(), m_arity, args))
             return curr;
     }
     return 0;
diff --git a/src/model/func_interp.h b/src/model/func_interp.h
index b10fe0dad..fd21a6a7c 100644
--- a/src/model/func_interp.h
+++ b/src/model/func_interp.h
@@ -58,9 +58,9 @@ public:
     expr * get_arg(unsigned idx) const { return m_args[idx]; }
     expr * const * get_args() const { return m_args; }
     /**
-       \brief Return true if m_args[i] == args[i] for all i in [0, arity)
+       \brief Return true if m.are_equal(m_args[i], args[i]) for all i in [0, arity)
     */
-    bool eq_args(unsigned arity, expr * const * args) const;
+    bool eq_args(ast_manager & m, unsigned arity, expr * const * args) const;
 };
 
 class func_interp {
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 34742e3a0..92110bc1a 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -155,7 +155,7 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu
     basic_simplifier_plugin * bs = static_cast<basic_simplifier_plugin*>(s.get_plugin(fi.m().get_basic_family_id()));
     for (unsigned k = 0; k < fi.num_entries(); k++) {
         func_entry const * curr = fi.get_entry(k);
-        SASSERT(!curr->eq_args(fi.get_arity(), args));
+        SASSERT(!curr->eq_args(fi.m(), fi.get_arity(), args));
         if (!actuals_are_values || !curr->args_are_values()) {
             expr_ref_buffer eqs(fi.m());
             unsigned i = fi.get_arity();
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 556222c33..b3f16a3ce 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -907,7 +907,7 @@ namespace smt {
         }
         enode * e           = enode::mk(m_manager, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true);
         TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
-        if (n->get_num_args() == 0 && m_manager.is_value(n))
+        if (n->get_num_args() == 0 && m_manager.is_unique_value(n))
             e->mark_as_interpreted();
         TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
         TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);
diff --git a/src/smt/user_plugin/user_decl_plugin.h b/src/smt/user_plugin/user_decl_plugin.h
index dc2fd55a1..9e6bd70c4 100644
--- a/src/smt/user_plugin/user_decl_plugin.h
+++ b/src/smt/user_plugin/user_decl_plugin.h
@@ -49,6 +49,8 @@ public:
     
     virtual bool is_value(app*) const;
 
+    virtual bool is_unique_value(app * a) const { return is_value(a); }
+
     bool is_value(func_decl *) const;
     
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp
index 78d532357..d81b4fa13 100644
--- a/src/tactic/core/cofactor_elim_term_ite.cpp
+++ b/src/tactic/core/cofactor_elim_term_ite.cpp
@@ -355,12 +355,12 @@ struct cofactor_elim_term_ite::imp {
                 expr * lhs;
                 expr * rhs;
                 if (m.is_eq(t, lhs, rhs)) {
-                    if (m.is_value(lhs)) {
+                    if (m.is_unique_value(lhs)) {
                         m_term  = rhs;
                         m_value = to_app(lhs); 
                         TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
                     }
-                    else if (m.is_value(rhs)) {
+                    else if (m.is_unique_value(rhs)) {
                         m_term  = lhs;
                         m_value = to_app(rhs);
                         TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 686c5128d..59ed2dcd3 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -128,7 +128,7 @@ struct reduce_args_tactic::imp {
             unsigned j    = n->get_num_args();        
             while (j > 0) {
                 --j;
-                if (m_manager.is_value(n->get_arg(j)))
+                if (m_manager.is_unique_value(n->get_arg(j)))
                     return;
             }  
             m_non_cadidates.insert(d);
@@ -185,13 +185,13 @@ struct reduce_args_tactic::imp {
                 it->m_value.reserve(j);
                 while (j > 0) {
                     --j;
-                    it->m_value.set(j, m_manager.is_value(n->get_arg(j)));
+                    it->m_value.set(j, m_manager.is_unique_value(n->get_arg(j)));
                 }
             } else {
                 SASSERT(j == it->m_value.size());                        
                 while (j > 0) {
                     --j;
-                    it->m_value.set(j, it->m_value.get(j) && m_manager.is_value(n->get_arg(j)));
+                    it->m_value.set(j, it->m_value.get(j) && m_manager.is_unique_value(n->get_arg(j)));
                 }
             }
         }