Generate and validate the XML documentation

[HowardvanRooijen]

Fixes #82.

The defect

No project set GenerateDocumentationFile, so the compiler never parsed a doc comment. Two
consequences: the test suite's documentation - which carries most of the reasoning behind this
stack - was unvalidated, and a malformed comment reached #81 and was caught by a reviewer rather
than the build, despite TreatWarningsAsErrors; and the package shipped no documentation file,
so consumers got no IntelliSense for anything.

What turning it on found first

Measured before any other change, with -p:GenerateDocumentationFile=true on the command line:

Code	Count	What
CS1591	21 unique in Z3.Linq	public members with no comment. The issue said 44 - the build log lists each warning twice, so that was 22 unique, and one has been documented since
CS1572	3	<param> tags for context, model and environment on a method with no such parameters
CS1573	2	member and instance with no tag on the same method
CS1711	1	a <typeparam name="T"> on a method with no T

The last three rows are one defect this stack introduced: the documentation for
GetSolution<T> came loose from its method when #75 inserted IsCollection between them, and
#78 then inserted GetMemberValue before that - so the block attached to GetMemberValue,
describing a T, a context, a model and an environment it does not have. Neither PR could
have noticed, because nothing parsed the comment. It is back on GetSolution<T>, with the
template parameter it gained in #78. That is the guard proving its worth before it exists.

The change

GenerateDocumentationFile=true in Directory.Build.props, for every project. Malformed XML
and unresolvable crefs are build errors from here, and the packable projects ship their
documentation. CS1591 is enforced for Z3.Linq only; the test, examples and demo projects
suppress it, each with a comment in its own project file saying why - a test's name is its
documentation, sample types are illustrations rather than an API, and the demo is a console
program. That answers the issue's open question about where the settings belong: the setting is
global, the suppression is per project, next to the reason.

The 21 public members are documented. Environment and its three members,
ExpressionVisitor, ITheoremGlobalRewriter and ITheoremPredicateRewriter and their methods,
the three attributes with their constructors and properties, and Optimization with both values.
Each comment says what the thing is for and, where it matters, when a wrong use fails - a
rewriter type that does not implement the interface is rejected at solve time, not when the
attribute is applied; a predicate rewriter that returns its input is refused; a mapped type
without the right constructor fails when the solution is read. Environment.IsArray says plainly
that nothing reads it, and points at #89.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean: 0 warnings, 0 errors, with
  TreatWarningsAsErrors on and documentation generation on for all four projects
• 247/247 tests, unchanged - this PR touches no behaviour
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• The package now ships the documentation. Before, lib/net10.0 held only the assembly;
  after, lib/net10.0 holds Z3.Linq.dll and a 47,833-byte Z3.Linq.xml. Straight from the ZeroFailed pipeline: every earlier package in _packages lists the dll alone, and Z3.Linq.2.0.2-xml-docs.47.nupkg lists both. Z3.Linq.Examples ships its 4 KB file too
• Z3.Linq.xml documents 93 members

Negative controls

Both run against the final code and restored byte-identical afterwards, because a clean build
proves nothing until the check has been seen to fail:

Break	Result
A cref in Environment changed to ExpressionVisitor.NoSuchMember	error CS1574: XML comment has cref attribute 'NoSuchMember' that could not be resolved
A duplicated </remarks> in a test class - the exact defect from #81	error CS1570: XML comment has badly formed XML -- 'End tag was not expected at this location.'

What this does not catch

Recorded on the issue and worth repeating here: the defect Copilot found on #86 was an inaccurate
<returns> - well-formed XML, resolving crefs, wrong sentence. This setting would not have caught
it and nothing mechanical will. It catches the malformed-XML and broken-reference classes, which
is what it found on #81 and what it found in this stack.

Coverage unchanged at 88.1% line (693 of 786) and 77.5% branch (459 of 592), as it should be for a change that touches no behaviour.

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org. This is the change
the issue asked to have in place before that hold lifts, so the first published 2.x carries its
documentation.

[github-actions]

Test Results

  1 files  ±0    1 suites  ±0   6s ⏱️ ±0s
236 tests ±0  236 ✅ ±0  0 💤 ±0  0 ❌ ±0 
247 runs  ±0  247 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit fa9a42c. ± Comparison against base commit 4acc666.