4 files changed, 74 insertions, 28 deletions

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index e309ab2e4..f6f1f3bb3 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -1296,15 +1296,18 @@ Node FpConverter::getValue(Valuation &val, TNode var)
   if (t.isRoundingMode())
   {
     rmMap::const_iterator i(d_rmMap.find(var));
-
-    Assert(i != d_rmMap.end())
-        << "Asking for the value of an unregistered expression";
+    if (i == d_rmMap.end())
+    {
+      return Node::null();
+    }
     return rmToNode((*i).second);
   }
-  fpMap::const_iterator i(d_fpMap.find(var));
 
-  Assert(i != d_fpMap.end())
-      << "Asking for the value of an unregistered expression";
+  fpMap::const_iterator i(d_fpMap.find(var));
+  if (i == d_fpMap.end())
+  {
+    return Node::null();
+  }
   return ufToNode(fpt(t), (*i).second);
 }
 
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 9900c2987..d589eff60 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -300,7 +300,10 @@ class FpConverter
   /** Adds a node to the conversion, returns the converted node */
   Node convert(TNode);
 
-  /** Gives the node representing the value of a given variable */
+  /**
+   * Gives the node representing the value of a word-blasted variable.
+   * Returns a null node if it has not been word-blasted.
+   */
   Node getValue(Valuation&, TNode);
 
   context::CDList<Node> d_additionalAssertions;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 1c8f10f77..9b5ac66d3 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -76,12 +76,13 @@ TheoryFp::TheoryFp(context::Context* c,
       d_abstractionMap(u),
       d_rewriter(u),
       d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::fp::", false)
+      d_im(*this, d_state, pnm, "theory::fp::", false),
+      d_wbFactsCache(u)
 {
   // indicate we are using the default theory state and inference manager
   d_theoryState = &d_state;
   d_inferManager = &d_im;
-} /* TheoryFp::TheoryFp() */
+}
 
 TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
 
@@ -304,6 +305,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
     Node floatValue = m->getValue(concrete[0]);
     Node undefValue = m->getValue(concrete[1]);
 
+    Assert(!abstractValue.isNull());
+    Assert(!floatValue.isNull());
+    Assert(!undefValue.isNull());
     Assert(abstractValue.isConst());
     Assert(floatValue.isConst());
     Assert(undefValue.isConst());
@@ -413,6 +417,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
     Node rmValue = m->getValue(concrete[0]);
     Node realValue = m->getValue(concrete[1]);
 
+    Assert(!abstractValue.isNull());
+    Assert(!rmValue.isNull());
+    Assert(!realValue.isNull());
     Assert(abstractValue.isConst());
     Assert(rmValue.isConst());
     Assert(realValue.isConst());
@@ -509,12 +516,16 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
   return false;
 }
 
-void TheoryFp::convertAndEquateTerm(TNode node) {
+void TheoryFp::convertAndEquateTerm(TNode node)
+{
   Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
-  size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size();
+
+  size_t oldSize = d_conv->d_additionalAssertions.size();
 
   Node converted(d_conv->convert(node));
 
+  size_t newSize = d_conv->d_additionalAssertions.size();
+
   if (converted != node) {
     Debug("fp-convertTerm")
         << "TheoryFp::convertTerm(): before " << node << std::endl;
@@ -522,12 +533,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
         << "TheoryFp::convertTerm(): after  " << converted << std::endl;
   }
 
-  size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size();
-  Assert(oldAdditionalAssertions <= newAdditionalAssertions);
+  Assert(oldSize <= newSize);
 
-  while (oldAdditionalAssertions < newAdditionalAssertions)
+  while (oldSize < newSize)
   {
-    Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions];
+    Node addA = d_conv->d_additionalAssertions[oldSize];
 
     Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion  "
                             << addA << std::endl;
@@ -538,7 +548,7 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
         nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U))),
         InferenceId::FP_EQUATE_TERM);
 
-    ++oldAdditionalAssertions;
+    ++oldSize;
   }
 
   // Equate the floating-point atom and the converted one.
@@ -578,10 +588,12 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
   return;
 }
 
-void TheoryFp::registerTerm(TNode node) {
+void TheoryFp::registerTerm(TNode node)
+{
   Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl;
 
-  if (!isRegistered(node)) {
+  if (!isRegistered(node))
+  {
     Kind k = node.getKind();
     Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC
            && k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ
@@ -646,14 +658,19 @@ void TheoryFp::registerTerm(TNode node) {
                   InferenceId::FP_REGISTER_TERM);
     }
 
-    // Use symfpu to produce an equivalent bit-vector statement
-    convertAndEquateTerm(node);
+    /* When not word-blasting lazier, we word-blast every term on
+     * registration. */
+    if (!options::fpLazyWb())
+    {
+      convertAndEquateTerm(node);
+    }
   }
   return;
 }
 
-bool TheoryFp::isRegistered(TNode node) {
-  return !(d_registeredTerms.find(node) == d_registeredTerms.end());
+bool TheoryFp::isRegistered(TNode node)
+{
+  return d_registeredTerms.find(node) != d_registeredTerms.end();
 }
 
 void TheoryFp::preRegisterTerm(TNode node)
@@ -714,7 +731,7 @@ bool TheoryFp::needsCheckLastEffort()
 
 void TheoryFp::postCheck(Effort level)
 {
-  // Resolve the abstractions for the conversion lemmas
+  /* Resolve the abstractions for the conversion lemmas */
   if (level == EFFORT_LAST_CALL)
   {
     Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl;
@@ -739,6 +756,13 @@ void TheoryFp::postCheck(Effort level)
 bool TheoryFp::preNotifyFact(
     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 {
+  /* Word-blast lazier if configured. */
+  if (options::fpLazyWb() && d_wbFactsCache.find(atom) == d_wbFactsCache.end())
+  {
+    d_wbFactsCache.insert(atom);
+    convertAndEquateTerm(atom);
+  }
+
   if (atom.getKind() == kind::EQUAL)
   {
     Assert(!(atom[0].getType().isFloatingPoint()
@@ -763,6 +787,16 @@ bool TheoryFp::preNotifyFact(
   return false;
 }
 
+void TheoryFp::notifySharedTerm(TNode n)
+{
+  /* Word-blast lazier if configured. */
+  if (options::fpLazyWb() && d_wbFactsCache.find(n) == d_wbFactsCache.end())
+  {
+    d_wbFactsCache.insert(n);
+    convertAndEquateTerm(n);
+  }
+}
+
 TrustNode TheoryFp::explain(TNode n)
 {
   Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl;
@@ -846,7 +880,10 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
         << "TheoryFp::collectModelInfo(): relevantVariable " << node
         << std::endl;
 
-    if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true))
+    Node converted = d_conv->getValue(d_valuation, node);
+    // We only assign the value if the FpConverter actually has one, that is,
+    // if FpConverter::getValue() does not return a null node.
+    if (!converted.isNull() && !m->assertEquality(node, converted, true))
     {
       return false;
     }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index ada9b39d0..14779cc3d 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -114,6 +114,8 @@ class TheoryFp : public Theory
   };
   friend NotifyClass;
 
+  void notifySharedTerm(TNode n) override;
+
   NotifyClass d_notification;
 
   /** General utility. */
@@ -148,18 +150,19 @@ class TheoryFp : public Theory
   Node abstractFloatToReal(Node);
 
  private:
-
   ConversionAbstractionMap d_realToFloatMap;
   ConversionAbstractionMap d_floatToRealMap;
   AbstractionMap d_abstractionMap;  // abstract -> original
 
   /** The theory rewriter for this theory. */
   TheoryFpRewriter d_rewriter;
-  /** A (default) theory state object */
+  /** A (default) theory state object. */
   TheoryState d_state;
-  /** A (default) inference manager */
+  /** A (default) inference manager. */
   TheoryInferenceManager d_im;
-}; /* class TheoryFp */
+  /** Cache of word-blasted facts. */
+  context::CDHashSet<Node> d_wbFactsCache;
+};
 
 }  // namespace fp
 }  // namespace theory