diff --git a/rsc/extra/worker_example.html b/rsc/extra/worker_example.html
index 533f8dd01..f4b49b9f3 100644
--- a/rsc/extra/worker_example.html
+++ b/rsc/extra/worker_example.html
@@ -1,11 +1,22 @@
-
Alt-Ergo JS
+
diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml
index 2b4a3a1c1..07a2294f1 100644
--- a/src/bin/js/options_interface.ml
+++ b/src/bin/js/options_interface.ml
@@ -130,6 +130,7 @@ let set_options r =
set_options_opt Options.set_age_bound r.age_bound;
set_options_opt Options.set_fm_cross_limit (get_numbers r.fm_cross_limit);
set_options_opt Options.set_steps_bound r.steps_bound;
+ set_options_opt Steps.set_steps_bound r.steps_bound;
set_options_opt Options.set_output_format
(get_output_format r.output_format);
diff --git a/src/bin/js/worker_example.ml b/src/bin/js/worker_example.ml
index b4d758647..665e045fb 100644
--- a/src/bin/js/worker_example.ml
+++ b/src/bin/js/worker_example.ml
@@ -33,14 +33,14 @@ module Html = Dom_html
let document = Html.window##.document
(* Example of the file to prove *)
-let file = ref "goal g : true"
+let file = ref "(set-logic ALL)\n(check-sat)"
(* This is the extension needed for the parser and corresponding to the input
file format*)
-let extension = ref ".ae"
+let extension = ref ".psmt2"
-(* Timeout *)
let timeout = ref 100.
+let steps_bound = ref 10000
(* Function that run the worker. *)
let exec worker file options =
@@ -61,15 +61,16 @@ let exec worker file options =
(* Create the web worker and launch 2 threads.
The first one for the timeout,
the second on for the call to Alt-Ergo through his web worker *)
-let solve () =
+let solve ?steps_bound () =
let options =
{(Worker_interface.init_options ()) with
input_format = None;
- debug = Some true;
- verbose = Some true;
+ debug = Some false;
+ verbose = Some false;
+ steps_bound;
answers_with_loc = Some false;
- sat_solver = Some Worker_interface.Tableaux;
- unsat_core = Some true;
+ sat_solver = Some Worker_interface.CDCL_Tableaux;
+ unsat_core = Some false;
} in
let worker = Worker.create "./alt-ergo-worker.js" in
@@ -111,22 +112,30 @@ let string_input f area_name area =
Dom.appendChild res (Html.createBr document);
res
-let float_input name value =
+type 'a parser = { of_string : string -> 'a; to_string : 'a -> string }
+
+let generic_input { of_string; to_string } name value =
let res = document##createDocumentFragment in
Dom.appendChild res (document##createTextNode (Js.string name));
Dom.appendChild res (Html.createBr document);
let input = Html.createInput document in
- input##.value := Js.string (string_of_float !value);
+ input##.value := Js.string (to_string !value);
input##.onchange :=
Html.handler (fun _ ->
- (try value := float_of_string (Js.to_string input##.value)
+ (try value := of_string (Js.to_string input##.value)
with Invalid_argument _ -> ());
- input##.value := Js.string (string_of_float !value);
+ input##.value := Js.string (to_string !value);
Js._false);
Dom.appendChild res input;
Dom.appendChild res (Html.createBr document);
res
+let float_input =
+ generic_input { of_string = float_of_string; to_string = string_of_float }
+
+let int_input =
+ generic_input { of_string = int_of_string; to_string = string_of_int }
+
let button name callback =
let res = document##createDocumentFragment in
let input = Html.createInput ~_type:(Js.string "submit") document in
@@ -140,49 +149,23 @@ let process_results = function
Some (String.concat "" r)
| None -> None
-let result = document##createTextNode (Js.string "")
-(* update result text area *)
-let print_res = function
- | Some res ->
- result##.data := Js.string res
- | None -> ()
-
-let error = document##createTextNode (Js.string "")
-(* update error text area *)
-let print_error = function
- | Some err ->
- error##.data := Js.string err
- | None -> ()
+let regular =
+ let div = Html.createDiv document in
+ div##.className := Js.string "regular";
+ div
-let warning = document##createTextNode (Js.string "")
-(* update warning text area *)
-let print_warning = function
- | Some wrn ->
- warning##.data := Js.string wrn
+let print_regular v =
+ match v with
+ | Some s ->
+ regular##.innerText := Js.string s
| None -> ()
-let debug = document##createTextNode (Js.string "")
-(* update error text area *)
-let print_debug = function
- | Some dbg ->
- debug##.data := Js.string dbg
- | None -> ()
-
-let model = document##createTextNode (Js.string "")
-(* update model text area *)
-let print_model = function
- | Some mdl ->
- model##.data := Js.string mdl
- | None -> ()
-
-let unsat_core = document##createTextNode (Js.string "")
-(* update unsat core text area *)
-let print_unsat_core = function
- | Some usc -> unsat_core##.data := Js.string usc
- | None -> ()
+let diagnostic =
+ let div = Html.createDiv document in
+ div##.className := Js.string "diagnostic";
+ div
let statistics = document##createTextNode (Js.string "")
-(* update statistics text area *)
let print_statistics = function
| None -> ()
| Some l ->
@@ -197,75 +180,46 @@ let print_statistics = function
) "" l in
statistics##.data := Js.string stats
+let print_diagnostic v =
+ match v with
+ | Some s ->
+ diagnostic##.innerText := Js.string s
+ | None -> ()
+
let onload _ =
let main = Js.Opt.get (document##getElementById (Js.string "main"))
(fun () -> assert false) in
- (* Create a text area for the input file *)
Dom.appendChild main
(string_input Html.createTextarea "Input file to solve" file);
Dom.appendChild main (Html.createBr document);
- (* Create a text area for the extension format *)
Dom.appendChild main (string_input Html.createInput "Extension" extension);
Dom.appendChild main (Html.createBr document);
- (* Create a text area for the timeout value *)
Dom.appendChild main (float_input "Timeout" timeout);
Dom.appendChild main (Html.createBr document);
- (* Create a button to start the solving *)
+ Dom.appendChild main (int_input "Steps bound" steps_bound);
+ Dom.appendChild main (Html.createBr document);
Dom.appendChild
main
(button "Ask Alt-Ergo" (fun _ ->
let div = Html.createDiv document in
Dom.appendChild main div;
Lwt_js_events.async (fun () ->
- (* Print "solving" until the end of the solving
- or until the timeout *)
- print_res (Some "Solving");
- print_error (Some "");
- let%lwt res = solve () in
- (* Update results area *)
- print_res (process_results res.regular);
- (* Update errors area if errors occurs at solving *)
- print_error (process_results res.diagnostic);
- (* Update warning area if warning occurs at solving *)
- print_warning (process_results res.diagnostic);
- (* Update debug area *)
- print_debug (process_results res.diagnostic);
- (* Update model *)
- print_model (process_results res.regular);
- (* Update unsat core *)
- print_unsat_core (process_results res.regular);
- (* Update statistics *)
+ print_regular (Some "Solving");
+ print_diagnostic (Some "");
+ let%lwt res = solve ~steps_bound:!steps_bound () in
+ print_regular (process_results res.regular);
+ print_diagnostic (process_results res.diagnostic);
print_statistics res.statistics;
Lwt.return_unit);
Js._false));
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
- (* Create a text area for the results *)
- Dom.appendChild main result;
- Dom.appendChild main (Html.createBr document);
- Dom.appendChild main (Html.createBr document);
- (* Create a text area for the errors *)
- Dom.appendChild main error;
- Dom.appendChild main (Html.createBr document);
- Dom.appendChild main (Html.createBr document);
- (* Create a text area for the warning *)
- Dom.appendChild main warning;
- Dom.appendChild main (Html.createBr document);
- Dom.appendChild main (Html.createBr document);
- (* Create a text area for the debug *)
- Dom.appendChild main debug;
- Dom.appendChild main (Html.createBr document);
- Dom.appendChild main (Html.createBr document);
- (* Create a text area for the model *)
- Dom.appendChild main model;
+ Dom.appendChild main regular;
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
- (* Create a text area for the unsat_core *)
- Dom.appendChild main unsat_core;
+ Dom.appendChild main diagnostic;
Dom.appendChild main (Html.createBr document);
Dom.appendChild main (Html.createBr document);
- (* Create a text area for the statistics *)
- Dom.appendChild main statistics;
Js._false
let _ = Html.window##.onload := Html.handler onload
diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml
index 9177a0c1b..a6c72679c 100644
--- a/src/bin/js/worker_js.ml
+++ b/src/bin/js/worker_js.ml
@@ -53,33 +53,59 @@ let create_buffer () =
in
buf, output
-let main worker_id filename filecontent =
- try
- (* Create buffer for each formatter
- The content of this buffers are then retrieved and send as results *)
- let buf_regular = create_buffer () in
- Options.Output.set_regular (snd buf_regular);
- let buf_diagnostic = create_buffer () in
- Options.Output.set_diagnostic (snd buf_diagnostic);
-
- (* Status updated regarding if AE succed or failed
- (error or steplimit reached) *)
- let returned_status = ref (Worker_interface.Unknown 0) in
+let main ~worker_id input =
+ let buf_regular = create_buffer () in
+ Options.Output.set_regular (snd buf_regular);
+ let buf_diagnostic = create_buffer () in
+ Options.Output.set_diagnostic (snd buf_diagnostic);
+ let return_answer ?statistics status =
+ let regular = check_buffer_content buf_regular in
+ let diagnostic = check_buffer_content buf_diagnostic in
+ Worker_interface.{ worker_id; status; regular; diagnostic; statistics }
+ in
+ let return_error fmt =
+ Format.kasprintf (fun s -> return_answer (Error s)) fmt
+ in
- (* let context = ref ([],[]) in *)
- let unsat_core = ref [] in
- let tbl = Hashtbl.create 53 in
+ let tbl = Hashtbl.create 53 in
+ (* Aux function used to record axioms used in instantiations *)
+ let selector_inst orig =
+ let id = Expr.uid orig in
+ begin
+ try incr (snd (Hashtbl.find tbl id))
+ with Not_found -> Hashtbl.add tbl id (orig, ref 1)
+ end;
+ true
+ in
+ let unsat_core = ref [] in
- (* Aux function used to record axioms used in instantiations *)
- let selector_inst orig =
- let id = Expr.uid orig in
- begin
- try incr (snd (Hashtbl.find tbl id))
- with Not_found -> Hashtbl.add tbl id (orig, ref 1)
- end;
- true
- in
+ let compute_statistics () =
+ let used =
+ List.fold_left (fun acc ({Explanation.f;_} as r) ->
+ Util.MI.add (Expr.uid f) r acc
+ ) Util.MI.empty (!unsat_core) in
+ Hashtbl.fold (fun id (f,nb) acc ->
+ match Util.MI.find_opt id used with
+ | None -> begin
+ match Expr.form_view f with
+ | Lemma {name=name;loc=loc;_} ->
+ let b,e = Loc.lexing_positions loc in
+ let used =
+ if Options.get_unsat_core () then Worker_interface.Unused
+ else Worker_interface.Unknown in
+ (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc
+ | _ -> acc
+ end
+ | Some r ->
+ let b,e = Loc.lexing_positions r.loc in
+ (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,
+ !nb,Worker_interface.Used)
+ :: acc
+ ) tbl []
+ in
+ try
+ let returned_status = ref (Worker_interface.Unknown 0) in
let print_status status n =
returned_status :=
begin match status with
@@ -91,98 +117,40 @@ let main worker_id filename filecontent =
end;
Frontend.print_status status n
in
-
- let compute_statistics () =
- let used =
- List.fold_left (fun acc ({Explanation.f;_} as r) ->
- Util.MI.add (Expr.uid f) r acc
- ) Util.MI.empty (!unsat_core) in
- Hashtbl.fold (fun id (f,nb) acc ->
- match Util.MI.find_opt id used with
- | None -> begin
- match Expr.form_view f with
- | Lemma {name=name;loc=loc;_} ->
- let b,e = Loc.lexing_positions loc in
- let used =
- if Options.get_unsat_core () then Worker_interface.Unused
- else Worker_interface.Unknown in
- (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc
- | _ -> acc
- end
- | Some r ->
- let b,e = Loc.lexing_positions r.loc in
- (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,
- !nb,Worker_interface.Used)
- :: acc
- ) tbl []
- in
- Solving_loop.process_source
- ~selector_inst ~print_status (`Raw (filename, filecontent));
- (* returns a records with compatible worker_interface fields *)
- {
- Worker_interface.worker_id = worker_id;
- Worker_interface.status = !returned_status;
- Worker_interface.regular = check_buffer_content buf_regular;
- Worker_interface.diagnostic = check_buffer_content buf_diagnostic;
- Worker_interface.statistics =
- check_context_content (compute_statistics ());
- }
-
+ Solving_loop.process_source ~selector_inst ~print_status input;
+ let statistics = check_context_content @@ compute_statistics () in
+ return_answer ?statistics !returned_status
with
- | Assert_failure (s,l,p) ->
- let res = Worker_interface.init_results () in
- { res with
- Worker_interface.worker_id = worker_id;
- Worker_interface.status = Error "Assertion failure";
- Worker_interface.diagnostic =
- Some [Format.sprintf "assertion failed: %s line %d char %d" s l p];
- }
+ | Assert_failure (s, l, p) ->
+ return_error "Assertion failure: %s %d %d" s l p
| Errors.Error e ->
- let res = Worker_interface.init_results () in
- { res with
- Worker_interface.worker_id = worker_id;
- Worker_interface.status = Error "";
- Worker_interface.diagnostic =
- Some [Format.asprintf "%a" Errors.report e]
- }
- | Solving_loop.Exit_with_code code ->
- let res = Worker_interface.init_results () in
- let msg = Fmt.str "exit code %d" code in
- { res with
- Worker_interface.worker_id = worker_id;
- Worker_interface.status = Error msg;
- }
+ return_error "%a" Errors.report e
| exn ->
- let res = Worker_interface.init_results () in
- let msg = Fmt.str "Unknown error: %s" (Printexc.to_string exn) in
- { res with
- Worker_interface.worker_id = worker_id;
- Worker_interface.status = Error msg;
- }
+ let exn = Printexc.to_string exn in
+ if Printexc.backtrace_status () then
+ let bt = Printexc.(raw_backtrace_to_string @@ get_raw_backtrace ()) in
+ return_error "Uncaught exception %s:@ %s" exn bt
+ else
+ return_error "Uncaught exception %s" exn
(** Worker initialisation
Run Alt-ergo with the input file (string)
and the corresponding set of options
Return a couple of list for status (one per goal) and errors *)
let () =
- at_exit Options.Output.close_all;
Worker.set_onmessage (fun (json_file, json_options) ->
Lwt_js_events.async (fun () ->
- let filename_opt, worker_id, filecontent =
+ Steps.reinit_steps ();
+ let filename, worker_id, content =
Worker_interface.file_from_json json_file
in
- let filecontent = String.concat "\n" filecontent in
-
- (* Extract options and set them *)
let options = Worker_interface.options_from_json json_options in
Options_interface.set_options options;
-
- (* Run the worker on the input file (filecontent) *)
- let filename = Option.get filename_opt in
- let results = main worker_id filename filecontent in
-
- (* Convert results and returns them *)
+ let input =
+ let content = String.concat "\n" content in
+ let filename = Option.value ~default:"" filename in
+ `Raw (filename, content)
+ in
+ let results = main ~worker_id input in
Worker.post_message (Worker_interface.results_to_json results);
- Lwt.return ();
- )
- )
+ Lwt.return ()))
diff --git a/src/lib/missing_primitives.js b/src/lib/missing_primitives.js
index 7cec671ea..cd10dce92 100644
--- a/src/lib/missing_primitives.js
+++ b/src/lib/missing_primitives.js
@@ -7,11 +7,43 @@ function unix_times () {
var utime = caml_unix_gettimeofday ();
return BLOCK(0, utime, utime, utime, utime)
}
+
//Provides: unix_setitimer
+//Version: < 5.0
function unix_setitimer () {
return BLOCK(0, 0, 0, 0)
}
+//Provides: caml_unix_setitimer
+//Version: >= 5.0
+function caml_unix_setitimer () {
+ return BLOCK(0, 0, 0, 0)
+}
+
+//Provides: unix_getpid
+//Version: < 5.0
+function unix_getpid() {
+ return 0;
+}
+
+//Provides: caml_unix_getpid
+//Version: >= 5.0
+function caml_unix_getpid() {
+ return 0;
+}
+
+//Provides: unix_kill
+//Version: < 5.0
+function unix_kill() {
+ return 0;
+}
+
+//Provides: caml_unix_kill
+//Version: >= 5.0
+function caml_unix_kill() {
+ return 0;
+}
+
// Camlzip primitives
//Provides: camlzip_inflateEnd
function camlzip_inflateEnd () {
@@ -29,13 +61,3 @@ function camlzip_inflate_bytecode () {
function camlzip_update_crc32 () {
return BLOCK(0, 0, 0, 0)
}
-
-//Provides: unix_getpid
-function unix_getpid() {
- return 0;
-}
-
-//Provides: unix_kill
-function unix_kill() {
- return 0;
-}
diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml
index bffbe5231..dfeb078cb 100644
--- a/src/lib/structures/satml_types.ml
+++ b/src/lib/structures/satml_types.ml
@@ -707,48 +707,55 @@ module Flat_Formula : FLAT_FORMULA = struct
then merge_rec l1 l2 h1
else merge_rec l1 l2 h2
- let mk_and =
- let exception Contradiction in
- fun hcons l ->
- try
- let so, nso =
+ exception Contradiction
+
+ let mk_and_aux hcons l =
+ let so, nso =
+ List.fold_left
+ (fun ((so,nso) as acc) e ->
+ match e.view with
+ | AND l -> merge_and_check so l, nso
+ | UNIT a when
+ not (Options.get_disable_flat_formulas_simplification ()) &&
+ a.Atom.var.Atom.level = 0 ->
+ begin
+ if a.Atom.neg.Atom.is_true then (
+ aaz a;
+ raise Contradiction
+ ); (* XXX*)
+ if a.Atom.is_true then (aaz a; acc)
+ else so, e::nso
+ end
+ | _ -> so, e::nso
+ )([],[]) l
+ in
+ let delta_inv = List.fast_sort (fun a b -> compare b a) nso in
+ let delta_u = match delta_inv with
+ | [] -> delta_inv
+ | e::l ->
+ let _, delta_u =
List.fold_left
- (fun ((so,nso) as acc) e ->
- match e.view with
- | AND l -> merge_and_check so l, nso
- | UNIT a when
- not (Options.get_disable_flat_formulas_simplification ()) &&
- a.Atom.var.Atom.level = 0 ->
- begin
- if a.Atom.neg.Atom.is_true then (
- aaz a;
- raise Contradiction
- ); (* XXX*)
- if a.Atom.is_true then (aaz a; acc)
- else so, e::nso
- end
- | _ -> so, e::nso
- )([],[]) l
+ (fun ((c,l) as acc) e ->
+ if complements c e then raise Contradiction;
+ if equal c e then acc
+ else (e, e::l)
+ )(e,[e]) l
in
- let delta_inv = List.fast_sort (fun a b -> compare b a) nso in
- let delta_u = match delta_inv with
- | [] -> delta_inv
- | e::l ->
- let _, delta_u =
- List.fold_left
- (fun ((c,l) as acc) e ->
- if complements c e then raise Contradiction;
- if equal c e then acc
- else (e, e::l)
- )(e,[e]) l
- in
- delta_u
- in
- match merge_and_check so delta_u with
- | [] -> vrai
- | [e]-> e
- | l -> make hcons (AND l) (OR (List.rev (List.rev_map mk_not l)))
- with Contradiction -> faux
+ delta_u
+ in
+ match merge_and_check so delta_u with
+ | [] -> vrai
+ | [e]-> e
+ | l -> make hcons (AND l) (OR (List.rev (List.rev_map mk_not l)))
+
+ let mk_and hcons l =
+ (* HOTFIX: Ensure that the exception cannot escape because of the
+ bug describe in https://github.com/OCamlPro/alt-ergo/issues/1348. *)
+ try
+ match mk_and_aux hcons l with
+ | exception Contradiction -> faux
+ | r -> r
+ with Contradiction -> faux
(* res = l1 inter l2 *)
let intersect_list l1 l2 =
@@ -835,62 +842,69 @@ module Flat_Formula : FLAT_FORMULA = struct
try Some (common, List.rev_map (diff_list common) ands)
with Not_included -> assert false
- let rec mk_or =
- let exception Tautology in
- fun hcons l ->
- try
- let so, nso =
+ exception Tautology
+
+ let rec mk_or_aux hcons l =
+ let so, nso =
+ List.fold_left
+ (fun ((so,nso) as acc) e ->
+ match e.view with
+ | OR l -> merge_and_check so l, nso
+ | UNIT a when
+ not (Options.get_disable_flat_formulas_simplification ()) &&
+ a.Atom.var.Atom.level = 0 ->
+ begin
+ if a.Atom.is_true then (aaz a; raise Tautology); (* XXX *)
+ if a.Atom.neg.Atom.is_true then (aaz a; acc)
+ else so, e::nso
+ end
+ | _ -> so, e::nso
+ )([],[]) l
+ in
+ let delta_inv = List.fast_sort (fun a b -> compare b a) nso in
+ let delta_u = match delta_inv with
+ | [] -> delta_inv
+ | e::l ->
+ let _, delta_u =
List.fold_left
- (fun ((so,nso) as acc) e ->
- match e.view with
- | OR l -> merge_and_check so l, nso
- | UNIT a when
- not (Options.get_disable_flat_formulas_simplification ()) &&
- a.Atom.var.Atom.level = 0 ->
- begin
- if a.Atom.is_true then (aaz a; raise Tautology); (* XXX *)
- if a.Atom.neg.Atom.is_true then (aaz a; acc)
- else so, e::nso
- end
- | _ -> so, e::nso
- )([],[]) l
+ (fun ((c,l) as acc) e ->
+ if complements c e then raise Tautology;
+ if equal c e then acc
+ else (e, e::l)
+ )(e,[e]) l
in
- let delta_inv = List.fast_sort (fun a b -> compare b a) nso in
- let delta_u = match delta_inv with
- | [] -> delta_inv
- | e::l ->
- let _, delta_u =
- List.fold_left
- (fun ((c,l) as acc) e ->
- if complements c e then raise Tautology;
- if equal c e then acc
- else (e, e::l)
- )(e,[e]) l
- in
- delta_u
- in
- match merge_and_check so delta_u with
- | [] -> faux
- | [e]-> e
- | l ->
- match extract_common l with
- | None ->
- begin match l with
- | [{ view = UNIT _; _ } as fa; { view = AND ands; _ }] ->
- begin
- try
- mk_or hcons
- [fa ; (mk_and hcons (remove_elt (mk_not fa) ands))]
- with Not_included ->
- make hcons (OR l) (AND (List.rev (List.rev_map mk_not l)))
- end
- | _ ->
+ delta_u
+ in
+ match merge_and_check so delta_u with
+ | [] -> faux
+ | [e]-> e
+ | l ->
+ match extract_common l with
+ | None ->
+ begin match l with
+ | [{ view = UNIT _; _ } as fa; { view = AND ands; _ }] ->
+ begin
+ try
+ mk_or hcons
+ [fa ; (mk_and hcons (remove_elt (mk_not fa) ands))]
+ with Not_included ->
make hcons (OR l) (AND (List.rev (List.rev_map mk_not l)))
end
- | Some (com,ands) ->
- let ands = List.rev_map (mk_and hcons) ands in
- mk_and hcons ((mk_or hcons ands) :: com)
- with Tautology -> vrai
+ | _ ->
+ make hcons (OR l) (AND (List.rev (List.rev_map mk_not l)))
+ end
+ | Some (com,ands) ->
+ let ands = List.rev_map (mk_and hcons) ands in
+ mk_and hcons ((mk_or hcons ands) :: com)
+
+ and mk_or hcons l =
+ (* HOTFIX: Ensure that the exception cannot escape because of the
+ bug describe in https://github.com/OCamlPro/alt-ergo/issues/1348. *)
+ try
+ match mk_or_aux hcons l with
+ | exception Tautology -> vrai
+ | r -> r
+ with Tautology -> vrai
(* translation from E.t *)