• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
        • Litp
        • Varp
        • Env$
        • Eval-formula
        • Max-index-formula
        • Max-index-clause
        • Formula-indices
        • Clause-indices
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Cnf

Formula-indices

Collect indices of all identifiers used throughout a formula.

Signature

(formula-indices formula) → *

Arguments

formula — Guard (lit-list-listp formula).

Definitions and Theorems

Function: formula-indices

(defun formula-indices (formula)
       (declare (xargs :guard (lit-list-listp formula)))
       (let ((__function__ 'formula-indices))
            (declare (ignorable __function__))
            (if (atom formula)
                nil
                (append (clause-indices (car formula))
                        (formula-indices (cdr formula))))))

Theorem: formula-indices-when-atom

(defthm formula-indices-when-atom
        (implies (atom formula)
                 (equal (formula-indices formula) nil)))

Theorem: formula-indices-of-cons

(defthm formula-indices-of-cons
        (equal (formula-indices (cons clause formula))
               (append (clause-indices clause)
                       (formula-indices formula))))

Theorem: formula-indices-of-lit-list-list-fix-formula

(defthm formula-indices-of-lit-list-list-fix-formula
        (equal (formula-indices (lit-list-list-fix formula))
               (formula-indices formula)))

Theorem: formula-indices-lit-list-list-equiv-congruence-on-formula

(defthm formula-indices-lit-list-list-equiv-congruence-on-formula
        (implies (lit-list-list-equiv formula formula-equiv)
                 (equal (formula-indices formula)
                        (formula-indices formula-equiv)))
        :rule-classes :congruence)