checking unbounded quantification

[Laplace-Demon]

discussion 23/08

[zapashcanon]

Do you want to start implementing it ?

In the meantime, we can probably take care of providing the missing model_exists(var, prop) function, although I'm not completely sure how we could implement it because it is more complicated than simply asking if a model exists. (cc @filipeom)

[Laplace-Demon]

Do you want to start implementing it ?

In the meantime, we can probably take care of providing the missing model_exists(var, prop) function, although I'm not completely sure how we could implement it because it is more complicated than simply asking if a model exists. (cc @filipeom)

There won't be much problem with respect to code generation, and I've just realized we no longer need the PNF form, a simple recursion works.

• model_exists(var, prop) which returns a boolean, indicating whether the proposition prop holds true for one possible value of var, prop may contain free variables.
• model_forall(var, prop) which returns a boolean, indicating whether the proposition prop holds true for all possible values of var, prop may contain free variables.

In the mean time, just like what you said, I'm not sure if those are feasible in the solver.

[filipeom]

Maybe I misunderstood this, but it seems like a lot of work, we'd essentially be trying to reimplement quantifier elimination for fixed size bitvectors?

This makes the analysis inherently undecidable which will make the solver poop its pants. But why wouldn't we want to use Z3's quantifiers? They probably do a good job a trying to solve these? It would output a bunch of Unknowns for harder formulas but adding then in smtml would be easy

[zapashcanon]

No, we actually want to use Z3! We are going to craft an example of what we want to achieve and show it to you on Friday :)