Skip to content
This repository was archived by the owner on Mar 16, 2024. It is now read-only.

Commit 6b55131

Browse files
SaswatPadhiSaswatPadhi
committed
first pass
1 parent 2b8704c commit 6b55131

11 files changed

Lines changed: 38 additions & 34 deletions

File tree

‎LoopInvGen.opam‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@ build: [
2222
]
2323

2424
depends: [
25-
"ocaml" {>= "4.07"}
25+
"ocaml" {>= "4.08"}
2626
"dune" {>= "1.6" & build}
2727
"alcotest" {>= "0.8" & with-test}
28-
"core" {>= "v0.12.2" & <= "v0.13"}
29-
"ppx_let" {>= "v0.12.0" & <= "v0.13"}
30-
]
28+
"core" {>= "v0.13" & <= "v0.14"}
29+
"ppx_let" {>= "v0.13" & <= "v0.14"}
30+
]

‎bin/Score.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ open Core
33
open LoopInvGen
44

55
let time_pseudolog x =
6+
let open Float in
67
if x > 3600.0 then 1
78
else if x >= 1000.0 then 2
89
else if x >= 300.0 then 3

‎src/Check.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ let is_sufficient_invariant ~(zpath : string) ~(sygus : SyGuS.t) (inv : string)
88
let open ZProc
99
in process ~zpath (fun z3 ->
1010
Simulator.setup sygus z3 ;
11-
if (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body) <> None
11+
if Option.is_none (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body)
1212
then (if String.equal inv "false" then NO_SOLUTION_PASS else NO_SOLUTION_FAIL)
1313
else let inv = SyGuS.func_definition {sygus.inv_func with body = inv}
1414
in ignore (run_queries ~scoped:false z3 [] ~db:[ inv ]) ;
@@ -26,5 +26,5 @@ let is_sufficient_invariant ~(zpath : string) ~(sygus : SyGuS.t) (inv : string)
2626
with
2727
| [ None ; None ; None ] -> PASS
2828
| x -> FAIL (List.filter_mapi x
29-
~f:(fun i v -> if v = None then None
29+
~f:(fun i v -> if Option.is_none v then None
3030
else Some [| "pre" ; "trans" ; "post" |].(i))))

‎src/Job.ml‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ type ('a, 'b) _t = {
2020

2121
type t = (Value.t list, Value.t) _t
2222

23+
let are_values_equal = List.equal Value.equal
24+
2325
let compute_feature_value (test : 'a) (feature : 'a feature with_desc) : bool =
2426
try (fst feature) test with _ -> false
2527
[@@inline always]
@@ -50,11 +52,11 @@ let create_unlabeled ~f ~args ~post ?(features = []) tests : t =
5052
in create ~f ~args ~post ~features ~pos_tests ~neg_tests ()
5153

5254
let add_pos_test ~(job : t) (test : Value.t list) : t =
53-
if List.exists job.pos_tests ~f:(fun (pt, _) -> pt = test)
55+
if List.exists job.pos_tests ~f:(fun (pt, _) -> are_values_equal pt test)
5456
then raise (Duplicate_Test ("New POS test (" ^ (String.concat ~sep:"," job.farg_names)
5557
^ ") = (" ^ (List.to_string_map ~sep:"," ~f:Value.to_string test)
5658
^ "), already exists in POS set!"))
57-
else if List.exists job.neg_tests ~f:(fun (nt, _) -> nt = test)
59+
else if List.exists job.neg_tests ~f:(fun (nt, _) -> are_values_equal nt test)
5860
then raise (Ambiguous_Test ("New POS test (" ^ (String.concat ~sep:"," job.farg_names)
5961
^ ") = (" ^ (List.to_string_map ~sep:"," ~f:Value.to_string test)
6062
^ ") already exists in NEG set!"))
@@ -70,11 +72,11 @@ let add_pos_test ~(job : t) (test : Value.t list) : t =
7072
^ "), does not belong in POS set!"))
7173

7274
let add_neg_test ~(job : t) (test : Value.t list) : t =
73-
if List.exists job.neg_tests ~f:(fun (nt, _) -> nt = test)
75+
if List.exists job.neg_tests ~f:(fun (nt, _) -> are_values_equal nt test)
7476
then raise (Duplicate_Test ("New NEG test (" ^ (String.concat ~sep:"," job.farg_names)
7577
^ ") = (" ^ (List.to_string_map ~sep:"," ~f:Value.to_string test)
7678
^ ") already exists in NEG set!"))
77-
else if List.exists job.pos_tests ~f:(fun (pt, _) -> pt = test)
79+
else if List.exists job.pos_tests ~f:(fun (pt, _) -> are_values_equal pt test)
7880
then raise (Ambiguous_Test ("New NEG test (" ^ (String.concat ~sep:"," job.farg_names)
7981
^ ") = (" ^ (List.to_string_map ~sep:"," ~f:Value.to_string test)
8082
^ ") already exists in POS set!"))

‎src/LIG.ml‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ let satisfyTrans ?(config = Config.default) ~(sygus : SyGuS.t) ~(z3 : ZProc.t)
3939
let invf'_call =
4040
"(invf " ^ (List.to_string_map sygus.inv_func.args ~sep:" "
4141
~f:(fun (s, _) -> s ^ "!")) ^ ")" in
42-
let eval_term = (if not (config.model_completion_mode = `UsingZ3) then "true"
42+
let eval_term = (if not (Poly.equal config.model_completion_mode `UsingZ3) then "true"
4343
else "(and " ^ invf_call ^ " " ^ sygus.trans_func.body ^ ")") in
4444
let rec helper inv =
4545
Log.info (lazy ("IND >> Strengthening for inductiveness:"
@@ -64,7 +64,7 @@ let satisfyTrans ?(config = Config.default) ~(sygus : SyGuS.t) ~(z3 : ZProc.t)
6464
~features: (List.map ~f:(fun (_, name) -> ( (ZProc.build_feature name z3)
6565
, ("(" ^ name ^ " " ^ all_state_vars ^ ")")))
6666
config.user_features)
67-
~post:(fun _ res -> res = Ok (Value.Bool false)))
67+
~post:(fun _ -> function Ok (Value.Bool false) -> true | _ -> false))
6868
in ZProc.close_scope z3
6969
; Log.debug (lazy ("IND Delta: " ^ pre_inv))
7070
; if String.equal pre_inv "true"
@@ -76,7 +76,7 @@ let satisfyTrans ?(config = Config.default) ~(sygus : SyGuS.t) ~(z3 : ZProc.t)
7676
in Log.info (lazy ("PRE >> Checking if the following candidate is weaker than precond:"
7777
^ (Log.indented_sep 4) ^ new_inv))
7878
; let ce = ZProc.implication_counter_example z3 sygus.pre_func.body new_inv
79-
in if ce = None then helper new_inv else (new_inv, ce))
79+
in if Option.is_none ce then helper new_inv else (new_inv, ce))
8080
in helper inv
8181

8282
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
111111
VPIE.learnVPreCond
112112
~z3 ~config:config._VPIE ~consts:sygus.constants
113113
~post_desc:sygus.post_func.body
114-
~eval_term:(if not (config.model_completion_mode = `UsingZ3)
114+
~eval_term:(if not (Poly.equal config.model_completion_mode `UsingZ3)
115115
then "true" else sygus.post_func.body)
116116
(Job.create ()
117117
~pos_tests:states
@@ -121,7 +121,7 @@ let rec learnInvariant_internal ?(config = Config.default) ~(states : Value.t li
121121
else ("(not (" ^ sygus.post_func.body ^ "))"))
122122
~z3 ~arg_names:(List.map sygus.synth_variables ~f:fst))
123123
~args: sygus.synth_variables
124-
~post: (fun _ res -> res = Ok (Value.Bool false)))
124+
~post:(fun _ -> function Ok (Value.Bool false) -> true | _ -> false))
125125
in stats.lig_time_ms <- stats.lig_time_ms +. vpie_stats.vpi_time_ms
126126
; stats.lig_ce <- stats.lig_ce + vpie_stats.vpi_ce
127127
; stats._VPIE <- vpie_stats :: stats._VPIE
@@ -137,7 +137,7 @@ let rec learnInvariant_internal ?(config = Config.default) ~(states : Value.t li
137137
^ (Log.indented_sep 4) ^ inv))
138138
; match satisfyTrans ~config ~sygus ~states ~z3 inv stats with
139139
| inv, None
140-
-> if inv <> "false" then ((ZProc.simplify z3 inv), stats)
140+
-> if not (String.equal inv "false") then ((ZProc.simplify z3 inv), stats)
141141
else restart_with_new_states (random_value ~seed:(`Deterministic seed_string)
142142
(gen_pre_state ~use_trans:true sygus z3))
143143
| _, (Some ce_model)
@@ -152,6 +152,6 @@ let learnInvariant ?(config = Config.default) ~(states : Value.t list list)
152152
~random_seed:(Some (Int.to_string (Quickcheck.(random_value ~seed:(`Deterministic config.base_random_seed)
153153
(Generator.small_non_negative_int)))))
154154
(fun z3 -> Simulator.setup sygus z3 ~user_features:(List.map ~f:fst config.user_features)
155-
; if (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body) <> None
155+
; if Option.is_none (implication_counter_example z3 sygus.pre_func.body sygus.post_func.body)
156156
then ("false", stats)
157157
else learnInvariant_internal ~config ~states sygus config.base_random_seed z3 stats)

‎src/PIE.ml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -38,13 +38,13 @@ type stats = {
3838
let conflictingTests (job : Job.t) : 'a conflict list =
3939
let make_f_vecs = List.map ~f:(fun (t, fvec) -> (t, Lazy.force fvec)) in
4040
let make_groups tests =
41-
List.group tests ~break:(fun (_, fv1) (_, fv2) -> fv1 <> fv2)
41+
List.group tests ~break:(fun (_, fv1) (_, fv2) -> not (List.equal Bool.equal fv1 fv2))
4242
in let (p_groups, n_groups) = (make_groups (make_f_vecs job.pos_tests),
4343
make_groups (make_f_vecs job.neg_tests))
4444
in List.(filter_map
4545
p_groups
4646
~f:(fun [@warning "-8"] (((_, pfv) :: _) as ptests) ->
47-
match find n_groups ~f:(fun ((_, nfv) :: _) -> nfv = pfv) with
47+
match find n_groups ~f:(fun ((_, nfv) :: _) -> List.equal Bool.equal nfv pfv) with
4848
| None -> None
4949
| Some ntests -> Some { pos = map ~f:fst ptests
5050
; neg = map ~f:fst ntests
@@ -65,7 +65,7 @@ let synthFeature ?(consts = []) ~(job : Job.t) ~(config : Synthesizer.Config.t)
6565
} in stats._Synthesizer <- result.stats :: stats._Synthesizer
6666
; stats.pi_time_ms <- stats.pi_time_ms +. result.stats.synth_time_ms
6767
; ((fun values -> try Value.equal (result.func values) (Value.Bool true) with _ -> false),
68-
(if result.constraints = [] then result.string
68+
(if List.is_empty result.constraints then result.string
6969
else "(and " ^ result.string ^ (String.concat ~sep:" " result.constraints) ^ ")"))
7070

7171
let resolveAConflict ?(config = Config.default) ?(consts = []) ~(job : Job.t)
@@ -95,15 +95,15 @@ let resolveAConflict ?(config = Config.default) ?(consts = []) ~(job : Job.t)
9595
let rec resolveSomeConflicts ?(config = Config.default) ?(consts = []) ~(job : Job.t)
9696
(conflict_groups : Value.t list conflict list) stats
9797
: Value.t list Job.feature Job.with_desc option =
98-
if conflict_groups = [] then None
98+
if List.is_empty conflict_groups then None
9999
else try Some (resolveAConflict (List.hd_exn conflict_groups) ~config ~consts ~job stats)
100100
with e -> Log.error (lazy ((Exn.to_string e) ^ (Printexc.get_backtrace ())))
101101
; resolveSomeConflicts (List.tl_exn conflict_groups) ~config ~consts ~job stats
102102

103103
let rec augmentFeatures ?(config = Config.default) ?(consts = []) (job : Job.t)
104104
stats : Job.t =
105105
let conflict_groups = conflictingTests job
106-
in if conflict_groups = [] then job
106+
in if List.is_empty conflict_groups then job
107107
else if config.disable_synth
108108
then (Log.error (lazy ("CONFLICT RESOLUTION FAILED")) ; raise NoSuchFunction)
109109
else match resolveSomeConflicts conflict_groups ~job ~config ~consts stats with

‎src/Simulator.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ let gen_state_from_model (s : SyGuS.t) (m : ZProc.model option)
2626
| Some m -> create (fun ~size ~random -> Some (
2727
List.map s.synth_variables
2828
~f:(fun (v, t) ->
29-
match List.Assoc.find m v ~equal:(=)
29+
match List.Assoc.find m v ~equal:String.equal
3030
with Some d -> d
3131
| None -> generate (TestGen.for_type t) ~size ~random)))
3232

@@ -63,7 +63,7 @@ let simulate_from (s : SyGuS.t) (z3 : ZProc.t) (head : Value.t list option)
6363
head :: (match size with
6464
| 0 -> []
6565
| n -> begin match generate (transition s z3 head) ~size ~random
66-
with Some next when next <> head
66+
with Some next when not (List.equal Value.equal next head)
6767
-> step_internal next (n-1)
6868
| _ -> []
6969
end)

‎src/SyGuS.ml‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ type t = {
3131
}
3232

3333
let replace bindings expr =
34-
if bindings = [] then expr else
34+
if List.is_empty bindings then expr else
3535
let table = ref (String.Map.empty)
3636
in List.iter bindings
3737
~f:(function [@warning "-8"]
@@ -111,9 +111,10 @@ let parse_sexps (sexps : Sexp.t list) : t =
111111
in if List.mem !variables new_var ~equal:(fun x y -> String.equal (fst x) (fst y))
112112
then raise (Parse_Exn ("Multiple declarations of variable " ^ (fst new_var)))
113113
else variables := new_var :: !variables
114+
| List [ (Atom "declare-fun") ; name ; (List []) ; rtype ]
115+
-> raise (Parse_Exn "Only nullary function (i.e. variable) declarations supported.")
114116
| List [ (Atom "declare-fun") ; name ; args ; rtype ]
115-
-> if args <> List [] then raise (Parse_Exn "Only nullary function (i.e. variable) declarations supported.") else
116-
let new_var = parse_variable_declaration (List [name ; rtype])
117+
-> let new_var = parse_variable_declaration (List [name ; rtype])
117118
in if List.mem !variables new_var ~equal:(fun x y -> String.equal (fst x) (fst y))
118119
then raise (Parse_Exn ("Multiple declarations of variable " ^ (fst new_var)))
119120
else variables := new_var :: !variables

‎src/SyGuS_Opt.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@ let make_call_table (sygus : t) : func_info String.Table.t =
4242
in List.iter sygus.functions ~f:(fun func -> String.Table.set table ~key:func.name ~data:(init_info func))
4343
; List.iter sygus.functions ~f:(fun func ->
4444
let parsed_expr = Parsexp.Single.parse_string_exn func.body in
45-
let ops = extract_operators parsed_expr in
46-
let callees = List.filter ops ~f:(fun op -> String.Table.find table op <> None)
45+
let ops = extract_operators parsed_expr in
46+
let callees = List.filter ops ~f:(fun op -> not (Option.is_none (String.Table.find table op)))
4747
in String.Table.update table func.name
4848
~f:(fun [@warning "-8"] (Some data) -> {data with callees ; parsed_expr}))
4949
; String.Table.update table sygus.post_func.name

‎src/Utils.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ let make_user_features feature_strings vars : (string * string) list =
4848
| true -> None
4949
| _ -> Some fs)
5050
in begin
51-
if feature_strings = [] then [] else
51+
if List.is_empty feature_strings then [] else
5252
let decl_var (s,t) = "(" ^ s ^ " " ^ (Type.to_string t) ^ ")" in
5353
let var_decls = List.to_string_map vars ~sep:" " ~f:decl_var in
5454
let sign = " (" ^ var_decls ^ ") Bool "

0 commit comments

Comments
 (0)