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.

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 627b87ba7e0a5f6a2ecceaeb702d888e8c86915b..4652f62d1cb425948ac7f410ddd296720bb9b1be 100644 (file)
--- 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;

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 77cdfb79be95dbf8c9a759ea210c3b6e76c5eb79..102979056df9cc27c4ddbad2fc104fbd402f4e5e 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -47,6 +47,14 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n)
       return !n.getType().isFunction();
     }
   }
+  else if (n.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGN)
+  {
+    // Extracting the sign of a floating-point number acts similar to a
+    // selector on a datatype, i.e. if `(sign x)` wasn't assigned a value, we
+    // can pick an arbitrary one. Note that the other components of a
+    // floating-point number should always be assigned a value.
+    return true;
+  }
   else
   {
     // non-function variables, and fully applied functions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c6ccab4643d2b96427b39fc2545904803410b7a2..13d1540f66b65ce191b0fbaac47e12422152cd62 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -451,6 +451,7 @@ set(regress_0_tests
   regress0/fp/abs-unsound2.smt2
   regress0/fp/ext-rew-test.smt2
   regress0/fp/simple.smt2
+  regress0/fp/wrong-model.smt2
   regress0/fuzz_1.smt
   regress0/fuzz_3.smt
   regress0/get-value-incremental.smt2

diff --git a/test/regress/regress0/fp/wrong-model.smt2 b/test/regress/regress0/fp/wrong-model.smt2
new file mode 100644 (file)
index 0000000..4bb7645
--- /dev/null
+++ b/test/regress/regress0/fp/wrong-model.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: symfpu
+; EXPECT: sat
+
+; NOTE: the (set-logic ALL) is on purpose because the problem was not triggered
+; with QF_FP.
+(set-logic ALL)
+(declare-const r RoundingMode) 
+(declare-const x (_ FloatingPoint 5 11))
+(declare-const y (_ FloatingPoint 5 11))
+(assert (not (= (fp.isSubnormal x) false)))
+(check-sat)