#| 

This module implements some functions to compute unsat cores over propositional logic formulas.

|#
(module unsat-core mzscheme
  
  (require (lib "file.ss")
           (lib "port.ss")
           (lib "process.ss")
           (lib "etc.ss")
           (lib "list.ss")
           (prefix srfi1: (lib "1.ss" "srfi"))
           (prefix srfi13: (lib "13.ss" "srfi"))
           "lprop2cnf.scm"
           "cnfrd-ly.scm"
           "proc-utils.scm")
  
  (provide zchaff-path
           compute-unsat-core)
  
  (define zchaff-path 
    (make-parameter "/home/pmatos/solvers/zchaff64/")) ; in galileu
    ;(make-parameter "/home/pmatos/solvers/zchaff-2007.3.12/")) ; in euler
  
  ;; Given a prop logic formula, returns a list of subformulas which
  ;; form the unsat core.
  (define (compute-unsat-core formula)
    ;; We first convert the formula to CNF.
    ;; Once the formula is in CNF, we dump the formula to a file and run zchaff on it.
    ;; After running zchaff we call zverify_df
    ;; Now we read in the unsat core from unsat-core.cnf using the CNF parser.
    ;; Each variable in each clause we replace it by its value in the hash table and return this.
    (let-values ([(hash clause-hash num-vars clauses) (lprop->cnf formula)])
      (let ([tmp-file (path->string (make-temporary-file))])
        (printf "UnsatCore: CNF ~a~n" tmp-file)
        (output-cnf num-vars clauses tmp-file)
        (parameterize ([current-directory (find-system-path 'temp-dir)])
          (let* ([resolve-trace-file (run-zchaff-on-unsat tmp-file)])
            (printf "UnsatCore: Trace ~a~n" resolve-trace-file)
            (let-values ([(stdout stdin pid stderr proc) (apply values (process*/ports (open-output-nowhere) (open-input-file "/dev/null") (open-output-nowhere) 
                                                                                               (string-append (zchaff-path) "zverify_df") tmp-file resolve-trace-file "-core"))]) 
              (proc 'wait)
              (printf "UnsatCore: Core ~a~n" (string-append (path->string (current-directory)) "unsat_core.cnf") )
              (let-values ([(info clauses) (get-clauses-from-cnf (string-append (path->string (current-directory)) "unsat_core.cnf") 
                                                                 (λ (c)
                                                                   (hash-table-get clause-hash (sort c <)
                                                                                   (λ () 
                                                                                     (if (and (= (length c) 1)
                                                                                              (= (car c) num-vars))
                                                                                         formula
                                                                                         (error 'compute-unsat-core 
                                                                                                "Can't find info for clause ~a on clause hash" c)))))
                                                                 identity)])
                (srfi1:delete-duplicates! clauses equal?))))))))
   
  (define (run-zchaff-on-unsat cnf-file)
;    (printf "CNF-file: ~a~n" cnf-file)
    (begin (with-input-from-subprocess 
            (λ ()
              (let loop ([line (read-line)])
                ;(printf "Line: ~a~n" line)
                (if (eof-object? line)
                    (error 'run-zchaff-on-unsat "While parsing zchaff output found eof before line starting with \"RESULT:\"")
                    (if (srfi13:string-prefix? "RESULT:" line)
                        (unless (string=? (srfi13:string-trim-both (srfi13:string-drop line 7)) "UNSAT")
                          (error 'run-zchaff-on-unsat "should be run only on UNSAT instances."))
                        (loop (read-line))))))
            (string-append (zchaff-path)  "zchaff") cnf-file)
           (string-append (path->string (current-directory)) "resolve_trace")))
        
  )