FP: Fix wrong model due to partial assignment (#2910)

For a simple query `(not (= (fp.isSubnormal x) false))`, we were getting
a wrong model. The issue was that `(sign x)` was not assigned a value
and did not appear in the shared terms. In
`TheoryFp::collectModelInfo()`, however, we generate an expression that
connects the components of `x` to `x`, which contains `(sign x)`. As a
result, the normalization while building a model did not result in a
constant. This commit fixes the issue by marking `(sign x)` (and
`(significand x)`) as assignable. Assignable terms can take any value
while building a model if there is no existing value.

1 files changed, 35 insertions, 0 deletions

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 627b87ba7..4652f62d1 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -1084,6 +1084,41 @@ bool TheoryFp::collectModelInfo(TheoryModel *m)
     {
       return false;
     }
+
+    if (Configuration::isAssertionBuild() && isLeaf(node) && !node.isConst()
+        && node.getType().isFloatingPoint())
+    {
+      // Check that the equality engine has asssigned values to all the
+      // components of `node` except `(sign node)` (the sign component is
+      // assignable, meaning that the model builder can pick an arbitrary value
+      // for it if it hasn't been assigned in the equality engine).
+      NodeManager* nm = NodeManager::currentNM();
+      Node compNaN = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, node);
+      Node compInf = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, node);
+      Node compZero = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, node);
+      Node compExponent =
+          nm->mkNode(kind::FLOATINGPOINT_COMPONENT_EXPONENT, node);
+      Node compSignificand =
+          nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, node);
+
+      eq::EqualityEngine* ee = m->getEqualityEngine();
+      Assert(ee->hasTerm(compNaN) && ee->getRepresentative(compNaN).isConst());
+      Assert(ee->hasTerm(compInf) && ee->getRepresentative(compInf).isConst());
+      Assert(ee->hasTerm(compZero)
+             && ee->getRepresentative(compZero).isConst());
+      Assert(ee->hasTerm(compExponent)
+             && ee->getRepresentative(compExponent).isConst());
+      Assert(ee->hasTerm(compSignificand));
+      Assert(ee->getRepresentative(compSignificand).isConst());
+
+      // At most one of the flags (NaN, inf, zero) can be set
+      Node one = nm->mkConst(BitVector(1U, 1U));
+      size_t numFlags = 0;
+      numFlags += ee->getRepresentative(compNaN) == one ? 1 : 0;
+      numFlags += ee->getRepresentative(compInf) == one ? 1 : 0;
+      numFlags += ee->getRepresentative(compZero) == one ? 1 : 0;
+      Assert(numFlags <= 1);
+    }
   }
 
   return true;