From be651820e81c5601e7faf0b0b633f5610f9b99ff Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 27 Nov 2019 20:44:36 -0800 Subject: [PATCH 1/4] first pass --- LoopInvGen.opam | 8 ++++---- bin/Score.ml | 3 ++- src/Check.ml | 4 ++-- src/Job.ml | 12 +++++++----- src/LIG.ml | 16 ++++++++-------- src/PIE.ml | 12 ++++++------ src/Simulator.ml | 4 ++-- src/SyGuS.ml | 5 +++-- src/SyGuS_Opt.ml | 6 +++--- src/Synthesizer.ml | 2 +- src/Utils.ml | 4 ++-- src/ZProc.ml | 8 ++++---- 12 files changed, 44 insertions(+), 40 deletions(-) diff --git a/LoopInvGen.opam b/LoopInvGen.opam index 029b33b..0dffe6e 100644 --- a/LoopInvGen.opam +++ b/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"} +] \ No newline at end of file diff --git a/bin/Score.ml b/bin/Score.ml index 8ab6dce..44c0fdf 100644 --- a/bin/Score.ml +++ b/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 \ No newline at end of file diff --git a/src/Check.ml b/src/Check.ml index 295ebd2..7d331b0 100644 --- a/src/Check.ml +++ b/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 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)))) \ No newline at end of file diff --git a/src/Job.ml b/src/Job.ml index 21c810b..f0cc4e5 100644 --- a/src/Job.ml +++ b/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 ; - } + } \ No newline at end of file diff --git a/src/LIG.ml b/src/LIG.ml index da70526..aa29c17 100644 --- a/src/LIG.ml +++ b/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 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) \ No newline at end of file diff --git a/src/PIE.ml b/src/PIE.ml index 992235f..343066f 100644 --- a/src/PIE.ml +++ b/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,7 +95,7 @@ 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 @@ -103,7 +103,7 @@ let rec resolveSomeConflicts ?(config = Config.default) ?(consts = []) ~(job : J 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 \ No newline at end of file diff --git a/src/Simulator.ml b/src/Simulator.ml index f8fe799..d0bffad 100644 --- a/src/Simulator.ml +++ b/src/Simulator.ml @@ -26,7 +26,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))) @@ -63,7 +63,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) diff --git a/src/SyGuS.ml b/src/SyGuS.ml index 5b392ed..2f06b23 100644 --- a/src/SyGuS.ml +++ b/src/SyGuS.ml @@ -90,9 +90,10 @@ let parse_sexps (sexps : Sexp.t list) : t = in if List.mem !variables new_var ~equal:(fun x y -> String.equal (fst x) (fst y)) then raise (Parse_Exn ("Multiple declarations of variable " ^ (fst new_var))) else variables := new_var :: !variables + | List [ (Atom "declare-fun") ; name ; (List []) ; rtype ] + -> raise (Parse_Exn "Only nullary function (i.e. variable) declarations supported.") | List [ (Atom "declare-fun") ; name ; args ; rtype ] - -> if args <> List [] then raise (Parse_Exn "Only nullary function (i.e. variable) declarations supported.") else - let new_var = parse_variable_declaration (List [name ; rtype]) + -> let new_var = parse_variable_declaration (List [name ; rtype]) in if List.mem !variables new_var ~equal:(fun x y -> String.equal (fst x) (fst y)) then raise (Parse_Exn ("Multiple declarations of variable " ^ (fst new_var))) else variables := new_var :: !variables diff --git a/src/SyGuS_Opt.ml b/src/SyGuS_Opt.ml index 6a61643..e16f5e8 100644 --- a/src/SyGuS_Opt.ml +++ b/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 \ No newline at end of file diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml index 129675d..b9df624 100644 --- a/src/Synthesizer.ml +++ b/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 diff --git a/src/Utils.ml b/src/Utils.ml index 00e4094..57b6edd 100644 --- a/src/Utils.ml +++ b/src/Utils.ml @@ -48,7 +48,7 @@ let get_in_channel = function | filename -> Stdio.In_channel.create filename let replace bindings expr = - if bindings = [] then expr else + if List.is_empty bindings then expr else let table = ref (String.Map.empty) in List.iter bindings ~f:(function [@warning "-8"] @@ -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 " diff --git a/src/ZProc.ml b/src/ZProc.ml index 9ce5c34..d725345 100644 --- a/src/ZProc.ml +++ b/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 From e4868adad23e016e21d0518e0a43e85be91fbaa3 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 27 Nov 2019 21:28:07 -0800 Subject: [PATCH 2/4] fix --- .travis.yml | 8 ++------ .travis/run.sh | 4 ++-- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/.travis.yml b/.travis.yml index 2352b8f..85ef114 100644 --- a/.travis.yml +++ b/.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 diff --git a/.travis/run.sh b/.travis/run.sh index 47037c4..d46bc99 100755 --- a/.travis/run.sh +++ b/.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 From 29fd269e59c29ffb970d2a5372100c92aa459f15 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Fri, 29 Nov 2019 22:12:03 -0800 Subject: [PATCH 3/4] fix --- .travis/run.sh | 2 +- Dockerfile | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.travis/run.sh b/.travis/run.sh index d46bc99..f444dc4 100755 --- a/.travis/run.sh +++ b/.travis/run.sh @@ -29,4 +29,4 @@ pwd ; ls -lah dune build --verbose dune build test/Runner.exe --verbose -dune build app/App.exe \ No newline at end of file +dune build app/App.exe --verbose \ No newline at end of file diff --git a/Dockerfile b/Dockerfile index 12324ea..ed40254 100644 --- a/Dockerfile +++ b/Dockerfile @@ -41,9 +41,9 @@ WORKDIR $HOME RUN opam install --yes alcotest.0.8.5 \ - core.v0.12.4 \ + core.v0.13.0 \ dune.1.11.4 \ - ppx_let.v0.12.0 \ + ppx_let.v0.13.0 \ && \ opam clean --yes && \ git clone https://github.com/SaswatPadhi/LoopInvGen.git From 7e478a53e3eb1a24b0f7b80642935d7211fa3d8f Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Tue, 14 Jan 2020 02:49:12 -0800 Subject: [PATCH 4/4] minor --- Dockerfile | 4 ++-- src/Check.ml | 2 +- src/LIG.ml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Dockerfile b/Dockerfile index ed40254..de04793 100644 --- a/Dockerfile +++ b/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 @@ -42,7 +42,7 @@ WORKDIR $HOME RUN opam install --yes alcotest.0.8.5 \ core.v0.13.0 \ - dune.1.11.4 \ + dune.2.1.2 \ ppx_let.v0.13.0 \ && \ opam clean --yes && \ diff --git a/src/Check.ml b/src/Check.ml index 7d331b0..f974df7 100644 --- a/src/Check.ml +++ b/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 Option.is_none (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body) + 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 ]) ; diff --git a/src/LIG.ml b/src/LIG.ml index aa29c17..5dcfd3f 100644 --- a/src/LIG.ml +++ b/src/LIG.ml @@ -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 Option.is_none (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body) + ; 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) \ No newline at end of file