diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/constraint.ml | 2 | ||||
| -rw-r--r-- | src/constraint.mli | 2 | ||||
| -rw-r--r-- | src/monomorphise.ml | 16 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 4 | ||||
| -rw-r--r-- | src/type_check.mli | 2 |
6 files changed, 14 insertions, 14 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index 09091655..2c5150a5 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -321,7 +321,7 @@ let call_smt l vars constraints = Profile.finish_smt t; result -let rec solve_smt l vars constraints var = +let rec solve_unique_smt l vars constraints var = let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in let smt_var = pp_sexpr (smt_var var) in diff --git a/src/constraint.mli b/src/constraint.mli index e86c764a..fb6e0fcd 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -63,4 +63,4 @@ val save_digests : unit -> unit val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result -val solve_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option +val solve_unique_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 8c52fce1..acc31456 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2263,7 +2263,7 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) = prove __POS__ env (NC_aux (NC_equal (size,nexp), Parse_ast.Unknown)) in if is_nexp_constant size then size else - match solve env size with + match solve_unique env size with | Some n -> nconstant n | None -> match List.find is_equal bound_nexps with @@ -2930,7 +2930,7 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps = | _ -> None let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) = - match solve typ_env nexp with + match solve_unique typ_env nexp with | Some n -> nconstant n | None -> let is_equal kid = @@ -3691,7 +3691,7 @@ let rec rewrite_app env typ (id,args) = let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in match size with | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp) - | _ -> match solve env size with + | _ -> match solve_unique env size with | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp) | None -> e in @@ -3711,7 +3711,7 @@ let rec rewrite_app env typ (id,args) = let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in let midsize = nminus size size1 in begin - match solve env midsize with + match solve_unique env midsize with | Some c -> let midtyp = vector_typ (nconstant c) order bittyp in E_app (append, @@ -3739,7 +3739,7 @@ let rec rewrite_app env typ (id,args) = let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in let midsize = nminus size size1 in begin - match solve env midsize with + match solve_unique env midsize with | Some c -> let midtyp = vector_typ (nconstant c) order bittyp in E_app (append, @@ -3797,7 +3797,7 @@ let rec rewrite_app env typ (id,args) = let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in let midsize = nminus size size1 in begin - match solve env midsize with + match solve_unique env midsize with | Some c -> let midtyp = vector_typ (nconstant c) order bittyp in try_cast_to_typ @@ -4000,7 +4000,7 @@ struct let simplify_size_nexp env quant_kids nexp = let rec aux (Nexp_aux (ne,l) as nexp) = - match solve env nexp with + match solve_unique env nexp with | Some n -> Some (nconstant n) | None -> let is_equal kid = @@ -4191,7 +4191,7 @@ let fill_in_type env typ = | K_order | K_bool -> subst | K_int -> - (match solve env (nvar kid) with + (match solve_unique env (nvar kid) with | None -> subst | Some n -> KBindings.add kid (nconstant n) subst)) tyvars KBindings.empty in subst_src_typ subst typ diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 3e7911fe..9d472e15 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -359,7 +359,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let mk_typ nexp = Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) in - match Type_check.solve env size with + match Type_check.solve_unique env size with | Some n -> mk_typ (nconstant n) | None -> let is_equal nexp = diff --git a/src/type_check.ml b/src/type_check.ml index 0c936860..ada04c24 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1405,7 +1405,7 @@ let prove_smt env (NC_aux (_, l) as nc) = | Constraint.Unsat -> typ_debug (lazy "unsat"); true | Constraint.Sat | Constraint.Unknown -> typ_debug (lazy "sat/unknown"); false -let solve env (Nexp_aux (_, l) as nexp) = +let solve_unique env (Nexp_aux (_, l) as nexp) = typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_nexp nexp ^ " = ?")); match nexp with @@ -1415,7 +1415,7 @@ let solve 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_smt l vars constr (mk_kid "solve#") + Constraint.solve_unique_smt l vars constr (mk_kid "solve#") let debug_pos (file, line, _, _) = "(" ^ file ^ "/" ^ string_of_int line ^ ") " diff --git a/src/type_check.mli b/src/type_check.mli index 8ea0b3e2..00439412 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -316,7 +316,7 @@ val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t untrustworthy. *) val prove : (string * int * int * int) -> Env.t -> n_constraint -> bool -val solve : Env.t -> nexp -> Big_int.num option +val solve_unique : Env.t -> nexp -> Big_int.num option val canonicalize : Env.t -> typ -> typ |