incremental-search

(in-package "CGEN")

(include-book "simple-search")

(include-book "select")

(defttag t)

(set-register-invariant-risk nil)

(defttag nil)

(defloop contains-var
  (x terms)
  "filter terms that contain variable x"
  (for ((term in terms))
    (append (and (member-eq x (all-vars term))
        (list term)))))

(def implied-symbolic-value
  (x type h vl state)
  (decl :sig ((symbol defdata-type
       pseudo-term-listp
       fixnum
       state) ->
      (mv erp pseudo-term state))
    :mode :program :doc "Assign to x: From type get the (recursive) type for
x. then look into additional constraints from H, to infer any lower-bounds or
narrower shape. return (mv exp new-hyps), where new-hyps are
new constraints on the introduced variables")
  (b* ((additional-constraints (contains-var x h)))
    (refine-enum-shape x
      type
      additional-constraints
      vl
      state)))

(defun remove-non-constant-value-entries
  (a)
  (declare (xargs :verify-guards nil
      :guard (alistp a)))
  (if (endp a)
    'nil
    (b* (((cons & val) (car a)) ((unless (possible-constant-value-p val)) (remove-non-constant-value-entries (cdr a))))
      (cons (car a)
        (remove-non-constant-value-entries (cdr a))))))

(def get-concrete-value
  (cs% partial-a
    sm
    vl
    ctx
    wrld
    state)
  (decl :sig ((fixnum cs%
       symbol-doublet-listp
       sampling-method
       fixnum
       symbol
       plist-world
       state) ->
      (mv erp
        (list pseudo-term keyword nil)
        state))
    :mode :program :doc "How: From cs% get the enumcall. trans-eval enumcall to
get value to be assigned. quote it to obtain a term. return (mv
val :decision nil), if size of type attributed to x is greater than 1,
otherwise return (mv val :implied nil) -- nil stands for empty
additional hyps")
  (f* ((_eval-single-value (call)
       (b* ((vexp (if partial-a
              `(let ,CGEN::PARTIAL-A
                (declare (ignorable ,@CGEN::BOUND-VARS))
                ,CGEN::CALL)
              call)) (- (cw? (debug-flag vl)
               "~|CEgen/Debug/incremental:  ASSIGN x to eval[~x0]~|"
               vexp)))
         (trans-eval-single-value vexp
           ctx
           state))))
    (b* ((- (assert$ (cs%-p cs%)
           'get-concrete-value)) (partial-a (remove-non-constant-value-entries partial-a))
        (bound-vars (strip-cars partial-a))
        ((mv size min max calls) (cs%-enumcalls cs%
            ctx
            wrld
            bound-vars))
        (seed. (getseed state))
        ((mv erp seed. ans state) (case sm
            (:uniform-random (b* (((mv m seed.) (choose-size min max seed.)) (call `(mv-list 2
                      (let ((seed. ,CGEN::SEED.))
                        ,(SUBST CGEN::M 'CGEN::M (SECOND CGEN::CALLS)))))
                  ((mv erp ans2 state) (_eval-single-value call)))
                (mv erp
                  (cadr ans2)
                  (car ans2)
                  state)))
            (otherwise (b* (((mv r seed.) (random-natural-seed seed.)) (call (subst r 'r (first calls)))
                  ((mv erp ans state) (_eval-single-value call)))
                (mv erp seed. ans state)))))
        ((when (or erp (equal size 0))) (mv t nil state))
        (state (putseed seed. state))
        (val-term (kwote ans)))
      (if (equal size 1)
        (value (list val-term :implied))
        (value (list val-term :decision))))))

(defloop get-corr-type-hyp
  (fn h)
  (for ((hyp in h))
    (if (and (consp hyp)
        (eq fn (car hyp))
        (proper-symbolp (cadr hyp)))
      (return hyp))))

(def assign-value
  (x cs%
    h
    partial-a
    sm
    vl
    ctx
    state)
  (decl :sig ((fixnum cs%
       pseudo-term-listp
       symbol-doublet-listp
       symbol-doublet-listp
       sampling-method
       fixnum
       symbol
       plist-world
       state) ->
      (mv erp
        (list pseudo-term keyword pseudo-term-listp)
        state))
    :mode :program :doc "assign a value (expression) to variable x under given constraints")
  (b* ((type (access cs% defdata-type)) (wrld (w state))
      (m (table-alist 'type-metadata-table wrld))
      (a (table-alist 'type-alias-table wrld))
      ((when (and (not (recursive-type-p type wrld))
           (record-p type wrld))) (b* (((mv rec-expansion field-type-hyps) (expand-record x type wrld)) (type-hyp (get-corr-type-hyp (predicate-name type a m)
                h))
            (updated-h (remove-equal type-hyp
                (union-equal field-type-hyps h))))
          (value (list rec-expansion :expand updated-h))))
      ((er ans) (implied-symbolic-value x
          type
          h
          vl
          state))
      ((list refined-term additional-hyps) ans))
    (if (or (null additional-hyps)
        (equal refined-term x))
      (b* (((er (list cval kind)) (get-concrete-value cs%
             partial-a
             sm
             vl
             ctx
             wrld
             state)))
        (value (list cval kind h)))
      (b* ((type-hyp (get-corr-type-hyp (predicate-name type a m)
             h)))
        (value (list refined-term
            :expand (remove-equal type-hyp
              (union-equal additional-hyps h))))))))

(defun put-val-a
  (name val dlist)
  "put list binding name->val in the front"
  (declare (xargs :guard (symbol-doublet-listp dlist)))
  (if (assoc-equal name dlist)
    (put-assoc-equal name
      (list val)
      dlist)
    (acons name (list val) dlist)))

(defrec a%
  ((hyps concl
     vars
     partial-a
     elim-bindings
     type-alist
     tau-interval-alist) ((var . cs) val
      kind
      i . inconsistent?))
  nil)

(defun a%-p
  (v)
  (declare (xargs :guard t))
  (case-match v
    (('a% (hyps concl
         vars
         partial-a
         elim-bindings
         type-alist
         tau-interval-alist)
       ((var . cs) val
         kind
         i . inconsistent?)) (and (symbol-listp vars)
        (pseudo-term-listp hyps)
        (pseudo-termp concl)
        (symbol-doublet-listp partial-a)
        (symbol-doublet-listp elim-bindings)
        (symbol-alistp type-alist)
        (symbol-alistp tau-interval-alist)
        (symbolp var)
        (pseudo-termp val)
        (member-eq kind
          (list :na :expand :implied :decision))
        (natp i)
        (booleanp inconsistent?)
        (or (null cs) (cs%-p cs))))))

(defun a%-listp
  (v)
  (declare (xargs :guard t))
  (if (atom v)
    (null v)
    (and (a%-p (car v))
      (a%-listp (cdr v)))))

(def assign-propagate
  (a% name
    sm
    top-vt-alist
    vl
    ctx
    state)
  (decl :sig ((a% string
       sampling-method
       symbol-doublet-list
       fixnum
       symbol
       state) ->
      (mv erp
        (list pseudo-term-list
          pseudo-term
          symbol-list
          symbol-doublet-list
          symbol-alist
          symbol-alist
          a%)
        state))
    :mode :program :doc "assign a value to a%.x and propagate this new info to obtain the updated a%")
  (b* ((`(a% ,CGEN::LV . &) a%) ((list h
         c
         vars
         partial-a
         elim-bindings
         type-alist
         tau-interval-alist) lv)
      ((mv x i) (mv (access a% var)
          (access a% i)))
      (wrld (w state))
      (acl2-vt-dlist (var-types-alist-from-acl2-type-alist type-alist
          vars
          'nil))
      ((mv erp top+-vt-dlist) (meet-type-alist acl2-vt-dlist
          top-vt-alist
          vl
          (w state)))
      (top+-vt-dlist (if erp
          (make-weakest-type-alist vars)
          top+-vt-dlist))
      (cs% (or (access a% cs)
          (assert$ (member-eq x vars)
            (cdr (assoc-eq x
                (collect-constraints% (cons (cgen-dumb-negate-lit c) h)
                  vars
                  top+-vt-dlist
                  type-alist
                  tau-interval-alist
                  vl
                  wrld))))))
      ((mv erp ans state) (assign-value x
          cs%
          (cons (cgen-dumb-negate-lit c) h)
          partial-a
          sm
          vl
          ctx
          state))
      ((when erp) (progn$ (cw? (normal-output-flag vl)
            "~|CEGen/Error/incremental: assign-value failed (in ~s0).~|"
            name)
          (cw? (verbose-stats-flag vl)
            "~|CEGen/Stats: Call was (assign-value ~x0 ~x1 ...)~|"
            x
            cs%)
          (mv erp nil state)))
      ((list a kind updated-h) ans)
      (i (if (eq kind :decision)
          (1+ i)
          i))
      (a% (change a%
          a%
          :cs cs%
          :val a
          :kind kind
          :i i))
      ((mv erp res state) (propagate x
          a
          updated-h
          c
          vl
          state))
      (str (if erp
          "inconsistent"
          "consistent"))
      (- (cw? (verbose-stats-flag vl)
          "~%CEgen/Stats/incremental: Propagate ~x0 := ~x1 (i:~x3) was ~s2.~|"
          x
          a
          str
          i)))
    (if erp
      (value (list 'nil
          ''t
          'nil
          'nil
          'nil
          'nil
          'nil
          (change a% a% :inconsistent? t)))
      (b* (((list vars~ h~ c~) res) (cl~ (clausify-hyps-concl h~ c~))
          (type-alist~ (get-acl2-type-alist cl~))
          (tau-interval-alist~ (tau-interval-alist-clause cl~ vars~))
          (- (cw? nil
              "~% new ta = ~x0 and old ta = ~x1~%"
              type-alist~
              type-alist))
          (- (cw? nil
              "~% new tau-int-alist = ~x0 and old tau-int-alist = ~x1~%"
              tau-interval-alist~
              tau-interval-alist))
          ((mv partial-a~ elim-bindings~) (if (eq kind :expand)
              (mv partial-a
                (put-val-a x a elim-bindings))
              (mv (put-val-a x a partial-a)
                elim-bindings))))
        (value (list h~
            c~
            vars~
            partial-a~
            elim-bindings~
            type-alist~
            tau-interval-alist~
            (change a% a% :inconsistent? nil)))))))

(defs (incremental-search (a% a.
      name
      mv-sig-alist
      test-outcomes%
      gcs%
      vl
      cgen-state
      programp
      ctx
      state)
    (decl :sig ((a% a%-listp
         string
         symbol-alist
         test-outcomes%-p
         gcs%-p
         fixnum
         cgen-state
         booleanp
         symbolp
         state) ->
        (mv erp
          (list boolean test-outcomes% gcs%)
          state))
      :mode :program :doc "DPLL like algorithm that searches for a non-vacuous assignment to
the form P (hyps / nconcl => nil).  This form returns (mv erp (list stop?
test-outcomes% gcs%) state).  The search consists of a Select, Assign, Propagate
loop.  Any inconsistency in P results in non-chronological backtracking to the
last decision made in Assign. For more details refer to the FMCAD paper.")
    (f* ((simple-search... nil
         (simple-search name
           h
           c
           vars
           partial-a
           elim-bindings
           type-alist
           tau-interval-alist
           mv-sig-alist
           test-outcomes%
           gcs%
           vl
           cgen-state
           programp
           t
           ctx
           state)) (backtrack... nil
          (backtrack a%
            a.
            name
            mv-sig-alist
            test-outcomes%
            gcs%
            vl
            cgen-state
            programp
            ctx
            state))
        (recurse... nil
          (incremental-search a%
            a.
            name
            mv-sig-alist
            test-outcomes%
            gcs%
            vl
            cgen-state
            programp
            ctx
            state)))
      (b* (((mv erp ap-res state) (trans-eval `(assign-propagate ',CGEN::A%
               ',CGEN::NAME
               ',(CGEN::CGET CGEN::SAMPLING-METHOD)
               ',(CGEN::CGET CGEN::TOP-VT-ALIST)
               ',CGEN::VL
               ',CGEN::CTX
               state)
             ctx
             state
             t)) ((when erp) (prog2$ (cw? (normal-output-flag vl)
                "~|CEGen/Error: Aborting incremental search!~|")
              (mv t
                (list nil test-outcomes% gcs%)
                state)))
          ((list h
             c
             vars
             partial-a
             elim-bindings
             type-alist
             tau-interval-alist
             a%) (cadr (cdr ap-res))))
        (if (not (access a% inconsistent?))
          (b* (((mv erp ss-result state) (simple-search...)) ((when erp) (mv t nil state))
              ((list stop? test-outcomes% gcs%) ss-result)
              ((when stop?) (mv erp
                  (list stop? test-outcomes% gcs%)
                  state))
              ((when (or (endp vars) (endp (cdr vars)))) (backtrack...))
              (a. (cons a% a.))
              (x1 (select (cons (cgen-dumb-negate-lit c) h)
                  vl
                  (w state)))
              (a% (make a%
                  :vars vars
                  :hyps h
                  :concl c
                  :partial-a partial-a
                  :elim-bindings elim-bindings
                  :type-alist type-alist
                  :tau-interval-alist tau-interval-alist
                  :inconsistent? nil
                  :cs nil
                  :var x1
                  :val ''?
                  :kind :na :i 0)))
            (recurse...))
          (backtrack...)))))
  (backtrack (a% a.
      name
      mv-sig-alist
      test-outcomes%
      gcs%
      vl
      cgen-state
      programp
      ctx
      state)
    (decl :sig ((a%-p a%-listp
         string
         variable-alist
         test-outcomes%-p
         gcs%-p
         fixnump
         cgen-state-p
         boolean
         symbol
         state) ->
        (mv erp
          (list boolean test-outcomes% gcs%)
          state))
      :mode :program :doc "backtrack in dpll like search")
    (if (or (not (eq (access a% kind) :decision))
        (> (access a% i)
          (cget backtrack-limit)))
      (if (null a.)
        (prog2$ (cw? (verbose-stats-flag vl)
            "~|CEGen/Note: Incremental search failed to even satisfy the hypotheses.~|")
          (value (list nil test-outcomes% gcs%)))
        (b* ((a% (car a.)) (x (access a% var))
            (- (cw? (verbose-stats-flag vl)
                "~|CEGen/Stats/incremental:  Backtrack to var : ~x0 -- i = ~x1~|"
                x
                (access a% i))))
          (backtrack a%
            (cdr a.)
            name
            mv-sig-alist
            test-outcomes%
            gcs%
            vl
            cgen-state
            programp
            ctx
            state)))
      (incremental-search a%
        a.
        name
        mv-sig-alist
        test-outcomes%
        gcs%
        vl
        cgen-state
        programp
        ctx
        state))))