5 files changed, 186 insertions, 212 deletions

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 5ee5fd7d8..d38b6d0fa 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -65,8 +65,6 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation)
       d_registeredTerms(userContext()),
       d_wordBlaster(new FpWordBlaster(userContext())),
       d_expansionRequested(false),
-      d_realToFloatMap(userContext()),
-      d_floatToRealMap(userContext()),
       d_abstractionMap(userContext()),
       d_rewriter(userContext()),
       d_state(env, valuation),
@@ -148,72 +146,6 @@ void TheoryFp::finishInit()
   d_equalityEngine->addFunctionKind(kind::ROUNDINGMODE_BITBLAST);
 }
 
-Node TheoryFp::abstractRealToFloat(Node node)
-{
-  Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
-  TypeNode t(node.getType());
-  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
-
-  NodeManager *nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-  ConversionAbstractionMap::const_iterator i(d_realToFloatMap.find(t));
-
-  Node fun;
-  if (i == d_realToFloatMap.end())
-  {
-    std::vector<TypeNode> args(2);
-    args[0] = node[0].getType();
-    args[1] = node[1].getType();
-    fun = sm->mkDummySkolem("floatingpoint_abstract_real_to_float",
-                            nm->mkFunctionType(args, node.getType()),
-                            "floatingpoint_abstract_real_to_float",
-                            NodeManager::SKOLEM_EXACT_NAME);
-    d_realToFloatMap.insert(t, fun);
-  }
-  else
-  {
-    fun = (*i).second;
-  }
-  Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
-
-  d_abstractionMap.insert(uf, node);
-
-  return uf;
-}
-
-Node TheoryFp::abstractFloatToReal(Node node)
-{
-  Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL);
-  TypeNode t(node[0].getType());
-  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
-
-  NodeManager *nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-  ConversionAbstractionMap::const_iterator i(d_floatToRealMap.find(t));
-
-  Node fun;
-  if (i == d_floatToRealMap.end())
-  {
-    std::vector<TypeNode> args(2);
-    args[0] = t;
-    args[1] = nm->realType();
-    fun = sm->mkDummySkolem("floatingpoint_abstract_float_to_real",
-                            nm->mkFunctionType(args, nm->realType()),
-                            "floatingpoint_abstract_float_to_real",
-                            NodeManager::SKOLEM_EXACT_NAME);
-    d_floatToRealMap.insert(t, fun);
-  }
-  else
-  {
-    fun = (*i).second;
-  }
-  Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
-
-  d_abstractionMap.insert(uf, node);
-
-  return uf;
-}
-
 TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
 {
   Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
@@ -226,53 +158,6 @@ TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
 
   Node res = node;
 
-  // Abstract conversion functions
-  if (node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL)
-  {
-    res = abstractFloatToReal(node);
-
-    // Generate some lemmas
-    NodeManager *nm = NodeManager::currentNM();
-
-    Node pd =
-        nm->mkNode(kind::IMPLIES,
-                   nm->mkNode(kind::OR,
-                              nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]),
-                              nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])),
-                   nm->mkNode(kind::EQUAL, res, node[1]));
-    handleLemma(pd, InferenceId::FP_PREPROCESS);
-
-    Node z =
-        nm->mkNode(kind::IMPLIES,
-                   nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
-                   nm->mkNode(kind::EQUAL, res, nm->mkConst(Rational(0U))));
-    handleLemma(z, InferenceId::FP_PREPROCESS);
-
-    // TODO : bounds on the output from largest floats, #1914
-  }
-  else if (node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL)
-  {
-    res = abstractRealToFloat(node);
-
-    // Generate some lemmas
-    NodeManager *nm = NodeManager::currentNM();
-
-    Node nnan =
-        nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, res));
-    handleLemma(nnan, InferenceId::FP_PREPROCESS);
-
-    Node z = nm->mkNode(
-        kind::IMPLIES,
-        nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))),
-        nm->mkNode(kind::EQUAL,
-                   res,
-                   nm->mkConst(FloatingPoint::makeZero(
-                       res.getType().getConst<FloatingPointSize>(), false))));
-    handleLemma(z, InferenceId::FP_PREPROCESS);
-
-    // TODO : rounding-mode specific bounds on floats that don't give infinity
-    // BEWARE of directed rounding!   #1914
-  }
 
   if (res != node)
   {
@@ -591,80 +476,132 @@ void TheoryFp::registerTerm(TNode node)
 {
   Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl;
 
-  if (!isRegistered(node))
+  if (isRegistered(node))
+  {
+    return;
+  }
+
+  Kind k = node.getKind();
+  Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC && k != kind::FLOATINGPOINT_SUB
+         && k != kind::FLOATINGPOINT_EQ && k != kind::FLOATINGPOINT_GEQ
+         && k != kind::FLOATINGPOINT_GT);
+
+  CVC5_UNUSED bool success = d_registeredTerms.insert(node);
+  Assert(success);
+
+  // Add to the equality engine
+  if (k == kind::EQUAL)
+  {
+    d_equalityEngine->addTriggerPredicate(node);
+  }
+  else
   {
-    Kind k = node.getKind();
-    Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC
-           && k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ
-           && k != kind::FLOATINGPOINT_GEQ && k != kind::FLOATINGPOINT_GT);
+    d_equalityEngine->addTerm(node);
+  }
 
-    bool success = d_registeredTerms.insert(node);
-    (void)success;  // Only used for assertion
-    Assert(success);
+  // Give the expansion of classifications in terms of equalities
+  // This should make equality reasoning slightly more powerful.
+  if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ)
+      || (k == kind::FLOATINGPOINT_ISINF))
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>();
+    Node equalityAlias = Node::null();
 
-    // Add to the equality engine
-    if (k == kind::EQUAL)
+    if (k == kind::FLOATINGPOINT_ISNAN)
     {
-      d_equalityEngine->addTriggerPredicate(node);
+      equalityAlias = nm->mkNode(
+          kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s)));
+    }
+    else if (k == kind::FLOATINGPOINT_ISZ)
+    {
+      equalityAlias = nm->mkNode(
+          kind::OR,
+          nm->mkNode(kind::EQUAL,
+                     node[0],
+                     nm->mkConst(FloatingPoint::makeZero(s, true))),
+          nm->mkNode(kind::EQUAL,
+                     node[0],
+                     nm->mkConst(FloatingPoint::makeZero(s, false))));
+    }
+    else if (k == kind::FLOATINGPOINT_ISINF)
+    {
+      equalityAlias =
+          nm->mkNode(kind::OR,
+                     nm->mkNode(kind::EQUAL,
+                                node[0],
+                                nm->mkConst(FloatingPoint::makeInf(s, true))),
+                     nm->mkNode(kind::EQUAL,
+                                node[0],
+                                nm->mkConst(FloatingPoint::makeInf(s, false))));
     }
     else
     {
-      d_equalityEngine->addTerm(node);
+      Unreachable() << "Only isNaN, isInf and isZero have aliases";
     }
 
-    // Give the expansion of classifications in terms of equalities
-    // This should make equality reasoning slightly more powerful.
-    if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ)
-        || (k == kind::FLOATINGPOINT_ISINF))
-    {
-      NodeManager *nm = NodeManager::currentNM();
-      FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>();
-      Node equalityAlias = Node::null();
+    handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias),
+                InferenceId::FP_REGISTER_TERM);
+  }
+  else if (k == kind::FLOATINGPOINT_TO_REAL_TOTAL)
+  {
+    // Purify (fp.to_real x)
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
+    Node sk = sm->mkPurifySkolem(node, "to_real", "fp purify skolem");
+    handleLemma(node.eqNode(sk), InferenceId::FP_REGISTER_TERM);
+    d_abstractionMap.insert(sk, node);
 
-      if (k == kind::FLOATINGPOINT_ISNAN)
-      {
-        equalityAlias = nm->mkNode(
-            kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s)));
-      }
-      else if (k == kind::FLOATINGPOINT_ISZ)
-      {
-        equalityAlias = nm->mkNode(
-            kind::OR,
-            nm->mkNode(kind::EQUAL,
-                       node[0],
-                       nm->mkConst(FloatingPoint::makeZero(s, true))),
-            nm->mkNode(kind::EQUAL,
-                       node[0],
-                       nm->mkConst(FloatingPoint::makeZero(s, false))));
-      }
-      else if (k == kind::FLOATINGPOINT_ISINF)
-      {
-        equalityAlias = nm->mkNode(
-            kind::OR,
-            nm->mkNode(kind::EQUAL,
-                       node[0],
-                       nm->mkConst(FloatingPoint::makeInf(s, true))),
-            nm->mkNode(kind::EQUAL,
-                       node[0],
-                       nm->mkConst(FloatingPoint::makeInf(s, false))));
-      }
-      else
-      {
-        Unreachable() << "Only isNaN, isInf and isZero have aliases";
-      }
+    Node pd =
+        nm->mkNode(kind::IMPLIES,
+                   nm->mkNode(kind::OR,
+                              nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]),
+                              nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])),
+                   nm->mkNode(kind::EQUAL, node, node[1]));
+    handleLemma(pd, InferenceId::FP_REGISTER_TERM);
 
-      handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias),
-                  InferenceId::FP_REGISTER_TERM);
-    }
+    Node z =
+        nm->mkNode(kind::IMPLIES,
+                   nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
+                   nm->mkNode(kind::EQUAL, node, nm->mkConst(Rational(0U))));
+    handleLemma(z, InferenceId::FP_REGISTER_TERM);
+    return;
 
-    /* When not word-blasting lazier, we word-blast every term on
-     * registration. */
-    if (!options().fp.fpLazyWb)
-    {
-      wordBlastAndEquateTerm(node);
-    }
+    // TODO : bounds on the output from largest floats, #1914
+  }
+  else if (k == kind::FLOATINGPOINT_TO_FP_REAL)
+  {
+    // Purify ((_ to_fp eb sb) rm x)
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
+    Node sk = sm->mkPurifySkolem(node, "to_real_fp", "fp purify skolem");
+    handleLemma(node.eqNode(sk), InferenceId::FP_REGISTER_TERM);
+    d_abstractionMap.insert(sk, node);
+
+    Node nnan =
+        nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node));
+    handleLemma(nnan, InferenceId::FP_REGISTER_TERM);
+
+    Node z = nm->mkNode(
+        kind::IMPLIES,
+        nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))),
+        nm->mkNode(kind::EQUAL,
+                   node,
+                   nm->mkConst(FloatingPoint::makeZero(
+                       node.getType().getConst<FloatingPointSize>(), false))));
+    handleLemma(z, InferenceId::FP_REGISTER_TERM);
+    return;
+
+    // TODO : rounding-mode specific bounds on floats that don't give infinity
+    // BEWARE of directed rounding!   #1914
+  }
+
+  /* When not word-blasting lazier, we word-blast every term on
+   * registration. */
+  if (!options().fp.fpLazyWb)
+  {
+    wordBlastAndEquateTerm(node);
   }
-  return;
 }
 
 bool TheoryFp::isRegistered(TNode node)
@@ -703,8 +640,6 @@ void TheoryFp::preRegisterTerm(TNode node)
 void TheoryFp::handleLemma(Node node, InferenceId id)
 {
   Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
-  // will be preprocessed when sent, which is important because it contains
-  // embedded ITEs
   if (rewrite(node) != d_true)
   {
     /* We only send non-trivial lemmas. */
@@ -737,17 +672,25 @@ void TheoryFp::postCheck(Effort level)
   /* Resolve the abstractions for the conversion lemmas */
   if (level == EFFORT_LAST_CALL)
   {
-    Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl;
+    Trace("fp-abstraction")
+        << "TheoryFp::check(): checking abstractions" << std::endl;
     TheoryModel* m = getValuation().getModel();
     bool lemmaAdded = false;
 
-    for (AbstractionMap::const_iterator i = d_abstractionMap.begin();
-         i != d_abstractionMap.end();
-         ++i)
+    for (const auto& [abstract, concrete] : d_abstractionMap)
     {
-      if (m->hasTerm((*i).first))
+      Trace("fp-abstraction")
+          << "TheoryFp::check(): Abstraction: " << abstract << std::endl;
+      if (m->hasTerm(abstract))
       {  // Is actually used in the model
-        lemmaAdded |= refineAbstraction(m, (*i).first, (*i).second);
+        Trace("fp-abstraction")
+            << "TheoryFp::check(): ... relevant" << std::endl;
+        lemmaAdded |= refineAbstraction(m, abstract, concrete);
+      }
+      else
+      {
+        Trace("fp-abstraction")
+            << "TheoryFp::check(): ... not relevant" << std::endl;
       }
     }
   }
@@ -846,40 +789,36 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
   }
 
   std::unordered_set<TNode> visited;
-  std::stack<TNode> working;
+  std::vector<TNode> working;
   std::set<TNode> relevantVariables;
-  for (std::set<Node>::const_iterator i(relevantTerms.begin());
-       i != relevantTerms.end(); ++i) {
-    working.push(*i);
+  for (const Node& n : relevantTerms)
+  {
+    working.emplace_back(n);
   }
 
   while (!working.empty()) {
-    TNode current = working.top();
-    working.pop();
-
-    // Ignore things that have already been explored
-    if (visited.find(current) == visited.end()) {
-      visited.insert(current);
+    TNode current = working.back();
+    working.pop_back();
 
-      TypeNode t(current.getType());
+    if (visited.find(current) != visited.end())
+    {
+      // Ignore things that have already been explored
+      continue;
+    }
+    visited.insert(current);
 
-      if ((t.isRoundingMode() || t.isFloatingPoint()) &&
-          this->isLeaf(current)) {
-        relevantVariables.insert(current);
-      }
+    TypeNode t = current.getType();
 
-      for (size_t i = 0; i < current.getNumChildren(); ++i) {
-        working.push(current[i]);
-      }
+    if ((t.isRoundingMode() || t.isFloatingPoint()) && this->isLeaf(current))
+    {
+      relevantVariables.insert(current);
     }
+
+    working.insert(working.end(), current.begin(), current.end());
   }
 
-  for (std::set<TNode>::const_iterator i(relevantVariables.begin());
-       i != relevantVariables.end();
-       ++i)
+  for (const TNode& node : relevantVariables)
   {
-    TNode node = *i;
-
     Trace("fp-collectModelInfo")
         << "TheoryFp::collectModelInfo(): relevantVariable " << node
         << std::endl;
@@ -889,6 +828,8 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
     // if FpWordBlaster::getValue() does not return a null node.
     if (!wordBlasted.isNull() && !m->assertEquality(node, wordBlasted, true))
     {
+      Trace("fp-collectModelInfo")
+          << "TheoryFp::collectModelInfo(): ... not converted" << std::endl;
       return false;
     }
 
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 9dd532a5d..807756c5b 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -141,12 +141,7 @@ class TheoryFp : public Theory
 
   bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
 
-  Node abstractRealToFloat(Node);
-  Node abstractFloatToReal(Node);
-
  private:
-  ConversionAbstractionMap d_realToFloatMap;
-  ConversionAbstractionMap d_floatToRealMap;
   AbstractionMap d_abstractionMap;  // abstract -> original
 
   /** The theory rewriter for this theory. */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 90ad99e70..301e26bf9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1595,6 +1595,7 @@ set(regress_1_tests
   regress1/decision/wishue160.smt2
   regress1/error.cvc
   regress1/errorcrash.smt2
+  regress1/fp/fp_to_real.smt2
   regress1/fp/rti_3_5_bug_report.smt2
   regress1/fmf-fun-dbu.smt2
   regress1/fmf/ALG008-1.smt2
@@ -2492,6 +2493,7 @@ set(regress_2_tests
   regress2/bv_to_int_mask_array_3.smt2
   regress2/bv_to_int_shifts.smt2
   regress2/error1.smtv1.smt2
+  regress2/fp/issue7056.smt2
   regress2/fuzz_2.smtv1.smt2
   regress2/hash_sat_06_19.smt2
   regress2/hash_sat_07_17.smt2
diff --git a/test/regress/regress1/fp/fp_to_real.smt2 b/test/regress/regress1/fp/fp_to_real.smt2
new file mode 100644
index 000000000..a24ae4cdc
--- /dev/null
+++ b/test/regress/regress1/fp/fp_to_real.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_FPLRA)
+(declare-const c1 Bool)
+(declare-const c2 Bool)
+(declare-const x Float32)
+(declare-const y Float32)
+(assert (= x ((_ to_fp 8 24) RNE (ite c1 4.0 2.0))))
+(assert (= y ((_ to_fp 8 24) RNE (ite c1 6.0 8.0))))
+(assert (= 2.0 (fp.to_real (ite c2 x y))))
+(set-info :status sat)
+(check-sat)
diff --git a/test/regress/regress2/fp/issue7056.smt2 b/test/regress/regress2/fp/issue7056.smt2
new file mode 100644
index 000000000..4defecd66
--- /dev/null
+++ b/test/regress/regress2/fp/issue7056.smt2
@@ -0,0 +1,26 @@
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
+(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
+
+(declare-sort t 0)
+(declare-const a t)
+(declare-fun first (t) Int)
+(declare-fun last (t) Int)
+(define-fun length ((b t)) Int (ite (<= (first b) (last b)) (+ (- (last b) (first b)) 1) 0))
+
+(define-fun contained ((x Float32)) Bool (and
+  (fp.leq x (fp #b0 #b01111111 #b00000000000000000000000))
+  (fp.leq (fp #b0 #b00000000 #b00000000000000000000000) x)))
+
+
+(declare-const i Int)
+(declare-const x Float32)
+(assert (and (<= (length a) 1000) (< 0 (length a))))
+(assert (= i (first a)))
+(assert (contained x))
+(assert (not (fp.isFinite32 (fp.mul RNE (fp.mul RNE (fp #b0 #b10010010 #b11101000010010000000000) ((_ to_fp 8 24) RNE (to_real (length a))))
+                                        x))))
+(set-info :status unsat)
+(check-sat)