• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-with-tracking
      • Aignet-complete-copy
      • Aignet-eval
      • Semantics
      • Aignet-transforms
      • Aignet-simplify-marked
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
        • Aignet-run-abc-core
        • Aignet-run-abc-core-st
        • Aignet-abc
        • Abc-example-scripts
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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)
     (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))))