(in-package "ACL2")

; Avoid some annoying warnings:
(set-inhibit-warnings "theory")

; Include the AIG+SAT proof-checker:
(include-book "/Users/kaufmann/fh/e/current/e/cbooks/aig/zz-check")

(defconst *aig*
  (aig-not (aig-iff (aig-or 'x (aig-or 'y 'z))
                    (aig-or 'z (aig-or 'y 'x)))))

(defconst *proof*
  '((0 ROOT ((Y) Z) Y Z)
    (1 ROOT ((X) (Y) Z) X (((Y) Z)))
    (2 ROOT (Y) (((Y) X)))
    (3 ROOT (X) (((Y) X)))
    (4 ROOT
       (((X) (Y) Z))
       (((Z) (Y) X))
       (((X) (Y) Z) (Z) (Y) X))
    (5 ROOT (((Z) (Y) X)) ((Y) X))
    (6 ROOT (Z) (((Z) (Y) X)))
    (7 ROOT Z ((Z) (Y) X) (((Y) X)))
    (8 ROOT X Y ((Y) X))
    (9 ROOT (((Y) Z)) (Z))
    (10 ROOT (((Y) Z)) (Y))
    (11 ROOT (((X) (Y) Z)) ((Y) Z))
    (12 ROOT (((X) (Y) Z)) (X))
    (13 ROOT
        ((((X) (Y) Z)) ((Z) (Y) X))
        ((X) (Y) Z)
        ((Z) (Y) X))
    (14 CHAIN
        7
        (((Y) X) . 8)
        ((Z) . 9)
        ((Y) . 10)
        (((Y) Z) . 11)
        ((X) . 12)
        (((X) (Y) Z) . 13))
    (15 ROOT
        (((((((X) (Y) Z)) ((Z) (Y) X)))
          (((X) (Y) Z) (Z) (Y) X)))
        ((((X) (Y) Z) (Z) (Y) X)))
    (16 ROOT
        (((((((X) (Y) Z)) ((Z) (Y) X)))
          (((X) (Y) Z) (Z) (Y) X)))
        (((((X) (Y) Z)) ((Z) (Y) X))))
    (17 CHAIN
        0
        ((((Y) Z)) . 1)
        ((Y) . 2)
        ((X) . 3)
        ((((X) (Y) Z)) . 4)
        (((Y) X) . 5)
        ((Z) . 6)
        (((Z) (Y) X) . 14)
        (((((X) (Y) Z) (Z) (Y) X)) . 15)
        ((((((X) (Y) Z)) ((Z) (Y) X))) . 16))))

; Redundant from included book:
(defthm zzchk-check-correct
  (implies (zzchk-check (aig-norm aig) proof)
           (not (aig-eval aig env))))

(defthm aig-is-unsat
  (not (aig-eval *aig* env))
  :hints 
  (("Goal"
    :use ((:instance zzchk-check-correct
                     (aig *aig*) (proof *proof*)))
    :in-theory '((zzchk-check) (aig-norm))))
  :rule-classes nil)

(defthm [not-aig]-is-valid
  (aig-eval (aig-not *aig*) env)
  :hints 
  (("Goal" :use aig-is-unsat)))