To load the system look compile and load each of the following files in sequence.
 "walk"
 "defs"
 "user"
 "replay"
 "vector"
 "blists"
 "batms3"
 "hash"
 "tms7"
 "interp"
 "cons3"
 "nml"
 "tree"
 "label"
 "examples"
 "diags"

To see if things basically work try (n-queens 8) and then (dn-queens 8
t).  Also try (setq *resolve-by-ordered-labeling* T) and run (dn-queens
7 t).

Comments to: dekleer@xerox.com

             Johan de Kleer
             Xerox PARC
             3333 Coyote Hill Road
             Palo Alto CA 94304	

	     Phone: 415-494-4398.


This version the ATMS is incomplete in many many ways.  I had hoped to
repair many of its deficiencies, but I simply haven't had the time to
pursue it.  I am distributing it in this way because I promised I would.

This particular version has serious known bugs and has some gross
inefficiencies.  I have yet to integrate good ideas from the other
versions.

I'm in the process of providing documentation.  It is incomplete.  Be
warned that the comments in the code are wrong.  Often there are many
versions of the same function.

* If you received this as a Symbolics tape, it is in carry-tape format.
  There are only a dozen or so files and you will be queried for where to put to the files.

* You can get the files from arisia.xerox.com as follows.
  Login as ftp, give your id as a password.
  cd pub
  cd atms
  mget <everything that is there>
  If you care about experimenting with the ATMS you might take the trace files in
  the trace subdirectory.  Be warned: they take a lot of space.

  I update arisia periodically so you can look here periodically for new versions.
  The file manual.txt contains very sparse information on how to use the
  ATMS.  The documentation is extremely minimal.

* To install the ATMS for a symbolics all you should have to do is install 
  tms.system -> sys:site;tms.system
  atms.translations -> sys:site;atms.translations
   Make sure the filenames on those files is correct...
  :compile system tms

* If you publish a paper which exploits this code, make sure to
reference that fact.

* This code is not the Gold Standard ATMS.  The papers are.  Please
don't go analyze the efficiency of this code and write critical papers.
This implementation has weak points which I don't have the time to fix.

* The system declaration in tp-rel6/tp-rel7.  You'll have to change it
to suit your site.  

* Sending out these tapes could get expensive.  It would be nice if you sent
  me it back, or send me another blank one.

It's extremely difficult for me to ensure that the changes I make work
in all commonlisp machines.  Let me know if I introduce any problems.

  Although there are many #+/- switches in the code for many machines.  Few at 
  the moment are guaranteed to work.  All that are known to work are:

  #+CL #+Symbolics --- known to work in Symbolics release 7.x for x=0,1,2,3 (The default now).
  It works on the Symbolics XL400 and the MACIVORY.

  At the moment I only have hash functions for Symbolics machines.  Picking good
  hash functions is extremely difficult, and CommonLisp makes it even more difficult.

* As the conventions of my various ATMS papers aren't consistent, it shouldn't be 
  surprising that the conventions of this program are inconsistent also.

* In some cases the ATMS code does more than advertised, sometimes less.
  There have been many implementations of the ATMS.  This one is the best one
  right now.

* Be warned that there is a lot of dead code in these files.  I have done a lot
  of experimentation with different ways of implementing this or that and
  much of that code is still sitting in the files.

* Although there are a lot of programs using this ATMS, they tend to be
  very large so they are not useful as examples.  Someday I might write a simple
  example that exploits the capabilities of the ATMS.

  A bunch of often stupid toy examples can be found in the file examples.

* I do update this ATMS periodicaly because I and many others are using it in many 
  applications.  If you want to get updates just let me know and I'll send you 
  updates periodically.

* There are three horrendously slow versions of ATMS's written by various people.  They
  are useful to look at for understanding ATMS algorithms.

    LATMS1.LISP (mine).
    FORBUS-ATMS.LISP (Ken Forbus).
    SHRAGER-LATMS1.LISP/ QV: ... LATMS1.LISP

* The file load-atms.lisp contains functions for compiling and loading the ATMS 
  for a non-Symbolics machine provided by Hiroshi "Gitchang" Okuno
  <Okuno@SUMEX-AIM.Stanford.EDU>

The following is grossly incomplete and out of date.  I've never gotten
around to writing a manual.

This is intended as a reference manual for ATMS operations.  Please do
not use any other functions or flags without asking me.  Otherwise
future versions of the ATMS may change without notice.  This is very
incomplete.

Definitions:

<assumption-set> a list of assumptions sorted with highest numbered assumptions first and
no duplicates.

<assumption> is an assumption.

<class> is a class.

<environment> is an environment

<justification> is a list the first element is ignored by the ATMS, the remaining a list
of <n-a>'s.

<n-a> is a node or an assumption.

<node> is a node.

<vector> an efficient representation of a set of assumptions.

Functions:

Upper case functions are those recommended for outside use.


ADD-CLASS-TO-NODE (<n-a> <class>)
 
	Adds <n-a> to <class>.  If the class is closed an error is
signalled.  The node inherits every consumer of the class and these are
queued for execution if the node holds in any environment.

ASSUME-NODE (<node>)

	Creates a new assumption and justifies the node with it.  If the node has already
been assumed, this function has no effect.

ASSUME-XOR-NODE (<node> <class>)

        Creates a new assumption and justifies node with it.  The assumption is added
to the other assumptions of the class.  This assumption is made inconsistent with every
other assumption of the class.  If the <node> was assumed with the assume-node function,
or the node is not member of the specified class, then an error is signalled.
        
ASSUMPTION-DATUM (<n-a>)

        A field of an assumption data structure allocated for the user.  The ATMS
completely ignores this field.

assumption-unique (<n-a>)

        A field of an assumption data structure containing the unique integer assigned
to it.  This integer is used for internal ATMS operations.

ASSUMPTION-VALUE (<assumption>)
	
        A field of an assumption containing its value.  This is usually set by the user.

assumption-variable (<assumption>)
        A field of an assumption which usually contains its unique class if it has one.

assumptions-union (<assumption-set1> <assumption-set2>)

	Merges the two assumption sets to produce their union.  If possible, the original
sets will be used but not modified.

BASIC-MAKE-ASSUMPTION (<variable> <value> <datum>)

	Creates an assumption with the specified value and datum (ignored by the ATMS).
If variable is a class, the assumption is added to the assumptions of that class.

careful-node? (<x>)

	Returns T if <x> is a node, and will never produce an error whatever <x> is.

CLASS-DATUM (<class>)

	A field of a class allocated for the user.  The ATMS completely ignores this field. 

class-nodes (<class>)

	The list of nodes in the class.

CLOSE-VARIABLE-CLASS(<class>)
        
	Adds an ATMS disjunction of all the assumptions of the class.  Any later attempt
to add anything else to the class will signal an error.

compare-env (<environment1> <environment2>)

	Compares the environments and returns SUBSET12, SUBSET21, EQUAL, or NIL depending
on how the the assumptions of the two environments compare.  If either environment
is contradictory, the results are meaningless.

cons-env (<environment> <assumption>)

	This returns the environment produced by adding the assumption
to the environment.  Note that if this environment is inconsistent, the
ATMS may just return *contra-env*.

consistent-in? (<n-a> <environment>)

	Returns T if there exists some superset (or equal) of <environment> in which
<n-a> holds.

CONTRADICTION (<justification>)

	Shorthand for (justify-node *contra-node* <justification>).

CONTRADICTORY-NODE (<n-a> <reason>).

	Equivalent to (justify-node *contra-node* (list <reason> <n-a>)).

CREATE-CLASS (<datum>)

        Creates an ATMS class.  <datum> is supplied by the user and
never looked by the ATMS.

CREATE-CONSUMER (<name> <nodes> <state-variable> <value> ...)

	This adds a consumer of type <name> to the set of nodes and
assigns initial values to the specified state (LISP) variables.

CREATE-IMPLIED-BY-CONSUMER
		
	Unimplemented.

create-in-implied-consumer

	Unimplemented.

CREATE-NODE (<datum>)

	Creates a node.  The datum is purely for the convenience of the user.

CREATE-VARIABLE (<name> <values>).

	Shorthand.  Creates the class <name>.  Creates nodes for each of
the values.  Assumes each one.  All the nodes and assumptions are
pairwise inconsistent.  Closes the class, thereby introducing the disjunction
that the variable must have one of the values.

DEFCONSUMER (<name> <arguments> <state-variables> <body>)

	Analogous to defun.  <state-variables> specifies instance variables created
for instance of the consumer.

E (<n>)

	For debugging.  Finds the environment with unique id n.  If the environment
is contradictory, it may not be found.

env-assumptions (<environment>)

	The assumption set associated with the environment.

ENV-CONTRADICTORY (<environment>)

	Non-NIL if the environment is consistent.  If contradictory returns a
concise explanation for the contradiction.  The first element of the list is
either BASE indicating the environment is a minimal nogood, or SUBSUMED indicating
it is contradictory but not minimal.

ENV-DATUM (<environment>)

	A field of the environment data structure allocated for user use.  The ATMS
does not access this field.

env-nodes (<environment>)

	A field of the environment data structure indicating all nodes in whose label
this environment appears.

env-unique (<environment>)

	A field of the environment data structure indicating a unique integer the
ATMS has assigned to it.

env-vector (<environment>)

	A field of the environment data structure used by ATMS algorithms to efficiently
represent the assumption set associated with the environment.  This is usually
some form of bit-vector.

EXPLANATION-FOR-NODE (<node> <env>)

	Finds a sequence of justifications all holding in <env> which support <node>.
If <env> is inconsistent, works only if at one time <env> was not nogood.

EXPLANATION-FOR-NOGOOD (<env>)

	Finds a sequence of justifications which make <env> a nogood.  Equivalent
to (explanation-for-node *contra-node* <env>).

FALSE? (<n-a>) 

	Returns T if the node has been determined to be FALSE.  Note that this function
might return nil even if the node is false because the ATMS is incomplete.

find-assumption-for

	Unimplemented.

find-or-make-env (<assumptions>)

	This takes an arbitrary list of assumptions and finds the
environment associated with it.  Note that if this environment is
inconsistent, the ATMS may just return *contra-env*.

find-variable-value (<class> <datum>)

	If a node with the specified datum is a member of the class, it is returned.
Otherwise a new node with the given datum is created and added to the class.

get-assumption-prop

	Unimplemented.

get-env-prop

	Unimplemented.

IN? (<n-a>)

	Non-nil if <n-a> is known to hold in any known environment.
Returns those environments.

INIT-TMS (<reuse>)

	Initializes the ATMS.  If <reuse> is T, the ATMS reuses all the
arrays it created on the previous run.  This is the default.

INTERPRETATIONS ()

	Returns a list of consistent environments each of which
satisfies every justification, every disjunction, to which no other
assumption can be added without introducing an inconsistency.

JUSTIFY-NODE (<n-a> <justification>)

	Adds justification to the given n-a.  Updates all the necessary ATMS labels.

make-a-assumption (<variable> <value>)

	Creates an assumption with the specified <value> (unused by the
ATMS).  If the value is :IN, the variable is presumed to be a node and
this acts like the function assume-node.  If the value is a class, the
created assumption is added to the assumptions of the class.  The assumptions
of the class are assumed to be a oneof disjunction.

node-assumption (<node>)

	The unique assumption underlying a node.  Set by assume-node and like functions.

node-classes (<n-a>)
	
	The classes in which <n-a> appears.

node-consequents (<n-a>)

	The entire set of (<consequent-node> . <justification>) in which <n-a>
appears in the justification.

NODE-DATUM (<n-a>)

	The node data structure field allocated to the user.

LABEL (<n-a>)
	
	Returns the nodes label.

node-justifications (<n-a>)

	The node data structure field containing the node's justifications.

node-status (<n-a>)

	Should not be used by users, but seems to be.  It contains IN or OUT.  But
this status is only maintained for <n-a>'s which are antecedents to active
consumers.

node? (<n-a>)

	Returns T if the <n-a> is a node instead of an assumption.

nodes ()

	Returns a list of all the nodes created by the user.

OUT? (<n-a>)

	Opposite of in?.

POSSIBLE-STATUS-OF-NODE (<n-a>)

	Returns: :FALSE if <n-a> can never hold in any consistent
environment, :IN if it could hold in some current consistent
environment, :TRUE if it holds and will hold in every consistent
environment, and :OUT otherwise.

put-assumption-prop

	Unimplemented.

put-env-prop

	Unimplemented.

RUN

	Executes all pending consumers.

STATUS-OF-NODE (<n-a>)

	A bit like possible-status-of-node, but different.  Returns: :FALSE
if <n-a> can never hold in any consistent environment, :OUT if <n-a> holds
in no current environment, :TRUE if it holds and will hold in every consistent
environment, and :IN otherwise.

STRING-ENV (<environment>)

	The string representing how the environment.

subset-env? (<environment1> <environment2>)

	Returns T if the assumptions of <environment1> are a subset of
those of <environment2>.  Undefined if either environment is
contradictory.

subsumed-envs?

	Obsolete.

TRUE? (<n-a>)

     	Returns T if ATMS has determined n-a has an empty label.  Note that because
incompleteness a node could be true but the ATMS might not have determined it.

TRUE-IN? (<n-a> <environment>)

	Does <n-a> occur in the context of the environment.

union-env (<environment1> <environment2>)

	Construct the environment whose assumptions is the union of its two arguments.
If the result is inconsistent, *contra-env* is returned.

union-envss (<environments1> <environments2>)

	The result is what the label of a node would be if it were justified
by two nodes with labels <environments1> and <environments2>.

vector-subset (<vector1> <vector2>)

	Returns T if the first vector is a subset of the second.

vector-union (<vector1> <vector2>)

	Returns the vector which is the union of both.  

Variables:

*assumption-counter*

	The unique integer assigned to the last assumption created.

*classes*

	The set of classes created by the user.

*contra-counter*

	The number of contradictions encountered by the ATMS.

*contra-node*

	A node which is defined to be false.

*contradictions*

	An array, the ith element contains all minimal nogoogds of size i.

*empty-env*

	The environment with no assumptions.  

*env-counter*

	The unique integer assigned to the last environment created.

*max-contra-count*
	
	The largest nogood encounter.

*node-counter*

	The unique integer assigned to the last node actually
constructed.  Note that internally generated nodes are garbage collected
by the ATMS, so this number does not necssarily belong to the last node
allocated.

*node-string*

	A user-supplied function used to construct the string for a node.


Flags:

Note there are so many ATMS flags that it is hard to maintain full ATMS
functionality for every combination.  

*break-coded* (NIL).

	If T the ATMS uses break coded bit vectors to represent
assumption sets.  If NIL the ATMS uses simple bit vectors.  Call
(install) after changing this flag.  There are ATMS problems which perform
better with either setting.

*c012* (NIL).

	The ATMS will look for easy contradictions (usually of size 0,
1, 2) first before doing full label propagation. There are ATMS problems
which perform better with either setting.

*h4* (NIL)

	NIL: Do nothing.  1 : Do full hyper-resolution. 2 : Only resolve binary
disjunctions.  This flag is hardly ever worth setting.

*45* (NIL)

	Be clever about binary disjunctions.  See paper.

*i-mode* (:NEW-DEPTH3).

	Controls the type of interpretation construction algorithm currently used.
This is the best one for all known examples.

*k* (NIL).

	This only has effect if *h4* is non-NIL.  NIL: Find all nogoods.  Otherwise
corresponds to Freuder's k-consistency.  *k*=1 means Mackworth's node-consistency,
*k*=2 means Mackworth's arc-consistency, *k*=3 means Mackworth's path-consistency.

*nogood-tree-flag* (T)

	Use a discrimation net to represent all the nogoods.

*reclaim-flag* (T)

	The ATMS tries to recycle nodes it creates internally.

*resolve-by-labeling* (NIL)

	The ensures the ATMS will find every nogood logically implied,
and it will do so by adding justifications for every minimal nogood discovered.

*smashing-alternatives* (T)

	A time-space-GC tradeoff.  This saves a lot of conses, but with the GC
turned off this is faster.

*union-check* (T)

	Check caches before trying to construct the union.


Basic interface:

This is the basic interface, without all the bells and whistles.

Functions: 

ADD-XOR-ASSUMPTION-TO-CLASS

BASIC-MAKE-ASSUMPTION

CLOSE-VARIABLE-CLASS

CREATE-CLASS

CREATE-NODE 

INIT-TMS

JUSTIFY-NODE

Variables:

*contra-node*

Functions you might think you can call, but shouldn't because they don't
do what you think:

CONTRADICTORY-ENV.

What you see in a trace file.

F --- User asked whether the node was false and it was.
NF --- User asked whether the node was false and we don't know.
TR --- User asked whether the node was true and it was.
NT --- User asked whether the node was true and we don't know.
IN --- The user asked whether a node was in/out and it was in.
OUT --- The user asked whether a node was in/out and it was out.
L --- The user asked for the label of this node.


(explanation-for-nogood nogood) 

Note: This will not work properly unless *explain-flag* is T during the
run.  It does not work for focussing right now.

Note: This is under construction.

There are two root causes for a nogood: (1) A direct justification for a
false node, (2) a node and its negation both justifying.  For a nogood
of the first type, this procedure returns a list (JUSTIFY-CONTRADICTION
<just> <contra-node> <antecedents>).  For a nogood of the second type,
this procedure returns (NEGATION <node> <net-node>).  (This data
structure is redundant.)

The actual explanation is stored in the n-a-support slots of the nodes.
It is a DAG.  Here are the possibilities:

<justification> --- Belief in this node is justified by the justification.

:ASSUMPTION --- this is an assumption which is part of the nogood.

:USER --- the user set this node true/false.

(<class> <neg-other-node>) --- the node is a member of exclusive <class> and it received
its label by virtue of the negation of some other in the class gaining support.

(:NEGATION-IS-FALSE <false-node>) --- This node is true because its negation is false.

The following are less obvious, but critical for constructing explanations.

((:INVERT . <just>) <false-consequent> . <other-antecedents>) --- This node is false, because
it appears in a justification for a false node in which all other antecedents are true.

(:NEGATION-IS-TRUE <true-node>) --- This node is false because its negation is true.

The function print-nogood-dependency will print out a primitive printer-style explanation.