		Search-engine friendly clone of the ACL2 documentation.

Aignet-abc-interface

Aignet-run-abc-core-st

Run abc on an aignet; takes and returns state.

Signature
(aignet-run-abc-core-st input-aignet output-aignet frames script &key script-filename input-filename output-filename ctrex-filename (force-status 'nil) (quiet 'nil) (state 'state)) → (mv status new-output-aignet new-frames new-state)
Arguments: input-aignet — input AIG.; output-aignet — output AIG.; frames — output ctrex.; script — Commands for ABC to run, including reading the input aiger file and writing the output, if desired.
Guard (stringp script).; script-filename — Guard (stringp script-filename).; input-filename — Guard (stringp input-filename).; output-filename — If set, implies that the script writes a new aignet to this file.
Guard (acl2::maybe-stringp output-filename).; ctrex-filename — If set, implies that the script may dump a counterexample in this file.
Guard (acl2::maybe-stringp ctrex-filename).; force-status — If set to true, causes an error if no proof status line is present in the output.; quiet — Don't print the output from ABC.
Returns: status — Either :refuted, :proved, :failed, NIL, or an error message. NIL implies that there was no error detected but also no proof status line, implying that maybe no proof was attempted.

See aignet-run-abc-core, which is identical except that it hides the usage of state.

Definitions and Theorems

Function: aignet-run-abc-core-st-fn

(defun aignet-run-abc-core-st-fn
       (input-aignet output-aignet
                     frames script script-filename
                     input-filename output-filename
                     ctrex-filename force-status quiet state)
 (declare (xargs :stobjs (input-aignet output-aignet frames state)))
 (declare (xargs :guard (and (stringp script)
                             (stringp script-filename)
                             (stringp input-filename)
                             (acl2::maybe-stringp output-filename)
                             (acl2::maybe-stringp ctrex-filename))))
 (let ((__function__ 'aignet-run-abc-core-st))
  (declare (ignorable __function__))
  (b*
   ((output-aignet (aignet-clear output-aignet))
    (input-filename (mbe :logic (acl2::str-fix input-filename)
                         :exec input-filename))
    (script-filename (mbe :logic (acl2::str-fix script-filename)
                          :exec script-filename))
    (state (aignet-write-aiger input-filename input-aignet state))
    ((mv channel state)
     (open-output-channel! script-filename
                           :character state))
    ((unless channel)
     (mv "Aignet-run-abc: Failed to write the ABC script."
         output-aignet frames state))
    (state (princ$ script channel state))
    (state (close-output-channel channel state))
    ((mv exit-status lines state)
     (acl2::tshell-call (str::cat (if quiet "abc -f " "abc -F ")
                                  script-filename)
                        :print (not quiet)
                        :save t))
    ((unless (equal exit-status 0))
     (mv (msg "Aignet-run-abc: abc failed with exit status ~x0"
              exit-status)
         output-aignet frames state))
    ((mv read-err output-aignet state)
     (if output-filename
      (aignet-read-aiger (mbe :logic (acl2::str-fix output-filename)
                              :exec output-filename)
                         output-aignet state)
      (mv nil output-aignet state)))
    ((when read-err)
     (mv (msg "Aignet-run-abc: failed to read result AIG: ~s0"
              read-err)
         output-aignet frames state))
    ((mv status frames state)
     (abc-output-status-and-trace
          lines ctrex-filename
          force-status (num-ins input-aignet)
          frames state)))
   (mv status output-aignet frames state))))

Theorem: frames-ncols-of-aignet-run-abc-core-st-when-refuted

(defthm frames-ncols-of-aignet-run-abc-core-st-when-refuted
 (b*
  (((mv ?status ?new-output-aignet
        ?new-frames ?new-state)
    (aignet-run-abc-core-st-fn input-aignet output-aignet frames
                               script script-filename input-filename
                               output-filename ctrex-filename
                               force-status quiet state)))
  (implies (and (equal status :refuted)
                ctrex-filename)
           (equal (stobjs::2darr->ncols new-frames)
                  (num-ins input-aignet)))))

Theorem: aignet-run-abc-core-st-preserves-state-p1

(defthm aignet-run-abc-core-st-preserves-state-p1
 (b*
  (((mv ?status ?new-output-aignet
        ?new-frames ?new-state)
    (aignet-run-abc-core-st-fn input-aignet output-aignet frames
                               script script-filename input-filename
                               output-filename ctrex-filename
                               force-status quiet state)))
  (implies (state-p1 state)
           (state-p1 new-state))))

Theorem: w-state-of-aignet-run-abc-core-st

(defthm w-state-of-aignet-run-abc-core-st
 (b*
  (((mv ?status ?new-output-aignet
        ?new-frames ?new-state)
    (aignet-run-abc-core-st-fn input-aignet output-aignet frames
                               script script-filename input-filename
                               output-filename ctrex-filename
                               force-status quiet state)))
  (equal (w new-state) (w state))))