<commit_before>﻿(*
   Copyright 2008-2014 <NAME> and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
#light "off"

module FStar.SMTEncoding.Z3
open FStar.ST
open FStar.Exn
open FStar.All
open FStar
open FStar.SMTEncoding.Term
open FStar.BaseTypes
open FStar.Util
module BU = FStar.Util

(****************************************************************************)
(* Z3 Specifics                                                             *)
(****************************************************************************)
type z3version =
| Z3V_Unknown of string
| Z3V of int * int * int

let z3version_as_string = function
    | Z3V_Unknown s -> BU.format1 "unknown version: %s" s
    | Z3V (i, j, k) -> BU.format3 "%s.%s.%s" (BU.string_of_int i) (BU.string_of_int j) (BU.string_of_int k)

let z3v_compare known (w1, w2, w3) =
    match known with
    | Z3V_Unknown _-> None
    | Z3V (k1, k2, k3) -> Some(
        if k1 <> w1 then w1 - k1 else
        if k2 <> w2 then w2 - k2 else
        w3 - k3
    )

let z3v_le known wanted =
    match z3v_compare known wanted with
    | None   -> false
    | Some i -> i >= 0

let _z3version : ref<option<z3version>> = BU.mk_ref None

let get_z3version () =
    let prefix = "Z3 version " in

    match !_z3version with
    | Some version -> version
    | None ->
        let _, out, _ = BU.run_proc (Options.z3_exe()) "-version" "" in
        let out =
            match splitlines out with
            | x :: _ when starts_with x prefix -> begin
                let x = trim_string (substring_from x (String.length prefix)) in
                let x = try List.map int_of_string (split x ".") with _ -> [] in
                match x with
                | [i1; i2; i3] -> Z3V (i1, i2, i3)
                | _ -> Z3V_Unknown out
            end
            | _ -> Z3V_Unknown out
        in
            _z3version := Some out; out

(* Check the Z3 commit hash once, and issue a warning if it is not
   equal to the one that we are expecting from the Z3 url below
*)
let _z3hash_checked : ref<bool> = BU.mk_ref false

let _z3hash_expected = "1f29cebd4df6"

let _z3url = "https://github.com/FStarLang/binaries/tree/master/z3-tested"

let z3hash_warning_message () =
    let _, out, _ = BU.run_proc (Options.z3_exe()) "-version" "" in
    match splitlines out with
    | x :: _ ->
        begin
            let trimmed = trim_string x in
            let parts = split trimmed " " in
            let rec aux = function
            | [hash] ->
              if hash = _z3hash_expected
              then begin
                  if Options.debug_any ()
                  then
                      let msg =
                          BU.format1
                              "Successfully found expected Z3 commit hash %s"
                              _z3hash_expected
                      in
                      print_string msg
                  else ();
                  None
              end else
                  let msg =
                      BU.format2
                          "Expected Z3 commit hash %s, got %s"
                          _z3hash_expected
                          hash
                  in
                  Some msg
            | _ :: q -> aux q
            | _ -> Some "No Z3 commit hash found"
            in
            aux parts
        end
    | _ -> Some "No Z3 version string found"

let check_z3hash () =
    if not !_z3hash_checked
    then begin
        _z3hash_checked := true;
        match z3hash_warning_message () with
        | None -> ()
        | Some msg ->
          let msg =
              BU.format4
                  "%s\n%s\n%s\n%s\n"
                  msg
                  "Please download the version of Z3 corresponding to your platform from:"
                  _z3url
                  "and add the bin/ subdirectory into your PATH"
          in
          FStar.Errors.add_one (FStar.Errors.mk_issue FStar.Errors.EWarning None msg)
    end

let ini_params () =
  let z3_v = get_z3version () in
  begin if z3v_le (get_z3version ()) (4, 4, 0)
  then raise <| BU.Failure (BU.format1 "Z3 4.5.0 recommended; at least Z3 v4.4.1 required; got %s\n" (z3version_as_string z3_v))
  else ()
  end;
  check_z3hash ();
  (String.concat " "
                (List.append
                 [ "-smt2 -in auto_config=false model=true smt.relevancy=2";
                   (Util.format1 "smt.random_seed=%s" (string_of_int (Options.z3_seed()))) ]
                 (Options.z3_cliopt())))

type label = string
type unsat_core = option<list<string>>
type z3status =
    | UNSAT   of unsat_core
    | SAT     of error_labels * option<string>         //error labels
    | UNKNOWN of error_labels * option<string>         //error labels
    | TIMEOUT of error_labels * option<string>         //error labels
    | KILLED
type z3statistics = BU.smap<string>

let status_tag = function
    | SAT  _ -> "sat"
    | UNSAT _ -> "unsat"
    | UNKNOWN _ -> "unknown"
    | TIMEOUT _ -> "timeout"
    | KILLED -> "killed"

let status_string_and_errors s =
    match s with<commit_msg>Remove old Z3 version check<commit_after>﻿(*
   Copyright 2008-2014 <NAME> and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
#light "off"

module FStar.SMTEncoding.Z3
open FStar.ST
open FStar.Exn
open FStar.All
open FStar
open FStar.SMTEncoding.Term
open FStar.BaseTypes
open FStar.Util
module BU = FStar.Util

(****************************************************************************)
(* Z3 Specifics                                                             *)
(****************************************************************************)

(* Check the Z3 commit hash once, and issue a warning if it is not
   equal to the one that we are expecting from the Z3 url below
*)
let _z3hash_checked : ref<bool> = BU.mk_ref false

let _z3hash_expected = "1f29cebd4df6"

let _z3url = "https://github.com/FStarLang/binaries/tree/master/z3-tested"

let z3hash_warning_message () =
    let _, out, _ = BU.run_proc (Options.z3_exe()) "-version" "" in
    match splitlines out with
    | x :: _ ->
        begin
            let trimmed = trim_string x in
            let parts = split trimmed " " in
            let rec aux = function
            | [hash] ->
              if hash = _z3hash_expected
              then begin
                  if Options.debug_any ()
                  then
                      let msg =
                          BU.format1
                              "Successfully found expected Z3 commit hash %s"
                              _z3hash_expected
                      in
                      print_string msg
                  else ();
                  None
              end else
                  let msg =
                      BU.format2
                          "Expected Z3 commit hash %s, got %s"
                          _z3hash_expected
                          hash
                  in
                  Some msg
            | _ :: q -> aux q
            | _ -> Some "No Z3 commit hash found"
            in
            aux parts
        end
    | _ -> Some "No Z3 version string found"

let check_z3hash () =
    if not !_z3hash_checked
    then begin
        _z3hash_checked := true;
        match z3hash_warning_message () with
        | None -> ()
        | Some msg ->
          let msg =
              BU.format4
                  "%s\n%s\n%s\n%s\n"
                  msg
                  "Please download the version of Z3 corresponding to your platform from:"
                  _z3url
                  "and add the bin/ subdirectory into your PATH"
          in
          FStar.Errors.add_one (FStar.Errors.mk_issue FStar.Errors.EWarning None msg)
    end

let ini_params () =
  check_z3hash ();
  (String.concat " "
                (List.append
                 [ "-smt2 -in auto_config=false model=true smt.relevancy=2";
                   (Util.format1 "smt.random_seed=%s" (string_of_int (Options.z3_seed()))) ]
                 (Options.z3_cliopt())))

type label = string
type unsat_core = option<list<string>>
type z3status =
    | UNSAT   of unsat_core
    | SAT     of error_labels * option<string>         //error labels
    | UNKNOWN of error_labels * option<string>         //error labels
    | TIMEOUT of error_labels * option<string>         //error labels
    | KILLED
type z3statistics = BU.smap<string>

let status_tag = function
    | SAT  _ -> "sat"
    | UNSAT _ -> "unsat"
    | UNKNOWN _ -> "unknown"
    | TIMEOUT _ -> "timeout"
    | KILLED -> "killed"

let status_string_and_errors s =
    match s with
{'fraction_non_alphanumeric': 0.11193329859301719, 'fraction_numerical': 0.0174048983845753, 'mean_word_length': 1.7030985915492958, 'pattern_counts': {'":': 0, '<': 24, '<?xml version=': 0, '>': 61, 'https://': 2, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6121693', 'n_tokens_mistral': 2827, 'n_tokens_neox': 2723, 'n_words': 883}