Apply workaround for Z3_OP_EQ

We explicitly check the argument sort of Z3_OP_EQ. In case they are of sort Z3_FLOATING_POINT_SORT we treat equality as Z3_OP_FPA_EQ, otherwise code for Z3_OP_EQ will be generated as usual. Partial fix for #8
abenkhadra · Jan 23, 2018 · f9a4464 · f9a4464
1 parent 1bc8df2
commit f9a4464
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 24 deletions.
diff --git a/src/IRGen/FPIRGenerator.cpp b/src/IRGen/FPIRGenerator.cpp
@@ -262,24 +262,8 @@ llvm::Value* FPIRGenerator::genExprIR
             else
                 return m_const_one;
         case Z3_OP_EQ:
-            if (expr_sym->isNegated()) {
-                return builder.CreateCall(m_func_fp64_neq_dis,
-                                          {arg_syms[0]->getValue(),
-                                           arg_syms[1]->getValue()});
-            } else {
-                return builder.CreateCall(m_func_fp64_eq_dis,
-                                          {arg_syms[0]->getValue(),
-                                           arg_syms[1]->getValue()});
-            }
         case Z3_OP_FPA_EQ:
-            if (expr_sym->isNegated()) {
-                auto result = builder.CreateFCmpONE(arg_syms[0]->getValue(),
-                                                    arg_syms[1]->getValue());
-                return builder.CreateSelect(result, m_const_zero, m_const_one);
-            } else {
-                return builder.CreateCall(m_func_fp64_dis, {arg_syms[0]->getValue(),
-                                                            arg_syms[1]->getValue()});
-            }
+            return genEqualityIR(builder, expr_sym, arg_syms);
         case Z3_OP_NOT:
             // Do nothing, negation is handled with de-morgans
             return arg_syms[0]->getValue();
@@ -453,6 +437,41 @@ llvm::Value* FPIRGenerator::genMultiArgMulIR
     return result;
 }
 
+llvm::Value *FPIRGenerator::genEqualityIR
+        (llvm::IRBuilder<> &builder, const IRSymbol *expr_sym,
+         std::vector<const IRSymbol *> &arg_syms) noexcept
+{
+
+    // workaround were we explicitly check the sort of the arguments,
+    // because z3 provides Z3_OP_EQ were we expect Z3_OP_FPA_EQ.
+    // See wintersteiger/eq/eq-has-no-other-solution-10015.smt2
+
+    bool is_fpa_args = (arg_syms[0]->expr()->get_sort().sort_kind() ==
+                        Z3_FLOATING_POINT_SORT);
+    assert(is_fpa_args == (arg_syms[1]->expr()->get_sort().sort_kind() ==
+                           Z3_FLOATING_POINT_SORT));
+    if (expr_sym->expr()->decl().decl_kind() == Z3_OP_FPA_EQ || is_fpa_args) {
+        if (expr_sym->isNegated()) {
+            auto result = builder.CreateFCmpONE(arg_syms[0]->getValue(),
+                                                arg_syms[1]->getValue());
+            return builder.CreateSelect(result, m_const_zero, m_const_one);
+        } else {
+            return builder.CreateCall(m_func_fp64_dis, {arg_syms[0]->getValue(),
+                                                        arg_syms[1]->getValue()});
+        }
+    }
+    // assuming Z3_OP_EQ
+    if (expr_sym->isNegated()) {
+        return builder.CreateCall(m_func_fp64_neq_dis,
+                                  {arg_syms[0]->getValue(),
+                                   arg_syms[1]->getValue()});
+    } else {
+        return builder.CreateCall(m_func_fp64_eq_dis,
+                                  {arg_syms[0]->getValue(),
+                                   arg_syms[1]->getValue()});
+    }
+}
+
 unsigned FPIRGenerator::getVarCount() const noexcept
 {
     return static_cast<unsigned>(m_var_sym_vec.size());

diff --git a/src/IRGen/FPIRGenerator.h b/src/IRGen/FPIRGenerator.h
@@ -116,6 +116,10 @@ class FPIRGenerator {
             (llvm::IRBuilder<>& builder,
              std::vector<const IRSymbol*>& arg_syms) noexcept;
 
+    llvm::Value *genEqualityIR
+            (llvm::IRBuilder<> &builder, const IRSymbol *expr_sym,
+             std::vector<const IRSymbol *> &arg_syms) noexcept;
+
     std::pair<IRSymbol*, bool> insertSymbol
             (const SymbolKind kind, const z3::expr expr, llvm::Value* value,
              unsigned id = 0) noexcept;

diff --git a/src/Utils/FPAUtils.cpp b/src/Utils/FPAUtils.cpp
@@ -62,13 +62,9 @@ double fp64_eq_dis(const double a, const double b)
         return 0;
     }
 
-    /* TODO: revisit this decision.
-     * commented out because z3 provides Z3_OP_EQ were we expect Z3_OP_FPA_EQ
-     * see wintersteiger/eq/eq-has-no-other-solution-10015.smt2
-     */
-//    if (a != 0 && b != 0) {
-//        return 0;
-//    }
+    if (a != 0 && b != 0) {
+        return 0;
+    }
 
     return fp64_dis(a, b);
 }