|
|
|---|
|
|
|
|---|
Prove that two items (DAGs or terms) over the same variables are equivalent for every value of the variables.
(prove-equivalence dag1 ;; The first DAG or term to compare dag2 ;; The second DAG or term to compare [:assumptions] ;; Assumptions to use when proving equivalence [:types] ;; An alist from variables to their types, or one of the special values :bits or :bytes. Used to generate test cases. [:tactic] ;; Should be :rewrite or :rewrite-and-sweep [:tests natp] ;; How many tests to use to find internal equivalences, Default: 100 [:print] ;; Print verbosity (allows nil, :brief, t, and :verbose), Default: :brief [:name] ;; A name to assign to the equivalence term, if desired [:debug] ;; Leave temp files around for debugging, Default: nil [:max-conflicts] ;; Initial value of STP max-conflicts (number of conflicts), or :auto (meaning use the default of 60000), or nil (meaning no maximum). [:extra-rules] ;; The names of extra rules to use when simplifying, Default: nil [:initial-rule-sets] ;; Sequence of rule-sets to apply initially to simplify the miter (:auto means used phased-bv-axe-rule-sets), Default: :auto [:monitor] ;; Rule names (symbols) to monitor when rewriting [:use-context-when-miteringp] ;; Whether to use over-arching context when rewriting nodes (causes memoization to be turned off) [:normalize-xors] ;; Whether to normalize XOR nests when simplifying [:interpreted-function-alist] ;; Provides definitions for non-built-in functions [:check-vars] ;; whether to check that the two DAGs/terms have exactly the same vars [:prove-theorem] ;; whether to produce an ACL2 theorem stating the equivalence (using skip-proofs, currently) [:local] ;; whether to make the generated events local )
If the call to