cgen-search

(in-package "CGEN")

(include-book "simple-search")

(include-book "incremental-search")

(include-book "acl2s/check-equal" :dir :system)

(defttag t)

(set-register-invariant-risk nil)

(defttag nil)

(set-state-ok t)

(def-const *initial-test-outcomes%*
  (make test-outcomes%
    :cts 'nil
    :wts 'nil
    :vacs 'nil
    :|#wts| 0
    :|#cts| 0
    :|#vacs| 0
    :|#dups| 0))

(def initial-s-hist-entry%
  (name hyps
    concl
    vars
    elide-map
    start)
  (decl :sig ((string pseudo-term-list
       pseudo-term
       symbol-list
       symbol-alist
       rational) ->
      s-hist-entry%)
    :doc "make initial s-hist-entry% given args")
  (make s-hist-entry%
    :name name
    :hyps hyps
    :concl concl
    :vars vars
    :elide-map elide-map
    :start-time start
    :end-time start
    :test-outcomes *initial-test-outcomes%*))

(mutual-recursion (defun all-functions.
    (term ans.)
    "gather all functions in term"
    (declare (xargs :verify-guards nil
        :guard (and (pseudo-termp term)
          (symbol-listp ans.))))
    (if (variablep term)
      ans.
      (if (fquotep term)
        ans.
        (let ((fn (ffn-symb term)) (args (fargs term)))
          (if (or (equal fn 'if) (consp fn))
            (all-functions-lst. args ans.)
            (all-functions-lst. args
              (add-to-set-eq fn ans.)))))))
  (defun all-functions-lst.
    (terms ans.)
    (declare (xargs :verify-guards nil
        :guard (and (pseudo-term-listp terms)
          (symbol-listp ans.))))
    (if (endp terms)
      ans.
      (all-functions-lst. (cdr terms)
        (union-eq (all-functions. (car terms) ans.)
          ans.)))))

(defun all-functions
  (term)
  (declare (xargs :verify-guards nil
      :guard (pseudo-termp term)))
  (all-functions. term 'nil))

(defun all-functions-lst
  (terms)
  (declare (xargs :verify-guards nil
      :guard (pseudo-term-listp terms)))
  (all-functions-lst. terms 'nil))

(defun mv-sig-alist1
  (fns wrld)
  "for each fn with output arity n>1, the result alist
   will have an entry (fn . n)"
  (declare (xargs :guard (and (symbol-listp fns)
        (plist-worldp wrld))))
  (if (endp fns)
    nil
    (let* ((fn (car fns)) (stobjs-out (acl2-getprop fn
            'stobjs-out
            wrld
            :default '(nil))))
      (if (and (consp stobjs-out)
          (consp (cdr stobjs-out)))
        (acons fn
          (len stobjs-out)
          (mv-sig-alist1 (cdr fns) wrld))
        (mv-sig-alist1 (cdr fns) wrld)))))

(defun mv-sig-alist
  (terms wrld)
  "for each fn with output arity n>1 in terms, the result alist
   will have an entry (fn . n)"
  (declare (xargs :verify-guards nil
      :guard (and (pseudo-term-listp terms)
        (plist-worldp wrld))))
  (b* ((fns (all-functions-lst terms)))
    (mv-sig-alist1 fns wrld)))

(defloop var-var-eq-hyps
  (hyps)
  (for ((h in hyps))
    (append (and (equiv-hyp? h) (list h)))))

(defun update-var-var-binding
  (rep other b)
  (if (endp b)
    (cons (list other rep) nil)
    (cons (list (caar b)
        (if (equal other (second (car b)))
          rep
          (second (car b))))
      (update-var-var-binding rep
        other
        (cdr b)))))

(defun insert-lexorder
  (e x)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) (list e))
    ((equal e (car x)) x)
    ((lexorder e (car x)) (cons e x))
    (t (cons (car x)
        (insert-lexorder e (cdr x))))))

(defthm insert-lexorder-tl
  (implies (true-listp x)
    (true-listp (insert-lexorder e x))))

(defun append-lexorder
  (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (if (endp x)
    y
    (insert-lexorder (car x)
      (append-lexorder (cdr x) y))))

(defthm append-lexorder-tl
  (implies (and (true-listp x) (true-listp y))
    (true-listp (append-lexorder x y))))

(defun merge-class-into-classes
  (class classes)
  (declare (xargs :guard (and (true-listp class)
        (true-list-listp classes))))
  (cond ((endp classes) (list (append-lexorder class nil)))
    ((intersectp class (car classes) :test 'equal) (merge-class-into-classes (append-lexorder class (car classes))
        (cdr classes)))
    (t (cons (car classes)
        (merge-class-into-classes class (cdr classes))))))

(defthm merge-class-into-classes-tll
  (implies (and (true-listp class)
      (true-list-listp classes))
    (true-list-listp (merge-class-into-classes class classes))))

(defun merge-bindings-into-classes
  (bindings classes)
  (declare (xargs :guard (and (true-list-listp bindings)
        (true-list-listp classes))))
  (if (endp bindings)
    classes
    (merge-bindings-into-classes (cdr bindings)
      (merge-class-into-classes (car bindings)
        classes))))

(defun merge-bindings
  (bindings)
  (merge-bindings-into-classes bindings nil))

(check= (merge-bindings '((w w) (u v)
      (w x)
      (u x)
      (b u)
      (w w)))
  '((b u v w x)))

(defun make-bindings-from-class
  (rep class)
  (if (endp class)
    nil
    (cons (list (car class) rep)
      (make-bindings-from-class rep (cdr class)))))

(check= (make-bindings-from-class 'a
    '(b c d))
  '((b a) (c a) (d a)))

(defun make-bindings-from-classes
  (classes)
  (if (endp classes)
    nil
    (append (make-bindings-from-class (caar classes)
        (cdar classes))
      (make-bindings-from-classes (cdr classes)))))

(check= (make-bindings-from-classes '((a b c d) (x y z)))
  '((b a) (c a)
    (d a)
    (y x)
    (z x)))

(defun make-bindings
  (bindings)
  (make-bindings-from-classes (merge-bindings bindings)))

(check= (make-bindings '((d d) (a b)
      (b c)
      (d c)
      (b a)
      (c c)
      (c d)
      (b b)
      (x z)
      (x y)
      (z y)))
  '((b a) (c a)
    (d a)
    (y x)
    (z x)))

(defun apply-bindings-to-hyps
  (bindings hyps)
  (if (endp bindings)
    hyps
    (apply-bindings-to-hyps (cdr bindings)
      (subst-var-lst (cadar bindings)
        (caar bindings)
        hyps))))

(check= (apply-bindings-to-hyps '((b a) (c a)
      (d a)
      (y x)
      (z x))
    '((f a
       b
       c
       d
       e
       y
       x
       z
       u
       v) (g z b)
      (b b)
      ((lambda (b c) (list b c)) d
        y)))
  '((f a
     a
     a
     a
     e
     x
     x
     x
     u
     v) (g x a)
    (b a)
    ((lambda (b c) (list b c)) a
      x)))

(defun var-var-cc
  (var-var-eq-hyps hyps)
  (b* ((bindings (make-bindings (strip-cdrs var-var-eq-hyps))))
    (mv bindings
      (apply-bindings-to-hyps bindings hyps))))

(check= (var-var-cc '((= a b) (= c d)
      (= d b))
    '((f a b c d) (b a b c d)))
  (mv '((b a) (c a) (d a))
    '((f a a a a) (b a a a a))))

(def cgen-search-local
  (name h
    c
    type-alist
    tau-interval-alist
    programp
    test-outcomes%
    gcs%
    cgen-state
    ctx
    state)
  (decl :sig ((string pseudo-term-list
       pseudo-term
       symbol-list
       alist
       symbol-alist
       boolean
       test-outcomes%-p
       gcs%-p
       cgen-state-p
       symbol
       state) ->
      (mv erp
        (list boolean test-outcomes% gcs%)
        state))
    :mode :program :doc "
* Synopsis       
  Local interface to subgoal-level counterexample and witness
  search using either naive testing or incremental dpll
  style search for counterexamples.

* Input parameters (other than those in csearch, that are accumulated)
  - test-outcomes% :: newly created test-outcomes% for this subgoal
  - gcs% :: reified gcs%

* Output signature 
  - (mv erp (list stop? test-outcomes% gcs%) state) where erp is the error tag which is non-nil
    when an error took place during evaluation of (search ...). 
    stop? is T if we should abort our search, i.e our stopping
    condition is satisfied (this value is given by run-tests), 
    otherwise stop? is NIL (by default). test-outcomes% and gcs% are 
    accumulated in the search for cts and wts in the current conjecture

* What it does
  1. retrieve the various search/testing parameters

  2. call simple or incremental search
     depending on the search-strategy set in defaults.
  
  3. return error triple with value (list stop? test-outcomes% gcs%)
")
  (b* ((vl (cget verbosity-level)) (mv-sig-alist (mv-sig-alist (cons c h)
          (w state)))
      (var-var-eq-hyps (var-var-eq-hyps h))
      ((mv elim-bindings h) (var-var-cc var-var-eq-hyps h))
      (- (cw? (and (consp elim-bindings)
            (debug-flag vl))
          "Cgen/Debug : cgen-search:: elim-bindings:~x0  H:~x1~%"
          elim-bindings
          h))
      (vars (vars-in-dependency-order h
          c
          vl
          (w state))))
    (case (cget search-strategy)
      (:simple (simple-search name
          h
          c
          vars
          'nil
          elim-bindings
          type-alist
          tau-interval-alist
          mv-sig-alist
          test-outcomes%
          gcs%
          vl
          cgen-state
          programp
          nil
          ctx
          state))
      (:incremental (if (endp vars)
          (simple-search name
            h
            c
            vars
            'nil
            elim-bindings
            type-alist
            tau-interval-alist
            mv-sig-alist
            test-outcomes%
            gcs%
            vl
            cgen-state
            programp
            nil
            ctx
            state)
          (b* ((- (cw? (verbose-stats-flag vl)
                 "~%~%CEgen/Note: Starting incremental (dpll) search~%")) (x0 (select (cons (cgen-dumb-negate-lit c) h)
                  vl
                  (w state)))
              (- (assert$ (proper-symbolp x0) x0))
              (a% (make a%
                  :vars vars
                  :hyps h
                  :concl c
                  :partial-a 'nil
                  :elim-bindings elim-bindings
                  :type-alist type-alist
                  :tau-interval-alist tau-interval-alist
                  :inconsistent? nil
                  :cs nil
                  :var x0
                  :val ''?
                  :kind :na :i 0)))
            (incremental-search a%
              'nil
              name
              mv-sig-alist
              test-outcomes%
              gcs%
              vl
              cgen-state
              programp
              ctx
              state))))
      (otherwise (prog2$ (cw? (normal-output-flag vl)
            "~|CEgen/Error: Only simple & incremental search strategy are available~|")
          (mv t nil state))))))

(def cgen-search-fn
  (name h
    c
    type-alist
    tau-interval-alist
    elide-map
    programp
    cgen-state
    ctx
    state)
  (decl :sig ((string pseudo-term-list
       pseudo-term
       alist
       symbol-alist
       symbol-alist
       boolean
       cgen-state-p
       symbol
       state) ->
      (mv erp cgen-state state))
    :mode :program :doc "
* Synopsis       
  Main Interface to searching for counterexamples (and witnesses)
  in the conjecture (H => C)

* Input parameters
  - name :: name of subgoal or "top" if run from test?
  - H :: hyps - the list of terms constraining the cts and wts search
  - C :: conclusion
  - type-alist :: ACL2 type-alist (from call of forward-chain)
  - tau-interval-alist :: tau interval inferred by caller
  - elide-map :: elide-map[v] = term for each elided variable v
  - programp :: T when form has a program mode fun or we are in :program
  - cgen-state :: current cgen-state (to be accumulated)
  - ctx :: ctx (context -- usually a symbol naming the caller function)
  - state :: state

* Output signature 
  - (mv erp cgen-state-p state) where erp is the error tag which is non-nil
    when an error took place during evaluation of (search ...). 
    cgen-state is the updated cgen-state.

* What it does
  1. construct a new s-hist-entry% and call cgen-search-local fun
     with globals reified as explicit arguments: gcs%, test-outcomes%
  2. the return values of test-outcomes% (a field in s-hist-entry%), gcs% 
     are recorded in cgen-state
  3. return (mv erp cgen-state state)
")
  (f* ((update-cgen-state nil
       (b* ((s-hist-entry% (change s-hist-entry%
              test-outcomes
              test-outcomes%)) (s-hist-entry% (change s-hist-entry% end-time end))
           (s-hist (cget s-hist))
           (s-hist (put-assoc-equal name
               s-hist-entry%
               s-hist))
           (cgen-state (cput s-hist s-hist))
           (cgen-state (cput gcs gcs%))
           (cgen-state (cput stopping-condition-p stop?)))
         cgen-state)))
    (b* (((mv start state) (read-run-time state)) (vl (cget verbosity-level))
        (vars (vars-in-dependency-order h
            c
            vl
            (w state)))
        (s-hist-entry% (initial-s-hist-entry% name
            h
            c
            vars
            elide-map
            start))
        (test-outcomes% (access s-hist-entry% test-outcomes))
        (gcs% (cget gcs))
        ((mv erp res state) (cgen-search-local name
            h
            c
            type-alist
            tau-interval-alist
            programp
            test-outcomes%
            gcs%
            cgen-state
            ctx
            state))
        ((when erp) (mv t cgen-state state))
        ((unless (and (= 3 (len res))
             (booleanp (first res))
             (test-outcomes%-p (second res))
             (gcs%-p (third res)))) (prog2$ (cw? (verbose-flag vl)
              "~|Cgen/Error : Ill-formed result from local Cgen/testing driver code!~|")
            (mv t cgen-state state)))
        ((list stop? test-outcomes% gcs%) res)
        ((mv end state) (read-run-time state))
        (cgen-state (update-cgen-state)))
      (value cgen-state))))