#6116

handle also nan/oo/0+ as numerals
Z3Prover · Aug 18, 2022 · 4be26eb · 4be26eb
1 parent 8e167aa
commit 4be26eb
Showing 1 changed file with 30 additions and 5 deletions.
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
@@ -147,11 +147,36 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a
 
 void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 0);
-    SASSERT(f->get_num_parameters() == 1);
-    SASSERT(f->get_parameter(0).is_external());
-    unsigned p_id = f->get_parameter(0).get_ext_id();
-    mpf const & v = m_plugin->get_value(p_id);
-    mk_numeral(f->get_range(), v, result);
+    sort* s = f->get_range();
+    if (f->get_num_parameters() == 1) {
+        SASSERT(f->get_parameter(0).is_external());
+        unsigned p_id = f->get_parameter(0).get_ext_id();
+        mpf const& v = m_plugin->get_value(p_id);
+        mk_numeral(s, v, result);
+        return;
+    }
+    scoped_mpf v(m_mpf_manager);   
+    unsigned ebits = m_util.get_ebits(s), sbits = m_util.get_sbits(s);
+    switch (f->get_decl_kind()) {
+    case OP_FPA_PLUS_INF:
+        m_util.fm().mk_pinf(ebits, sbits, v);
+        break;
+    case OP_FPA_MINUS_INF:
+        m_util.fm().mk_ninf(ebits, sbits, v);
+        break;
+    case OP_FPA_NAN:        
+        m_util.fm().mk_nan(ebits, sbits, v);
+        break;
+    case OP_FPA_PLUS_ZERO:
+        m_util.fm().mk_pzero(ebits, sbits, v);
+        break;
+    case OP_FPA_MINUS_ZERO:
+        m_util.fm().mk_nzero(ebits, sbits, v);
+        break;
+    default:
+        UNREACHABLE();
+    }
+    mk_numeral(s, v, result);
 }
 
 void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) {