prepare for min/max i

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 16, 2021 · c3c5c14 · c3c5c14
1 parent 50375df
commit c3c5c14
Show file tree

Hide file tree

Showing 7 changed files with 26 additions and 0 deletions.
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1267,6 +1267,16 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) {
     result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), exp, sig);
 }
 
+void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_MIN, 0, nullptr, num, args), m);
+    mk_min(fu, num, args, result);
+}
+
+void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_MAX, 0, nullptr, num, args), m);
+    mk_max(fu, num, args, result);
+}
+
 void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
 

diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
@@ -149,6 +149,8 @@ class fpa2bv_converter {
 
     void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y);
 
     void reset();

diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -124,6 +124,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
         case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
         case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
+        case OP_FPA_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
+        case OP_FPA_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
         case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
         case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
         case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;

diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
@@ -375,6 +375,8 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters
     case OP_FPA_REM: name = "fp.rem"; break;
     case OP_FPA_MIN: name = "fp.min"; break;
     case OP_FPA_MAX: name = "fp.max"; break;
+    case OP_FPA_MIN_I: name = "fp.min_i"; break;
+    case OP_FPA_MAX_I: name = "fp.max_i"; break;
     default:
         UNREACHABLE();
         break;
@@ -756,6 +758,8 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_FPA_REM:
     case OP_FPA_MIN:
     case OP_FPA_MAX:
+    case OP_FPA_MIN_I:
+    case OP_FPA_MAX_I:
         return mk_binary_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_ADD:
     case OP_FPA_MUL:
@@ -829,6 +833,8 @@ void fpa_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("fp.roundToIntegral", OP_FPA_ROUND_TO_INTEGRAL));
     op_names.push_back(builtin_name("fp.min", OP_FPA_MIN));
     op_names.push_back(builtin_name("fp.max", OP_FPA_MAX));
+    op_names.push_back(builtin_name("fp.min_i", OP_FPA_MIN_I));
+    op_names.push_back(builtin_name("fp.max_i", OP_FPA_MAX_I));
     op_names.push_back(builtin_name("fp.leq", OP_FPA_LE));
     op_names.push_back(builtin_name("fp.lt",  OP_FPA_LT));
     op_names.push_back(builtin_name("fp.geq", OP_FPA_GE));

diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
@@ -58,6 +58,8 @@ enum fpa_op_kind {
     OP_FPA_ABS,
     OP_FPA_MIN,
     OP_FPA_MAX,
+    OP_FPA_MIN_I,
+    OP_FPA_MAX_I,
     OP_FPA_FMA, // x*y + z
     OP_FPA_SQRT,
     OP_FPA_ROUND_TO_INTEGRAL,

diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
@@ -66,6 +66,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_ABS:       SASSERT(num_args == 1); st = mk_abs(args[0], result); break;
     case OP_FPA_MIN:       SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break;
     case OP_FPA_MAX:       SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
+    case OP_FPA_MIN_I:     SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break;
+    case OP_FPA_MAX_I:     SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
     case OP_FPA_FMA:       SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break;
     case OP_FPA_SQRT:      SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
     case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break;

diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
@@ -82,6 +82,8 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
 
 func_interp* model_core::update_func_interp(func_decl* d, func_interp* fi) {
     TRACE("model", tout << "register " << d->get_name() << "\n";);
+    std::cout << d->get_name() << "\n";
+
     SASSERT(d->get_arity() > 0);
     SASSERT(&fi->m() == &m);
     func_interp* old_fi = nullptr;