Commit 0b0568b9 authored by Andrei Paskevich's avatar Andrei Paskevich

produce up to 256 constructor disequalities for TPTP provers

parent 1c22b121
......@@ -136,14 +136,6 @@ let print_decl info fmt d = match d.d_node with
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let dao_ax =
let pr = create_prsymbol (id_fresh "dao") in
let yi = create_vsymbol (id_fresh "ying") ty_int in
let ya = create_vsymbol (id_fresh "yang") ty_int in
let f = f_neq (t_var yi) (t_var ya) in
let f = f_exists_close [yi;ya] [] f in
create_prop_decl Paxiom pr f
let print_task pr thpr fmt task =
print_prelude fmt pr;
print_th_prelude task fmt thpr;
......@@ -151,8 +143,8 @@ let print_task pr thpr fmt task =
info_syn = get_syntax_map task;
info_rem = get_remove_set task }
in
let decls = dao_ax :: Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
ignore (print_list_opt (add_flush newline2)
(print_decl info) fmt (Task.task_decls task))
let () = register_printer "tptp"
(fun _env pr thpr ?old:_ fmt task ->
......
......@@ -211,10 +211,30 @@ let add_indexer (state,task) ts ty csl =
let task = List.fold_left mt_add task csl in
state, task
let add_discriminator (state,task) ts ty csl =
let d_add c1 task c2 =
let id = c1.ls_name.id_string ^ "_" ^ c2.ls_name.id_string in
let pr = create_prsymbol (id_derive id ts.ts_name) in
let ul = List.rev_map (create_vsymbol (id_fresh "u")) c1.ls_args in
let vl = List.rev_map (create_vsymbol (id_fresh "v")) c2.ls_args in
let t1 = t_app c1 (List.rev_map t_var ul) ty in
let t2 = t_app c2 (List.rev_map t_var vl) ty in
let ax = f_neq t1 t2 in
let ax = f_forall_close (List.rev vl) [[Term t2]] ax in
let ax = f_forall_close (List.rev ul) [[Term t1]] ax in
add_decl task (create_prop_decl Paxiom pr ax)
in
let rec dl_add task = function
| c :: cl -> List.fold_left (d_add c) task cl
| _ -> task
in
state, dl_add task csl
let add_indexer (state,task) ts ty = function
| [_] -> state, task
| _ when not state.in_smt -> state, task
| csl -> add_indexer (state,task) ts ty csl
| csl when state.in_smt -> add_indexer (state,task) ts ty csl
| csl when List.length csl <= 16 -> add_discriminator (state,task) ts ty csl
| _ -> state, task
let add_projections (state,task) _ts _ty csl =
(* declare and define the projection functions *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment