From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: ** X-Spam-Status: No, score=2.8 required=5.0 tests=DNS_FROM_RFC_POST, HTML_MESSAGE,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 488D8BBAF for ; Sun, 8 Mar 2009 20:13:28 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ar0CACO1s0lKfSwck2dsb2JhbACCIDGKI4d3PwEBAQEJCQoJEQOvMzCFEIhIAQMBA4QCBoUi X-IronPort-AV: E=Sophos;i="4.38,325,1233529200"; d="scan'208";a="36254499" Received: from yx-out-2324.google.com ([74.125.44.28]) by mail4-smtp-sop.national.inria.fr with ESMTP; 08 Mar 2009 20:13:27 +0100 Received: by yx-out-2324.google.com with SMTP id 31so601439yxl.3 for ; Sun, 08 Mar 2009 12:13:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:sender:received:date :x-google-sender-auth:message-id:subject:from:to:content-type; bh=nrlbXlkmerhcMwS7szyYyQydQ5zlbEe3oozst9njaok=; b=MgbLaa3P7c/6iZiEW7V1ojFDBY6CokYcmER4o4inV0yeIoNCy0V5X5ZzRwtAjPVMj3 oxaeq2D065DyPuymjGCITbHoBEzUA5aX5bB18eofblolLpiwakcD010nk+kd1QRfLGBh 9r6CJ+xVDlNNBbf2NnwxEWW8gAsJqyc4hgc+0= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=mUxDrsVQLU4kI75URBuoIIkAdmOeUmyjAihBuBU99rxqWeYMg1reKlNMQQ3bCfYLaQ e0WicJgjD5QZxPjAL4EkQUcH7jLBk+KSs3utHoe1Nsz8tvxwfY4nzYCYbz42WjAcXdNr IG6+9XBA0gLSIRR3BcpiV0P3IvrjUzLqOaPpk= MIME-Version: 1.0 Sender: jean.yang.writeme@gmail.com Received: by 10.100.125.14 with SMTP id x14mr3118662anc.66.1236539606847; Sun, 08 Mar 2009 12:13:26 -0700 (PDT) Date: Sun, 8 Mar 2009 15:13:26 -0400 X-Google-Sender-Auth: b65213a5b595698b Message-ID: <1bd843010903081213j5d3e4581p9ff192eda3396f79@mail.gmail.com> Subject: Using OCaml with SMT solvers From: Jean Yang To: caml-list@yquem.inria.fr Content-Type: multipart/alternative; boundary=0016e645b9b404510d0464a0508b X-Spam: no; 0.00; ocaml:01 smt:01 solvers:01 smt:01 solver:01 ocaml:01 solver:01 seems:03 seems:03 interface:06 interface:06 linux:07 linux:07 think:13 think:13 --0016e645b9b404510d0464a0508b Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Hello, I don't know if this is the right place to ask this question, but what is the best way of using an SMT solver with an OCaml interface on Linux? After a brief search it seems that Z3 is the most popular solver with an OCaml interface, but unfortunately it only supports Windows. Thanks, Jean -- Jean Yang http://web.mit.edu/jeanyang/www/ Save us! Think before you print. *^^` --0016e645b9b404510d0464a0508b Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Hello,

=A0 I don't know if this is the right place to ask this q= uestion, but what is the best way of using an SMT solver with an OCaml inte= rface on Linux?

=A0 After a brief search it seems that Z3 is the mos= t popular solver with an OCaml interface, but unfortunately it only support= s Windows.

Thanks,
Jean

--
Jean Yang
http://web.mit.edu/jeanyang/www/
Save= us! =A0Think before you print.
*^^`
--0016e645b9b404510d0464a0508b--