From 3fa9b545a7e85b06b3ef99f799264679f293a68e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?=
 <129742207+bclement-ocp@users.noreply.github.com>
Date: Tue, 5 Sep 2023 09:54:38 +0000
Subject: [PATCH] Restore record printing functionality (#793)

This got lost somewhere along the way as the conditions for model
generation changed.

Note that it is a bit weird that the accumulation of record accesses
happens in `models.ml` while the accumulation of array accesses happens
in `uf.ml`.  We should pick a single one for both (probably in `models`
but even better would be to expose the appropriate APIs so that each
theory can build its own model values), but for now this patch should
wrangle the `if`s properly and restore the existing functionality.
---
 src/lib/frontend/models.ml                   |  8 ++++++-
 src/lib/reasoners/uf.ml                      |  4 +++-
 tests/dune.inc                               | 25 ++++++++++++++++++++
 tests/models/records/record1.models.expected |  5 ++++
 tests/models/records/record1.models.smt2     |  8 +++++++
 5 files changed, 48 insertions(+), 2 deletions(-)
 create mode 100644 tests/models/records/record1.models.expected
 create mode 100644 tests/models/records/record1.models.smt2

diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index 0849ff6c8..a9533764e 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -416,7 +416,13 @@ module SmtlibCounterExample = struct
            else
              reps_aux representants
          in
-         print_fun_def fmt f xs_ty_named ty rep;
+         (* Only print declared (but not defined!) function symbols -- note
+            that we still need to *handle* other symbols without printing them
+            because they could be record accessors that must be added to the
+            `records` reference *)
+         match f with
+         | Sy.Name (_, _, false) -> print_fun_def fmt f xs_ty_named ty rep
+         | _ -> ()
       ) fprofs;
     !records
 end
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 81dd4095a..b16f6a854 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1026,7 +1026,9 @@ let compute_concrete_model ({ make; _ } as env) =
   ME.fold
     (fun t _mk ((fprofs, cprofs, carrays, mrepr) as acc) ->
        let { E.f; xs; ty; _ } = E.term_view t in
-       if X.is_solvable_theory_symbol f ty
+       (* Keep record constructors because models.ml expects them to be there *)
+       if (X.is_solvable_theory_symbol f ty
+           && not (Shostak.Records.is_mine_symb f ty))
        || E.is_fresh t || E.is_fresh_skolem t
        || E.equal t E.vrai || E.equal t E.faux
        then
diff --git a/tests/dune.inc b/tests/dune.inc
index 7660e372c..eb90a49c3 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -186828,6 +186828,31 @@
 ; Auto-generated part end
 ; File auto-generated by gentests
 
+; Auto-generated part begin
+(subdir models/records
+  (rule
+   (target record1.models_tableaux.output)
+   (deps (:input record1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff record1.models.expected record1.models_tableaux.output))))
+; Auto-generated part end
+; File auto-generated by gentests
+
 ; Auto-generated part begin
 (subdir models/uf
   (rule
diff --git a/tests/models/records/record1.models.expected b/tests/models/records/record1.models.expected
new file mode 100644
index 000000000..da5e88f8f
--- /dev/null
+++ b/tests/models/records/record1.models.expected
@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun a () Pair (pair 5 0))
+)
diff --git a/tests/models/records/record1.models.smt2 b/tests/models/records/record1.models.smt2
new file mode 100644
index 000000000..2739fc71d
--- /dev/null
+++ b/tests/models/records/record1.models.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-datatype Pair
+((pair (first Int) (second Int))))
+(declare-const a Pair)
+(assert (= (first a) 5))
+(check-sat)
+(get-model)