Bug when using FBA and treating RoundingMode as a variable

Jul 25, 2014 at 9:02 PM
Edited Jul 25, 2014 at 9:03 PM
http://rise4fun.com/Z3/ayWHD
  • This should result in unsat as there are only 5 rounding modes and I have excluded all of them
  • The model formatting isn't nice
I understand the FPA theory is not completed. Just wanted to make sure you are aware of these issues.

Here's another problem: http://rise4fun.com/Z3/brgj

First of all, this should return unsat because of the rounding mode issue I mentioned above. But even disregarding that - the rest of the formula should be unsat as well. It becomes unsat if you manually replace "rm" by any of the specific rounding modes.

http://rise4fun.com/Z3/ytKAA

Restricting rm to one of the 5 possible values correctly returns unsat. But leaving just one value for rm is invalidly sat: http://rise4fun.com/Z3/jCA3

I hope those are some useful test cases for you.

(I was trying to prove that x - x == 0 which is a true statement.)

What is the plan for the FPA theory? When can we expect it to appear in the .NET API of the unstable builds? It's nice.
Coordinator
Jul 28, 2014 at 7:46 PM
Thanks for reporting this issue! Indeed, there were a couple of branches for numerals with unspecified rounding mode in the code that weren't implemented yet. Those are now implemented (as of this commit) and everything should work as expected.

Yes, there are plans for FPA to be integrated in all the APIs (there is a branch called fpa-api in which we have started implementing this).

For your third testcase (http://rise4fun.com/Z3/ytKAA) Z3 says sat, with a model of x = +0.0 and r = -0.0 which I think is correct. Did you intend to use '==' instead if '='? Changing the last line to
(not (== r ((_ asFloat 11 53) rm 0.0 0)))
indeed makes the formula unsat.
Jul 28, 2014 at 10:44 PM
I believe you are right regarding the 3rd test case. Could you let me know when the online Z3 is updated so that I can run through a few tests?

Are you interested in failing tests and bug reports for the FPA theory in general?

Are you aware, that quantifiers are not working with FPA yet?
Coordinator
Jul 29, 2014 at 6:31 PM
It might take a while until the binaries on rise4fun are updated, but the nightly unstable binaries already contain these fixes.

Of course, we are interested in all kinds of benchmarks/tests/problems!

Regarding floating-point numbers we currently only support the QF_FPA and QF_FPABV logics, no other combinations yet. I'm working on an actual theory that translates on demand in the fpa-api branch, but that's not finished yet, so it's quite possible that it doesn't work with quantifiers yet. I'm not so optimistic about solving the resulting QBFs though, those would be very hard problems.
Coordinator
Aug 21, 2014 at 3:05 PM
The binaries on rise4fun have been updated and they produce the expected results. The model formatting is not finished yet, as I haven't decided what the final format will be. However, I am thinking about just making that into hex numbers like for bit-vectors. At the moment, models may also contain some of the intermediate variables that were introduced during the solving process (named k!<nr>), these should be ignored.