• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
          • 4v-shannon-expansion
          • Onehot-rewriting
          • 4v-sexpr-restrict-with-rw
          • 4v-sexpr-compose-with-rw
          • Sexpr-rewrite
          • Sexpr-rewrite-default
          • Sexpr-rewriting-internals
            • Sexpr-unify
            • Sexpr-rewrite
            • Sexpr-rewrite-try-rules
            • Sexpr-rewrite-ground
            • 4v-sexpr-compose-nofal
            • Sexpr-rewrite-sigma
            • Sexpr-rewrite-fncall
          • *sexpr-rewrites*
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Sexpr-rewriting-internals

Sexpr-rewrite-try-rules

Given the args of a term and a list of possible rewrites for terms with the same top function symbol, tries each of the rewrites until one matches.

Signature

(sexpr-rewrite-try-rules args rewrites) 
  → 
(mv successp rhs sigma)

Returns (mv successp rhs sigma), where successp indicates that there was a rule that matched, rhs is the right-hand side of that rule, and sigma is the substitution alist, such that the composition of rhs and sigma is equivalent to some (implicit) function applied to the args.

Regarding the function symbol: Rewrite rules are stored by leading LHS function symbol, and omit this function symbol from the LHS. So the LHS is just represented as a list of arguments. A rewrite rule is correct if that (implicit) function symbol applied to the LHS args is sexpr-equivalent to the corresponding RHS.

Definitions and Theorems

Function: sexpr-rewrite-try-rules

(defun sexpr-rewrite-try-rules (args rewrites)
  (declare (xargs :guard t))
  (let ((__function__ 'sexpr-rewrite-try-rules))
    (declare (ignorable __function__))
    (b* (((when (atom rewrites))
          (mv nil nil nil))
         ((when (atom (car rewrites)))
          (sexpr-rewrite-try-rules args (cdr rewrites)))
         ((mv ok subst)
          (sexpr-unify-list (caar rewrites)
                            args nil))
         ((when ok)
          (mv t (cdar rewrites) subst)))
      (sexpr-rewrite-try-rules args (cdr rewrites)))))

Function: 4v-sexpr-fn-rewritesp

(defun 4v-sexpr-fn-rewritesp (fn rewrites)
  (if (atom rewrites)
      t
    (and (consp (car rewrites))
         (4v-sexpr-equiv (cons fn (caar rewrites))
                         (cdar rewrites))
         (4v-sexpr-fn-rewritesp fn (cdr rewrites)))))

Theorem: sexpr-rewrite-try-rules-correct

(defthm sexpr-rewrite-try-rules-correct
  (mv-let (successp rhs subst)
          (sexpr-rewrite-try-rules args rewrites)
    (implies (and successp
                  (4v-sexpr-fn-rewritesp fn rewrites))
             (4v-sexpr-equiv (4v-sexpr-compose rhs subst)
                             (cons fn args)))))

Theorem: sexpr-rewrite-try-rules-vars

(defthm sexpr-rewrite-try-rules-vars
 (b* (((mv ?successp ?rhs subst)
       (sexpr-rewrite-try-rules args rewrites)))
  (implies (not (member v (4v-sexpr-vars-list args)))
           (not (member v
                        (4v-sexpr-vars-list (alist-vals subst)))))))