int<->real coercions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

c++/z3++.h

@@ -246,6 +246,7 @@ namespace z3 {
         ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
         ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
         operator Z3_ast() const { return m_ast; }
+        operator bool() const { return m_ast != 0; }
         ast & operator=(ast const & s) { Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; }
         Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
         unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }

lib/arith_decl_plugin.cpp

@@ -332,8 +332,8 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
     case OP_SUB:     return is_real ? m_r_sub_decl : m_i_sub_decl;
     case OP_UMINUS:  return is_real ? m_r_uminus_decl : m_i_uminus_decl;
     case OP_MUL:     return is_real ? m_r_mul_decl : m_i_mul_decl;
-    case OP_DIV:     SASSERT(is_real);   return m_r_div_decl;
+    case OP_DIV:     return m_r_div_decl;
-    case OP_IDIV:    SASSERT(!is_real);  return m_i_div_decl;
+    case OP_IDIV:    return m_i_div_decl;
     case OP_REM:     return m_i_rem_decl;
     case OP_MOD:     return m_i_mod_decl;
     case OP_TO_REAL: return m_to_real_decl;
@@ -415,6 +415,24 @@ func_decl * arith_decl_plugin::mk_num_decl(unsigned num_parameters, parameter co
     else
         return m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, num_parameters, parameters));
 }
+
+static bool use_coercion(decl_kind k) {
+    return k == OP_ADD || k == OP_SUB || k == OP_MUL || k == OP_POWER || k == OP_LE || k == OP_GE || k == OP_LT || k == OP_GT || k == OP_UMINUS;
+}
+
+static bool has_real_arg(unsigned arity, sort * const * domain, sort * real_sort) {
+    for (unsigned i = 0; i < arity; i++)
+        if (domain[i] == real_sort)
+            return true;
+    return false;
+}
+
+static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args, sort * real_sort) {
+    for (unsigned i = 0; i < num_args; i++)
+        if (m->get_sort(args[i]) == real_sort)
+            return true;
+    return false;
+}
     
 func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                           unsigned arity, sort * const * domain, sort * range) {
@@ -424,8 +442,13 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         m_manager->raise_exception("no arguments supplied to arithmetical operator");
         return 0;
     }
-    bool is_real = arity > 0 && domain[0] == m_real_decl;
+    if (m_manager->int_real_coercions() && use_coercion(k)) {
-    return mk_func_decl(fix_kind(k, arity), is_real);
+        return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl));
+    }
+    else {
+        bool is_real = arity > 0 && domain[0] == m_real_decl;
+        return mk_func_decl(fix_kind(k, arity), is_real);
+    }
 }
 
 func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
@@ -436,8 +459,13 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         m_manager->raise_exception("no arguments supplied to arithmetical operator");
         return 0;
     }
-    bool is_real = num_args > 0 && m_manager->get_sort(args[0]) == m_real_decl;
+    if (m_manager->int_real_coercions() && use_coercion(k)) {
-    return mk_func_decl(fix_kind(k, num_args), is_real);
+        return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl));
+    }
+    else {
+        bool is_real = num_args > 0 && m_manager->get_sort(args[0]) == m_real_decl;
+        return mk_func_decl(fix_kind(k, num_args), is_real);
+    }
 }
 
 void arith_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) {

lib/arith_rewriter.cpp

@@ -943,6 +943,42 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
         return BR_DONE;
     }
     else {
+        if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) {
+            // Try to apply simplifications such as:
+            //    (to_int (+ 1.0 (to_real x))) --> (+ 1 x)
+
+            // if all arguments of arg are
+            //   - integer numerals, OR
+            //   - to_real applications
+            // then, to_int can be eliminated
+            unsigned num_args = to_app(arg)->get_num_args();
+            unsigned i = 0;
+            for (; i < num_args; i++) {
+                expr * c = to_app(arg)->get_arg(i);
+                if (m_util.is_numeral(c, a) && a.is_int())
+                    continue;
+                if (m_util.is_to_real(c))
+                    continue;
+                break; // failed
+            }
+            if (i == num_args) {
+                // simplification can be applied
+                expr_ref_buffer new_args(m());
+                for (i = 0; i < num_args; i++) {
+                    expr * c = to_app(arg)->get_arg(i);
+                    if (m_util.is_numeral(c, a) && a.is_int()) {
+                        new_args.push_back(m_util.mk_numeral(a, true));
+                    }
+                    else {
+                        SASSERT(m_util.is_to_real(c));
+                        new_args.push_back(to_app(c)->get_arg(0));
+                    }
+                }
+                SASSERT(num_args == new_args.size());
+                result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), new_args.size(), new_args.c_ptr());
+                return BR_REWRITE1;
+            }
+        }
         return BR_FAILED;
     }
 }

lib/array_decl_plugin.cpp

@@ -237,18 +237,20 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
         m_manager->raise_exception("select requires as many arguments as the size of the domain");
         return 0;
     }
-    if (domain[0] != s) {
+    ptr_buffer<sort> new_domain; // we need this because of coercions.
-        m_manager->raise_exception("first argument of select needs to be an array");
+    new_domain.push_back(s);
-        return 0;
-    }
     for (unsigned i = 0; i + 1 < num_parameters; ++i) {
-        if (!parameters[i].is_ast() || domain[i+1] != parameters[i].get_ast()) {
+        if (!parameters[i].is_ast() || 
+            !is_sort(parameters[i].get_ast()) || 
+            !m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) {
             m_manager->raise_exception("domain sort and parameter do not match");
             UNREACHABLE();
             return 0;
         }
+        new_domain.push_back(to_sort(parameters[i].get_ast()));
     }
-    return m_manager->mk_func_decl(m_select_sym, arity, domain, get_array_range(domain[0]),
+    SASSERT(new_domain.size() == arity);
+    return m_manager->mk_func_decl(m_select_sym, arity, new_domain.c_ptr(), get_array_range(domain[0]),
                                    func_decl_info(m_family_id, OP_SELECT));
 }
 
@@ -273,18 +275,22 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
         UNREACHABLE();
         return 0;
     }
+    ptr_buffer<sort> new_domain; // we need this because of coercions.
+    new_domain.push_back(s);
     for (unsigned i = 0; i < num_parameters; ++i) {
-        if (!parameters[i].is_ast()) {
+        if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast())) {
             m_manager->raise_exception("expecting sort parameter");
             return 0;
         }
-        if (parameters[i].get_ast() != domain[i+1]) {
+        if (!m_manager->compatible_sorts(to_sort(parameters[i].get_ast()), domain[i+1])) {
             m_manager->raise_exception("domain sort and parameter do not match");
             UNREACHABLE();
             return 0;
         }
+        new_domain.push_back(to_sort(parameters[i].get_ast()));
     }
-    return m_manager->mk_func_decl(m_store_sym, arity, domain, domain[0],
+    SASSERT(new_domain.size() == arity);
+    return m_manager->mk_func_decl(m_store_sym, arity, new_domain.c_ptr(), domain[0],
                                    func_decl_info(m_family_id, OP_STORE));
 }
 

lib/ast.cpp

@@ -1231,6 +1231,7 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs):
 }
 
 void ast_manager::init() {
+    m_int_real_coercions = true;
     m_debug_ref_count = false;
     m_fresh_id = 0;
     m_expr_id_gen.reset(0);
@@ -1241,6 +1242,7 @@ void ast_manager::init() {
     m_pattern_family_id        = get_family_id("pattern");
     m_model_value_family_id    = get_family_id("model-value");
     m_user_sort_family_id      = get_family_id("user-sort");
+    m_arith_family_id          = get_family_id("arith");
     basic_decl_plugin * plugin = alloc(basic_decl_plugin);
     register_plugin(m_basic_family_id, plugin);
     m_bool_sort = plugin->mk_bool_sort();
@@ -1772,7 +1774,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
         sort * expected = decl->get_domain(0);
         for (unsigned i = 0; i < num_args; i++) {
             sort * given = get_sort(args[i]);
-            if (expected != given) {	
+            if (!compatible_sorts(expected, given)) {
                 string_buffer<> buff;
                 buff << "invalid function application, sort mismatch on argument at position " << (i+1);
                 throw ast_exception(buff.c_str());
@@ -1786,7 +1788,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
         for (unsigned i = 0; i < num_args; i++) {
             sort * expected = decl->get_domain(i);
             sort * given    = get_sort(args[i]);
-            if (expected != given) {	
+            if (!compatible_sorts(expected, given)) {
                 string_buffer<> buff;
                 buff << "invalid function application, sort mismatch on argument at position " << (i+1);
                 throw ast_exception(buff.c_str());
@@ -1822,11 +1824,80 @@ bool ast_manager::check_sorts(ast const * n) const {
     }
 }
 
+bool ast_manager::compatible_sorts(sort * s1, sort * s2) const {
+    if (s1 == s2)
+        return true;
+    if (m_int_real_coercions)
+        return s1->get_family_id() == m_arith_family_id && s2->get_family_id() == m_arith_family_id;
+    return false;
+}
+
+bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * const * args) {
+    SASSERT(m_int_real_coercions);
+    if (decl->is_associative()) {
+        sort * d = decl->get_domain(0);
+        if (d->get_family_id() == m_arith_family_id) {
+            for (unsigned i = 0; i < num_args; i++) {
+                if (d != get_sort(args[i]))
+                    return true;
+            }
+        }
+    }
+    else {
+        for (unsigned i = 0; i < num_args; i++) {
+            sort * d = decl->get_domain(i);
+            if (d->get_family_id() == m_arith_family_id && d != get_sort(args[i]))
+                return true;
+        }
+    }
+    return false;
+}
+
 app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const * args) {
     unsigned sz       = app::get_obj_size(num_args);
     void * mem        = allocate_node(sz);
-    app * new_node    = new (mem) app(decl, num_args, args);
+    app * new_node;
-    app * r           = register_node(new_node);
+    app * r;
+    if (m_int_real_coercions && coercion_needed(decl, num_args, args)) {
+        expr_ref_buffer new_args(*this);
+        if (decl->is_associative()) {
+            sort * d = decl->get_domain(0);
+            for (unsigned i = 0; i < num_args; i++) {
+                sort * s = get_sort(args[i]);
+                if (d != s && d->get_family_id() == m_arith_family_id && s->get_family_id() == m_arith_family_id) {
+                    if (d->get_decl_kind() == REAL_SORT)
+                        new_args.push_back(mk_app(m_arith_family_id, OP_TO_REAL, args[i]));
+                    else
+                        new_args.push_back(mk_app(m_arith_family_id, OP_TO_INT, args[i]));
+                }
+                else {
+                    new_args.push_back(args[i]);
+                }
+            }
+        }
+        else {
+            for (unsigned i = 0; i < num_args; i++) {
+                sort * d = decl->get_domain(i);
+                sort * s = get_sort(args[i]);
+                if (d != s && d->get_family_id() == m_arith_family_id && s->get_family_id() == m_arith_family_id) {
+                    if (d->get_decl_kind() == REAL_SORT)
+                        new_args.push_back(mk_app(m_arith_family_id, OP_TO_REAL, args[i]));
+                    else
+                        new_args.push_back(mk_app(m_arith_family_id, OP_TO_INT, args[i]));
+                }
+                else {
+                    new_args.push_back(args[i]);
+                }
+            }
+        }
+        SASSERT(new_args.size() == num_args);
+        new_node = new (mem) app(decl, num_args, new_args.c_ptr());
+        r = register_node(new_node);
+    }
+    else {
+        new_node = new (mem) app(decl, num_args, args);
+        r = register_node(new_node);
+    }
 #ifndef SMTCOMP
     if (m_trace_stream != NULL && r == new_node) {
         *m_trace_stream << "[mk-app] #" << r->get_id() << " ";        

lib/ast.h

@@ -1282,6 +1282,8 @@ enum proof_gen_mode {
 //
 // -----------------------------------
 
+class arith_decl_plugin;
+
 class ast_manager {
 protected:
 protected:
@@ -1331,11 +1333,13 @@ protected:
     expr_dependency_array_manager m_expr_dependency_array_manager;
     ptr_vector<decl_plugin>   m_plugins;
     proof_gen_mode            m_proof_mode;
+    bool                      m_int_real_coercions; // If true, use hack that automatically introduces to_int/to_real when needed.
     family_id                 m_basic_family_id;
     family_id                 m_label_family_id;
     family_id                 m_pattern_family_id;
     family_id                 m_model_value_family_id;
     family_id                 m_user_sort_family_id;
+    family_id                 m_arith_family_id;
     ast_table                 m_ast_table;       
     id_gen                    m_expr_id_gen;
     id_gen                    m_decl_id_gen;
@@ -1355,11 +1359,19 @@ protected:
 
     void init();
 
+    bool coercion_needed(func_decl * decl, unsigned num_args, expr * const * args);
+
 public:
     ast_manager(proof_gen_mode = PGM_DISABLED, std::ostream * trace_stream = NULL, bool is_format_manager = false);
     ast_manager(ast_manager const & src, bool disable_proofs = false);
     ~ast_manager();
+
+    void enable_int_real_coercions(bool f) { m_int_real_coercions = f; }
+    bool int_real_coercions() const { return m_int_real_coercions; }
     
+    // Return true if s1 and s2 are equal, or coercions are enabled, and s1 and s2 are compatible.
+    bool compatible_sorts(sort * s1, sort * s2) const;
+
     // For debugging purposes
     void display_free_ids(std::ostream & out) { m_expr_id_gen.display_free_ids(out); out << "\n"; m_decl_id_gen.display_free_ids(out); }
     

lib/basic_cmds.cpp

@@ -258,6 +258,7 @@ protected:
     symbol      m_global_decls;
     symbol      m_numeral_as_real;
     symbol      m_error_behavior;
+    symbol      m_int_real_coercions;
     ini_params  m_ini;
 
     bool is_builtin_option(symbol const & s) const {
@@ -288,6 +289,7 @@ public:
         m_global_decls(":global-decls"),
         m_numeral_as_real(":numeral-as-real"),
         m_error_behavior(":error-behavior"),
+        m_int_real_coercions(":int-real-coercions"),
         m_ini(false) {
         params.register_params(m_ini);
         register_pp_params(m_ini);
@@ -376,6 +378,9 @@ class set_option_cmd : public set_get_option_cmd {
         else if (m_option == m_numeral_as_real) {
             ctx.set_numeral_as_real(to_bool(value));
         }
+        else if (m_option == m_int_real_coercions) {
+            ctx.m().enable_int_real_coercions(to_bool(value));
+        }
 #ifdef Z3DEBUG
         else if (m_option == ":enable-assertions") {
             enable_assertions(to_bool(value));
@@ -536,6 +541,9 @@ public:
                 print_string(ctx, "continued-execution");
             }
         }
+        else if (opt == m_int_real_coercions) {
+            print_bool(ctx, ctx.m().int_real_coercions());
+        }
         else {
             std::string iopt = smt_keyword2opt_name(opt);
             std::string r;

lib/cmd_context.cpp

@@ -532,6 +532,8 @@ void cmd_context::init_manager() {
     m_manager  = alloc(ast_manager, m_params.m_proof_mode, m_params.m_trace_stream);
     m_pmanager = alloc(pdecl_manager, *m_manager);
     init_manager_core(true);
+    if (m_params.m_smtlib2_compliant)
+        m_manager->enable_int_real_coercions(false);
 }
 
 void cmd_context::init_external_manager() {

lib/front_end_params.h

@@ -95,8 +95,7 @@ struct front_end_params : public preprocessor_params, public spc_params, public
 #else
         m_auto_config(false), 
 #endif
-#if    1 
+#if    0 
-        // #if defined(SMTCOMP) TODO: put it back after SMTCOMP
         m_smtlib2_compliant(true),
 #else
         m_smtlib2_compliant(false),