This is not yet accessible from the front end command line.

We can't explicitly mark this deprecated because it triggers compiler warnings
when calling the implicit copy constructor from within Ptr's copy constructor.

This means ExprID::referent->is_in_state() is now usable as the offset
information within referents is consistent in a way
ExprID::referent->state_variable is not.

The latter was probably introduced too hastily and doesn't make for a good API.
We would like to have the freedom to change how we decide whether something is
in the state.

The purpose of this is to ensure that resolved symbols (e.g. ExprID::referent)
have the same final index as their original target declaration.

The offset calculation did not have much to do with reindexing and I think it
may have just been put here because it was a convenient post-resolution place
for it. An unfortunate side effect of this design was that resolved referents
had an invalid offset. To see why this is, note that symbol resolution (1)
replaces null referents with a *copy* of the target node and (2) runs prior to
reindexing. That is, the offset calculation in reindexing would only affect the
original state VarDecl, not its copies in ExprID referents.

None of what has just been described was a bug. The offsets of the VarDecl
copies are never used. But its presence incorrectly suggests to librumur clients
that it is usable.

In this commit we move the offset calculation to its more natural place within
symbol resolution. We do offset calculation *prior* to declaring a VarDecl in
the symbol table. This results in ExprIDs now receiving a referent with correct
offset information. Note that we need to do some extra checks because a
just-parsed VarDecl is part of an unvalidated model and may be invalid.

All this is part of a broader direction to make all the fields of a referent
valid and usable.

This will be removed in a future release.

This is the equivalent of validate_model, but for *any* node in the AST.

We're about to introduce a function for validating any subpart of the AST. That
is, effectively calling validate_model with a node other than the topmost node.
This means that the referent of a reference node (ExprID, FunctionCall or
TypeExprID) may not yet have been validated. So we need to drop the optimization
that avoids descending into these.

This makes validating a model take longer, but the difference should be
negligible. If this becomes a problem, we could start memoising visitor
dispatch.

The AST node indices (unique_id) are not used by the dump utility, so reindexing
is unnecessary.

We don't have any currently, but in theory you could write a put statement that
prints XML-breaking content. Once we introduce RelaxNG validation for this step
any put statement will cause problems.

declare-const was only added in SMTLIB 2.5 as a shortcut for a declare-fun
taking no parameters. Some solvers only support the base SMTLIB 2.0, so using
the expanded syntax gives us access to more alternative solvers.

We were using F_SETFD/F_GETFD to set O_NONBLOCK, but this is meant to be used on
the status flags, not the file descriptor. We correct this to use
F_SETFL/F_GETFL. Surprisingly this bug caused no visible misbehaviour on Ubuntu
Linux, macOS or FreeBSD. It was detected by a user on Arch Linux under WSL.

Github: related to #140 "Unit test fail on smt-simplify.m"

When using a toolchain without 32-bit support, the check that eventually skips
this test was causing some output about missing headers that could look
confusing when running the test suite. Even on macOS where the test is not
skipped, it was producing a linker warning. We now pipe all output to /dev/null
as it is not informative for the user.

It turns out this is useful when writing librumur-based tools.

This avoids collision with SMT solver keywords.

Github: related to #130 "interact with SMT solver"

These literals are already as simple as they can be. Any attempt to ask the SMT
solver to simplify them just produces themselves. So avoid calling the solver
altogether in these cases.

Github: closes #139 "avoid calling SMT solver for "true" and "false""

Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""

This will save us having to reconstruct these repeatedly when we just want to
ask the question "is the expression I have the literal true or false?"

Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""

Github: related to #130 "interact with SMT solver"

When diagnosing why a model you expect to be SMT-simplified is not getting
simplified, it is helpful for Rumur to actually tell you the reason it gave up.

Github: related to #130 "interact with SMT solver"

Github: related to #130 "interact with SMT solver"

We were aborting SMT simplification whenever we hit an unsupported expression.
This was unnecessarily conservative as one unsupported expression does not mean
that every later expression in the model will be unsupported. Note that we still
*do* need to abort on unsupported definitions and similar constructs while
traversing the model because skipping these can affect the correctness of later
simplification decisions.

Github: related to #130 "interact with SMT solver"

Rather interesting screw up there. We were bailing out of SMT simplification
when encountering an enum, as we don't support it yet. However, every model
begins with the implicit definition of the built-in type boolean. So SMT
simplification was previously useless as it would bail out on every single
model.

We still don't handle full enums, but we can at least cope with boolean now.

Github: related to #130 "interact with SMT solver"

Github: related to #130 "interact with SMT solver"

Less error prone than using raw literals when it comes to adding new command
line options.

This implementation is pretty minimal and simply bails out (throwing
smt::Unsupported) when it encounters any complicated feature. However, it's
already enough to simplify the example in tests/disabled/smt-simplify.m.

Github: related to #130 "interact with SMT solver"