I have a few noob questions regarding usage and style in z3 (smt syntax directly). I don't have a theoretical background on solvers, but I would still like to be able to take advantage of the neatness of Z3 without needing to deeply understand the theory (that's fair, no?).

Sample problem: I want to assign Students to distinct Seats. The Seats have letter names because I think that's simpler to write in SMT than if they were numbered. The Student type only has a name and seat field so far, but please consider that the Students might get several more fields and additional seating constraints in the future.

(declare-datatypes () ((Seat A B C D E F G)))

(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))

(declare-const S001 Student)
(declare-const S002 Student)

(assert (= (name S001) "Alice"))
(assert (= (name S002) "Bob"))

(assert (forall ((l Student) (r Student)) (xor (= l r) (distinct (seat l) (seat r)))))
; (assert (forall ((l Student) (r Student)) (implies (distinct l r) (distinct (seat l) (seat r))))) ; doesn't work either
(check-sat)
;(get-model)

This is Unsat currently. Why? I think I'm saying that "For all pairs of known Students that exist, either the student is paired with itself XOR the compared students are in distinct seats." But I might be saying "For all pairs of imaginable Students .."

If its the later, do I need to express the set of students as an array and forall over their indexes? Or is there a more natural way to say it?

It feels awkward to have to declare S001, S002 and then assert each field independently. If using an array is correct anyway, I'd rather say something like:

(declare-datatypes () ((Seat A B C D E F G)))

(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))

(declare-const students [
    (mkstudent "Alice" _)
    (mkstudent "Bob" _)
])

where there is some placeholder (an uninterpreted constraint?) for the seat field. But I cannot figure out how to leave that free anonymously. And I don't know if there's such a syntax for arrays.

The only way I can get close to this is by pre-declaring a named Seat for each Student and using that in the constructor, but this feels really awful ergonomically - and therefore feels like I'm just doing it wrong. Like, what would be the point of a Record if we have to declare unique identifiers for the instance fields anyway?? Especially presuming that I wouldn't ever have to mention those identifiers again since there are other Record-accessors to get at them. Sure, I could assert (= (name (select students 0)) "Alice") leaving the seat field unconstrained, but as my Student type grows with new valued-fields, this would get ugly and then it makes constructors not so useful.

(declare-const SeatAlice Seat)
(declare-const SeatBob Seat)

(declare-const students (Array Int Student))
(assert (= (select students 0) (mkstudent "Alice" SeatAlice)))
(assert (= (select students 1) (mkstudent "Bob" SeatBob)))

I'm not finding any documentation on how to use arrays and records and constructors and uninterpreted constraints all together. Just minimal examples of them independently, at best.

Many of my questions here are syntax-related - and maybe SMT/Z3 language just isn't prioritizing ergonomics and that is important to know - but again I'm checking with you here because maybe the awkwardness is a signal that I'm just doing it wrong and that there's a much more elegant way that is more readable and possibly even better for Z3 itself.

Updates

This feels a little better using sequence instead of array.

(declare-datatypes () ((Seat A B C D E F G)))
(declare-datatypes () ((Student (mk-student-ctor (fname String) (lname String) (seat Seat)))))

(define-fun mk-student ((fname String) (lname String)) Student
    ((declare-const s Seat)
    (mk-student-ctor fname lname s))
)

;; (define-fun mk-student ((fname String) (lname String)) Student
;;     ; doesn't work, but how could (define-const s Seat) be used in an expression as a local?
;;     (let ((s Seat))
;;     (mk-student-ctor fname lname s))
;; )

(declare-const students (Seq Student))

(assert (= students (seq.++ 
    (seq.unit (mk-student "Alice" "Smith")) 
    (seq.unit (mk-student "Bob" "Baker"))
    ; ...
)))

But I still can't figure out how to encapsulate the concept of an uninterpreted seat field in a constructed Student. Because declare-const is a command, I don't know how it could be used in an expression or if there is an alternative syntax for declaring a const locally (or inline). And in a define-fun, I don't see any way to make a Student without the constructor function which requires all arguments and thus I cannot even resign to constraining the fields one-at-a-time in my new mk_student() factory.

Your hunch is correct. You are saying For all pairs of imaginable Students ..

A relevant/question answer was posted before, please refer to: https://stackoverflow.com/a/60998125/936310

Regarding "factories": Your hunch is again correct that you want to be able to generate these on the fly satisfying certain characteristics. While you can do this in SMTLib (again, see the linked answer), SMTLib is not a language that's very suitable for doing these sorts of things. This is why we have higher level wrappers (from Python/C/Java/Haskell/OCaml) that provide better programming ergonomics over SMTLib, where you can use the features of the meta-level language to code such factories. (In particular, SMTLib has no looping constructs, and no real control-structures to speak of at the top-level, which is what you really need here.) So, pick one of those bindings, and use SMTLib as an "assembly" for reasoning, not for end-user coding.