Upgrade core to v0.13

.travis.yml

@@ -11,12 +11,8 @@ services:
 install: bash .travis/install.sh
 
 env:
-  - OCAML_VERSION=4.07.0           MIN_REQS_ONLY="true"
-  - OCAML_VERSION=4.07.0+flambda   MIN_REQS_ONLY="true"
-  - OCAML_VERSION=4.07.1
-  - OCAML_VERSION=4.07.1+flambda
-  - OCAML_VERSION=4.08.0
-  - OCAML_VERSION=4.08.0+flambda
+  - OCAML_VERSION=4.08.0           MIN_REQS_ONLY="true"
+  - OCAML_VERSION=4.08.0+flambda   MIN_REQS_ONLY="true"
   - OCAML_VERSION=4.08.1
   - OCAML_VERSION=4.08.1+flambda
   - OCAML_VERSION=4.09.0

.travis/run.sh

@@ -17,9 +17,9 @@ if [ -z "${MIN_REQS_ONLY}" ]; then
     opam install --yes --deps-only --with-test ./LoopInvGen.opam
 else
     opam install --yes alcotest.0.8.0   \
-                       core.v0.12.2     \
+                       core.v0.13.0     \
                        dune.1.6.0       \
-                       ppx_let.v0.12.0
+                       ppx_let.v0.13.0
 fi
 
 opam list
@@ -29,4 +29,4 @@ pwd ; ls -lah
 
 dune build --verbose
 dune build test/Runner.exe --verbose
-dune build app/App.exe
+dune build app/App.exe --verbose

Dockerfile

@@ -7,7 +7,7 @@ LABEL maintainer="padhi@cs.ucla.edu"
 
 ENV OPAM_VERSION  2.0.5
 ENV OCAML_VERSION 4.09.0+flambda
-ENV Z3_VERSION    z3-4.8.7
+ENV Z3_VERSION    Nightly
 
 ENV HOME /home/opam
 
@@ -41,9 +41,9 @@ WORKDIR $HOME
 
 
 RUN opam install --yes alcotest.0.8.5 \
-                       core.v0.12.4 \
-                       dune.1.11.4 \
-                       ppx_let.v0.12.0 \
+                       core.v0.13.0 \
+                       dune.2.1.2 \
+                       ppx_let.v0.13.0 \
                        && \
     opam clean --yes && \
     git clone https://github.com/SaswatPadhi/LoopInvGen.git

LoopInvGen.opam

@@ -22,9 +22,9 @@ build: [
 ]
 
 depends: [
-  "ocaml"         {>= "4.07"}
+  "ocaml"         {>= "4.08"}
   "dune"          {>= "1.6" & build}
   "alcotest"      {>= "0.8" & with-test}
-  "core"          {>= "v0.12.2" & <= "v0.13"}
-  "ppx_let"       {>= "v0.12.0" & <= "v0.13"}
-]
+  "core"          {>= "v0.13" & <= "v0.14"}
+  "ppx_let"       {>= "v0.13" & <= "v0.14"}
+]

bin/Score.ml

@@ -3,6 +3,7 @@ open Core
 open LoopInvGen
 
 let time_pseudolog x =
+  let open Float in
   if x > 3600.0 then 1
   else if x >= 1000.0 then 2
   else if x >= 300.0 then 3
@@ -47,4 +48,4 @@ let command =
     ]
 
 let () =
-  Command.run command
+  Command.run command

src/Check.ml

@@ -8,7 +8,7 @@ let is_sufficient_invariant ~(zpath : string) ~(sygus : SyGuS.t) (inv : string)
   let open ZProc
    in process ~zpath (fun z3 ->
      Simulator.setup sygus z3 ;
-     if (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body) <> None
+     if not ( Option.is_none (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body))
      then (if String.equal inv "false" then NO_SOLUTION_PASS else NO_SOLUTION_FAIL)
      else let inv = SyGuS.func_definition {sygus.inv_func with body = inv}
            in ignore (run_queries ~scoped:false z3 [] ~db:[ inv ]) ;
@@ -26,5 +26,5 @@ let is_sufficient_invariant ~(zpath : string) ~(sygus : SyGuS.t) (inv : string)
                   with
                   | [ None ; None ; None ] -> PASS
                   | x -> FAIL (List.filter_mapi x
-                                 ~f:(fun i v -> if v = None then None
+                                 ~f:(fun i v -> if Option.is_none v then None
                                                 else Some [| "pre" ; "trans" ; "post" |].(i))))

src/Job.ml

@@ -20,6 +20,8 @@ type ('a, 'b) _t = {
 
 type t = (Value.t list, Value.t) _t
 
+let are_values_equal = List.equal Value.equal
+
 let compute_feature_value (test : 'a) (feature : 'a feature with_desc) : bool =
   try (fst feature) test with _ -> false
   [@@inline always]
@@ -50,11 +52,11 @@ let create_unlabeled ~f ~args ~post ?(features = []) tests : t =
    in create ~f ~args ~post ~features ~pos_tests ~neg_tests ()
 
 let add_pos_test ~(job : t) (test : Value.t list) : t =
-  if List.exists job.pos_tests ~f:(fun (pt, _) -> pt = test)
+  if List.exists job.pos_tests ~f:(fun (pt, _) -> are_values_equal pt test)
   then raise (Duplicate_Test ("New POS test (" ^ (String.concat ~sep:"," job.farg_names)
                              ^ ") = (" ^ (List.to_string_map ~sep:"," ~f:Value.to_string test)
                              ^ "), already exists in POS set!"))
-  else if List.exists job.neg_tests ~f:(fun (nt, _) -> nt = test)
+  else if List.exists job.neg_tests ~f:(fun (nt, _) -> are_values_equal nt test)
   then raise (Ambiguous_Test ("New POS test (" ^ (String.concat ~sep:"," job.farg_names)
                              ^ ") = (" ^ (List.to_string_map ~sep:"," ~f:Value.to_string test)
                              ^ ") already exists in NEG set!"))
@@ -70,11 +72,11 @@ let add_pos_test ~(job : t) (test : Value.t list) : t =
                                        ^ "), does not belong in POS set!"))
 
 let add_neg_test ~(job : t) (test : Value.t list) : t =
-  if List.exists job.neg_tests ~f:(fun (nt, _) -> nt = test)
+  if List.exists job.neg_tests ~f:(fun (nt, _) -> are_values_equal nt test)
   then raise (Duplicate_Test ("New NEG test (" ^ (String.concat ~sep:"," job.farg_names)
                              ^ ") = (" ^ (List.to_string_map ~sep:"," ~f:Value.to_string test)
                              ^ ") already exists in NEG set!"))
-  else if List.exists job.pos_tests ~f:(fun (pt, _) -> pt = test)
+  else if List.exists job.pos_tests ~f:(fun (pt, _) -> are_values_equal pt test)
   then raise (Ambiguous_Test ("New NEG test (" ^ (String.concat ~sep:"," job.farg_names)
                              ^ ") = (" ^ (List.to_string_map ~sep:"," ~f:Value.to_string test)
                              ^ ") already exists in POS set!"))
@@ -98,4 +100,4 @@ let add_feature ~(job : t) (feature : 'a feature with_desc) : t =
        features = feature :: job.features ;
        pos_tests = List.map job.pos_tests ~f:add_to_fv ;
        neg_tests = List.map job.neg_tests ~f:add_to_fv ;
-     }
+     }

src/LIG.ml

@@ -39,7 +39,7 @@ let satisfyTrans ?(config = Config.default) ~(sygus : SyGuS.t) ~(z3 : ZProc.t)
   let invf'_call =
     "(invf " ^ (List.to_string_map sygus.inv_func.args ~sep:" "
                   ~f:(fun (s, _) -> s ^ "!")) ^ ")" in
-  let eval_term = (if not (config.model_completion_mode = `UsingZ3) then "true"
+  let eval_term = (if not (Poly.equal config.model_completion_mode `UsingZ3) then "true"
                    else "(and " ^ invf_call ^ " " ^ sygus.trans_func.body ^ ")") in
   let rec helper inv =
     Log.info (lazy ("IND >> Strengthening for inductiveness:"
@@ -64,7 +64,7 @@ let satisfyTrans ?(config = Config.default) ~(sygus : SyGuS.t) ~(z3 : ZProc.t)
               ~features: (List.map ~f:(fun (_, name) -> ( (ZProc.build_feature name z3)
                                                         , ("(" ^ name ^ " " ^ all_state_vars ^ ")")))
                                    config.user_features)
-              ~post:(fun _ res -> res = Ok (Value.Bool false)))
+              ~post:(fun _ -> function Ok (Value.Bool false) -> true | _ -> false))
         in ZProc.close_scope z3
          ; Log.debug (lazy ("IND Delta: " ^ pre_inv))
          ; if String.equal pre_inv "true"
@@ -76,7 +76,7 @@ let satisfyTrans ?(config = Config.default) ~(sygus : SyGuS.t) ~(z3 : ZProc.t)
                    in Log.info (lazy ("PRE >> Checking if the following candidate is weaker than precond:"
                                      ^ (Log.indented_sep 4) ^ new_inv))
                     ; let ce = ZProc.implication_counter_example z3 sygus.pre_func.body new_inv
-                       in if ce = None then helper new_inv else (new_inv, ce))
+                       in if Option.is_none ce then helper new_inv else (new_inv, ce))
    in helper inv
 
 let rec learnInvariant_internal ?(config = Config.default) ~(states : Value.t list list)
@@ -111,7 +111,7 @@ let rec learnInvariant_internal ?(config = Config.default) ~(states : Value.t li
           VPIE.learnVPreCond
             ~z3 ~config:config._VPIE ~consts:sygus.constants
             ~post_desc:sygus.post_func.body
-            ~eval_term:(if not (config.model_completion_mode = `UsingZ3)
+            ~eval_term:(if not (Poly.equal config.model_completion_mode `UsingZ3)
                         then "true" else sygus.post_func.body)
           (Job.create ()
               ~pos_tests:states
@@ -121,7 +121,7 @@ let rec learnInvariant_internal ?(config = Config.default) ~(states : Value.t li
                       else ("(not (" ^ sygus.post_func.body ^ "))"))
                      ~z3 ~arg_names:(List.map sygus.synth_variables ~f:fst))
                ~args: sygus.synth_variables
-               ~post: (fun _ res -> res = Ok (Value.Bool false)))
+               ~post:(fun _ -> function Ok (Value.Bool false) -> true | _ -> false))
          in stats.lig_time_ms <- stats.lig_time_ms +. vpie_stats.vpi_time_ms
           ; stats.lig_ce <- stats.lig_ce + vpie_stats.vpi_ce
           ; stats._VPIE <- vpie_stats :: stats._VPIE
@@ -137,7 +137,7 @@ let rec learnInvariant_internal ?(config = Config.default) ~(states : Value.t li
                            ^ (Log.indented_sep 4) ^ inv))
           ; match satisfyTrans ~config ~sygus ~states ~z3 inv stats with
             | inv, None
-              -> if inv <> "false" then ((ZProc.simplify z3 inv), stats)
+              -> if not (String.equal inv "false") then ((ZProc.simplify z3 inv), stats)
                   else restart_with_new_states (random_value ~seed:(`Deterministic seed_string)
                                                             (gen_pre_state ~use_trans:true sygus z3))
             | _, (Some ce_model)
@@ -152,6 +152,6 @@ let learnInvariant ?(config = Config.default) ~(states : Value.t list list)
        ~random_seed:(Some (Int.to_string (Quickcheck.(random_value ~seed:(`Deterministic config.base_random_seed)
                                                                    (Generator.small_non_negative_int)))))
        (fun z3 -> Simulator.setup sygus z3 ~user_features:(List.map ~f:fst config.user_features)
-                ; if (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body) <> None
+                ; if not (Option.is_none (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body))
                   then ("false", stats)
-                  else learnInvariant_internal ~config ~states sygus config.base_random_seed z3 stats)
+                  else learnInvariant_internal ~config ~states sygus config.base_random_seed z3 stats)

src/PIE.ml

@@ -38,13 +38,13 @@ type stats = {
 let conflictingTests (job : Job.t) : 'a conflict list =
   let make_f_vecs = List.map ~f:(fun (t, fvec) -> (t, Lazy.force fvec)) in
   let make_groups tests =
-    List.group tests ~break:(fun (_, fv1) (_, fv2) -> fv1 <> fv2)
+    List.group tests ~break:(fun (_, fv1) (_, fv2) -> not (List.equal Bool.equal fv1 fv2))
   in let (p_groups, n_groups) = (make_groups (make_f_vecs job.pos_tests),
                                  make_groups (make_f_vecs job.neg_tests))
   in List.(filter_map
        p_groups
        ~f:(fun [@warning "-8"] (((_, pfv) :: _) as ptests) ->
-             match find n_groups ~f:(fun ((_, nfv) :: _) -> nfv = pfv) with
+             match find n_groups ~f:(fun ((_, nfv) :: _) -> List.equal Bool.equal nfv pfv) with
              | None -> None
              | Some ntests -> Some { pos = map ~f:fst ptests
                                    ; neg = map ~f:fst ntests
@@ -65,7 +65,7 @@ let synthFeature ?(consts = []) ~(job : Job.t) ~(config : Synthesizer.Config.t)
   } in stats._Synthesizer <- result.stats :: stats._Synthesizer
      ; stats.pi_time_ms <- stats.pi_time_ms +. result.stats.synth_time_ms
      ; ((fun values -> try Value.equal (result.func values) (Value.Bool true) with _ -> false),
-        (if result.constraints = [] then result.string
+        (if List.is_empty result.constraints then result.string
          else "(and " ^ result.string ^ (String.concat ~sep:" " result.constraints) ^ ")"))
 
 let resolveAConflict ?(config = Config.default) ?(consts = []) ~(job : Job.t)
@@ -95,15 +95,15 @@ let resolveAConflict ?(config = Config.default) ?(consts = []) ~(job : Job.t)
 let rec resolveSomeConflicts ?(config = Config.default) ?(consts = []) ~(job : Job.t)
                              (conflict_groups : Value.t list conflict list) stats
                              : Value.t list Job.feature Job.with_desc option =
-  if conflict_groups = [] then None
+  if List.is_empty conflict_groups then None
   else try Some (resolveAConflict (List.hd_exn conflict_groups) ~config ~consts ~job stats)
        with e -> Log.error (lazy ((Exn.to_string e) ^ (Printexc.get_backtrace ())))
                ; resolveSomeConflicts (List.tl_exn conflict_groups) ~config ~consts ~job stats
 
 let rec augmentFeatures ?(config = Config.default) ?(consts = []) (job : Job.t)
                         stats : Job.t =
   let conflict_groups = conflictingTests job
-   in if conflict_groups = [] then job
+   in if List.is_empty conflict_groups then job
       else if config.disable_synth
            then (Log.error (lazy ("CONFLICT RESOLUTION FAILED")) ; raise NoSuchFunction)
       else match resolveSomeConflicts conflict_groups ~job ~config ~consts stats with
@@ -142,4 +142,4 @@ let learnPreCond ?(config = Config.default) ?(consts = []) (job : Job.t)
 let cnf_opt_to_desc (pred : ('a Job.feature Job.with_desc) CNF.t option) : Job.desc =
   match pred with
   | None -> "false"
-  | Some pred -> CNF.to_string pred ~stringify:snd
+  | Some pred -> CNF.to_string pred ~stringify:snd

src/Simulator.ml

@@ -25,7 +25,7 @@ let gen_state_from_model (s : SyGuS.t) (m : ZProc.model option)
   | Some m -> create (fun ~size ~random -> Some (
                 List.map s.synth_variables
                          ~f:(fun (v, t) ->
-                               match List.Assoc.find m v ~equal:(=)
+                               match List.Assoc.find m v ~equal:String.equal
                                with Some d -> d
                                   | None -> generate (TestGen.for_type t) ~size ~random)))
 
@@ -62,7 +62,7 @@ let simulate_from (s : SyGuS.t) (z3 : ZProc.t) (head : Value.t list option)
           head :: (match size with
                   | 0 -> []
                   | n -> begin match generate (transition s z3 head) ~size ~random
-                               with Some next when next <> head
+                               with Some next when not (List.equal Value.equal next head)
                                     -> step_internal next (n-1)
                                   | _ -> []
                         end)

src/SyGuS.ml

@@ -117,9 +117,10 @@ let parse_sexps (sexps : Sexp.t list) : t =
     ; if String.equal !logic ""
       then (logic := "LIA" ; Log.debug (lazy ("Using default logic: LIA")))
     ; let dups = List.filter !extra_variables ~f:(List.mem !variables ~equal:(fun x y -> String.equal (fst x) (fst y)))
-       in if dups <> [] then raise (Parse_Exn ( "Multiple declarations of ["
-                                              ^ (List.to_string_map dups ~sep:", " ~f:fst)
-                                              ^ "]"))
+       in if not (List.is_empty dups)
+          then raise (Parse_Exn ( "Multiple declarations of ["
+                                ^ (List.to_string_map dups ~sep:", " ~f:fst)
+                                ^ "]"))
           else { constants = !consts
                ; functions = List.rev !funcs
                ; logic = !logic

src/SyGuS_Opt.ml

@@ -42,8 +42,8 @@ let make_call_table (sygus : t) : func_info String.Table.t =
       in List.iter sygus.functions ~f:(fun func -> String.Table.set table ~key:func.name ~data:(init_info func))
        ; List.iter sygus.functions ~f:(fun func ->
            let parsed_expr = Parsexp.Single.parse_string_exn func.body in
-           let ops =  extract_operators parsed_expr in
-           let callees = List.filter ops ~f:(fun op -> String.Table.find table op <> None)
+           let ops = extract_operators parsed_expr in
+           let callees = List.filter ops ~f:(fun op -> not (Option.is_none (String.Table.find table op)))
             in String.Table.update table func.name
                                    ~f:(fun [@warning "-8"] (Some data) -> {data with callees ; parsed_expr}))
        ; String.Table.update table sygus.post_func.name
@@ -108,4 +108,4 @@ let optimize (sygus : t) : t =
                           (Int.to_string (List.length sygus.synth_variables)) ^
                           "): " ^
                           (List.to_string_map sygus.synth_variables ~sep:"; " ~f:fst)))
-       ; sygus
+       ; sygus

src/Synthesizer.ml

@@ -190,7 +190,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) =
     | Type.STRING  -> string_candidates
     | Type.LIST _  -> list_candidates
     | Type.ARRAY _ -> array_candidates
-    | Type.TVAR _ when no_tvar = false
+    | Type.TVAR _ when not no_tvar
       -> raise (Internal_Exn "No candidates for TVAR")
     | Type.TVAR _ -> let (@) = Array.append
                       in int_candidates @ bool_candidates @ char_candidates

src/Utils.ml

@@ -47,8 +47,8 @@ let get_in_channel = function
   | "-"      -> Stdio.In_channel.stdin
   | filename -> Stdio.In_channel.create filename
 
-let replace (bindings : Sexp.t list) (expr : Sexp.t) : Sexp.t =
-  if bindings = [] then expr else
+let replace bindings expr =
+  if List.is_empty bindings then expr else
   let open Sexp in
   let table = ref (String.Map.empty)
    in List.iter bindings
@@ -76,7 +76,7 @@ let make_user_features feature_strings vars : (string * string) list =
                                         | true -> None
                                         | _ -> Some fs)
    in begin
-     if feature_strings = [] then [] else
+     if List.is_empty feature_strings then [] else
      let decl_var (s,t) = "(" ^ s ^ " " ^ (Type.to_string t) ^ ")" in
      let var_decls = List.to_string_map vars ~sep:" " ~f:decl_var in
      let sign = " (" ^ var_decls ^ ") Bool "

src/ZProc.ml

@@ -57,8 +57,8 @@ let flush_and_collect (z3 : t) : string =
    ; let lines = ref [] in
      let rec read_line () : unit =
        let l = Option.value (In_channel.input_line z3.stdout) ~default:""
-        in if l = last_line then ()
-           else if l <> "" then (lines := l :: (!lines) ; read_line ())
+        in if String.equal l last_line then ()
+           else if not (String.equal l "") then (lines := l :: (!lines) ; read_line ())
        in read_line () ; lines := List.rev (!lines)
         ; Log.debug (lazy ("    " ^ (String.concat (!lines) ~sep:(Log.indented_sep 4))))
         ; String.concat ~sep:" " (!lines)
@@ -74,9 +74,9 @@ let close_scope (z3 : t) : unit =
 
 let run_queries ?(scoped = true) (z3 : t) ?(db = []) (queries : string list)
                 : string list =
-  if queries = []
+  if List.is_empty queries
   then begin
-    if not scoped && db <> [] then
+    if not scoped && not (List.is_empty db) then
       begin
         Log.debug (lazy (String.concat ("New z3 call:" :: db) ~sep:(Log.indented_sep 4)))
       ; Out_channel.output_lines z3.stdin db