Trivial queries sent to the solvers

[hra687261]

While working on #569, I noticed that some trivial queries are sent to solvers, such as:

• Trivially SAT cases (Which I though would be simplified to (assert true) with Symex's substitutions, cc @redianthus ):

  (set-info :status sat)
  (set-logic ALL)
  (declare-fun choice_i32_1 () (_ BitVec 32))
  (assert (= choice_i32_1 (_ bv8389664 32)))
  (check-sat) 

• Trivially UNSAT cases (Which should be eliminated before reaching the solver):

  (set-info :status sat)
  (set-logic ALL)
  (declare-fun symbol_0 () (_ BitVec 32))
  (assert (= symbol_0 (_ bv1 32)))
  (assert false)
  (check-sat)

  (The :status sat is a bit worrying because it is supposed to be what the solver answered, so there is possibly a bug in query selection before logging)

[redianthus]

I don't think the first case would be simplified by Symex equality substitution for two reasons :

1. I decided to only substitute new equalities once we know the PC is sat. In your example, I believe the equality was added for the first time, so, it'll first be tested for satisfiability, and only later, when something else is added, we'll substitute choice_i32_1 with its value.
2. We can't make symbol disappear. If we have x = 42, then, it'll stay there in all cases, what we simplify is, if we had x > 0 and later we discover x = 42, then, we'll have x > 0 simplified to true but x = 42 will stay there.

[hra687261]

Indeed, Symex should not do that. While a solver will do it quickly, we can still probably save a solver call, either by doing the substitution in smtml (for assertions of the form x = c, the model can't be anything other than c if it is sat), or more naively when a query only has one assertion (notably of the form x ? c or x ? y, with x,y as variables, ?˙ a relop and c` a const) and simply generate the values that satisfy that assertion when it is trivial.

[redianthus]

Yes, I believe it should not do 2. either. For 1., maybe I'll find a satisfying way to do it in the future, but for now, it was not worth it according to my testing (i.e. substituting something that we'll likely throw away costs more than what we gain, instead I only substiture after being sure we'll reuse it, that, it is SAT and will be part of the PC in all future branches starting at the current point of execution).

either by doing the substitution in smtml (for assertions of the form x = c, the model can't be anything other than c if it is sat), or more naively when a query only has one assertion (notably of the form x ? c or x ? y, with x,y as variables, ?˙ a relop and c` a const) and simply generate the values that satisfy that assertion when it is trivial.

I think there are some cases where you'd have to be cautious, for instance x ? y when x = y and they are floats. But yes, that is something that might be worth it (but does it happen a lot in practice?).

[hra687261]

think there are some cases where you'd have to be cautious, for instance x ? y when x = y and they are floats.

Of course!

But yes, that is something that might be worth it (but does it happen a lot in practice?).

In one run, no. But at the start of every execution there are a few trivial queries, which is pretty annoying in #569.
I'm thinking that simply eliminating trivial queries before extraction should suffice for now, a bigger change in smtml would be risky (as one would also have to take into account added assertions with add and the state of the solver add, doing a check on a trivial assertion, does not mean that more complex assertions have not been added before...)