MathSAT5 with FP does not parse PI again

[kfriedberger]

The last column of our Buildbot table contains several exceptions from MathSAT5, where PI is already declared (standard symbol in FP theory?) and parsed again from SMTLIB. If this is a bug in the parser, we need to report to Alberto.

TODO: Get a minimal working example in JavaSMT (or even directly in C).

[baierd]

Declaring "pi" as a variable always directly results in this exception. The variable "pi" is a pre-declared constant according to Alberto and we have to work around it. The type of "pi" is Real and not FP (I tested).

I don't think that we can do much here besides not using the name.

[kfriedberger]

Then we need to either exclude this symol from being defined in the SMTLIB header or ask MathSAT to not export this symbol. Could you take a look, if other symbols make such problems as well or how they are handled? I assume that special tokens like true,false,select,store are not exported by MathSAT5. If that is correct, I will ask Alberto for also exluding pi.

[baierd]

true and false is fine. select, store as well as +, -, and, or, not etc. are built-in functions and you get an exception when declaring something with those names (So same issue as with pi). I assume all functions/constants (numerals) that are predefined are like this.

[kfriedberger]

Where does this need to be fixed? If MathSAT dumps pi in SMTLIB, that might be the bug. Does MathSAT dump other functions (except pi) in SMTLIB? I think not.

[baierd]

Communication hickup on my side. Declaring functions with those names is not possible with declare-fun. (As it should be?) define-fun works with all of them except pi. Thats probably what you meant.

[kfriedberger]

Yes, then it looks like a missing case in the parser of MathSAT5. Can you provide SMTLIB input for a crashing example with pi?

[baierd]

(define-fun pi () Int) parsed is enough for a crash.

[kfriedberger]

oh, I did not think of that simple query. thanks.

[kfriedberger]

Actually, the behaviour of MathSAT is correct: the symbol is defined and never actively printed. The reported issue is already discussed in CPAchecker, where symbols are not properly escaped.

This issue can not be fixed in JavaSMT or the underlying solver.

[kfriedberger]

Further investigation required: Why does MathSAT fail for the commandline in the Buildbot table mentioned above? There is no pi in the parser query, but only true. CPAchecker uses only one single solver instance and translates the query true from itself towards itself.

The bug in CPAchecker was avoided by commit CPA#r35353. The bug was additionally (redundantly) avoided by commit e9f13353746cc47746e507d4f5d00ae09eb30e98 in JavaSMT. However, none of these commits solves the underlying problem.

[baierd]

Is this issue still relevant? You mentioned yesterday that you fixed this in CPAchecker.

[kfriedberger]

Yes, still relevant, but minor priority. because there is a bug, it is just hidden.

[baierd]

All the failed tasks fail in the same way when parsed by Mathsat itself:

(error "unknown symbol: FP_AS_IEEEBV (line: 449)") // With line: xyz being an example

FP_AS_IEEEBV is not declared before being used. Naturally is fails and from that point onwards all other declarations. I can not reproduce a failure based on pi, just this. (Example: (define-fun .268 () (_ BitVec 64) (FP_AS_IEEEBV .216)))

[kfriedberger]

Is FP_AS_IEEEBV deifned in the SMTLIB standard or is it optional? Can you provide a minimal SMTLIB query for using this? Does the latest nightly build (from website) of MathSAT5 suceed with parsing this? If MathSAT5 can not parse it, we need to report this to Alberto.

[baierd]

FP_AS_IEEEBV is not defined in SMTLIB2 but i can find sources that say that Mathsat5 does offer the functionality (and it does so in the regular API) but i can not verify this from an source directly form the Mathsat devs or in any way for parsing.

Nightly build fails as well as older builds.

I do not know if that helps, but the SMTLIB2 standard recommends another way of converting FP to BV:

 There is no function for converting from (_ FloatingPoint eb sb) to the
  corresponding IEEE 754-2008 binary format, as a bit vector (_ BitVec m) with 
  m = eb + sb, because (_ NaN eb sb) has multiple, well-defined representations.
  Instead, an encoding of the kind below is recommended, where f is a term
  of sort (_ FloatingPoint eb sb):

   (declare-fun b () (_ BitVec m))
   (assert (= ((_ to_fp eb sb) b) f)) 

Example SMT2 program: (Parse with Mathsat via commandline i.e.: ./mathsat-5.6.3 -input=smt2 < mathsat_minimal_fp_as_ieeebv.smt2)

;; This illustrades a problem with FP_AS_IEEEBV in Mathsat5

(set-option :global-declarations true)
(set-option :config "model_generation=true")

(declare-fun fpn () (_ FloatingPoint 8 24))
(define-fun .1 () (_ FloatingPoint 8 24) fpn)
(define-fun .2 () (_ BitVec 32) (FP_AS_IEEEBV .1))

(assert .2)
(check-sat)

[kfriedberger]

Thanks for the example and explanation. The NaN problem is known, but is certainly irrelevant for CPAchecker's usage. Can you report to Alberto, that MathSAT writes something like SMTLIB (using FP_AS_IEEEBV), but can not parse it afterwards? It should be simple for him to fix the parser.

[baierd]

Sure can do. I'll add you in CC.

[baierd]

Mathsat5 version 5.6.4 is released and Alberto added the function fp.as_ieee_bv for us right away. I tested the function in smtlib2 and it works as expected.

[kfriedberger]

Have seen it. I will update the library in the ivy repository soon.

[kfriedberger]

Just for clarification:

• the exported/dumped name is now fp.as_ieee_bv?
• the parser does understand fp.as_ieee_bv?

[baierd]

Yes.