fixers-gl-backend

(defun gl-my-satlink-config
  nil
  (declare (xargs :guard t))
  *my-config*)

(defun collect-vars
  (term)
  (reverse (all-vars term)))

(defun has-output
  (f x)
  (member x (g1 :out f)))

(defun has-input
  (f x)
  (member x (g1 :in f)))

(defun i/o-compat
  (f1 f2)
  "f1 and f2 are I/O compatible"
  (or (intersection-eq (g1 :out f1)
      (g1 :in f2))
    (intersection-eq (g1 :out f2)
      (g1 :in f1))))

(defun can-flow
  (x f1 f2)
  "value of x can possibly flow from f1 to f2"
  (member-eq x
    (intersection-eq (g1 :out f1)
      (g1 :in f2))))

(defun sfixes-lit
  (fixer l)
  (and (member-equal l (g1 :fixes fixer))
    t))

(defun subst-args
  (new-arg old-arg args)
  (if (endp args)
    'nil
    (if (equal old-arg (car args))
      (if (and (true-listp new-arg) (consp new-arg))
        (append (cdr new-arg) (cdr args))
        (cons new-arg (cdr args)))
      (cons (car args)
        (subst-args new-arg
          old-arg
          (cdr args))))))

(defun to-string
  (x)
  (declare (xargs :mode :program))
  (coerce (cdr (coerce (fms-to-string "~x0" (list (cons #\0 x)))
        'list))
    'string))

(defun all-vars/fixer
  (f)
  (union-eq (g1 :in f)
    (g1 :out f)))

(defun all-vars/lit
  (l)
  "assume literal l is a term; return all variables in l"
  (collect-vars l))

(defun lit-name
  (lit)
  (fix-intern-in-pkg-of-sym (to-string lit)
    'x))

(defun chosen-fixer-var
  (f lit)
  (s+ (g1 :name f)
    "**"
    (lit-name lit)))

(defun final-value-var
  (f1x)
  (b* (((list f1 x) f1x))
    (s+ (g1 :name f1) "!" x)))

(defun final-value-var-table
  (vars fixers)
  "map final-value-var to its (list fixer variable) pair"
  (pairlis$ (pvars/final vars fixers)
    (final-fixer-variable-pairs vars fixers)))

(defun all-connections
  (fixers vars)
  (all-connections1 (all-pairs fixers :distinct-p t)
    vars))

(defun connection-var
  (f1xf2)
  (b* (((list f1 x f2) f1xf2))
    (s+ (g1 :name f1)
      "-"
      x
      "->"
      (g1 :name f2))))

(defun pvars/conn
  (fixers vars)
  (connection-vars (all-connections fixers vars)))

(defun connection-var-table
  (vars fixers)
  "map connection-var to the connection"
  (b* ((conns (all-connections fixers vars)))
    (connection-var-table1 conns)))

(defun valid-var
  (f1)
  (s+ (g1 :name f1) ".VALID"))

(defun valid-var-table
  (fixers)
  "map valid-var to its fixer name"
  (pairlis$ (pvars/valid fixers)
    (g1-lst :name fixers)))

(defun trans-conn-with-flow-var
  (f1xf2)
  (b* (((list f1 x f2) f1xf2))
    (s+ (g1 :name f1)
      "---"
      x
      "--->"
      (g1 :name f2))))

(defun pvars/trans-flow
  (fixers vars)
  (trans-conn-with-flow-vars (all-connections1 (all-pairs fixers :distinct-p nil)
      vars)))

(defun trans-conn-var
  (f1f2)
  (b* (((list f1 f2) f1f2))
    (s+ (g1 :name f1)
      "--->"
      (g1 :name f2))))

(defun all-possible-trans-pairs
  (fixers)
  (all-possible-trans-pairs1 (all-pairs fixers)))

(defun pvars/trans
  (fixers)
  (trans-conn-vars (all-possible-trans-pairs fixers)))

(defun pvar/sat-term
  (term)
  (s+ (lit-name term) ".is_SAT"))

(defun pvar/sat-lit
  (lit)
  (s+ (lit-name lit) ".is_SAT"))

(defun pvars-fn
  (vars fixers lits terms)
  (append (pvars/chosen-fixer lits fixers)
    (pvars/final vars fixers)
    (pvars/conn fixers vars)
    (pvars/valid fixers)
    (pvars/trans-flow fixers vars)
    (pvars/trans fixers)
    (union-equal (pvars/sat-term terms)
      (pvars/sat-lit lits))))

(defun pvars-type-constraints
  (vars fixers lits terms)
  (b* ((pvars (pvars-fn vars
         fixers
         lits
         terms)) (n (len pvars))
      (booleanps (make-list n :initial-element 'booleanp)))
    (list-up-lists booleanps pvars)))

(defun c/f-is-thefixer-for-lit
  (f lit)
  `(implies ,(CGEN::CHOSEN-FIXER-VAR CGEN::F CGEN::LIT)
    ,(CGEN::VALID-VAR CGEN::F)))

(defun c/thechosenfixer
  (lits fixers)
  (append (c/thechosenfixer-def lits fixers)
    (c/thecf-uniquely-valid1 lits
      fixers
      fixers)))

(defun c/connection-implies-valid
  (fixers vars)
  (c/connection-implies-valid1 (all-connections fixers vars)))

(defun c/atmost-one-input-conn
  (fixers vars)
  (c/atmost-one-input-conn1 fixers
    (all-pairs fixers :distinct-p t)
    vars))

(defun c/atleast-one-input-conn
  (fixers vars)
  (c/atleast-one-input-conn1 fixers
    fixers
    vars))

(defun drop-flow-var
  (f1xf2)
  (b* (((list f1 & f2) f1xf2))
    (list f1 f2)))

(defun c/trans1/basis
  (fixers vars)
  (c/trans1/basis1 (all-connections fixers vars)))

(defun c/trans-with-flow1/rec
  (fixers vars)
  (b* ((xf1f2f3-list (triples-with-flow fixers
         (all-connections fixers vars))))
    (c/trans-with-flow1/rec1 xf1f2f3-list)))

(defun c/trans1/rec
  (fixers)
  (b* ((f1f2f3-list (triples-without-flow fixers
         (all-possible-trans-pairs fixers))))
    (c/trans1/rec1 f1f2f3-list)))

(defun c/trans1
  (fixers vars)
  (append (c/trans1/basis fixers vars)
    (c/trans-with-flow1/rec fixers vars)
    (c/trans1/rec fixers)))

(defun fixers-between-with-flow
  (fixers f1 f3 x)
  (if (endp fixers)
    'nil
    (b* ((f2 (car fixers)) ((when (or (equal f2 f1) (equal f2 f3))) (fixers-between-with-flow (cdr fixers)
            f1
            f3
            x))
        ((unless (and (can-flow x f1 f2)
             (can-flow x f2 f3))) (fixers-between-with-flow (cdr fixers)
            f1
            f3
            x)))
      (cons f2
        (fixers-between-with-flow (cdr fixers)
          f1
          f3
          x)))))

(defun c/trans-with-flow-only-if-direction
  (fixers vars)
  (c/trans-with-flow-only-if1 (all-connections fixers vars)
    fixers))

(defun c/trans
  (fixers vars)
  (append (c/trans1 fixers vars)
    (c/trans-with-flow-only-if-direction fixers
      vars)))

(defun spreserves-lit
  (fixer l)
  (or (and (member-equal l
        (g1 :preserves fixer))
      t)
    (and (member-equal l (g1 :fixes fixer))
      t)
    (null (intersection-eq (g1 :out fixer)
        (all-vars/lit l)))
    (and (consp l) (= (len l) 2))))

(defun bool->0/1
  (b)
  (declare (xargs :mode :logic))
  (if b
    1
    0))

(defun num-sat-literals
  (terms)
  `(+ . ,(CGEN::NUM-SAT-LITERALS1 CGEN::TERMS)))

(defun indices-of-len1
  (n acc)
  (if (zp n)
    acc
    (b* ((n (1- n)))
      (indices-of-len1 n (cons n acc)))))

(defun indices-of-len
  (n)
  (indices-of-len1 n 'nil))

(defun pvars-g-bindings
  (vars fixers lits terms)
  (b* ((pvars (pvars-fn vars
         fixers
         lits
         terms)) (n (len pvars))
      (g-booleans (make-list n :initial-element :g-boolean))
      (indices (indices-of-len n))
      (g-boolean-forms (pairlis$ g-booleans indices)))
    (list-up-lists pvars g-boolean-forms)))

(defun make-bedges-adjlist1
  (connvar-edges conn-var-table ans)
  "given edges in form of symbols F1xF2, return an adjacency list with
   backward edges of the form (fixer-name . flow-var).
   Initially ans has all fixers mapped to their in-list"
  (if (endp connvar-edges)
    ans
    (b* ((connvar (car connvar-edges)) ((list from var to) (g1 connvar conn-var-table))
        (in-list (g1 to ans))
        (in-list1 (substitute (cons from var)
            var
            in-list))
        (ans1 (put-assoc-equal to in-list1 ans)))
      (make-bedges-adjlist1 (cdr connvar-edges)
        conn-var-table
        ans1))))

(defun make-bedges-adjlist
  (connvar-edges conn-var-table
    fixer-inst-table)
  (make-bedges-adjlist1 connvar-edges
    conn-var-table
    (fixer-in-list-map fixer-inst-table)))

(defun dag-term-at
  (fx b-adjlist |FXRI{}| flag)
  "given a acyclic adjlist (with backward edges), and (f . x),
   find the term/expression at that node.
   Note:Each node is a function symbol and the backward-edges are in order of
   the inputs to that node."
  (declare (xargs :mode :logic :measure (llist (len b-adjlist)
        (acl2-count fx))
      :well-founded-relation l<))
  (if (eq flag :node)
    (b* (((cons f x) fx) ((unless (assoc-equal f b-adjlist)) (er hard?
            'dag-term-at
            "~| ~x0 not found in adjlist!~%"
            f))
        (adj-in-nodes (g1 f b-adjlist))
        (b-adjlist1 (remove1-assoc-equal f b-adjlist))
        (in-terms (dag-term-at adj-in-nodes
            b-adjlist1
            |FXRI{}|
            :nodes))
        (fxri-data (g1 f |FXRI{}|))
        (out-list (g1 :out fxri-data))
        (x-pos (position x out-list))
        (in (g1 :in fxri-data))
        (fxr-b (g1 :fixer-let-binding fxri-data))
        (fxr-term (cadr (assoc-eq x fxr-b)))
        (actual-term (if fxr-b
            (sublis-var (pairlis$ in in-terms)
              fxr-term)
            (cons f in-terms)))
        (dag-term (if (null in-terms)
            (list :enum f :out x)
            actual-term)))
      (if (and (null fxr-b)
          (consp out-list)
          (consp (cdr out-list)))
        (list 'mv-nth
          (kwote x-pos)
          (list 'mv-list
            (kwote (len out-list))
            dag-term))
        dag-term))
    (let ((fxs fx))
      (if (endp fxs)
        'nil
        (cons (dag-term-at (car fxs)
            b-adjlist
            |FXRI{}|
            :node)
          (dag-term-at (cdr fxs)
            b-adjlist
            |FXRI{}|
            :nodes))))))

(defun strip-mv-nth
  (term)
  (case-match term
    (('mv-nth & ('mv-list & exp)) exp)
    (('mv-nth & exp) exp)
    (& term)))

(defun let-binding->dep-graph-alst
  (vt-lst ans)
  "Walk down the var-term list vt-lst and add edges.
   Build graph alist in ans"
  (if (endp vt-lst)
    ans
    (b* (((list var term) (car vt-lst)) (fvars (all-vars term)))
      (let-binding->dep-graph-alst (cdr vt-lst)
        (union-entry-in-adj-list var
          fvars
          ans)))))

(defun get-ordered-alst
  (keys alst ans)
  (declare (xargs :guard (and (true-listp keys)
        (alistp ans)
        (alistp alst))))
  "accumulate entries of alist in ans in the order of keys"
  (if (endp keys)
    ans
    (let ((at (assoc-equal (car keys) alst)))
      (if at
        (get-ordered-alst (cdr keys)
          alst
          (append ans (list at)))
        (get-ordered-alst (cdr keys)
          alst
          ans)))))

(defun do-let*-ordering1
  (vars vt-lst debug-flag)
  (declare (xargs :guard (symbol-alistp vt-lst)
      :mode :program))
  (b* ((dep-g (let-binding->dep-graph-alst vt-lst
         (make-empty-adj-list vars))) (sorted-vars (approximate-topological-sort dep-g
          debug-flag)))
    (get-ordered-alst (reverse sorted-vars)
      vt-lst
      nil)))

(defun dlist-to-alist
  (dlist)
  (pairlis$ (strip-cars dlist)
    (strip-cadrs dlist)))

(defun convert-to-let*-binding
  (a)
  (declare (xargs :guard (symbol-alistp a)
      :mode :program))
  (b* ((exp->var-map (invert-alist a)) (svals (subst-common-subterms-with-corr-vars exp->var-map
          (strip-cdrs a)))
      (svals (replace-enum-exp-with-out-var/terms svals))
      (vars (strip-cars a))
      (let*-b (listlis vars svals))
      (let*-b (remove-x=x-bindings let*-b))
      (let*-b (do-let*-ordering1 vars let*-b nil)))
    let*-b))

(defun soln-sigma-top
  (sat-assignment vars |FXRI{}|)
  (b* ((fixers (strip-cdrs |FXRI{}|)) (pvars/valid (filter-true-vars sat-assignment
          (pvars/valid fixers)))
      (valid-var-table (valid-var-table fixers))
      (valid-var-table/true (assoc-lst pvars/valid valid-var-table))
      (fixer-names/valid (strip-cdrs valid-var-table/true))
      (|FXRI{}/VALID| (assoc-lst fixer-names/valid |FXRI{}|))
      (conn-var-table (connection-var-table vars fixers))
      (final-value-var-table (final-value-var-table vars fixers))
      (fixers/valid (strip-cdrs |FXRI{}/VALID|))
      (connvar-edges (filter-true-vars sat-assignment
          (pvars/conn fixers/valid vars)))
      (bedges-adjlist (make-bedges-adjlist connvar-edges
          conn-var-table
          |FXRI{}/VALID|))
      (final-value-vars (filter-true-vars sat-assignment
          (pvars/final vars fixers/valid)))
      (- (assert$ (= (len vars)
            (len final-value-vars))
          "Invariant broken: Some var does not have a final-value expression!"))
      (a (soln-sigma vars
          final-value-vars
          final-value-var-table
          |FXRI{}/VALID|
          bedges-adjlist)))
    a))

(defun make-gl-sat-encoding
  (vars lits |TERM->FLITS{}| |FXRI{}|)
  (b* ((fixers (strip-cdrs |FXRI{}|)) (terms (strip-cars |TERM->FLITS{}|))
      (bindings (pvars-g-bindings vars
          fixers
          lits
          terms))
      (hyp `(and . ,(CGEN::PVARS-TYPE-CONSTRAINTS CGEN::VARS CGEN::FIXERS CGEN::LITS CGEN::TERMS)))
      (concl-hypothesis `(and . ,(APPEND (CGEN::C/ATLEAST-ONE-FINAL-VALUE CGEN::VARS CGEN::FIXERS)
         (CGEN::C/FINAL-VALUE-IMPLIES-VALID CGEN::VARS CGEN::FIXERS)
         (CGEN::C/CONNECTION-IMPLIES-VALID CGEN::FIXERS CGEN::VARS)
         (CGEN::C/ATMOST-ONE-INPUT-CONN CGEN::FIXERS CGEN::VARS)
         (CGEN::C/ATLEAST-ONE-INPUT-CONN CGEN::FIXERS CGEN::VARS)
         (CGEN::C/TRANS CGEN::FIXERS CGEN::VARS)
         (CGEN::C/NO-CYCLES CGEN::FIXERS)
         (CGEN::C/FINAL-VALUE-DEF CGEN::VARS CGEN::FIXERS)
         (CGEN::C/THEFIXER-IS-PRESERVED CGEN::LITS CGEN::FIXERS)
         (CGEN::C/THECHOSENFIXER CGEN::LITS CGEN::FIXERS)
         (CGEN::C/VALID-FIXES-AT-LEAST-ONE-LIT CGEN::FIXERS CGEN::LITS)
         (CGEN::C/SAT-LITS CGEN::LITS CGEN::FIXERS)
         (CGEN::C/SAT-TERMS CGEN::TERM->FLITS{})))))
    (mv bindings hyp concl-hypothesis)))

(defun fixers-sat-glcp-query
  (num-sat-lits top-hyps
    bindings
    trhyp
    concl-hyp
    vl
    state)
  (declare (xargs :mode :program :stobjs (state)))
  (b* (((mv start-sat-query state) (read-run-time state)) (concl `(implies ,CGEN::CONCL-HYP
          (not (equal ,(CGEN::NUM-SAT-LITERALS CGEN::TOP-HYPS)
              ,CGEN::NUM-SAT-LITS))))
      (ctx 'fixers-sat-glcp-query)
      ((er trconcl) (translate concl
          t
          t
          nil
          ctx
          (w state)
          state))
      (concl-vars (collect-vars trconcl))
      (missing-vars (set-difference-eq concl-vars
          (strip-cars bindings)))
      (- (and missing-vars
          (let ((msg (msg "~
The following variables are present in the theorem but have no symbolic object ~
bindings:
~x0~%"
                 missing-vars)))
            (cw? (normal-output-flag vl)
              "****  ERROR ****~%~@0~%"
              msg))))
      ((when missing-vars) (mv :missing-vars nil state))
      (param-bindings nil)
      (trparam nil)
      (config (make-glcp-config :abort-ctrex t
          :abort-vacuous t
          :n-counterexamples 1))
      ((local-stobjs interp-st) (mv err ans interp-st state))
      ((mv erp ?val interp-st state) (glcp nil
          (list bindings
            param-bindings
            trhyp
            trparam
            trconcl
            concl
            config)
          interp-st
          state))
      ((mv end-sat-query state) (read-run-time state))
      (- (cw? (verbose-stats-flag vl)
          "~|Cgen/Note: GL/SAT Engine: Time taken = "))
      ((mv err & state) (if (verbose-stats-flag vl)
          (pprogn (print-rational-as-decimal (- end-sat-query start-sat-query)
              (standard-co state)
              state)
            (princ$ " seconds"
              (standard-co state)
              state)
            (newline (standard-co state) state)
            (newline (standard-co state) state)
            (value :invisible))
          (value nil)))
      ((when err) (mv err nil interp-st state))
      ((unless erp) (mv :unsat nil interp-st state))
      (x (car (@ glcp-counterex-assignments)))
      (sat-a (glcp-obj-ctrex->obj-alist x)))
    (mv nil sat-a interp-st state)))

(defun fixers-maxsat-glcp-query-loop
  (n top-hyps
    bindings
    trhyp
    concl-hyp
    mode
    vl
    state)
  (declare (xargs :mode :program :stobjs (state)))
  (if (zp n)
    (mv :unsat nil 0 state)
    (b* (((mv erp a state) (fixers-sat-glcp-query n
           top-hyps
           bindings
           trhyp
           concl-hyp
           vl
           state)) ((unless erp) (prog2$ (cw? (verbose-stats-flag vl)
              "~|Got a sat assignment for #literals = ~x0~%"
              n)
            (mv nil a n state)))
        ((when (eq mode :sat)) (mv erp a n state)))
      (fixers-maxsat-glcp-query-loop (1- n)
        top-hyps
        bindings
        trhyp
        concl-hyp
        mode
        vl
        state))))

(defun fixers-maxsat-glcp-query
  (vars lits
    |TERM->FLITS{}|
    relevant-hyps
    |FXRI{}|
    mode
    vl
    state)
  (declare (xargs :mode :program :stobjs (state)))
  (b* (((when (or (null vars)
          (null lits)
          (null |TERM->FLITS{}|)
          (null relevant-hyps))) (mv :null nil state)) (ctx 'fixers-maxsat-glcp-query)
      ((mv start-code-gen state) (read-run-time state))
      ((mv bindings hyp concl-hyp) (make-gl-sat-encoding vars
          lits
          |TERM->FLITS{}|
          |FXRI{}|))
      ((mv end-code-gen state) (read-run-time state))
      (- (cw? (debug-flag vl)
          "~|concl-hyp is ~x0~%"
          concl-hyp))
      (- (cw? (verbose-stats-flag vl)
          "~|Cgen/Note: fixer-sat-encoding: Time taken = "))
      ((er &) (if (verbose-stats-flag vl)
          (pprogn (print-rational-as-decimal (- end-code-gen start-code-gen)
              (standard-co state)
              state)
            (princ$ " seconds"
              (standard-co state)
              state)
            (newline (standard-co state) state)
            (newline (standard-co state) state)
            (value :invisible))
          (value nil)))
      ((er trhyp) (translate hyp
          t
          t
          nil
          ctx
          (w state)
          state))
      ((mv erp sat-a ?n state) (fixers-maxsat-glcp-query-loop (len relevant-hyps)
          relevant-hyps
          bindings
          trhyp
          concl-hyp
          mode
          vl
          state))
      ((when erp) (mv erp nil state))
      (terms (strip-cars |TERM->FLITS{}|))
      (fixers (strip-cdrs |FXRI{}|))
      (all-basis-pvars (append (pvars/chosen-fixer lits fixers)
          (pvars/final vars fixers)
          (pvars/conn fixers vars)
          (pvars/valid fixers)
          (union-equal (pvars/sat-term terms)
            (pvars/sat-lit lits))))
      (pvars/true (filter-true-vars sat-a all-basis-pvars))
      (sat-a/true (listlis pvars/true
          (make-list (len pvars/true) :initial-element 't)))
      (- (cw? (debug-flag vl)
          "True pvars: ~x0~%"
          (filter-true-vars sat-a
            (pvars-fn vars
              fixers
              lits
              terms))))
      (- (cw? (verbose-stats-flag vl)
          "SAT Assignment: ~x0~%"
          sat-a/true)))
    (mv nil sat-a/true state)))

(defun fxri-let*-soln/gl
  (flits |TERM->FLITS{}|
    relevant-terms
    |FXRI{}|
    vl
    state)
  (declare (xargs :stobjs (state)))
  (b* ((flits-vars (all-vars1-lst flits 'nil)) (- (tshell-ensure))
      ((mv erp sat-a state) (fixers-maxsat-glcp-query flits-vars
          flits
          |TERM->FLITS{}|
          relevant-terms
          |FXRI{}|
          :maxsat vl
          state))
      ((when (equal :null erp)) (value (list nil nil)))
      ((when (equal :unsat erp)) (progn$ (cw? (verbose-flag vl)
            "~| Cgen/Note: GL query is UNSAT. No fixer arrangement found for~%")
          (cw? (verbose-flag vl)
            "~| ~x0~%"
            relevant-terms)
          (value (list nil nil))))
      (rterms-pvars/sat (pvars/sat-term relevant-terms))
      (rterms-pvars/true (filter-true-vars sat-a rterms-pvars/sat))
      (rterms/true (strip-cdrs (assoc-lst rterms-pvars/true
            (pairlis$ rterms-pvars/sat relevant-terms))))
      (ssigma (soln-sigma-top sat-a
          flits-vars
          |FXRI{}|))
      (let*-soln0 (convert-to-let*-binding ssigma)))
    (mv erp
      (list let*-soln0 rterms/true)
      state)))