symbolic-sat/symbolic-sat.org

Symbolic SAT Solver

Introduction

TOC   ignore

Expression Classification

  (defvar *expression-types* '())

  (defmacro define-expression-type (type-name &rest predicate)
    (check-type type-name symbol)
    (let ((predicate-name (symbolicate type-name '-p)))
      `(progn
         (defun ,predicate-name (expression)
           ,@predicate)
         (pushnew '(,type-name . ,predicate-name) *expression-types* :key #'first :test #'equal)
         (export ',type-name)
         ',type-name)))

  (defun expression-type-p (expression-type expression)
    (if (eq '* expression-type)
        t
        (funcall (cdr (assoc expression-type *expression-types*))
                 expression)))

  <<not-classification>>
  <<and-classification>>
  <<or-classification>>

Not

  (define-expression-type sentential-not
      (and (equal (first expression) 'not)
         (= (length expression) 2)))

  (define-expression-type double-not
      (and (expression-type-p 'sentential-not expression)
         (listp (second expression))
         (expression-type-p 'sentential-not (second expression))))

And

  (define-expression-type sentential-and
      (and (equal (first expression) 'and)
         (>= (length (rest expression)) 2)))

  (define-expression-type not-and
      (and (expression-type-p 'sentential-not expression)
         (listp (second expression))
         (expression-type-p 'sentential-and (second expression))))

Or

  (define-expression-type sentential-or
      (and (equal (first expression) 'or)
         (>= (length (rest expression)) 3)))

  (define-expression-type not-or
      (and (expression-type-p 'sentential-not expression)
         (listp (second expression))
         (expression-type-p 'sentential-or (second expression))))

Implication

Biconditional

Other

Driver

Expression Handlers

Utilities

Packaging

  (ql:quickload :alexandria)

  (defpackage #:symbolic-sat
    (:use #:cl)
    (:import-from #:alexandria
                  #:symbolicate)
    (:export #:expression-type-p
             #:implies
             #:iff))

  <<expression-classification>>