(module lprop2cnf mzscheme
  
  (require (prefix srfi1: (lib "1.ss" "srfi"))
           (prefix srfi71: (lib "71.ss" "srfi"))
           (lib "42.ss" "srfi")
           (lib "list.ss")
           (lib "file.ss")
           (lib "etc.ss")
           (lib "contract.ss")
           (lib "plt-match.ss")
           "cardinality-constraints.scm")
  
  ;; Given f with binary ops <->, ->, ite, xor, not, and, or, simplifies formula for binary
  ;; not, and, or operators
  (define (remove-redundant-ops f)
    ;(printf "Removing ROps: ~a~n" f)
    (match f
      (`(=> ,op1 ,op2)
        `(or (not ,(remove-redundant-ops op1))
             ,(remove-redundant-ops op2)))
      (`(<=> ,op1 ,op2)
        (remove-redundant-ops
         `(and (=> ,op1 ,op2)
               (=> ,op2 ,op1))))
      (`(xor ,op1 ,op2)            ;; Binary xor
        (remove-redundant-ops
         `(not (<=> ,op1 ,op2))))
      (`(ite ,op1 ,op2 ,op3)
        (remove-redundant-ops
         `(and (=> ,op1 ,op2)
               (=> (not ,op1) ,op3))))
      (`(xor ,ops ..3)            ;; Multiple argument xor, which is true iff exactly only one of the ops is true
       (remove-redundant-ops
        `(and (or ,@ops)
              ,(apply encode-atmost1/lprop ops))))
      (`(am1 ,ops ..2)            ;; Multiple argument atmost1 operator, encoding of cardinality constraints used
       (remove-redundant-ops (apply encode-atmost1/lprop ops)))
      (`(and ,ops ..1)
        `(and ,@(map remove-redundant-ops ops)))
      (`(or ,ops ..1)
        `(or ,@(map remove-redundant-ops ops)))
      (`(not ,op)
        `(not ,(remove-redundant-ops op)))
      ((? (λ (a) (or (symbol? a)
                     (boolean? a))) s)
       s)
      (_ (error 'remove-redundant-ops "Couldn't find a match for ~a" f))))
  
  (define (lprop->cnf formula)
    (let ([var-hash (make-hash-table)]   ; hash-table code -> var
          [clause-hash (make-hash-table 'equal)] ; hash-table clause (list-of integer?) -> lprop-formula
          [code-hash (make-hash-table 'equal)]) ; hash-table var or formula -> code
      (letrec ([new-code
                (let ([avail-code 1])
                  (λ ()
                    (begin0
                      avail-code
                      (set! avail-code (+ avail-code 1)))))]
               [insert-var 
                (λ (v)
                  (let ([code (new-code)])
                    (hash-table-put! var-hash code v)
                    (hash-table-put! code-hash v code)
                    code))]
               [insert-formula
                (λ (f) 
                  (let ([code (new-code)])
                    (hash-table-put! code-hash f code)
                    code))]
               [get-var-code 
                (λ (v) (hash-table-get code-hash v (λ () (insert-var v))))]
               [get-formula-code
                (λ (f) (hash-table-get code-hash f (λ () #f)))]
               [insert-clauses ;; Inserts the clauses in clause-hash with respect to formula f
                               ;; and returns a list with the clauses.
                (λ (f . clauses)
                  (for-each (λ (c) (hash-table-put! clause-hash (sort c <) f)) clauses)
                  clauses)])
        (apply values 
               var-hash
               clause-hash
               (let-values ([(top-level-code top-level-clauses)
                             (let loop ([f formula])
                               (match f 
                                 (`(and ,ops ..1)
                                  (let ([ids/clauses (map (λ (op) (srfi71:values->list (loop op))) ops)])
                                    (let* ([ids (sort! (map car ids/clauses) <)]
                                           [clauses (apply append (map cadr ids/clauses))]
                                           [reuse-code (get-formula-code `(and ,@ids))])
                                      (if reuse-code
                                          (values reuse-code clauses)
                                          (let ([code (insert-formula `(and ,@ids))])
                                            (values code
                                                    (append (apply insert-clauses f
                                                                   (cons (cons code (map (λ (id) (- id)) ids))
                                                                         (map (λ (id) (list id (- code))) ids)))
                                                            clauses)))))))
                                 (`(or ,ops ..1)
                                  (let ([ids/clauses (map (λ (op) (srfi71:values->list (loop op))) ops)])
                                    (let* ([ids (sort! (map car ids/clauses) <)]
                                           [clauses (apply append (map cadr ids/clauses))]
                                           [reuse-code (get-formula-code `(or ,@ids))])
                                      (if reuse-code
                                          (values reuse-code clauses)
                                          (let ([code (insert-formula `(or ,@ids))])
                                            (values code
                                                    (append (apply insert-clauses f
                                                                   (cons (cons (- code) ids)
                                                                         (map (λ (id) (list (- id) code)) ids)))
                                                            clauses)))))))
                                 (`(not ,op)
                                  (let-values ([(id clauses) (loop op)])
                                    (let ([reuse-code (get-formula-code `(not ,id))])
                                      (if reuse-code
                                          (values reuse-code clauses)
                                          (let ([code (insert-formula `(not ,id))])
                                            (values code
                                                    (append (insert-clauses f 
                                                                            (list id code)
                                                                            (list (- id) (- code)))
                                                            clauses)))))))
                                 ((? (λ (a) (or (symbol? a)
                                                (boolean? a))) s) (values (get-var-code s) '()))
                                 ;; Auxiliary formula definitions
                                 (`(=> ,op1 ,op2)
                                  (let-values ([(id1 clauses1) (loop op1)]
                                               [(id2 clauses2) (loop op2)])
                                    (let ([reuse-code (get-formula-code `(=> ,id1 ,id2))])
                                      (if reuse-code
                                          (values reuse-code (append clauses1 clauses2))
                                          (let ([code (insert-formula `(=> ,id1 ,id2))])
                                            (values code
                                                    (append (insert-clauses f
                                                                            (list (- id1) id2 (- code))
                                                                            (list id1 code)
                                                                            (list (- id2) code))
                                                            clauses1 
                                                            clauses2)))))))
                                 (`(<=> ,op1 ,op2)
                                  (let-values ([(id1 clauses1) (loop op1)]
                                               [(id2 clauses2) (loop op2)])
                                    (let* ([sorted-ids (sort (list id1 id2) <)]
                                           [reuse-code (get-formula-code `(<=> ,@sorted-ids))])
                                      (if reuse-code
                                          (values reuse-code (append clauses1 clauses2))
                                          (let ([code (insert-formula `(<=> ,@sorted-ids))])
                                            (values code
                                                    (append (insert-clauses f
                                                                            (list id1 id2 code)
                                                                            (list id1 (- id2) (- code))
                                                                            (list (- id1) (- id2) code)
                                                                            (list (- id1) id2 (- code)))
                                                            clauses1 
                                                            clauses2)))))))
                                 (`(xor ,op1 ,op2)
                                  (let-values ([(id1 clauses1) (loop op1)]
                                               [(id2 clauses2) (loop op2)])
                                    (let* ([sorted-ids (sort (list id1 id2) <)]
                                           [reuse-code (get-formula-code `(<=> ,@sorted-ids))])
                                      (if reuse-code
                                          (values reuse-code (append clauses1 clauses2))
                                          (let ([code (insert-formula `(<=> ,@sorted-ids))])
                                            (values code
                                                    (append (insert-clauses f
                                                                            (list id1 id2 (- code))
                                                                            (list id1 (- id2) code)
                                                                            (list (- id1) (- id2) (- code))
                                                                            (list (- id1) id2 code))
                                                            clauses1 
                                                            clauses2)))))))
                                 (`(ite ,op1 ,op2 ,op3)
                                  (let-values ([(id1 clauses1) (loop op1)]
                                               [(id2 clauses2) (loop op2)]
                                               [(id3 clauses3) (loop op3)])
                                    (let* ([coded-f `(ite ,id1 ,id2 ,id3)]
                                           [reuse-code (get-formula-code coded-f)])
                                      (if reuse-code
                                          (values reuse-code (append clauses1 clauses2 clauses3))
                                          (let ([code (insert-formula coded-f)])
                                            (values code 
                                                    (append (insert-clauses f 
                                                                            (list id1 id3 (- code))
                                                                            (list id1 (- id3) code)
                                                                            (list (- id1) id2 (- code)))
                                                            clauses1 
                                                            clauses2)))))))
                                 (`(am1 ,ops ..2)
                                  (let ([ids/clauses (map (λ (op) (srfi71:values->list (loop op))) ops)])
                                    (let* ([ids (sort! (map car ids/clauses) <)]
                                           [clauses (apply append (map cadr ids/clauses))]
                                           [coded-f `(am1 ,@ids)]
                                           [reuse-code (get-formula-code coded-f)])
                                      (if reuse-code
                                          (values reuse-code clauses)
                                          (let ([aux-vars (build-list (apply encode-atmost1/needed-vars ids) (λ (n) (new-code)))]
                                                [code (insert-formula coded-f)])
                                            (values code
                                                    (append (apply insert-clauses f (apply encode-atmost1 aux-vars ids)) clauses)))))))
                                 (`(xor ,ops ..3)
                                  (loop `(and (or ,@ops) (am1 ,@ops))))
                                 (_ (error 'lprop2cnf "Couldn't find a match for ~a" f))))])
                 (let* ([false-code (get-var-code #f)]
                        [true-code (get-var-code #t)]
                        [false-needed (>= top-level-code false-code)]
                        [true-needed (>= top-level-code true-code)]
                        [mid-clause-set (if false-needed (cons (list (- false-code)) top-level-clauses) top-level-clauses)]
                        [final-clause-set (if true-needed (cons (list true-code) mid-clause-set) mid-clause-set)])
                   (list top-level-code final-clause-set)))))))
  
  (define (output-cnf num-vars clauses path)
    (let ([num-clauses (length clauses)])
      (call-with-output-file* path
                              (lambda (fp)
                                (fprintf fp "p cnf ~a ~a~n" num-vars (+ 1 num-clauses))
                                (for-each (λ (clause)
                                            (for-each (λ (literal) (fprintf fp "~a " literal)) clause)
                                            (fprintf fp "0~n"))
                                          clauses)
                                (fprintf fp "~a 0~n" num-vars))
                              'truncate)))
  
  (provide lprop->cnf output-cnf)
  
  )