Quantified FPA formula incorrectly marked as SAT

[nunoplopes]

See this:

(declare-fun %fb () (_ FloatingPoint 8 24))

(assert
  (forall ((undef_1 (_ FloatingPoint 8 24))
           (undef_3 (_ FloatingPoint 8 24)))
    (let ((a!1 (bvnot (bvor
                        (bvnot ((_ fp.to_sbv 32) roundNearestTiesToEven %fb))
                        ((_ fp.to_sbv 32) roundNearestTiesToEven undef_3))))
          (a!2 (bvnot (bvor
                        (bvnot ((_ fp.to_sbv 32) roundNearestTiesToEven undef_1))
                        ((_ fp.to_sbv 32) roundNearestTiesToEven %fb)))))

          (not (= (bvnot (bvor a!1 a!2))
                  (bvxor #xffffffff
                         #x00000000
                         ((_ fp.to_sbv 32) roundNearestTiesToEven %fb)))))))

(check-sat)
(get-model)

; this is the model of %fb
(assert (= %fb (fp #b0 #x81 #b00101000000010001001000)))
(check-sat)

Prints:

sat
(model
  (define-fun %fb () (_ FloatingPoint 8 24)
    (fp #b0 #x81 #b00101000000010001001000))
)
unsat

The first check gives sat, while the second gives unsat. The value assertedfor %fb is its model, which shouldn't change the satisfiability of the formula.

[nunoplopes]

@NikolajBjorner Christoph found out that just changing the seed makes the first query flip from sat (smt.random_seed=2) to unsat (smt.random_seed=1).
Also, using "(check-sat-using (then fpa2bv ufbv))" always gives unsat regardless of seed. Could it be a bug in the smt_context?

[NikolajBjorner]

bv2fpa_converter inserts an interpretation for fp.to_sbv. Under that interpretation, the negation of the formula under the quantifier becomes unsat in the current model.
Then it determines that the quantified formula is satisfiable.
@wintersteiger: consider line 467 in bv2fpa_converter.cpp for the purpose of model-based quantifier instantiation. Is it sound to fix an arbitrary interpretation for fp.to_sbv?

[wintersteiger]

No, it probably isn't, thanks for the pointer!

[NikolajBjorner]

@wintersteiger: it would be good to address this.
I see that fpa2bv_converter inserts an uninterpreted function and this gets passed to the bv2fpa_converter.

1. If the original fpa function is fully interpreted we should just be able to skip its inclusion in the model.
2. If the original fpa function is not fully interpreted, one option is to operate with three incarnations of the function: (1) the original, (2) the fully interpreted version, assuming adequate pre-conditions hold on the arguments, (3) the uninterpreted version. This requires of course additional copies of the decl_kinds. Painful, but systematic. The original function maps into an if-then-else to filter pre-conditions for interpreted case and uninterpreted case.

The "to_ieee" function seems to be internal, not part of the smtlib2 formalism on
http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml, or at least I could not spot it there.

The to_sbv function is said to be under-specified among certain arguments in the notes

   "fp.to_* functions are unspecified for NaN and infinity input values.
      In addition, fp.to_ubv and fp.to_sbv are unspecified for finite number inputs
      that are out of range (which includes all negative numbers for fp.to_ubv).

Thus, it may be required to do something along option 2.
The implementation uses dynamically generated uninterpreted functions, so it isn't necessary to enrich the signature with uninterpreted versions of these functions, but for model building to make sense we should map fp.to_sbv to an adequate ite, it seems.
Having two copes for
OP_FPA_TO_FP,
OP_FPA_TO_FP_UNSIGNED,
OP_FPA_TO_UBV,
OP_FPA_TO_SBV,
OP_FPA_TO_REAL,

introduces 5 new operators with identical rewriting and bit-blasting
behavior as their original counter-parts.
What are the cases where this kind of underspecification applies and,
the most useful question, could you make this surgery as you know how to navigate the semantics?

[NikolajBjorner]

ref ce06cd0

[NikolajBjorner]

alas, a simpler solution seems available: pass in the expression built around the uninterpreted function to the model converter, use this for defining the original function and also include the uninterpreted helper function.

[nunoplopes]

FWIW, my understanding of "to_ieee" is that it returns the internal BV representation as-is. This is so that we can have the round-trip of a float->BV->float to be a no-op. None of the other functions allows this.
So this "to_ieee" should be the easiest to fix hopefully. (btw the rewriter doesn't seem to fold these round-trips though)

[NikolajBjorner]

Even the simpler fix requires some extensive work. The function to_fp functions assume that its arguments are of a special form, something like (fp.to_sbv (rm xx) (fp sgn exp sig)).
The functions rm and fp seem not to have inverses (yet). If they had inverse functions, then we could access the values of xx, sgn, exp and sig when passing arbitrary two arguments, including variables.
I have outlined a way to create a generic unfolding for the fp.to_.. functions, but it cannot be completed without a way of dealing with the nested arguments. I presume fp function is a bijection so we could define projection functions. Perhaps using partial inverses for fp.bv2rm is fine as long as the model construction guarantees that the arguments to fp.to_sbv are in the right form.
@wintersteiger, could you take a look at either take over or comment?

[wintersteiger]

Yes, I'll fix this, but I have zero time at the moment, so this will take a while.

to_ieee is a Z3-only function with no guarantees whatsoever. to_sbv and many others are unspecified for some inputs, so the "else" case in the models should not be added in the context of MBQI (is model completion on during that step?). The fpa2bv conversion assumes that all arguments of a function are already translated to bit-vectors, usually in the form of three bit-vectors and often a rounding mode too.

The initial idea for quantified formulas was to just translate all (quantified) floats to (quantified) bit-vectors and then run the smt tactic, but later I added a proper FP theory which does the conversion when things become relevant and I never properly tested that in the presence of quantifiers.

[NikolajBjorner]

This query is UNSAT with E-matching (correct) and SAT with MBQI (wrong):

(declare-fun undef_2 () (_ FloatingPoint 8 24))
(declare-fun blks_val () (Array (_ BitVec 80) (_ BitVec 85)))
(assert (forall ((undef_1 (_ FloatingPoint 8 24)))
             (let ((a!1 (forall ((|#idx0| (_ BitVec 80)))
                          (= ((_ extract 84 84) (select blks_val |#idx0|)) #b0)))
                   (a!2 (fp.to_ieee_bv (fp.neg ((_ to_fp 8 24) (fp.to_ieee_bv undef_1)))))
                   (a!3 (fp.to_ieee_bv (fp.neg ((_ to_fp 8 24) (fp.to_ieee_bv undef_2))))))
             (let ((a!4 (not (= ((_ to_fp 8 24) a!3) ((_ to_fp 8 24) a!2)))))
               (and a!1 a!4)))))

(check-sat)

Output:

$ z3 bug.smt2
unsat
$ z3 smt.ematching=false bug.smt2
sat

[wintersteiger]

@NikolajBjorner: fp is not a bijection (multiple representations of NaN) and neither is bv2rm (unspecified cases). What's the purpose of inverses? The reverse translation from bit-vectors back to floats is in bv2fp_converter, which is used in the fpa2bv_model_converter and I don't think we need more than that, do we?

[wintersteiger]

Aside: I don't seem to be able to disable MBQI, e.g. with

(set-option :smt.ematching false)
(set-option :smt.mbqi true)

it still runs it instead of returning unknown.

[NikolajBjorner]

also need to disable smt.auto_config to disable mbqi.

[NikolajBjorner]

What's the purpose of inverses?

Only an indirect purpose: we can define functions f(x,y) when the arguments are variables,
but not f(rm(z), fp(u,v,w)). The auxiliary fresh functions that are introduced work when the arguments have this special form. If rm and fp are not surjective, then it can be ambiguous what is z, u, v, w if f can only be defined in terms of 'x' and 'y'.
This is the impasse I reached when attempting to register a function definition of the form:

 f(x, y) := ite(c1,..., ite(c2, ..., ite(c3, f_fresh(x, y))))

The idea would be to synthesize the model for f(x,y) using this definition.

The current conversion code is written such that every ground instance of f(rm(t1), fp(t2, t3, t4)) is translated to an extended definition. The function f_fresh is cached so that it is recycled across different t1, t2, t3, t4 arguments. Model construction for f would somehow need to reflect
the equation for f, as far as I understand. Of course, I could very well be off somewhere in the reading of the intent.

[wintersteiger]

Fix is now merged!

@NikolajBjorner: Your evaluate, get_macro and my evaluate_partial_theory_func in model_evaluator seem to do similar things, perhaps those could be simplified?