Commit ac4f6321 authored by Sylvain Dailler's avatar Sylvain Dailler

Q327-007 Change printer specific to cvc4 ce

Added a counter for constructors. We print a new functions to redefine
constructors only if there is a need.

* src/printer/smtv2_cvc_ce.ml
(print_constructor_decl): Added counter.
(print_data_decl): Added counter.
(print_saved_constructors): Print only if number of constructors in the
list is greater than counter.

Change-Id: Iad0f29caac961644dcbf4137341abd76c01e1090
parent 9ef97dbb
......@@ -492,7 +492,8 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
queried_terms = model_list; }
| Plemma| Pskip -> assert false
let print_constructor_decl global_stuff add_stuff info fmt (ls,args) =
let print_constructor_decl global_stuff add_stuff nb_cons info fmt (ls,args) =
nb_cons := !nb_cons + 1;
let _ = flush_str_formatter () in
fprintf str_formatter "%a" (print_ident info) ls.ls_name;
let ls_ls_name = flush_str_formatter () in
......@@ -546,13 +547,13 @@ let print_constructor_decl global_stuff add_stuff info fmt (ls,args) =
add_stuff := ls_ls_name :: !add_stuff
with _ -> ()
let print_data_decl global_stuff add_stuff info fmt (ts,cl) =
let print_data_decl global_stuff add_stuff nb_cons info fmt (ts,cl) =
let _ = flush_str_formatter () in
fprintf str_formatter "%a" (print_ident info) ts.ts_name;
let s = flush_str_formatter () in
fprintf fmt "@[(%s@ %a)@]"
s
(print_list space (print_constructor_decl global_stuff add_stuff info)) cl;
(print_list space (print_constructor_decl global_stuff add_stuff nb_cons info)) cl;
global_stuff := s :: !global_stuff;
add_stuff := s :: !add_stuff
......@@ -571,7 +572,8 @@ let print_arg fmt (a, b) =
else
fprintf fmt "(%s %s)" a b
let print_saved_constructors fmt l =
let print_saved_constructors nb_cons fmt l =
if List.length l <= nb_cons + 1 then () else
match l with
| [] -> ()
| [_hd] -> ()
......@@ -594,10 +596,11 @@ let print_decl vc_loc cntexample args info fmt d = match d.d_node with
| Ddata dl ->
let global_stuff = ref [] in
let add_stuff = ref [] in
let nb_cons = ref 0 in
fprintf fmt "@[(declare-datatypes ()@ (%a))@]@\n"
(print_list space (print_data_decl global_stuff add_stuff info)) dl;
(print_list space (print_data_decl global_stuff add_stuff nb_cons info)) dl;
print_saved_projections fmt !global_stuff;
print_saved_constructors fmt !add_stuff
print_saved_constructors !nb_cons fmt !add_stuff
| Dparam ls ->
collect_model_ls info ls;
print_param_decl info fmt ls
......
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