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

@@ -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) &&

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

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

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

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

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;
 };

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

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

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) {

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

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); }
+
     
 };
 

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.