; ************************************************************
; genmodal.lsp
; Version:       1.1 (1997-04-16)
;
; Modifications: Ullrich Hustadt     1996-1997
;                Roberto Sebastiani
;                Enrico  Franconi
;
; CHANGES since Version 1.0 (1997-02-26) Ullrich Hustadt
; - Added a function gen-test
;   A call to gen-test will generate a random modal formula
;   and write it to three different files according to the
;   syntax of KSAT, KRIS, and FT.
; - Added the necessary output functions for gen-test.
;
; ************************************************************

; Declaration of parameters

(defvar *neg_prob*)        ; ratio negative literals
(defvar *var_num*)         ; variable number
(defvar *rule_num*)        ; number of distinct modalities (only for MK)
(defvar *and_br*)          ; and branching
(defvar *or_br*)           ; or branching
(defvar *prim_conc_prob*)  ; ratio primitive concepts/concepts
(defvar *mod_degree*)      ; modal depth

; You have to set the parameters before calling 
; (generate-rand-formula)
; to generate a random modal formula. 
;
; According to the guidelines of Hustadt and Schmidt (1997) 
; the parameters *rule_num*, *or_br*, *prim_conc_prob*, and *mod_degree*
; should be set as follows:

(setq *rule_num* 1)
(setq *or_br* 3)
(setq *prim_conc_prob* 0)
(setq *mod_degree* 1)

; *neg_prob* should be 0.5

(setq *neg_prob* 0.5)

; The only parameters remaining are the number of propositional variables
; and the number of conjunctions in the formula.

(setq *var_num* 4)
(setq *and_br*  40)

(setq *random-state* (make-random-state t))

; *gent-pathname*
; Directory where the files containing the random formula in KRIS, KSAT,
; and FT syntax should be placed.
; Note: A backslash "/" at the end of the string is required
(setq *gent-pathname* "./samples/")


;--------------------------------------------------------------------------------
; Nothing needs to be changed below this line
;--------------------------------------------------------------------------------

; gen-test 
; Generates a random modal formula and writes to three different files
; according to the syntax of KRIS, KSAT, and FT.

(defun gen-test ()
  (let ((concept (generate-rand-formula)))
    (write-prolog concept)
    (write-ksat   concept)
    (write-kris   concept))
  t)

(defun write-ksat (term)
  (format t "Writing ~Aalc.ksat~%" *gent-pathname*)
  (with-open-file (tfile (format nil "~aalc.ksat" *gent-pathname*)
			 :direction :output)
		  (princ "(setq test-concept '" tfile)
		  (princ term tfile)
		  (princ ")" tfile)
		  (terpri tfile)
		  (princ "(setq role-num " tfile)
		  (princ *rule_num* tfile)
		  (princ ")" tfile)
		  (terpri tfile)))

(defun write-kris (term)
  (format t "Writing ~Aalc.kris~%" *gent-pathname*)
  (with-open-file (tfile (format nil "~aalc.kris" *gent-pathname*)
			 :direction :output)
		  (do ((i 1 (setq i (1+ i)))) ((eq i (1+ *var_num*)))
		      (princ "(defprimconcept " tfile)
		      (princ (format nil "c~a" i) tfile)
		      (princ ")" tfile)
		      (terpri tfile))
		  (do ((i 1 (setq i (1+ i)))) ((eq i (1+ *rule_num*)))
		      (princ "(defprimrole " tfile)
		      (princ (format nil "r~a" i) tfile)
		      (princ ")" tfile)
		      (terpri tfile))
		  (princ "(defconcept d0 " tfile)
		  (princ term tfile)
		  (princ ")" tfile)
		  (terpri tfile)))

(defun write-prolog (term)
  (format t "Writing ~Aalc.pl~%" *gent-pathname*)
  (with-open-file (tfile (format nil "~aalc.pl" *gent-pathname*)
			 :direction :output)
		  (printProlog term tfile)
		  (princ "." tfile)))

(defun printProlog (term tfile)
  (if (and term
	   (listp term))
      (cond ((equal (car term) 'not)
	     (princ "not(" tfile)
	     (printProlog (car (cdr term)) tfile)
	     (princ ")" tfile))
	    ((equal (car term) 'and)
	     (princ "and([" tfile)
	     (printPrologList (cdr term) tfile)
	     (princ "])" tfile)
	     )
	    ((equal (car term) 'or)
	     (princ "or([" tfile)
	     (printPrologList (cdr term) tfile)
	     (princ "])" tfile)
	     )
	    ((equal (car term) 'some)
	     (princ "some(" tfile)
	     (printProlog (car (cdr term)) tfile)
	     (princ "," tfile)
	     (printProlog (car (cdr (cdr term))) tfile)
	     (princ ")" tfile)
	     )
	    ((equal (car term) 'all)
	     (princ "all(" tfile)
	     (printProlog (car (cdr term)) tfile)
	     (princ "," tfile)
	     (printProlog (car (cdr (cdr term))) tfile)
	     (princ ")" tfile)
	     )
	    (T 
	     (princ "**[" tfile)
	     (princ term tfile)
	     (princ "]**" tfile))
	    )
    (if term
	(princ term tfile))))

(defun printPrologList (list tfile)
  (if (and list
	   (listp list))
      (progn
	(printProlog (car list) tfile)
	(if (cdr list)
	    (progn
	      (princ "," tfile)
	      (terpri tfile))
	  )
	(printPrologList (cdr list) tfile))
    ))


;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%% random formulas ALC / K(n) generator
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

;;; Adapted from rseba@frege.mrg.dist.unige.it

;******************* general *************************************************

(defun generate-rand-formula ()
  (c-mkand (rand-conj_clist-mak *and_br* *mod_degree*)))


;******************* conjunction *********************************************

(defun rand-conj_clist-mak (branch_rate grade)
 (cond
  ((equal branch_rate 0) NIL)
  ((equal branch_rate 1) (list (rand-disj_conc-mak grade)))
  (T (cons (rand-disj_conc-mak grade)
           (rand-conj_clist-mak (- branch_rate 1) grade)))))

;******************* disjunction *********************************************

(defun rand-disj_conc-mak (grade)
  (c-mkor (rand-fixed-length-disjunction *or_br* grade NIL)))

(defun rand-fixed-length-disjunction (branch_rate grade subterm_list)
 (cond
  ((equal branch_rate 0) NIL)
  ((equal branch_rate 1) (list (rand-literal-mak grade subterm_list)))
  (T (let ((subterm (rand-literal-mak grade subterm_list)))
       (cons subterm
	     (rand-fixed-length-disjunction (- branch_rate 1) 
					    grade 
					    (cons subterm subterm_list)))))))


(defun add-term (term list)
  (if (and term (listp term))
      list
    (cons term list)))

;******************* rules *****************************************************

(defun rand-literal-mak (grade subterm_list)
 (if (equal grade 0)
  (rand-prim_conc-mak subterm_list)
  (if (rand-event *prim_conc_prob*)
    (rand-prim_conc-mak subterm_list)
    (rand-ruled_conc-mak grade))))

;grade must be > 0
(defun rand-ruled_conc-mak (grade)
 (let ((c (rand-disj_conc-mak (- grade 1)))
       (r (rand-rule-mak)))
   (let ((modal_term (c-mkall r c))
	 (neg_event (rand-event *neg_prob*)))
     (if neg_event
	 (c-mknot modal_term)
       modal_term))))
 
;******************* primitive **********************************************
   
(defun rand-prim_conc-mak (subterm_list)
  (let ((atom (c-mkatom (+ 1 (random *var_num*)))))
    (if (or (member atom subterm_list :test #'equal)
	    (member (c-mknot atom) subterm_list :test #'equal))
	(rand-prim_conc-mak subterm_list)
      (if (rand-event *neg_prob*)
	  (c-mknot atom)
	atom))))

(defun rand-rule-mak () (c-mkrule (+ 1 (random *rule_num*))))

;******************* costructors ****************************************


(defun c-mknot (c) (list 'not c))
(defun c-mkand (c_list) (cons 'and c_list))
(defun c-mkor  (c_list) (cons 'or  c_list))
(defun c-mksome (r c) (list 'some r c))
(defun c-mkall  (r c) (list 'all  r c))

(defun c-mkrule (num) (intern (concatenate 'string "r" (write-to-string num))))
(defun c-mkatom (num) (intern (concatenate 'string "c" (write-to-string num))))

;returns T with probability prob, NIL with prbability 1-prob;
(defvar *MAX_NUM*)
(setq *MAX_NUM* 1000000)
(defun rand-event (prob) (> (* prob *MAX_NUM*) (random *MAX_NUM*) ))

; Function:  printProlog
; Arguments: 1. Modal formula generated by (generate-rand-formula)
;            2. Output stream
; Prints the given modal formula to the given output stream using the
; syntax appropriate for the translator of modal formulae to first-order
; logic.

(defun printProlog (term tfile)
  (if (and term
	   (listp term))
      (cond ((equal (car term) 'not)
	     (princ "not(" tfile)
	     (printProlog (car (cdr term)) tfile)
	     (princ ")" tfile))
	    ((equal (car term) 'and)
	     (princ "and([" tfile)
	     (printPrologList (cdr term) tfile)
	     (princ "])" tfile)
	     )
	    ((equal (car term) 'or)
	     (princ "or([" tfile)
	     (printPrologList (cdr term) tfile)
	     (princ "])" tfile)
	     )
	    ((equal (car term) 'some)
	     (princ "some(" tfile)
	     (printProlog (car (cdr term)) tfile)
	     (princ "," tfile)
	     (printProlog (car (cdr (cdr term))) tfile)
	     (princ ")" tfile)
	     )
	    ((equal (car term) 'all)
	     (princ "all(" tfile)
	     (printProlog (car (cdr term)) tfile)
	     (princ "," tfile)
	     (printProlog (car (cdr (cdr term))) tfile)
	     (princ ")" tfile)
	     )
	    (T 
	     (princ "**[" tfile)
	     (princ term tfile)
	     (princ "]**" tfile))
	    )
    (if term
	(princ term tfile)))
  t
)

(defun printPrologList (list tfile)
  (if (and list
	   (listp list))
      (progn
	(printProlog (car list) tfile)
	(if (cdr list)
	    (progn
	      (princ "," tfile)
	      (terpri tfile))
	  )
	(printPrologList (cdr list) tfile))
    ))