OCamlPro
checking unbounded quantification
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)
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,propmay contain free variables.model_forall(var, prop)which returns a boolean, indicating whether the proposition prop holds true for all possible values of var,propmay contain free variables.
In the mean time, just like what you said, I'm not sure if those are feasible in the solver.
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
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 :)