lit-lists

(in-package "AIGNET")

(include-book "centaur/satlink/litp" :dir :system)

(include-book "arrays")

(include-book "std/stobjs/clone" :dir :system)

(local (add-default-post-define-hook :fix))

(define lits-max-id-val
  ((lits lit-listp))
  (if (atom lits)
    0
    (max (lit->var (car lits))
      (lits-max-id-val (cdr lits))))
  ///
  (deffixequiv lits-max-id-val)
  (defthm lits-max-id-val-of-cdr
    (<= (lits-max-id-val (cdr x))
      (lits-max-id-val x))
    :rule-classes :linear)
  (defthm lits-max-id-val-of-car
    (<= (lit->var (car x))
      (lits-max-id-val x))
    :rule-classes :linear))

(define lit-copy
  ((lit litp) copy)
  :guard (< (lit->var lit)
    (lits-length copy))
  :inline t
  :returns (copylit litp
    :rule-classes :type-prescription)
  (lit-negate-cond (get-lit (lit->var lit)
      copy)
    (lit->neg lit))
  ///
  (defret lit->var-of-lit-copy
    (equal (lit->var copylit)
      (lit->var (get-lit (lit->var lit)
          copy))))
  (defretd lit->neg-of-lit-copy
    (equal (lit->neg copylit)
      (b-xor (lit->neg lit)
        (lit->neg (get-lit (lit->var lit)
            copy))))))

(define lit-list-copies-aux
  ((lits lit-listp) copy
    (acc lit-listp))
  :guard (< (lits-max-id-val lits)
    (lits-length copy))
  :hooks nil
  (if (atom lits)
    acc
    (lit-list-copies-aux (cdr lits)
      copy
      (cons (lit-copy (car lits) copy)
        acc))))

(define lit-list-copies
  ((lits lit-listp) (copy))
  :guard (< (lits-max-id-val lits)
    (lits-length copy))
  :returns (new-lits lit-listp)
  :verify-guards nil
  (mbe :logic (if (atom lits)
      nil
      (cons (lit-copy (car lits) copy)
        (lit-list-copies (cdr lits) copy)))
    :exec (lit-list-copies-aux (reverse lits)
      copy
      nil))
  ///
  (defret len-of-<fn>
    (equal (len new-lits)
      (len lits)))
  (local (defthm rev-of-revappend
      (equal (rev (revappend x y))
        (append (rev y) (true-list-fix x)))
      :hints (("Goal" :in-theory (enable rev)))))
  (local (defthm lit-list-copies-aux-elim
      (equal (lit-list-copies-aux lits
          copy
          acc)
        (append (lit-list-copies (rev lits) copy)
          acc))
      :hints (("Goal" :in-theory (enable lit-list-copies-aux rev)))))
  (local (defthm lits-max-id-val-of-revappend
      (equal (lits-max-id-val (revappend x y))
        (max (lits-max-id-val x)
          (lits-max-id-val y)))
      :hints (("Goal" :in-theory (enable lits-max-id-val)))))
  (local (defthm lit-listp-revappend
      (implies (and (lit-listp x)
          (lit-listp y))
        (lit-listp (revappend x y)))))
  (verify-guards lit-list-copies))

(define lit-list-marked
  ((lits lit-listp) (mark))
  :guard (< (lits-max-id-val lits)
    (bits-length mark))
  :guard-hints (("goal" :in-theory (enable lits-max-id-val)))
  (if (atom lits)
    t
    (and (eql (get-bit (lit->var (car lits))
          mark)
        1)
      (lit-list-marked (cdr lits) mark))))

(define lit-list-vars
  ((x lit-listp))
  :returns (vars nat-listp)
  (if (atom x)
    nil
    (cons (lit->var (car x))
      (lit-list-vars (cdr x))))
  ///
  (defret len-of-<fn>
    (equal (len vars) (len x))))