FP: Add option to word-blast more lazily. (#6904)

When enabled, this does not word-blast when registering term but at preNotifyFact (= more lazily) instead.
This is enabled via option --fp-lazy-wb.

8 files changed, 99 insertions, 29 deletions

diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml
index 6fd632a7c..be40b49e2 100644
--- a/src/options/fp_options.toml
+++ b/src/options/fp_options.toml
@@ -8,3 +8,11 @@ name   = "Floating-Point"
   type       = "bool"
   default    = "false"
   help       = "Allow floating-point sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental)"
+
+[[option]]
+  name       = "fpLazyWb"
+  category   = "experimental"
+  long       = "fp-lazy-wb"
+  type       = "bool"
+  default    = "false"
+  help       = "Enable lazier word-blasting (on preNotifyFact instead of registerTerm)"
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 87f3f25cd..8dee3c2c4 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -120,7 +120,7 @@ class BVSolverBitblast : public BVSolver
   /**
    * Bit-blast queue for facts sent to this solver.
    *
-   * Get populated on preNotifyFact().
+   * Gets populated on preNotifyFact().
    */
   context::CDQueue<Node> d_bbFacts;
 
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
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6ebb91f9e..22a222369 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -604,6 +604,7 @@ set(regress_0_tests
   regress0/fp/issue6164.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2
+  regress0/fp/word-blast.smt2
   regress0/fp/wrong-model.smt2
   regress0/fuzz_1.smtv1.smt2
   regress0/fuzz_3.smtv1.smt2
diff --git a/test/regress/regress0/fp/word-blast.smt2 b/test/regress/regress0/fp/word-blast.smt2
new file mode 100644
index 000000000..65290a3b3
--- /dev/null
+++ b/test/regress/regress0/fp/word-blast.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --fp-lazy-wb
+; EXPECT: unsat
+(set-logic QF_BVFP)
+(declare-fun meters_ackermann!0 () (_ BitVec 64))
+(assert
+ (let ((?x8 ((_ to_fp 11 53) meters_ackermann!0)))
+ (fp.geq ?x8 ((_ to_fp 11 53) (_ bv0 64)))))
+(assert
+ (let ((?x8 ((_ to_fp 11 53) meters_ackermann!0)))
+ (fp.leq ?x8 ((_ to_fp 11 53) (_ bv4652007308841189376 64)))))
+(assert
+ (let ((?x19 ((_ sign_extend 32) ((_ fp.to_sbv 32) roundTowardZero (fp.abs ((_ to_fp 11 53) meters_ackermann!0))))))
+(not (not (bvult (_ bv9223372036854775807 64) ?x19)))))
+(check-sat)
+(exit)