; Depends on er.plf

; Type for representing success when testing a side-condition
(declare TestSuccess type)

; Test for clause_add_suffix_all
(declare test_clause_add_suffix_all
         (! list clause
            (! suffix clause
               (! result cnf
                  (! (^ (clause_add_suffix_all list suffix) result)
                     TestSuccess)))))

(check
  (% a lit
  (% b lit
  (% c lit
     (test_clause_add_suffix_all
       (clc a (clc b cln))
       (clc c cln)
       (cnfc (clc a (clc c cln))
        (cnfc (clc b (clc c cln))
        cnfn))
     )
  )))
)

; This is a circuitous proof that uses the definition introduction and
; unrolling rules
(check
  (% v1 var
  (% v2 var
    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln)))
    (% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln)))
    (% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln)))
    (% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln)))
       (: (holds cln)
          (decl_definition
            (neg v1)
            (clc (neg v2) cln)
            (\ v3
            (\ def3
              (clausify_definition _ _ _ def3 _ _
                (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln)))
                (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln)))
                (\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn))
                  (cnfc_unroll_towards_bottom _ _ pf_cnf3
                    (\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln)))
                    (\ pf_cnfn
                                                                          ; Clauses
                  (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1)  (\ pf_c8 ; v2
                  (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2)  (\ pf_c9 ; v3
                  (satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3)  (\ pf_c10 ; ~v2  ~v1
                  (satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2)  (\ pf_c11 ; ~v1
                  (satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1)  (\ pf_c12 ; ~v2
                  (satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2)  (\ pf_c13 ; empty
                        pf_c13
                  ))
                  ))
                  ))
                  ))
                  ))
                  ))
                  )))
                )))
              )
            ))
          )
        )
    ))))
  ))
)

; This is a test of ER proof produced by drat2er on Example 1 from:
; https://www.cs.utexas.edu/~marijn/drat-trim/
(check
  (% v1 var
  (% v2 var
  (% v3 var
  (% v4 var
    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
       (: (holds cln)
          (decl_definition
            (neg v1)
            cln
            (\ v5
            (\ def1
              (clausify_definition _ _ _ def1 _ _
                (\ pf_c9 ; type: (holds (clc (pos def1v) cln))
                (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln)))
                (\ idc0 ; type: (cnf_holds cnfn)
                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11
                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12
                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13
                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14
                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15
                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16
                  (satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17
                  (satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18
                    pf_c18
                  ))))))))))))))))
                )))
              )
            ))
          )
       )
    ))))))))
  ))))
)