Issue while creating model from scratch

[m-carrasco]

Hi,

I'm trying to create a Z3::model given a set of equalities (variable == constant) that satisfy a formula. This doesn't always work, and I'm unsure if this is a bug or if I'm incorrectly using the API (4.12.4).

My first attempt was to assert the set of equalities in a z3::solver and generate a model (s.check(); s.get_model();). This approach always works without issues.

My second attempt aimed to make things faster by creating the model using the z3::model API without calling the solver. This approach fails in the following case, and I'm trying to figure out why.

The steps to reproduce the issue are:

1. g++ main.cpp -lz3
2. ./a.out formula.smt2 model.smt2

The steps above show how to reproduce the issue with the second approach (construct_model_fast). The formula is not evaluated as True by the model. Instead, it returns:

(let ((a!1 (fp.mul roundNearestTiesToEven
                   (fp.mul roundNearestTiesToEven
                           (fp.mul roundNearestTiesToEven
                                   (fp #b0 #b10000000000 #x8000000000000)
                                   (fp #b0 #b01010111111 #xfffffffff89ff))
                           (_ NaN 11 53))
                   (_ NaN 11 53))))
(let ((a!2 (fp.mul roundNearestTiesToEven
                   (fp.mul roundNearestTiesToEven
                           (fp.mul roundNearestTiesToEven
                                   (fp #b0 #b01010111111 #xfffffffff89ff)
                                   (_ NaN 11 53))
                           (_ NaN 11 53))
                   (fp.add roundNearestTiesToEven
                           (fp #b1 #b10000000010 #x4000000000000)
                           a!1))))
(let ((a!3 (= (_ NaN 11 53)
              (fp.div roundNearestTiesToEven
                      (fp.mul roundNearestTiesToEven
                              (_ NaN 11 53)
                              (fp.add roundNearestTiesToEven
                                      (fp #b0 #b10000000010 #xe000000000000)
                                      a!2))
                      (fp #b0 #b10000000010 #x0000000000000)))))
  (and a!3
       (= (_ NaN 11 53)
          (fp.mul roundNearestTiesToEven
                  (fp #b0 #b00000000000 #xc000000000009)
                  (_ NaN 11 53)))))))

However, if construct_model_slow is used, the model correctly evaluates the formula as True.

Best,
Manuel.

[wintersteiger]

This looks as if the FP simplifier doesn't always propagate NaNs through fp.mul/fp.div, i.e. this is a bug.

[NikolajBjorner]

I can see the place in ast\rewriter\fpa_rewriter.cpp that would be relevant, but will have to look up semantics. AI tells me that NaN x 1.5 = NaN, or in other words, the result of multiplication or any other arithmetical operation with NaN is always a NaN. There are also cases for +infinity/-infinity. Could they be simplified?

[wintersteiger]

Yes, NaNs propagate; if one of the inputs is a NaN, then so is the output. This is not the case for infinities though. At first glance, it looks like the rewriter only rewrites if all of the inputs are numerals, but for NaNs we can do better, because we know the result won't depend on the rounding mode or the other input(s) (but infinities do need to be rounded).

In the example provided here, they all are numerals though, so I don't know what else is going wrong there. Maybe the model evaluator doesn't call the FP rewriter at all?!

[NikolajBjorner]

Actually, m_util.is_numeral covers also NaN. If I simplify the snippet directly it reduces to true.
So a repro requires running the code.

[NikolajBjorner]

Alright, it isn't a bug with fps.

Model evaluation does not necessarily apply simplification. But you can add it:

auto val = m.eval(constraint);        

std::cout << "Evaluation: " << val << std::endl;
std::cout << "Evaluation simplified: " << val.simplify() << std::endl;

This suggests you can update the application to ensure full normalization.

Not sure if "fixing" this within z3 is necessary or even well-advised.

[wintersteiger]

Thanks for chasing this down! I also assumed that the model evaluator would always simplify all the way, but you're probably right that it isn't always necessary.

[NikolajBjorner]

Digging further: the model.smt2 uses terms of the form (fp ...). These rewrite to fp numerals, but are skipped during model evaluation. Therefore fp.mul etc fail to rewrite them directly.

[NikolajBjorner]

One of potential takeaways is that it will be possible to rewrite (fp.mul rm NaN x) to NaN no matter what rm and x.
It is possibly more fun and ultimately productive to "mine and synthesize" for missing rewrite opportunities using a combination of delta-debugging, fuzzing and learning than a manual review. Enumerate potential redexes and compare result of simplification with result of check-sat:

(declare-fun x () (_ FloatingPoint 11 53))

(simplify
(fp.mul roundNearestTiesToEven x (_ NaN 11 53)))

(assert (not (= (fp.mul roundNearestTiesToEven x (_ NaN 11 53)) (_ NaN 11 53))))
(check-sat)

[m-carrasco]

Thank you both for fixing this issue! @NikolajBjorner @wintersteiger

I'll be testing it on a wider set of formulas.