ce-parsing: Do not confuse constructors with no arguments from variables

This is solved by collecting names of constructors with no arguments
during printing.

src/core/model_parser.ml

@@ -404,7 +404,7 @@ let default_model = {
 type model_parser =  string -> Printer.printer_mapping -> model
 
 type raw_model_parser =
-  Sstr.t -> ((string * string) list) Mstr.t ->
+  Sstr.t -> ((string * string) list) Mstr.t -> string list ->
     string -> model_element list
 
 (*
@@ -884,7 +884,8 @@ let make_mp_from_raw (raw_mp:raw_model_parser) =
   fun input printer_mapping ->
     let list_proj = printer_mapping.list_projections in
     let list_records = printer_mapping.list_records in
-    let raw_model = raw_mp list_proj list_records input in
+    let noarg_cons = printer_mapping.noarg_constructors in
+    let raw_model = raw_mp list_proj list_records noarg_cons input in
     build_model raw_model printer_mapping
 
 let register_model_parser ~desc s p =
@@ -903,4 +904,4 @@ let list_model_parsers () =
 
 let () = register_model_parser
   ~desc:"Model@ parser@ with@ no@ output@ (used@ if@ the@ solver@ does@ not@ support@ models." "no_model"
-  (fun _ _ _ -> [])
+  (fun _ _ _ _ -> [])

src/core/model_parser.mli

@@ -333,11 +333,16 @@ type model_parser =  string -> Printer.printer_mapping -> model
 
 type raw_model_parser =
   Wstdlib.Sstr.t -> ((string * string) list) Wstdlib.Mstr.t ->
-    string -> model_element list
-(** Parses the input string into model elements. It contains the list of
-    projections and a map associating the name of printed projections to the
-    fields (couple of printed field and model_trace name) that are collected in
-    the task.
+    string list -> string -> model_element list
+(** Parses the input string into model elements.
+    [raw_model_parser: proj->record_map->noarg_cons->s->mel]
+    [proj]: is the list of projections
+    [record_map]: is a map associating the name of printed projections to the
+      fields (couple of printed field and model_trace name).
+    [noarg_cons]: List of constructors with no arguments (collected to avoid
+      confusion between variable and constructors)
+    [s]: model
+    [mel]: collected model
  *)
 
 val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit

src/core/printer.ml

@@ -36,6 +36,7 @@ type printer_mapping = {
   queried_terms : Term.term Mstr.t;
   list_projections: Sstr.t;
   list_records: ((string * string) list) Mstr.t;
+  noarg_constructors: string list;
 }
 
 type printer_args = {
@@ -61,6 +62,7 @@ let get_default_printer_mapping = {
   queried_terms = Mstr.empty;
   list_projections = Sstr.empty;
   list_records = Mstr.empty;
+  noarg_constructors = [];
 }
 
 let register_printer ~desc s p =

src/core/printer.mli

@@ -37,6 +37,9 @@ type printer_mapping = {
   list_projections: Sstr.t;
   (* List of projections as printed in the model *)
   list_records: ((string * string) list) Mstr.t;
+  (* List of constructors with no arguments that can be confused for variables
+     during parsing. *)
+  noarg_constructors: string list
 }
 
 type printer_args = {

src/driver/collect_data_model.ml

@@ -451,7 +451,8 @@ let convert_to_model_element name (t: term) =
   let value = convert_to_model_value t in
   Model_parser.create_model_element ~name ~value ()
 
-let default_apply_to_record (list_records: (string list) Mstr.t) (t: term) =
+let default_apply_to_record (list_records: (string list) Mstr.t)
+    (noarg_constructors: string list) (t: term) =
 
   let rec array_apply_to_record (a: array) =
     match a with
@@ -468,6 +469,10 @@ let default_apply_to_record (list_records: (string list) Mstr.t) (t: term) =
   and apply_to_record (v: term) =
     match v with
     | Sval _ -> v
+    (* Variable with no arguments can actually be constructors. We check this
+       here and if it is the case we change the variable into a value. *)
+    | Variable s when List.mem s noarg_constructors ->
+        Apply (s, [])
     | Cvc4_Variable _ | Function_Local_Variable _ | Variable _ -> v
     | Array a ->
         Array (array_apply_to_record a)
@@ -499,16 +504,16 @@ let apply_to_records_ref = ref None
 let register_apply_to_records f =
   apply_to_records_ref := Some f
 
-let apply_to_record list_records t =
+let apply_to_record list_records noarg_constructors t =
   match !apply_to_records_ref with
-  | None -> default_apply_to_record list_records t
-  | Some f -> f list_records t
+  | None -> default_apply_to_record list_records noarg_constructors t
+  | Some f -> f list_records noarg_constructors t
 
-let definition_apply_to_record list_records d =
+let definition_apply_to_record list_records noarg_constructors d =
     match d with
     | Function (lt, t) ->
-        Function (lt, apply_to_record list_records t)
-    | Term t -> Term (apply_to_record list_records t)
+        Function (lt, apply_to_record list_records noarg_constructors t)
+    | Term t -> Term (apply_to_record list_records noarg_constructors  t)
     | Noelement -> Noelement
 
 let rec convert_to_tree_def (d: definition) : tree_definition =
@@ -581,7 +586,7 @@ and convert_tarray_to_array a =
   | TStore (a, t1, t2) -> Store (convert_tarray_to_array a, convert_tterm_to_term t1, convert_tterm_to_term t2)
 
 let create_list (projections_list: Sstr.t) (list_records: ((string * string) list) Mstr.t)
-    (table: definition Mstr.t) =
+    (noarg_constructors: string list) (table: definition Mstr.t) =
 
   (* Convert list_records to take replace fields with model_trace when
      necessary. *)
@@ -590,10 +595,13 @@ let create_list (projections_list: Sstr.t) (list_records: ((string * string) lis
       Mstr.add key (List.map (fun (a, b) -> if b = "" then a else b) l) acc) list_records Mstr.empty
   in
 
-  (* Convert Apply that were actually recorded as record to Record. *)
+  (* Convert Apply that were actually recorded as record to Record. Also replace
+     Variable that are originally unary constructor  *)
   let table =
     Mstr.fold (fun key value acc ->
-      let value = definition_apply_to_record list_records value in
+      let value =
+        definition_apply_to_record list_records noarg_constructors value
+      in
       Mstr.add key value acc) table Mstr.empty
   in
 

src/driver/collect_data_model.mli

@@ -19,10 +19,11 @@ open Wstdlib
    This function has the information of the records that were saved.
 *)
 val register_apply_to_records:
-    ((string list) Mstr.t -> Smt2_model_defs.term -> Smt2_model_defs.term) ->
+    ((string list) Mstr.t -> string list ->
+     Smt2_model_defs.term -> Smt2_model_defs.term) ->
       unit
 
 (* From the table generated by the parser, build a list of model_element *)
 val create_list:
-    Sstr.t -> ((string * string) list) Mstr.t -> Smt2_model_defs.definition Mstr.t ->
-      Model_parser.model_element list
+    Sstr.t -> ((string * string) list) Mstr.t -> string list ->
+      Smt2_model_defs.definition Mstr.t -> Model_parser.model_element list

src/driver/parse_smtv2_model.ml

@@ -57,16 +57,17 @@ let do_parsing model =
        l;
      Wstdlib.Mstr.empty
 
-let do_parsing list_proj list_records model =
+let do_parsing list_proj list_records noarg_constructors model =
   let m = do_parsing model in
-  Collect_data_model.create_list list_proj list_records m
+  Collect_data_model.create_list list_proj list_records noarg_constructors m
 
 (* Parses the model returned by CVC4, Z3 or Alt-ergo.
    Returns the list of pairs term - value *)
 (* For Alt-ergo the output is not the same and we
    match on "I don't know". But we also need to begin
    parsing on a fresh new line ".*" ensures it *)
-let parse : raw_model_parser = fun list_proj list_records input ->
+let parse : raw_model_parser =
+  fun list_proj list_records noarg_constructors input ->
   try
 (*    let r = Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
     ignore (Str.search_forward r input 0);
@@ -74,7 +75,7 @@ let parse : raw_model_parser = fun list_proj list_records input ->
     let nr = Str.regexp "^)+" in
     let res = Str.search_backward nr input (String.length input) in
     let model_string = String.sub input 0 (res + String.length (Str.matched_string input)) in
-    do_parsing list_proj list_records model_string
+    do_parsing list_proj list_records noarg_constructors model_string
   with
   | Not_found -> []
 

src/printer/alt_ergo.ml

@@ -421,7 +421,8 @@ let print_prop_decl vc_loc args info fmt k pr f =
 				vc_term_loc = vc_loc;
 				queried_terms = model_list;
                                 list_projections = info.list_projs;
-                                list_records = Mstr.empty};
+                                list_records = Mstr.empty;
+                                noarg_constructors = []};
       fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
         (print_ident info) pr.pr_name (print_fmla info) f
   | Plemma -> assert false

src/printer/smtv2.ml

@@ -135,6 +135,9 @@ type info = {
   info_version : version;
   meta_model_projection : Sls.t;
   mutable list_records : ((string * string) list) Mstr.t;
+  (* For algebraic type counterexamples: constructors with no arguments can be
+     misunderstood for variables *)
+  mutable noarg_constructors: string list;
   info_cntexample_need_push : bool;
   info_cntexample: bool;
   info_incremental: bool;
@@ -568,13 +571,17 @@ let print_prop_decl vc_loc args info fmt k pr f = match k with
                                 vc_term_loc = vc_loc;
                                 queried_terms = model_list;
                                 list_projections = info.list_projs;
-                                Printer.list_records = info.list_records}
+                                Printer.list_records = info.list_records;
+                                noarg_constructors = info.noarg_constructors}
   | Plemma -> assert false
 
 let print_constructor_decl info fmt (ls,args) =
   let field_names =
     (match args with
-    | [] -> fprintf fmt "(%a)" (print_ident info) ls.ls_name; []
+    | [] -> fprintf fmt "(%a)" (print_ident info) ls.ls_name;
+        let cons_name = sprintf "%a" (print_ident info) ls.ls_name in
+        info.noarg_constructors <- cons_name :: info.noarg_constructors;
+        []
     | _ ->
         fprintf fmt "@[(%a@ " (print_ident info) ls.ls_name;
         let field_names, _ =
@@ -698,6 +705,7 @@ let print_task version args ?old:_ fmt task =
     info_version = version;
     meta_model_projection = Task.on_tagged_ls meta_projection task;
     list_records = Mstr.empty;
+    noarg_constructors = [];
     info_cntexample_need_push = need_push;
     info_cntexample = cntexample;
     info_incremental = incremental;