Re: [Caml-list] Mathematical Expression Library

[Drup <drupyog+caml@zoho.com>]

[-- Attachment #1: Type: text/plain, Size: 1525 bytes --]


> Can you also explain in more depth your justification of Z3 doing 
> expression simplification on my behalf for anything submitted? That 
> was also my guess, but I didn't have that substantiated before my 
> colleagues, so I wanted to be thorough.
Knowledge of Z3, I guess ? It calls the simplification function (which 
is exposed as Z3.Expr.simplify in the ml-ng bindings) before solving. 
It's a bit more complicated when in the so-called "interactive" mode but 
still doing it. Note that the function is still useful when printing the 
formula for debugging purposes.

>
>     Shape?? I don't know what you mean.
>
I mean that, for a solver like Z3, two encodings of the same problem can 
result in different results (between UNSAT and UNKNOWN, in particular) 
and can result, and that's more sneaky, in completely different 
performance profiles. Solvers (and Z3 in particular) uses heuristics to 
know which branches to solve first so it's rather guess-y.

You mostly notice that when trying them though, it's rather pointless to 
try to guess in advance, since it's very implementation-sensible.

>
>     In any case, my plan was to use OCamlgraph and some hash-consing
>     to construct correspondingly equivalent semantics, then reason
>     about it in a distributed fashion.
>
If you are looking to encode an SSA control flow graph in Z3's SMT, I 
have the code to do that. I could extract it and get it into shape. It's 
based on llvm's IR, but It should be fairly reusable. Tell me if you are 
interested.



[-- Attachment #2: Type: text/html, Size: 2945 bytes --]