Fix unification missing variables in generated SMT

Some SMT goals in unification would generate problems with missing
variables. Turns out the SMT solver would happily ignore this and
return the correct unsat/sat result anyway. However, this does affect
the error code from the solver so if we now check the return code we
must make sure that we don't generate any smtlib files that generate
warnings or errors.

Now that kopts_of_X functions exist in ast_util we can just use those
to get well-kinded variables from the constraint itself rather than
relying on the typechecker to pass in a list of variables which makes
things simpler to boot!

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