<commit_before><commit_msg>Z3 theorem prover: new formula<commit_after>require 'formula'

class Z3 < Formula
  homepage 'http://z3.codeplex.com/'
  version '4.3.1'
  url 'http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=z3&changeSetId=89c1785b73225a1b363c0e485f854613121b70a7'
  sha1 '91726a94a6bc0c1035d978b225f3f034387fdfe0'
  head 'https://git01.codeplex.com/z3', :using => :git

  depends_on :autoconf
  depends_on :automake
  depends_on :python

  def patches
    # Fixes compilation with Clang.
    DATA
  end

  def install
    package_dir = lib/"python2.7/site-packages"
    mkdir_p package_dir
    inreplace 'scripts/mk_util.py', /^PYTHON_PACKAGE_DIR=.*/, "PYTHON_PACKAGE_DIR=\"#{package_dir}\""

    system 'autoconf'
    system './configure', "--prefix=#{prefix}"
    system 'python', 'scripts/mk_make.py'
    cd 'build' do
      system 'make'
      system 'make', 'install'
      (share/'z3').install 'test-z3'
    end
  end

  def test
      # There doesn't seem to be a convenient way to run all unit tests...
      `#{share}/z3/test-z3 -h`.split[33..-1].each do |testcase|
        system "#{share}/z3/test-z3", testcase
      end
  end
end

__END__
diff -aur z3.orig/src/util/hwf.cpp z3/src/util/hwf.cpp
--- z3.orig/src/util/hwf.cpp	2014-02-13 20:59:07.000000000 +0100
+++ z3/src/util/hwf.cpp	2014-02-13 20:59:22.000000000 +0100
@@ -16,6 +16,8 @@
 Revision History:
 
 --*/
+#include <emmintrin.h>
+
 #include<float.h>
 
 #ifdef _WINDOWS
{'fraction_non_alphanumeric': 0.14782608695652175, 'fraction_numerical': 0.09632107023411371, 'mean_word_length': 3.374269005847953, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 6, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 2, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7494220', 'n_tokens_mistral': 671, 'n_tokens_neox': 593, 'n_words': 112}