From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 044447FCEF for ; Fri, 3 Apr 2015 00:18:51 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of drupyog+caml@zoho.com) identity=pra; client-ip=74.201.84.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="drupyog+caml@zoho.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of drupyog+caml@zoho.com designates 74.201.84.155 as permitted sender) identity=mailfrom; client-ip=74.201.84.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="drupyog+caml@zoho.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@sender1.zohomail.com) identity=helo; client-ip=74.201.84.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="postmaster@sender1.zohomail.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CjAACqvx1Vm5tUyUpchDaDFchRAoFMTAEBAQEBARIBAQEBAQYLCwkULoQfAQQBIyABNAMDCwsEHRYLAgIJAwIBAgFFBgEMCAEBiBYBAwEEBAgEtFZwhGgCjSMiKCWFGgELARgHiymFAIJogUWRdYZ5ggGBHRGBAYRfiXKDSIIkHYFSbYJDAQEB X-IPAS-Result: A0CjAACqvx1Vm5tUyUpchDaDFchRAoFMTAEBAQEBARIBAQEBAQYLCwkULoQfAQQBIyABNAMDCwsEHRYLAgIJAwIBAgFFBgEMCAEBiBYBAwEEBAgEtFZwhGgCjSMiKCWFGgELARgHiymFAIJogUWRdYZ5ggGBHRGBAYRfiXKDSIIkHYFSbYJDAQEB X-IronPort-AV: E=Sophos;i="5.11,513,1422918000"; d="scan'208,217";a="108175693" Received: from sender1.zohomail.com ([74.201.84.155]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-MD5; 03 Apr 2015 00:18:49 +0200 DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=zapps768; d=zoho.com; h=message-id:date:from:user-agent:mime-version:to:subject:references:in-reply-to:content-type; b=VvISn3dIYXHFyzpkQiTJ7EnVgN4IAAlKQpztAqIQMk70Gi4+2FGGyPDoH0Vq+sm1D9KD5fpy3LMT WrtnYbJwbhSllNuufvbhILBYwfpC9/EksjARXsDaJHhrq5x0/Z/y Received: from [192.168.1.8] (did75-8-82-228-42-129.fbx.proxad.net [82.228.42.129]) by mx.zohomail.com with SMTPS id 1428013119946243.66824664036926; Thu, 2 Apr 2015 15:18:39 -0700 (PDT) Message-ID: <551DC03D.7050905@zoho.com> Date: Fri, 03 Apr 2015 00:18:37 +0200 From: Drup User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0 MIME-Version: 1.0 To: Kenneth Adam Miller , caml-list@inria.fr References: <551DB78D.1040705@zoho.com> In-Reply-To: Content-Type: multipart/alternative; boundary="------------020509040009090304040305" Subject: Re: [Caml-list] Mathematical Expression Library This is a multi-part message in MIME format. --------------020509040009090304040305 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit > 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. --------------020509040009090304040305 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 7bit

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.


--------------020509040009090304040305--