• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
      • Equal-by-eval-bdds
        • Equal-by-eval-bdds-hint-heavy
        • Term-is-bdd
        • Equal-by-eval-bdds-hint
        • Max-depth
      • Ubdd-constructors
      • Eval-bdd
      • Ubddp
      • Ubdd-fix
      • Q-sat
      • Bdd-sat-dfs
      • Eval-bdd-list
      • Qcdr
      • Qcar
      • Q-sat-any
      • Canonicalize-to-q-ite
      • Ubdd-listp
      • Qcons
    • Bdd
    • Faig
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Equal-by-eval-bdds

Equal-by-eval-bdds-hint

Basic automation of equal-by-eval-bdds.

This is a computed hint in the spirits of the ordered sets library's pick-a-point automation. It reduces questions of BDD equality to questions of BDD evaluation.

Definitions and Theorems

Function: equal-by-eval-bdds-hint-fn

(defun
 equal-by-eval-bdds-hint-fn
 (id clause hist pspv ctx stable world state)
 (declare (xargs :stobjs state)
          (ignorable id))
 (if
  (not stable)
  nil
  (let*
   ((rcnst (access prove-spec-var pspv :rewrite-constant))
    (ens (access rewrite-constant
                 rcnst :current-enabled-structure)))
   (if
    (not (enabled-numep (fnume '(:rewrite equal-by-eval-bdds)
                               world)
                        ens))
    nil
    (let
     ((conclusion (car (last clause))))
     (if
      (not (and (consp conclusion)
                (or (eq (car conclusion) 'equal)
                    (eq (car conclusion) 'not))))
      nil
      (let
       ((lhs (second conclusion))
        (rhs (or (third conclusion) *nil*))
        (hyps (dumb-negate-lit-lst (butlast clause 1))))
       (let
        ((lhs-okp
              (term-is-bdd lhs
                           hyps clause hist pspv world ctx state)))
        (if
         (not lhs-okp)
         nil
         (let
          ((rhs-okp
               (term-is-bdd rhs
                            hyps clause hist pspv world ctx state)))
          (if
           (not rhs-okp)
           nil
           (let
            ((hint
              (cons
               ':use
               (cons
                (cons
                 ':functional-instance
                 (cons
                  'equal-by-eval-bdds
                  (cons
                   (cons
                    'bdd-hyps
                    (cons (cons 'lambda
                                (cons 'nil
                                      (cons (cons 'and hyps) 'nil)))
                          'nil))
                   (cons
                    (cons 'bdd-lhs
                          (cons (cons 'lambda
                                      (cons 'nil (cons lhs 'nil)))
                                'nil))
                    (cons
                      (cons 'bdd-rhs
                            (cons (cons 'lambda
                                        (cons 'nil (cons rhs 'nil)))
                                  'nil))
                      'nil)))))
                'nil))))
            (prog2$
             (cw
              "~|~%We now appeal to ~s3 in an ~
                                attempt to show that ~x0 and ~x1 ~
                                are equal because all of their ~
                                evaluations under ~s2 are the ~
                                same.  (You can disable ~s3 to ~
                                avoid this.  See :doc ~s3 for more ~
                                details.)~|~%"
              (untranslate lhs nil world)
              (untranslate rhs nil world)
              'eval-bdd
              'equal-by-eval-bdds)
             hint)))))))))))))