Category : Files from Magazines
Archive   : DDJ8604.ZIP
Filename : BROWN.PRO

; File: BOYER.LIB

(PUTD 'DEFUN '(NLAMBDA (NAM$ EXP$) (PUTD NAM$ EXP$) NAM$))



(DEFUN VARIABLEP (LAMBDA (V)
(* determine if V is a variable: if it starts with lower-case
it is *)
((ATOM V)
(GREATERP (ASCII (CAR (UNPACK V))) (ASCII `)) )
NIL ))

(DEFUN LPAR (LAMBDA (R)
(* return left parent *)
(CAR R) ))

(DEFUN LLIT# (LAMBDA (R)
(* return left litteral number *)
(CADR R) ))

(DEFUN RPAR (LAMBDA (R)
(* return right parent *)
(CADDR R) ))

(DEFUN RLIT# (LAMBDA (R)
(* return right litteral number *)
(CAR (CDDDR R)) ))

(DEFUN NLITS (LAMBDA (R)
(* return number of litterals *)
(CADR (CDDDR R)) ))

(DEFUN MAXNDX (LAMBDA (R)
(* return maximum index *)
(CADDR (CDDDR R)) ))

(DEFUN BINDINGS (LAMBDA (R)
(* return the bindings *)
(CAR (CDDDR (CDDDR R))) ))

(DEFUN SETLPAR (LAMBDA (R V)
(* set left parent *)
(RPLACA R V) ))

(DEFUN SETLLIT# (LAMBDA (R V)
(* set left litteral number *)
(RPLACA (CDR R) V) ))

(DEFUN SETRPAR (LAMBDA (R V)
(* set right parent *)
(RPLACA (CDDR R) V) ))

(DEFUN SETRLIT# (LAMBDA (R V)
(* set right litteral number *)
(RPLACA (CDDDR R) V) ))

(DEFUN SETNUMLITS (LAMBDA (R V)
(* set number of litterals *)
(RPLACA (CDR (CDDDR R)) V) ))

(DEFUN SETMAXNDX (LAMBDA (R V)
(* set maximum index *)
(RPLACA (CDDR (CDDDR R)) V) ))

(DEFUN SETBINDINGS (LAMBDA (R V)
(* set bindings *)
(RPLACA (CDDDR (CDDDR R)) V) ))

(DEFUN INRECP (LAMBDA (R)
(* is R an input record? *)
(NULL (RPAR R)) ))

(DEFUN LEQP (LAMBDA (X Y)
(* is X less than or equal to Y ? *)
(NOT (GREATERP X Y)) ))

(DEFUN NMEMS (LAMBDA (L)
(* return the number of members in the list L *)
((NULL L) 0)
(ADD1 (NMEMS (CDR L))) ))

(DEFUN EXTRACT (LAMBDA (K L TMP)
(* return the Kth member of L *)
(* TMP is a local variable *)
(LOOP
((ZEROP K) TMP)
(SETQ K (SUB1 K))
(SETQ TMP (POP L)) ) ))

(DEFUN RESOLVE (LAMBDA (CL1 I CL2 J LLIT RLIT LNDX RNDX BNDEV
LSIGN RSIGN)
(* resolve clause CL1 litteral I with clause CL2 litteral J
returning a new clause record representing the resolvent:
UNIFY will extend the binding environment: returns NIL if
impossible *)
(GETLIT CL1 I)
(SETQ LLIT LITG)
(SETQ LNDX INDEXG)
(SETQ LSIGN SIGNG)
(GETLIT CL2 J)
(SETQ RLIT LITG)
(SETQ RNDX (PLUS INDEXG (MAXNDX CL1)))
(SETQ RSIGN SIGNG)
(* create the new clause record *)
(SETQ BNDEV (LIST CL1 I CL2 J (DIFFERENCE (PLUS (NLITS CL1)
(NLITS CL2)) 2) (PLUS (MAXNDX CL1) (MAXNDX CL2)) NIL))
(* test for opposite signs *)
((EQ LSIGN RSIGN) NIL)
(* extend the environment by the unification algorithm *)
((UNIFY LLIT LNDX RLIT RNDX) BNDEV)
NIL ))

(DEFUN GETLIT (LAMBDA (CL K)
(* get the Kth litteral in clause CL: return the litteral
gotten in LITG: and the associated index in INDEXG *)
(* if CL is an input clause then extract the Kth litteral and
set the index to 1 *)
((INRECP CL)
(SETQ LITG (EXTRACT K (LPAR CL)))
(SETQ SIGNG (EQ K 1))
(SETQ INDEXG 1) )
(* if it is in the left parent of the clause then get the
litteral from the left parent *)
(* this is true if K is less than the litteral last resolved
upon in the left parent of the current clause *)
((LESSP K (LLIT# CL))
(GETLIT (LPAR CL) K) )
(* this is also true if K is less than the number of litterals
in the left parent but in this case we must adjust K by 1
*)
((LESSP K (NUMLITS (LPAR CL)))
(GETLIT (LPAR CL) (ADD1 K)) )
(* if the selected litteral is in the right parent but left of
the litteral last resolved upon then get the litteral from
the right parent with the appropriate adjustment to K *)
((LESSP K (PLUS (SUB1 (NUMLITS (LPAR CL))) (RLIT# CL)))
(GETLIT (RPAR CL) (ADD1 (DIFFERENCE K (NUMLITS (LPAR CL)))))
(* in this case adjust the index got *)
(SETQ INDEXG (PLUS INDEXG (MAXNDX (LPAR CL)))) )
(* otherwise the selected litteral is in the right parent to
the right of last litteral resolved upon so adjust K
accordingly and get the litteral *)
(GETLIT (RPAR CL) (PLUS (DIFFERENCE K (NUMLITS (LPAR CL))) 2))
(* and adjust the index gotten *)
(SETQ INDEXG (PLUS INDEXG (MAXNDX (LPAR CL)))) ))

(DEFUN UNIFY (LAMBDA (TERM1 INDEX1 TERM2 INDEX2)
(* attempt to unify TERM1 under INDEX1 with TERM2 under INDEX2
and extend the binding environment represented in the
global variable BNDEV: return T if successful or NIL if the
unification is impossible *)
(* if both terms and indices are equal then return T: no
extension to BNDEV is needed *)
((EQUAL TERM1 TERM2)
(EQ INDEX1 INDEX2)
T )
(* if TERM1 is a variable *)
((VARIABLEP TERM1)
(* then if it is bound in the current environment *)
((ISBOUND TERM1 INDEX1 BNDEV)
(* then substitute that binding and attempt to unify again
*)
(UNIFY TERMB INDEXB TERM2 INDEX2) )
(* else if the variable of TERM1 occurs in TERM2 then we
have a recursive """black" "hole""" situation so return
NIL *)
((OCCUR TERM1 INDEX1 TERM2 INDEX2) NIL)
(* else force a unification by adding the necessary binding
and return T for success *)
(BIND TERM1 INDEX1 TERM2 INDEX2 BNDEV)
T )
(* if TERM2 is a variable then swap the 2 terms and UNIFY the
other way *)
((VARIABLEP TERM2)
(UNIFY TERM2 INDEX2 TERM1 INDEX1) )
(* otherwise if the heads of the terms unify then return the
result of unifying the tails of the terms: the environment
is extended as needed *)
((UNIFY (CAR TERM1) INDEX1 (CAR TERM2) INDEX2)
(UNIFY (CDR TERM1) INDEX1 (CDR TERM2) INDEX2) ) ))

(DEFUN ISBOUND (LAMBDA (VAR INDEX BNDEV)
(* determine if the variable VAR under the index INDEX is
bound in the binding environment BNDEV: if it is then
return T and set the free variables TERMB and INDEXB to
the term and index respectively to which it is bound: *)
(* otherwise return NIL and do not alter the values of TERMB and
INDEXB *)
(* if BNDEV is an input record then it cannot be bound so
return NIL *)
((INRECP BNDEV) NIL)
(* if VAR under INDEX is equal to the head of the binding
environment at this level then return T and set TERMB and
INDEXB accordingly *)
((EQUAL (CONS VAR INDEX) (CAR (BINDINGS BNDEV)))
(SETQ TERMB (CADAR (BINDINGS BNDEV)))
(SETQ INDEXB (CAR (CDDAR (BINDINGS BNDEV))))
T )
(* else see if it is bound in the tail of the binding
environment at this level *)
((ISBOUND VAR INDEX (CDR (BINDINGS BNDEV))) T)
(* if not then check INDEX to see whether to search the left
or right parent binding environment *)
((LEQP INDEX (MAXNDX (LPAR BNDEV)))
(* search left parent *)
(ISBOUND VAR INDEX (LPAR BNDEV)) )
(* search right parent *)
((ISBOUND VAR (DIFFERENCE INDEX (MAXNDX (LPAR BNDEV))) (RPAR
BNDEV))
(* adjust INDEXB accordingly *)
(SETQ INDEXB (PLUS INDEXB (MAXNDX (LPAR BNDEV))))
(* and return success *)
T )
(* all possible approaches failed so return NIL for not bound *)
NIL ))

(DEFUN OCCUR (LAMBDA (V I TERM J)
(* see if the variable V under the index I occurs in the term
TERM under the index J and return T or NIL *)
(* if TERM is a variable *)
((VARIABLEP TERM)
(* then if it is bound *)
((ISBOUND TERM J BNDEV)
(* then make the substitution and test for occurance *)
(OCCUR V I TERMB INDEXB) )
(* if V equals TERM *)
((EQ V TERM)
(* then return T if I=J else NIL *)
(EQ I J) ) )
(* if TERM is atomic and not a variable *)
(* then it is a constant so return NIL *)
((ATOM TERM) NIL)
(* otherwise if V under I occurs in the head of TERM under J
then return T *)
((OCCUR V I (CAR TERM) J) T)
(* otherwise return T if V under I occurs in the tail of TERM
under J and NIL otherwise *)
(OCCUR V I (CDR TERM) J) ))

(DEFUN BIND (LAMBDA (V I TERM J BNDEV)
(* bind V under I to TERM under J in BNDEV *)
(SETBINDINGS BNDEV (CONS (CONS (CONS V I) (CONS TERM J))
(BINDINGS BNDEV))) ))

(DEFUN * (LAMBDA COMMENTS
NIL ))

(DEFUN MAKECL (LAMBDA (CL)
(* make a clause record out of the expression CL *)
(LIST CL 0 NIL 0 (NMEMS CL) 1 NIL) ))


(RDS)
AKECL (LAMBDA (CL)
(* make a clause record out of the expression CL *)
(LI