		Search-engine friendly clone of the ACL2 documentation.

Prove-equal-with-axe

A tool for proving that DAGs / terms are equivalent.

Description:

The equivalence claim to be proved is universally quantified over all values of the variables in the two terms/DAGs.

If the call to prove-equal-with-axe completes without error, the DAG/terms are equal, given the :assumptions (including the :types).

Usually, the two items (DAGs or terms) have the same set of free variables.

See also prove-equal-with-axe+, for a variant that supports more exotic options.

General Form:

(prove-equal-with-axe dag-or-term1
                      dag-or-term2
                      &key
                      :assumptions                ; default nil
                      :types                      ; default nil
                      :interpreted-function-alist ; default nil
                      :test-types                 ; default nil
                      :tests                      ; default 50
                      :tactic                     ; default :rewrite-and-sweep
                      :print                      ; default :brief
                      :debug-nodes                ; default nil
                      :extra-rules                ; default nil
                      :remove-rules               ; default nil
                      :initial-rule-sets          ; default :auto
                      :monitor                    ; default nil
                      :use-context-when-miteringp ; default nil
                      :random-seed                ; default nil
                      :max-conflicts              ; default :auto
                      :normalize-xors             ; default t
                      :prove-constants            ; default t
                      :proof-name                 ; default :auto
                      :keep-temp-dir              ; default :auto
                      :check-vars                 ; default t
                      :prove-theorem              ; default nil
                      :local                      ; default t
                      )

Inputs:

dag-or-term1 — (required)

The first DAG or term to compare

dag-or-term2 — (required)

The second DAG or term to compare

:assumptions — default nil

Assumptions to use when proving equivalence, a list of terms (not necessarily translated). The proof is done assuming all of the :assumptions are non-nil.

:types — default nil

A var-type-alist (alist mapping variables to their axe-types), or one of the special values :bits or :bytes. The proof is done assuming the variables have their associated types. Entries in this alist can be overridden for testing purposes by the :test-types option.

:interpreted-function-alist — default nil

Provides definitions for non-built-in functions. An alist mapping function symbols to their bodies.

:test-types — default nil

Overrides of the :types for use in the testing that identifies probable facts for sweeping-and-merging (example, to restrict the length of arrays).

:tests — default 50

How many tests to use to find internal equivalences (a natp)

:tactic — default :rewrite-and-sweep

Proof tactic to use for the proof (either :rewrite or :rewrite-and-sweep)

:print — default :brief

Print verbosity (allows nil, :brief, t, and :verbose)

:debug-nodes — default nil

Nodenums whose values should be printed for each test-case, and whose subdags should be printing when attempting a merge. These nodenums refer to the DAG used for sweeping-and-merging (after pre-simplification, etc, if any), specifically the DAG for the first sweep.

:extra-rules — default nil

A symbol list containing the names of extra rules to use when simplifying

:remove-rules — default nil

A symbol list containing the names of rules to be removed from the set of rules used when simplifying

:initial-rule-sets — default :auto

Sequence of rule-sets to apply initially to simplify the miter (:auto means used phased-bv-axe-rule-sets)

:monitor — default nil

Rule names (symbols) to monitor when rewriting

:use-context-when-miteringp — default nil

Whether to use over-arching context when rewriting nodes (causes memoization to be turned off)

:random-seed — default nil

Seed for the random number generator used to make test cases, or nil meaning use the default.

:max-conflicts — default :auto

Initial value of STP max-conflicts (number of conflicts), or :auto (meaning use the default of 60000), or nil (meaning no maximum).

:normalize-xors — default t

Whether to normalize XOR nests when simplifying

:prove-constants — default t

Whether, when sweeping, to try to prove nodes are constants (and replace them with those constants if the proof succeeds).

:proof-name — default :auto

A name to assign to the proof, if desired. A symbol, or :auto to let Axe choose a name.

:keep-temp-dir — default :auto

Whether to keep the directory with temp files in place, for debugging. If :auto, the temp-dir is kept whenever there is an error.

:check-vars — default t

Whether to check that the two DAGs/terms have exactly the same vars. Can be t (throw an error if the var lists differ), nil (do not check the var lists), or :warn (print a warning if the var lists differ but then continue).

:prove-theorem — default nil

Whether to produce an ACL2 theorem stating the equivalence (using skip-proofs, currently)

:local — default t

whether to make the generated events local