From a1d7dc8a237dbbc5eacbec71ca2a258bc48b4234 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 29 Apr 2020 20:32:40 +0100 Subject: Add progress reporting to monomorphisation --- src/monomorphise.ml | 31 +++++++++++++++++++++---------- 1 file changed, 21 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 8c10b63f..5fce15f7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1147,7 +1147,9 @@ let split_defs target all_errors splits env defs = List.map (fun fcl' -> SD_aux (SD_funcl fcl', annot)) (map_funcl fcl) | _ -> [sd] in - let map_def d = + let num_defs = List.length defs in + let map_def idx d = + Util.progress "Monomorphising " (string_of_int idx ^ "/" ^ string_of_int num_defs) idx num_defs; match d with | DEF_type _ | DEF_spec _ @@ -1168,10 +1170,11 @@ let split_defs target all_errors splits env defs = Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should have been rewritten before now" in - Defs (List.concat (List.map map_def defs)) + Defs (List.concat (List.mapi map_def defs)) in - let defs'' = map_locs splits defs' in - !no_errors_happened, defs'' + let (Defs defs'') = map_locs splits defs' in + Util.progress "Monomorphising " "done" (List.length defs'') (List.length defs''); + !no_errors_happened, (Defs defs'') @@ -2725,11 +2728,17 @@ let argset_to_list splits = List.map argelt l let analyse_defs debug env (Defs defs) = - let def (globals,r) d = + let def (idx,globals,r) d = + begin match d with + | DEF_fundef fd -> + Util.progress "Analysing " (string_of_id (id_of_fundef fd)) idx (List.length defs) + | _ -> () + end; let globals,r' = analyse_def debug env globals d in - globals, merge r r' + idx + 1, globals, merge r r' in - let _,r = List.fold_left def (Bindings.empty,empty) defs in + let _,_,r = List.fold_left def (0,Bindings.empty,empty) defs in + let _ = Util.progress "Analysing " "done" (List.length defs) (List.length defs) in (* Resolve the interprocedural dependencies *) @@ -3770,13 +3779,15 @@ let add_bitvector_casts global_env (Defs defs) = let pexp = construct_pexp (pat,guard,body,annot) in FCL_aux (FCL_Funcl (id,pexp),fcl_ann) in - let rewrite_def = function - | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),fd_ann)) -> + let rewrite_def idx = function + | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),fd_ann) as fd) -> + Util.progress "Adding casts " (string_of_id (id_of_fundef fd)) idx (List.length defs); DEF_fundef (FD_aux (FD_function (r,t,e,List.map rewrite_funcl fcls),fd_ann)) | d -> d in specs_required := IdSet.empty; - let defs = List.map rewrite_def defs in + let defs = List.mapi rewrite_def defs in + let _ = Util.progress "Adding casts " "done" (List.length defs) (List.length defs) in let l = Generated Unknown in let Defs cast_specs,_ = (* TODO: use default/relevant order *) -- cgit v1.2.3 From 929469c81d863703aa5817bbbd92c697eca3af26 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 4 May 2020 17:53:12 +0100 Subject: Try to fix bug in size parameter rewriting If we call a function where some arguments need to be rewritten, we might need to rewrite those parameters in the caller as well. --- src/monomorphise.ml | 61 +++++++++++++++++++++++++++++++++++------------------ 1 file changed, 41 insertions(+), 20 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 5fce15f7..4d2ade50 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1394,31 +1394,52 @@ let rewrite_size_parameters target type_env (Defs defs) = print_endline ("Nexp map for " ^ string_of_id id); List.iter (fun (nexp, i) -> print_endline (" " ^ string_of_nexp nexp ^ " -> " ^ string_of_int i)) nexp_list in *) - let parameters_for tannot = - match destruct_tannot tannot with - | Some (env,typ,_) -> - begin match Env.base_typ_of env typ with - | Typ_aux (Typ_app (Id_aux (Id "bitvector",_), [A_aux (A_nexp size,_);_]),_) - when not (is_nexp_constant size) -> - begin - match NexpMap.find size nexp_map with - | i -> IntSet.singleton i - | exception Not_found -> - (* Look for equivalent nexps, but only in consistent type env *) - if prove __POS__ env (NC_aux (NC_false,Unknown)) then IntSet.empty else - match List.find (fun (nexp,i) -> - prove __POS__ env (NC_aux (NC_equal (nexp,size),Unknown))) nexp_list with - | _, i -> IntSet.singleton i - | exception Not_found -> IntSet.empty + let parameters_for e tannot = + let parameters_for_nexp env size = + match solve_unique env size with + | Some _ -> IntSet.empty + | None -> + match NexpMap.find size nexp_map with + | i -> IntSet.singleton i + | exception Not_found -> + (* Look for equivalent nexps, but only in consistent type env *) + if prove __POS__ env (NC_aux (NC_false,Unknown)) then IntSet.empty else + match List.find (fun (nexp,i) -> + prove __POS__ env (NC_aux (NC_equal (nexp,size),Unknown))) nexp_list with + | _, i -> IntSet.singleton i + | exception Not_found -> IntSet.empty + in + let parameters_for_typ = + match destruct_tannot tannot with + | Some (env,typ,_) -> + begin match Env.base_typ_of env typ with + | Typ_aux (Typ_app (Id_aux (Id "bitvector",_), [A_aux (A_nexp size,_);_]),_) + when not (is_nexp_constant size) -> + parameters_for_nexp env size + | _ -> IntSet.empty end - | _ -> IntSet.empty - end - | None -> IntSet.empty + | None -> IntSet.empty + in + let parameters_for_exp = match e with + | E_app (id, args) when Bindings.mem id fsizes -> + let add_arg (i, s) arg = + if IntSet.mem i (fst (Bindings.find id fsizes)) then + try match destruct_numeric (typ_of arg) with + | Some ([], _, nexp) -> + (i + 1, IntSet.union s (parameters_for_nexp env nexp)) + | _ -> (i + 1, s) + with _ -> (i + 1, s) + else (i + 1, s) + in + snd (List.fold_left add_arg (0, IntSet.empty) args) + | _ -> IntSet.empty + in + IntSet.union parameters_for_typ parameters_for_exp in let parameters_to_rewrite = fst (fold_pexp { (compute_exp_alg IntSet.empty IntSet.union) with - e_aux = (fun ((s,e),(l,annot)) -> IntSet.union s (parameters_for annot),E_aux (e,(l,annot))) + e_aux = (fun ((s,e),(l,annot)) -> IntSet.union s (parameters_for e annot),E_aux (e,(l,annot))) } pexp) in let new_nexps = NexpSet.of_list (List.map fst -- cgit v1.2.3 From dc674a7320e4684e4dbe3ccf618c644bd83796ca Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 4 May 2020 17:57:49 +0100 Subject: Mono: Try to fix bug in inter-procedural analysis The monomorphisation analysis decides whether to split function arguments in the callee or in callers. The code previously used a datastructure that can hold results of either the one case or the other, but there might be functions that are called in different contexts leading to different decisions. This patch changes the datastructure to support storing all instances of either case. --- src/monomorphise.ml | 58 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 36 insertions(+), 22 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4d2ade50..465ed30f 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1749,9 +1749,19 @@ let string_of_dep = function (* If a callee uses a type variable as a size, does it need to be split in the current function, or is it also a parameter? (Note that there may be multiple calls, so more than one parameter can be involved) *) -type call_dep = - | InFun of dependencies - | Parents of CallerKidSet.t +type call_dep = { + in_fun : dependencies option; + parents : CallerKidSet.t; +} + +let empty_call_dep = { + in_fun = None; + parents = CallerKidSet.empty; +} + +let in_fun_call_dep deps = { in_fun = Some deps; parents = CallerKidSet.empty } + +let parents_call_dep cks = { in_fun = None; parents = cks } (* Result of analysing the body of a function. The split field gives the arguments to split based on the body alone, the extra_splits @@ -1811,17 +1821,16 @@ let dep_bindings_merge a1 a2 = let dep_kbindings_merge a1 a2 = KBindings.merge (opt_merge dmerge) a1 a2 +let call_dep_merge k d1 d2 = { + in_fun = opt_merge dmerge k d1.in_fun d2.in_fun; + parents = CallerKidSet.union d1.parents d2.parents +} + let call_kid_merge k x y = match x, y with | None, x -> x | x, None -> x - | Some (InFun deps), Some (Parents _) - | Some (Parents _), Some (InFun deps) - -> Some (InFun deps) - | Some (InFun deps), Some (InFun deps') - -> Some (InFun (dmerge deps deps')) - | Some (Parents fns), Some (Parents fns') - -> Some (Parents (CallerKidSet.union fns fns')) + | Some d1, Some d2 -> Some (call_dep_merge k d1 d2) let call_arg_merge k args args' = match args, args' with @@ -1989,11 +1998,11 @@ and deps_of_typ_arg l fn_id env arg_deps (A_aux (aux, _)) = match aux with | A_nexp (Nexp_aux (Nexp_var kid,_)) when List.exists (fun k -> Kid.compare kid k == 0) env.top_kids -> - Parents (CallerKidSet.singleton (fn_id,kid)) - | A_nexp nexp -> InFun (deps_of_nexp l env.kid_deps arg_deps nexp) - | A_order _ -> InFun dempty - | A_typ typ -> InFun (deps_of_typ l env.kid_deps arg_deps typ) - | A_bool nc -> InFun (deps_of_nc env.kid_deps nc) + parents_call_dep (CallerKidSet.singleton (fn_id,kid)) + | A_nexp nexp -> in_fun_call_dep (deps_of_nexp l env.kid_deps arg_deps nexp) + | A_order _ -> in_fun_call_dep dempty + | A_typ typ -> in_fun_call_dep (deps_of_typ l env.kid_deps arg_deps typ) + | A_bool nc -> in_fun_call_dep (deps_of_nc env.kid_deps nc) let mk_subrange_pattern vannot vstart vend = let (len,ord,typ) = vector_typ_args_of (Env.base_typ_of (env_of_annot vannot) (typ_of_annot vannot)) in @@ -2221,7 +2230,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let rdep,r' = if Id.compare fn_id id == 0 then let bad = Unknown (l,"Recursive call of " ^ string_of_id id) in - let kid_deps = KBindings.map (fun _ -> InFun bad) kid_deps in + let kid_deps = KBindings.map (fun _ -> in_fun_call_dep bad) kid_deps in bad, { empty with split_on_call = Bindings.singleton id kid_deps } else dempty, { empty with split_on_call = Bindings.singleton id kid_deps } in @@ -2683,11 +2692,12 @@ let print_set_assertions set_assertions = let print_result r = let _ = print_endline (" splits: " ^ string_of_argsplits r.split) in let print_kbinding kid dep = - let s = match dep with - | InFun dep -> "InFun " ^ string_of_dep dep - | Parents cks -> string_of_callerkidset cks + let s1 = match dep.in_fun with + | Some dep -> "InFun " ^ string_of_dep dep + | None -> "" in - let _ = print_endline (" " ^ string_of_kid kid ^ ": " ^ s) in + let s2 = string_of_callerkidset dep.parents in + let _ = print_endline (" " ^ string_of_kid kid ^ ": " ^ s1 ^ "; " ^ s2) in () in let print_binding id kdep = @@ -2773,8 +2783,12 @@ let analyse_defs debug env (Defs defs) = match Bindings.find id r.split_on_call with | kid_deps -> begin match KBindings.find kid kid_deps with - | InFun deps -> separate_deps deps - | Parents fns -> CallerKidSet.fold add_kid fns (ArgSplits.empty, ExtraSplits.empty, Failures.empty) + | call_dep -> + let (splits, extras, fails) = match call_dep.in_fun with + | Some deps -> separate_deps deps + | None -> (ArgSplits.empty, ExtraSplits.empty, Failures.empty) + in + CallerKidSet.fold add_kid call_dep.parents (splits, extras, fails) | exception Not_found -> ArgSplits.empty,ExtraSplits.empty,Failures.empty end | exception Not_found -> ArgSplits.empty,ExtraSplits.empty,Failures.empty -- cgit v1.2.3 From 01d1586f3dea234609b68f332646882e6474c6da Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 4 May 2020 17:59:20 +0100 Subject: Add some more cases in mono rewrites --- src/monomorphise.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 465ed30f..149162d8 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3042,11 +3042,11 @@ let rec rewrite_app env typ (id,args) = [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) (* variable-slice @ local-var *) - | [E_aux (E_app (op, - [vector1; start1; length1]),_); + | [(E_aux (E_app (op, + [vector1; start1; length1]),_) as exp1); (E_aux (E_id _,_) as vector2)] when (is_slice op || is_subrange op) && is_bitvector_typ (typ_of vector1) && - not (is_constant length1) -> + not (is_constant_vec_typ env (typ_of exp1)) -> let op' = if is_subrange op then "subrange_subrange_concat" else "slice_slice_concat" in let zero = mk_exp (E_lit (mk_lit (L_num Big_int.zero))) in let one = mk_exp (E_lit (mk_lit (L_num (Big_int.of_int 1)))) in @@ -3063,11 +3063,11 @@ let rec rewrite_app env typ (id,args) = | [E_aux (E_app (append1, [e1; - E_aux (E_app (op, [vector1; start1; length1]),_)]),_); + (E_aux (E_app (op, [vector1; start1; length1]),_) as slice1)]),_); E_aux (E_app (zeros1, [length2]),_)] when is_append append1 && (is_slice op || is_subrange op) && is_zeros zeros1 && is_constant_vec_typ env (typ_of e1) && is_bitvector_typ (typ_of vector1) && - not (is_constant length1 || is_constant length2) -> + not (is_constant_vec_typ env (typ_of slice1) || is_constant length2) -> let op' = mk_id (if is_subrange op then "subrange_zeros_concat" else "slice_zeros_concat") in 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 -- cgit v1.2.3 From 87db18e7d1736f168491b49b7b339039260d7ac6 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 4 May 2020 17:59:39 +0100 Subject: Lem: Add some reserved identifiers --- src/pretty_print_lem.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 9e636b59..b18541a3 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -95,9 +95,9 @@ let rec fix_id remove_tick name = match name with | "with" | "check" | "field" - | "LT" - | "GT" - | "EQ" + | "LT" | "lt" | "lteq" + | "GT" | "gt" | "gteq" + | "EQ" | "eq" | "neq" | "integer" -> name ^ "'" | _ -> -- cgit v1.2.3 From b8f99df745e03ca5805110f52f5263c2ee2813fe Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 7 May 2020 20:07:00 +0100 Subject: Add another type annotation in bitvector cast rewrite --- src/monomorphise.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 149162d8..0e946f96 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3336,8 +3336,10 @@ let rec rewrite_app env typ (id,args) = match get_constant_vec_len ~solve:true env typ, args with | Some i, [vector1; start1; end1] when is_bitvector_typ (typ_of vector1) && not (is_constant start1 && is_constant end1) -> - let low = if is_inc_vec (typ_of vector1) then start1 else end1 in - E_app (mk_id "slice", [vector1; low; mk_exp (E_lit (mk_lit (L_num i)))]) + let inc = is_inc_vec (typ_of vector1) in + let low = if inc then start1 else end1 in + let exp' = rewrap (E_app (mk_id "slice", [vector1; low; mk_exp (E_lit (mk_lit (L_num i)))])) in + E_cast (bitvector_typ (nconstant i) (if inc then inc_ord else dec_ord), exp') | _, _ -> E_app (id, args) (* Rewrite (v[x .. y] + i) to (v + (i << y))[x .. y], which is more amenable to further rewriting *) -- cgit v1.2.3 From bed9f2f05813afec446a26e441e1df3d08d9c251 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 8 May 2020 13:37:25 +0100 Subject: Only check int kids when simplifying nexps --- src/monomorphise.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 0e946f96..f4d0aa56 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2108,7 +2108,9 @@ let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) = | None -> let is_equal kid = try - prove __POS__ typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + if Env.get_typ_var kid typ_env = K_int then + prove __POS__ typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + else false with _ -> false in match ne with -- cgit v1.2.3 From 336522767a1c3b564fd4798851993afef9f629ed Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 9 May 2020 22:10:49 +0100 Subject: Make Isabelle lemma generation work with grouped regstate --- src/state.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/state.ml b/src/state.ml index 478a3fd5..8d487d3e 100644 --- a/src/state.ml +++ b/src/state.ml @@ -410,12 +410,12 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = let id' = remove_trailing_underscores id in separate_map hardline string [ "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:"; - " \"\\read_reg " ^ id ^ "_ref\\\\<^sub>S = readS (" ^ id' ^ " \\ regstate)\""; - " by (auto simp: liftState_read_reg_readS register_defs)"; + " \"\\read_reg " ^ id ^ "_ref\\\\<^sub>S = read_regS " ^ id ^ "_ref\""; + " by (intro liftState_read_reg) (auto simp: register_defs)"; ""; "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:"; - " \"\\write_reg " ^ id ^ "_ref v\\\\<^sub>S = updateS (regstate_update (" ^ id' ^ "_update (\\_. v)))\""; - " by (auto simp: liftState_write_reg_updateS register_defs)" + " \"\\write_reg " ^ id ^ "_ref v\\\\<^sub>S = write_regS " ^ id ^ "_ref v\""; + " by (intro liftState_write_reg) (auto simp: register_defs)" ] in string "abbreviation liftS (\"\\_\\\\<^sub>S\") where \"liftS \\ liftState (get_regval, set_regval)\"" ^^ -- cgit v1.2.3 From 33be6201fa34557a46652658445f9c48c819ad34 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 11 May 2020 21:57:39 +0100 Subject: Add caching of calls to solve_unique --- src/constraint.ml | 55 +++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 43 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/constraint.ml b/src/constraint.ml index 74f3ec69..3ceb0aae 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -230,6 +230,7 @@ type smt_result = Unknown | Sat | Unsat module DigestMap = Map.Make(Digest) let known_problems = ref (DigestMap.empty) +let known_uniques = ref (DigestMap.empty) let load_digests_err () = let in_chan = open_in_bin "z3_problems" in @@ -241,6 +242,10 @@ let load_digests_err () = | 0 -> known_problems := DigestMap.add digest Unknown !known_problems | 1 -> known_problems := DigestMap.add digest Sat !known_problems | 2 -> known_problems := DigestMap.add digest Unsat !known_problems + | 3 -> known_uniques := DigestMap.add digest None !known_uniques + | 4 -> + let solution = input_binary_int in_chan in + known_uniques := DigestMap.add digest (Some solution) !known_uniques | _ -> assert false end; load () @@ -254,14 +259,21 @@ let load_digests () = let save_digests () = let out_chan = open_out_bin "z3_problems" in - let output digest result = + let output_problem digest result = Digest.output out_chan digest; match result with | Unknown -> output_byte out_chan 0 | Sat -> output_byte out_chan 1 | Unsat -> output_byte out_chan 2 in - DigestMap.iter output !known_problems; + DigestMap.iter output_problem !known_problems; + let output_solution digest result = + Digest.output out_chan digest; + match result with + | None -> output_byte out_chan 3 + | Some i -> output_byte out_chan 4; output_binary_int out_chan i + in + DigestMap.iter output_solution !known_uniques; close_out out_chan let kopt_pair kopt = (kopt_kid kopt, unaux_kind (kopt_kind kopt)) @@ -344,16 +356,17 @@ let call_smt l constraints = Profile.finish_smt t; result -let solve_smt l constraints var = +let solve_smt_file l constraints = 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 + smtlib_of_constraints ~get_model:true l vars constraints +let call_smt_solve l smt_file smt_vars var = + let smt_var = pp_sexpr (smt_vars var) in if !opt_smt_verbose then prerr_endline (Printf.sprintf "SMTLIB2 constraints are (solve for %s): \n%s%!" smt_var smt_file) else (); @@ -389,6 +402,10 @@ let solve_smt l constraints var = with | Not_found -> None +let solve_smt l constraints var = + let smt_file, smt_vars = solve_smt_file l constraints in + call_smt_solve l smt_file smt_vars 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 @@ -402,10 +419,24 @@ let solve_all_smt l constraints var = aux [] let solve_unique_smt l constraints var = - match solve_smt l constraints var with - | Some result -> - begin match call_smt l (nc_and constraints (nc_neq (nconstant result) (nvar var))) with - | Unsat -> Some result - | _ -> None - end - | None -> None + let smt_file, smt_vars = solve_smt_file l constraints in + let digest = Digest.string (smt_file ^ pp_sexpr (smt_vars var)) in + match DigestMap.find_opt digest !known_uniques with + | Some (Some result) -> Some (Big_int.of_int result) + | Some (None) -> None + | None -> + match call_smt_solve l smt_file smt_vars var with + | Some result -> + begin match call_smt l (nc_and constraints (nc_neq (nconstant result) (nvar var))) with + | Unsat -> + if Big_int.less_equal Big_int.zero result && Big_int.less result (Big_int.pow_int_positive 2 30) then + known_uniques := DigestMap.add digest (Some (Big_int.to_int result)) !known_uniques + else (); + Some result + | _ -> + known_uniques := DigestMap.add digest None !known_uniques; + None + end + | None -> + known_uniques := DigestMap.add digest None !known_uniques; + None -- cgit v1.2.3