diff options
| -rw-r--r-- | src/constraint.ml | 120 | ||||
| -rw-r--r-- | src/constraint.mli | 8 | ||||
| -rw-r--r-- | src/type_check.ml | 12 |
3 files changed, 75 insertions, 65 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index 79702340..7debc902 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -259,7 +259,15 @@ let save_digests () = DigestMap.iter output !known_problems; close_out out_chan -let call_smt' l vars constraints : smt_result = +let kopt_pair kopt = (kopt_kid kopt, unaux_kind (kopt_kind kopt)) + +let call_smt' l constraints : smt_result = + let vars = + kopts_of_constraint constraints + |> KOptSet.elements + |> List.map kopt_pair + |> List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty + in let problems = [constraints] in let smt_file, _ = smtlib_of_constraints l vars constraints in @@ -278,57 +286,61 @@ let call_smt' l vars constraints : smt_result = in let digest = Digest.string smt_file in - try - let result = DigestMap.find digest !known_problems in - result - with - | Not_found -> - begin - let (input_file, tmp_chan) = - try Filename.open_temp_file "constraint_" ".smt2" with - | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling SMT: " ^ msg)) - in - output_string tmp_chan smt_file; - close_out tmp_chan; - let status, smt_output = - try - let smt_out, smt_in, smt_err = Unix.open_process_full (!opt_solver.command ^ " " ^ input_file) (Unix.environment ()) in - let smt_output = - try List.combine problems (input_lines smt_out (List.length problems)) with - | End_of_file -> List.combine problems ["unknown"] - in - let status = Unix.close_process_full (smt_out, smt_in, smt_err) in - status, smt_output - with - | exn -> raise (Reporting.err_general l ("Error when calling smt: " ^ Printexc.to_string exn)) - in - let _ = match status with - | Unix.WEXITED 0 -> () - | Unix.WEXITED n -> - raise (Reporting.err_general l ("SMT solver returned unexpected status " ^ string_of_int n)) - | Unix.WSIGNALED n | Unix.WSTOPPED n -> - raise (Reporting.err_general l ("SMT solver killed by signal " ^ string_of_int n)) - in - Sys.remove input_file; - try - let (problem, _) = List.find (fun (_, result) -> result = "unsat") smt_output in - known_problems := DigestMap.add digest Unsat !known_problems; - Unsat - with - | Not_found -> - let unsolved = List.filter (fun (_, result) -> result = "unknown") smt_output in - if unsolved == [] - then (known_problems := DigestMap.add digest Sat !known_problems; Sat) - else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown) - end - -let call_smt l vars constraints = + + match DigestMap.find_opt digest !known_problems with + | Some result -> result + | None -> + let (input_file, tmp_chan) = + try Filename.open_temp_file "constraint_" ".smt2" with + | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling SMT: " ^ msg)) + in + output_string tmp_chan smt_file; + close_out tmp_chan; + let status, smt_output = + try + let smt_out, smt_in, smt_err = Unix.open_process_full (!opt_solver.command ^ " " ^ input_file) (Unix.environment ()) in + let smt_output = + try List.combine problems (input_lines smt_out (List.length problems)) with + | End_of_file -> List.combine problems ["unknown"] + in + let status = Unix.close_process_full (smt_out, smt_in, smt_err) in + status, smt_output + with + | exn -> + raise (Reporting.err_general l ("Error when calling smt: " ^ Printexc.to_string exn)) + in + let _ = match status with + | Unix.WEXITED 0 -> () + | Unix.WEXITED n -> + raise (Reporting.err_general l ("SMT solver returned unexpected status " ^ string_of_int n)) + | Unix.WSIGNALED n | Unix.WSTOPPED n -> + raise (Reporting.err_general l ("SMT solver killed by signal " ^ string_of_int n)) + in + Sys.remove input_file; + try + let (problem, _) = List.find (fun (_, result) -> result = "unsat") smt_output in + known_problems := DigestMap.add digest Unsat !known_problems; + Unsat + with + | Not_found -> + let unsolved = List.filter (fun (_, result) -> result = "unknown") smt_output in + if unsolved == [] + then (known_problems := DigestMap.add digest Sat !known_problems; Sat) + else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown) + +let call_smt l constraints = let t = Profile.start_smt () in - let result = call_smt' l vars constraints in + let result = call_smt' l constraints in Profile.finish_smt t; result -let solve_smt l vars constraints var = +let solve_smt l constraints var = + let vars = + kopts_of_constraint constraints + |> KOptSet.elements + |> List.map kopt_pair + |> List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty + in let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in let smt_var = pp_sexpr (smt_var var) in @@ -367,22 +379,22 @@ let solve_smt l vars constraints var = with | Not_found -> None -let solve_all_smt l vars constraints var = +let solve_all_smt l constraints var = let rec aux results = let constraints = List.fold_left (fun ncs r -> (nc_and ncs (nc_neq (nconstant r) (nvar var)))) constraints results in - match solve_smt l vars constraints var with + match solve_smt l constraints var with | Some result -> aux (result :: results) | None -> - match call_smt l vars constraints with + match call_smt l constraints with | Unsat -> Some results | _ -> None in aux [] -let solve_unique_smt l vars constraints var = - match solve_smt l vars constraints var with +let solve_unique_smt l constraints var = + match solve_smt l constraints var with | Some result -> - begin match call_smt l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with + begin match call_smt l (nc_and constraints (nc_neq (nconstant result) (nvar var))) with | Unsat -> Some result | _ -> None end diff --git a/src/constraint.mli b/src/constraint.mli index b5d6ff6b..34e83964 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -61,10 +61,10 @@ type smt_result = Unknown | Sat | Unsat val load_digests : unit -> unit val save_digests : unit -> unit -val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result +val call_smt : l -> n_constraint -> smt_result -val solve_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option +val solve_smt : l -> n_constraint -> kid -> Big_int.num option -val solve_all_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num list option +val solve_all_smt : l -> n_constraint -> kid -> Big_int.num list option -val solve_unique_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option +val solve_unique_smt : l -> n_constraint -> kid -> Big_int.num option diff --git a/src/type_check.ml b/src/type_check.ml index 48a64226..12832ad5 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1239,7 +1239,7 @@ end = struct else if KidSet.cardinal power_vars = 1 && !opt_smt_linearize then let v = KidSet.choose power_vars in let constrs = List.fold_left nc_and nc_true (get_constraints env) in - begin match Constraint.solve_all_smt l (get_typ_vars env) constrs v with + begin match Constraint.solve_all_smt l constrs v with | Some solutions -> typ_print (lazy (Util.("Linearizing " |> red |> clear) ^ string_of_n_constraint constr ^ " for " ^ string_of_kid v ^ " in " ^ Util.string_of_list ", " Big_int.to_string solutions)); @@ -1493,10 +1493,8 @@ which is then a problem we can feed to the constraint solver expecting unsat. *) let prove_smt env (NC_aux (_, l) as nc) = - let vars = Env.get_typ_vars env in - let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in let ncs = Env.get_constraints env in - match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs) with + match Constraint.call_smt l (List.fold_left nc_and (nc_not nc) ncs) with | Constraint.Unsat -> typ_debug (lazy "unsat"); true | Constraint.Sat -> typ_debug (lazy "sat"); false | Constraint.Unknown -> @@ -1504,7 +1502,7 @@ let prove_smt env (NC_aux (_, l) as nc) = constraints, even when such constraints are irrelevant *) let ncs' = List.concat (List.map constraint_conj ncs) in let ncs' = List.filter (fun nc -> KidSet.is_empty (constraint_power_variables nc)) ncs' in - match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs') with + match Constraint.call_smt l (List.fold_left nc_and (nc_not nc) ncs') with | Constraint.Unsat -> typ_debug (lazy "unsat"); true | Constraint.Sat | Constraint.Unknown -> typ_debug (lazy "sat/unknown"); false @@ -1518,7 +1516,7 @@ let solve_unique env (Nexp_aux (_, l) as nexp) = let vars = Env.get_typ_vars env in let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in - Constraint.solve_unique_smt l vars constr (mk_kid "solve#") + Constraint.solve_unique_smt l constr (mk_kid "solve#") let debug_pos (file, line, _, _) = "(" ^ file ^ "/" ^ string_of_int line ^ ") " @@ -2071,7 +2069,7 @@ let rec subtyp l env typ1 typ2 = let kids2 = KidSet.elements (KidSet.diff (KidSet.of_list kids2) (nexp_frees nexp2)) in if not (kids2 = []) then typ_error env l ("Universally quantified constraint generated: " ^ Util.string_of_list ", " string_of_kid kids2) else (); let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) (Env.get_typ_vars env) in - begin match Constraint.call_smt l vars (nc_eq nexp1 nexp2) with + begin match Constraint.call_smt l (nc_eq nexp1 nexp2) with | Constraint.Sat -> let env = Env.add_constraint (nc_eq nexp1 nexp2) env in if prove __POS__ env nc2 then |