Note, this probably breaks for DragonFly and NetBSD that don't have sandboxing
options. We should disable this test for them before the next release.

This removes the need to lean on our hacky toy SMT solver going forwards.

GCC 4.7 apparently does not understand C++11 attributes.

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"