; main function is testgen -- toward the bottom

(define (list->goal goal-list module)
 (make-boolean-state-expression
  (string-append "(or "
   (apply string-append
     (map (lambda (g) (string-append g " ")) 
     goal-list))
   ")")
  module))

(define (goal-reduce scan goal-list path)
  (let loop ((acc '())
	     (gl goal-list))
    (if (null? gl)
	acc
	(loop
	 (if (boolean-value-at scan path (car gl) (sal-path/length path))
	     (begin
	       (display "----- Discharged ")(display (car gl)) (newline)
	       acc
	       )
	     (cons (car gl) acc))
	 (cdr gl)))))

(define (minimal-goal-reduce scan goal-list path)
  (let loop ((acc '())
	     (gl goal-list))
;;    (breakpoint "minimal" (path scan gl) #t)
    (if (boolean-value-at scan path (car gl) (sal-path/length path))
	(begin
	  (display "----- Discharged ")(display (car gl)) (newline)
	  (append acc (cdr gl)))
	(loop (cons (car gl) acc) (cdr gl)))))

(define (boolean-value-at scan path v id)
  (if scan
      (let loop ((pos id))
	(if (> pos 0)
	    (let ((val (sal-path/state-variable-value-at path (string->symbol v) (- pos 1))))
;;	      (breakpoint "innerloop" (path v id val) (< pos id))
	      (if val
		  (if (sal-expr/true? val)
		      #t
		      (loop (- pos 1)))
		  #f))
	    #f))
      (let ((val (sal-path/state-variable-value-at path (string->symbol v) (- id 1))))
	(if val (sal-expr/true? val) #f))))

(define (extend-search module goal-list path scan prune innerslice start step stop)
  (begin
    (display "+++++ Path now of length ")(display (sal-path/length path))(newline)
  (let ((new-goal-list (if prune
			   (goal-reduce scan goal-list path)
			   (minimal-goal-reduce scan goal-list path))))
;;    (breakpoint "reduce" (goal-list path new-goal-list) '#t)
    (cond ((null? new-goal-list) (cons '() path))
	  ((> start stop) (cons new-goal-list path))
	  (else
	   (let* ((goal (list->goal new-goal-list module))
		  (mod (if innerslice (sal-module/slice-for module goal) module))
		  (new-path
		   (let loop ((depth start))
;;			(breakpoint "extend" (depth npath) #t)
			(cond ((> depth stop) '())
			      ((sal-bmc/extend-path path mod goal depth 'ics))
			      (else
			       (loop (+ depth step)))))))
	     (if (pair? new-path)
		 (extend-search mod new-goal-list new-path scan prune innerslice start step stop)
	       (cons new-goal-list path))))))))

(define (iterative-search module goal-list scan prune slice innerslice bmcinit start step stop)
  (let* ((goal (list->goal goal-list module))
         (mod (if slice (sal-module/slice-for module goal) module))
         (path (if bmcinit
		   (sal-bmc/find-path-from-initial-state mod goal bmcinit 'ics)
		 (sal-smc/find-path-from-initial-state mod goal))))
      (if path
          (extend-search mod goal-list path scan prune innerslice start step stop)
          #f)))

; Arguments to testgen (mostly passed on to subsidiary functions)
; module: the boolean-flat-module to be analyzed
; goal-list: list of trap variables
; scan: whether full path should be scanned to see if a trap variable has become true
;   (if trap variables latch, leave this false and only the last state will be checked)
; prune: whether the goal list should be purged of all trap variables that have become true
;   (otherwise only the one targeted is removed)
; slice: whether to slice before starting a new path
; innerslice: whether to slice before each extension to the current path
; bmcinit: if #f, use SMC to start each path; otherwise the depth of BMC to be used
; start: the initial depth of BMC to be used in constructing an extension
; step: the increment in BMC depth to be used
; stop: the max BMC depth to be used; if 0, extensions will not be constructed

; output is a list: undischarged goals followed by a null-terminated list of paths.

(define (testgen module goal-list scan prune slice innerslice bmcinit start step stop)
  (let loop ((result '())
	     (goals goal-list))
       (if (null? goals) (cons goals result)
	 (let ((new-result (iterative-search module goals scan prune
						  slice innerslice bmcinit start step stop)))
;	   (breakpoint "innerloop" (new-result result goals) #t)
	   (if new-result
	     (loop (cons (cdr new-result) result) (car new-result))
	       (cons goals result))))))

(define (print-tests test-list inputs-only?)
  (map (lambda (x) 
	 (if (null? x) x
	     (sal-path/pp (sal-derived-input-seq->original-input-seq x) inputs-only?)))
       test-list))

(define (count-tests test-list)
  (let loop ((acc 0)
	     (l test-list))
    (if (null? l)
	acc
	(loop (+ acc (- (sal-path/length (car l)) 1)) (cdr l)))))