lrat-interface

(in-package "SATLINK")

(include-book "cnf")

(include-book "projects/sat/lrat/list-based/lrat-checker" :dir :system)

(include-book "std/alists/alist-keys" :dir :system)

(local (include-book "cnf-basics"))

(define lit-to-lrat-literal
  ((x litp))
  :returns (lrat-x literalp
    :hints (("Goal" :in-theory (enable literalp
         lit->neg
         lit->var))))
  (b* ((negate (mbe :logic (if (eql (lit->neg x) 1)
           -1
           1)
         :exec (- 1 (* 2 (lit->neg x))))))
    (* negate (+ 1 (lit->var x))))
  ///
  (defret negate-of-lit-to-lrat-literal
    (equal (negate lrat-x)
      (lit-to-lrat-literal (lit-negate x))))
  (local (defthmd lit-fix-is-make-lit
      (equal (lit-fix x)
        (make-lit (lit->var x)
          (lit->neg x)))))
  (defthm equal-of-lit-to-lrat-literal
    (equal (equal (lit-to-lrat-literal x)
        (lit-to-lrat-literal y))
      (equal (lit-fix x)
        (lit-fix y)))
    :hints (("Goal" :in-theory (e/d (equal-of-make-lit lit-fix-is-make-lit)
         (make-lit-identity))))))

(define env$-to-lrat-assignment
  ((idx natp) (env$))
  :returns (assign literal-listp)
  :guard (<= idx (bits-length env$))
  (b* (((when (zp idx)) nil) (idx (1- idx))
      (val (eval-var idx env$))
      (lit (make-lit idx
          (b-not val))))
    (cons (lit-to-lrat-literal lit)
      (env$-to-lrat-assignment idx
        env$)))
  ///
  (local (defret not-member-literal
      (implies (<= (nfix idx)
          (lit->var lit))
        (not (member (lit-to-lrat-literal lit)
            assign)))
      :hints (("Goal" :in-theory (enable equal-of-make-lit)))))
  (defret unique-literalsp-of-env$-to-lrat-assignment
    (unique-literalsp assign))
  (defret not-conflicting-literalsp-of-env$-to-lrat-assignment
    (not (conflicting-literalsp assign)))
  (defret clause-or-assignment-p-of-env$-to-lrat-assignment
    (clause-or-assignment-p assign)
    :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
  (defret evaluate-literal-of-env$-to-lrat-assignment
    (implies (< (lit->var lit)
        (nfix idx))
      (equal (evaluate-literal (lit-to-lrat-literal lit)
          assign)
        (bit->bool (eval-lit lit env$))))
    :hints (("Goal" :in-theory (enable eval-lit
         equal-of-make-lit)))))

(local (in-theory (disable evaluate-literal)))

(define clause-to-lrat-clause
  ((clause lit-listp))
  :returns (mv tautologyp
    (lrat-clause literal-listp))
  (b* (((when (atom clause)) (mv nil nil)) ((mv taut rest) (clause-to-lrat-clause (cdr clause)))
      ((when taut) (mv t nil))
      (new-lit (lit-to-lrat-literal (car clause)))
      ((when (member (negate new-lit) rest)) (mv t nil))
      ((when (member new-lit rest)) (mv nil rest)))
    (mv nil (cons new-lit rest)))
  ///
  (defret unique-literals-of-clause-to-lrat-clause
    (unique-literalsp lrat-clause))
  (defret not-conflicting-literals-of-clause-to-lrat-clause
    (not (conflicting-literalsp lrat-clause)))
  (defret clause-or-assignment-p-of-clause-to-lrat-clause
    (clause-or-assignment-p lrat-clause)
    :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
  (local (defret eval-clause-when-true-member
      (implies (and (member (lit-to-lrat-literal lit)
            lrat-clause)
          (equal (eval-lit lit env$) 1))
        (equal (eval-clause clause env$)
          1))
      :hints (("Goal" :in-theory (enable eval-clause)))))
  (defret clause-to-lrat-clause-tautologyp-implies
    (implies tautologyp
      (equal (eval-clause clause env$)
        1))
    :hints (("Goal" :in-theory (enable eval-clause eval-lit))))
  (defret eval-of-clause-to-lrat-clause
    (implies (and (not tautologyp)
        (< (max-index-clause clause)
          (nfix idx)))
      (equal (evaluate-clause lrat-clause
          (env$-to-lrat-assignment idx
            env$))
        (bit->bool (eval-clause clause env$))))
    :hints (("Goal" :in-theory (enable eval-clause
         max-index-clause)))))

(local (in-theory (disable formula-truep)))

(local (defthm formula-truep-redef
    (implies (no-duplicatesp (alist-keys formula))
      (equal (formula-truep formula assign)
        (if (atom formula)
          t
          (if (and (consp (car formula))
              (not (deleted-clause-p (cdar formula))))
            (and (equal (evaluate-clause (cdar formula)
                  assign)
                t)
              (formula-truep (cdr formula) assign))
            (formula-truep (cdr formula) assign)))))
    :hints (("goal" :cases ((formula-truep formula assign))) (and stable-under-simplificationp
        (b* ((lit (assoc 'formula-truep clause)) ((unless lit) '(:use ((:instance formula-truep-necc
                   (index (caar formula))
                   (assignment assign)
                   (formula formula)))
                :in-theory (disable formula-truep-necc)))
            (other-form (if (eq (cadr lit) 'formula)
                '(cdr formula)
                'formula)))
          `(:expand (,SATLINK::LIT (alist-keys formula))
            :use ((:instance formula-truep-necc
               (index ,(CONS 'LRAT::FORMULA-TRUEP-WITNESS (CDR SATLINK::LIT)))
               (assignment assign)
               (formula ,SATLINK::OTHER-FORM)))
            :in-theory (disable formula-truep-necc)))))
    :rule-classes ((:definition :controller-alist ((formula-truep t nil))))))

(local (defthm formula-truep-of-cons
    (implies (no-duplicatesp (alist-keys (cons a b)))
      (equal (formula-truep (cons a b)
          assign)
        (if (and (consp a)
            (not (deleted-clause-p (cdr a))))
          (and (equal (evaluate-clause (cdr a) assign)
              t)
            (formula-truep b assign))
          (formula-truep b assign))))))

(define formula-to-lrat-formula
  ((formula lit-list-listp) (clause-idx posp))
  :returns (lrat-formula formula-p)
  (b* (((when (atom formula)) nil) ((mv taut lrat-clause) (clause-to-lrat-clause (car formula)))
      ((when taut) (formula-to-lrat-formula (cdr formula)
          clause-idx))
      (clause-idx (lposfix clause-idx)))
    (hons-acons clause-idx
      lrat-clause
      (formula-to-lrat-formula (cdr formula)
        (+ 1 clause-idx))))
  ///
  (defret formula-to-lrat-formula-lookup-key-too-small
    (implies (< key (lposfix clause-idx))
      (not (hons-assoc-equal key
          lrat-formula)))
    :hints (("Goal" :in-theory (enable hons-assoc-equal))))
  (defret no-duplicate-keys-of-formula-to-lrat-formula
    (no-duplicatesp (alist-keys lrat-formula)))
  (defret eval-of-formula-to-lrat-formula
    (implies (< (max-index-formula formula)
        (nfix idx))
      (equal (formula-truep lrat-formula
          (env$-to-lrat-assignment idx
            env$))
        (bit->bool (eval-formula formula env$))))
    :hints (("Goal" :in-theory (enable eval-formula
         max-index-formula)))))