Do you remember who you discussed it with? It had to be either Sklower or Foderaro, unless you talked with Fateman.
Were the macros originally from another dialect of Lisp?
Re:The lost cause of the Lisp machines
by Animats on Thursday November 20, 2025 @04:23PM
(#45997947)
Franz LISP had, I think, MacLISP macros, while Common LISP has a different system.
I talked to Fateman at some point. Too long ago to remember about what.
Re:The lost cause of the Lisp machines
by specialgoodness on Thursday November 20, 2025 @11:26PM
(#46001221)
The Nelson-Oppen simplifier is a great piece of work, but it is not the first SAT solver. Boyer and Moore published their formally verified SAT solver in their 1979 A Computational Logic, the first book on the Boyer-Moore Theorem Prover, though it was first implemented I believe in 1973. This algorithm, based on IF-normalization and lifting, was also a core part of the original Boyer-Moore prover. One interesting note is that it actually was almost an earlier discovery of BDDs - they have the core BDD data structure and normalization algorithm but were just missing memoization and the fact that orderings on variables induce canonicity for checking boolean equivalence! But in any case, Boyer-Moore had a (formally verified, even!) implemented and used SAT solver long before Nelson and Oppen.
This is the original Oppen-Nelson simplifier, the first SAT solver. It was modified by them under contract for the Pascal-F Verifier, a very early program verifier.
We kept all the code under SCCS and built with make, because the LISP part was only part of the whole system.
[1] https://github.com/John-Nagle/pasv/tree/master/src/CPC4