Improve backtracking strategy

Improve the backtracking strategy and the interaction with
Snark.  In particular
* Try harder to avoid creating choice points that cannot lead
  to new solutions.
* Optionally continue execution after tests/preconditions that
  are not decidable, depending on the values of the variables
  *continue-after-undecidable-test* and
  *continue-after-undecidable-precondition*.
Before committing to a strategy the interpreter should check
all undecidable proofs again, to see whether they have become
decidable by subsequent instantiations of variables; if this
is not the case the interpreter should (optionally) fail.

In detail:
* Add functions DECLARE-OPERATOR-SORT, DECLARED-OPERATOR-SORTS
  and (SETF DECLARED-OPERATOR-SORTS).
* Add condition NO-DEFINITION-FOR-PRIMITIVE-ACTION and
  function LOOKUP-PRIMITIVE-ACTION.
* Add a slot DECLARED-OPERATOR-SORTS to COMPILATION-UNIT.
* Make function DECLARED-SORT depend on the context and add a
  method for application terms.
* Add a slot GLOBAL to class VARIABLE-TERM that can be used
  to add :GLOBAL keyword arguments to variables when
  translating to Snark syntax.  Add :GLOBAL keyword to
  MAKE-VARIABLE-TERM.
* Move function DESTRUCTURE-VARIABLE-NAME to terms.lisp and
  add a function MAKE-UNIQUE-VARIABLE-NAME.
* Add a method ACTION-PRECONDITION to PRIMITIVE-ACTION-TERM
  that retrieves the precondition from the action definition.
* Add keyword arguments AS-LIST and INCLUDE-GLOBAL to function
  TO-SEXPR to control the conversion of variables.  Convert
  the bound variables in quantified terms as lists.
* Improve various PRINT-OBJECT methods.
* Add methods NEGATE, BUILD-QUANTIFIED-TERM,
  UNIVERSALLY-QUANTIFY, EXISTENTIALLY-QUANTIFY.
* Improve implementation of generic function
  VARIABLES-AND-TERMS-FOR-UNIVERSAL-QUANTIFICATION.
* Improve the implementation of PROCESS-DECLARATION-FOR-SNARK.
* Add variables *ASSERT-REWRITE-FOR-DECLARATIONS*,
  *ASSERT-REWRITE-FOR-PRECONDITIONS* and
  *ASSERT-REWRITE-FOR-UNIQUE-NAMES-AXIOMS*, as well as
  *SUPPORT-DECLARATIONS*, *SUPPORT-PRECONDITIONS* and
  *SUPPORT-UNIQUE-NAME-AXIOMS* that control the behavior of
  Snark when processing declarations.
* Call DECLARE-OPERATOR-SORT from various methods of the
  generic function PROCESS-DECLARATION-FOR-PARSING.
* Introduce variables *RUN-TIME-LIMIT*, *IDA-RUN-TIME-LIMIT*
  and *IDA-ITERATIONS* that control how Snark is executed.
* Improve setting of Snark defaults.
* Move processing of Snark arguments into a dedicated function
  PROCESS-SNARK-ARGUMENTS.
* Fix the error reporting in the default implementation of
  generic function STATE.
* Store the STATE-MAP of BASIC-INTERPRETER instances in their
  memento.
* Add variable *TRACE-CHOICE-POINT-CREATION* that controls
  whether creation of choice points is traced.
* Add function PROOF-AND-SUBSTITUTION-FOUND that checks
  whether an invocation of Snark returned a proof that
  contains non-variable substitutions.
* Create all choice points with ADD-CHOICE-POINT to simplify
  tracing.
* Add function MAYBE-ADD-CHOICE-POINT that adds a choice point
  if doing so can actually lead to a solution with new values
  for the bound variables.
* Add function INTERPRET-1-PRIMITIVE-ACTION-SUCCESS that
  performs the main work of interpreting an action after its
  precondition was successful, since this functionality is now
  used in two places.
* Add variables *CONTINUE-AFTER-UNDECIDABLE-TEST* and
  *CONTINUE-AFTER-UNDECIDABLE-PRECONDITIONS* that control
  whether the interpreter should create a choice point after
  Snark has determined a test or precondition to be
  undecidable.  Update INTERPRET-1 accordingly.
* Add a function DEFAULT-CONTEXT that returns the context of
  the default interpreter to simplify interactive exploration.
Handle deferred proofs

* Move the classes NAME-MIXIN and REQUIRED-NAME-MIXIN to file
  utilities.lisp.  (This was done to resolve a complaint by
  SBCL about an undeclared superclass for condition
  NO-DEFINITION-FOR-PRIMITIVE-ACTION.  Since this class no
  longer inherits from NAME-MIXIN this change could be
  reverted.)
* Define functions CONSTANTS-FOR-SORT-TABLE,
  DECLARE-CONSTANT-SORT and CONSTANTS-FOR-SORT to keep track
  of all declared constants with sorts.
* Add a slot CONSTANTS-FOR-SORT-TABLE to COMPILATION-UNIT.
* Define function PRECONDITION-TERM for primitive actions.
* Define functions MAKE-CONJUNCTION and MAKE-DISJUNCTION.
* Fix a bug in PROCESS-DECLARATION-FOR-SNARK: the keyword
  :REWRITE-TOO was not removed from the argument list when its
  value was NIL.
* Call DECLARE-CONSTANT-SORT when parsing a constant
  declaration.
* Add a :CONTINUATION-FUNCTION keyword argument to BACKTRACK
  so that we can also use it in the INTERPRET function.
* Add a slot DEFERRED-PROOFS to class BASIC-INTERPRETER and to
  its memento class.
* Add variable *STORE-ALL-NON-REFUTED-PROOF-TERMS* to enable
  storing of all proof terms that were not refuted.  (This is
  not a particularly useful option except for testing some
  specialized cases.)
* Treat timeouts like undecidable proofs in INTERPRET-1.
* Store the undecidable proof in DEFERRED-PROOFS when
  continuing after such a proof.
* Try to prove the conjunction of all deferred proofs when the
  interpreter finishes a program.  This is handled by the new
  function PERFORM-DEFERRED-ACTIONS.
* Add an option *INSTANTIATE-UNDECIDABLE-CHOICES* that causes
  INTERPRET to instantiate all variables in terms that Snark
  determines to be undecidable.  Add functions
  MAYBE-INSTANTIATE-VARIABLES, INSTANTIATE-VARIABLES,
  PROVE-WITH-INSTANTIATED-VARIABLES and INSTANTIATIONS-FOR
  that implement this.

Additionally:
* Fix minor compatibility problems.  The program should now
  cleanly compile and load in CCL, CMUCL, and SBCL.
Merge branch 'feature/improve-proof-handling' into develop