• 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
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Equal-by-eval-bdds

Equal-by-eval-bdds-hint-heavy

Experimental "heavyweight" hint.

Sometimes it is difficult to make use of equalities between BDDs when carrying out the pick-a-point proof. QS-SUBSET-MODE is one way to approach this. And the HEAVY hint below is another. The idea is to replace other equalities between BDDs with what they mean in terms of the arbitrary-values which have just been picked.

BOZO this was a precursor to the defwitness stuff, right? Should we port this to use defwitness, etc.?

Definitions and Theorems

Function: lit-find-equality

(defun lit-find-equality (lit)
       (case-match lit
                   (('not ('ubddp . &) . &)
                    (mv nil nil nil))
                   (('ubddp . &) (mv nil nil nil))
                   (('not ('equal a b . &) . &)
                    (mv 'ineq a b))
                   (('not a . &) (mv 'eq a *nil*))
                   (('equal a b . &) (mv 'eq a b))
                   (& (mv 'ineq lit *nil*))))

Function: collect-ubddp-eq-and-ineqs

(defun
 collect-ubddp-eq-and-ineqs
 (clause whole hyps hist pspv ctx world state)
 (declare (xargs :stobjs state))
 (if
  (atom clause)
  (mv nil nil nil state)
  (mv-let
   (eqs ineqs remhyps state)
   (collect-ubddp-eq-and-ineqs (cdr clause)
                               whole hyps hist pspv ctx world state)
   (let
    ((conclusion (car clause)))
    (mv-let
     (sense lhs rhs)
     (lit-find-equality conclusion)
     (let
      ((lhs-okp (term-is-bdd lhs
                             hyps whole hist pspv world ctx state)))
      (if
       (not lhs-okp)
       (mv eqs ineqs
           (cons (dumb-negate-lit conclusion)
                 remhyps)
           state)
       (let
          ((rhs-okp
                (term-is-bdd rhs
                             hyps whole hist pspv world ctx state)))
          (if (not rhs-okp)
              (mv eqs ineqs
                  (cons (dumb-negate-lit conclusion)
                        remhyps)
                  state)
              (case sense
                    (eq (mv (cons (cons lhs rhs) eqs)
                            ineqs
                            (cons (dumb-negate-lit conclusion)
                                  remhyps)
                            state))
                    (ineq (mv eqs (cons (cons lhs rhs) ineqs)
                              remhyps state))
                    (t (mv eqs ineqs
                           (cons (dumb-negate-lit conclusion)
                                 remhyps)
                           state))))))))))))

Function: collect-eq-hyps

(defun
  collect-eq-hyps (eq-hyps acc)
  (if (atom eq-hyps)
      acc
      (collect-eq-hyps
           (cdr eq-hyps)
           (cons (cons 'equal
                       (cons (cons 'eval-bdd
                                   (cons (caar eq-hyps)
                                         '(arbitrary-values)))
                             (cons (cons 'eval-bdd
                                         (cons (cdar eq-hyps)
                                               '(arbitrary-values)))
                                   'nil)))
                 acc))))

Function: collect-hints

(defun
 collect-hints (eqs hyps)
 (if
  (atom eqs)
  nil
  (cons
   (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 (caar eqs) 'nil)))
                     'nil))
         (cons (cons 'bdd-rhs
                     (cons (cons 'lambda
                                 (cons 'nil (cons (cdar eqs) 'nil)))
                           'nil))
               'nil)))))
     'nil))
   (collect-hints (cdr eqs) hyps))))

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

(defun
 equal-by-eval-bdds-hint-heavy-fn
 (id clause hist pspv ctx stable world state)
 (declare (xargs :stobjs state)
          (ignorable id))
 (if
  (not stable)
  (value 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))
    (value nil)
    (let
     ((hyps (dumb-negate-lit-lst clause)))
     (mv-let (eqs ineqs new-hyps state)
             (collect-ubddp-eq-and-ineqs
                  clause
                  clause hyps hist pspv ctx world state)
             (if (not eqs)
                 (value nil)
                 (let* ((new-hyps (collect-eq-hyps ineqs new-hyps))
                        (hints (collect-hints eqs new-hyps)))
                       (prog2$ nil (value (list :or hints)))))))))))

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

(defun
 equal-by-eval-bdds-inst-fn
 (lhs rhs concl add-hyps instantiate-hyps
      clause hist pspv ctx world state)
 (declare (xargs :stobjs state))
 (let
  ((clhyps (dumb-negate-lit-lst clause)))
  (mv-let
   (cleqs clineqs cl-new-hyps state)
   (collect-ubddp-eq-and-ineqs
        clause
        clause clhyps hist pspv ctx world state)
   (mv-let
    (lhs rhs state)
    (cond
     ((and lhs rhs)
      (mv (car lhs) (car rhs) state))
     (concl
          (er-let* ((concl (translate (car concl)
                                      t t t 'equal-by-eval-bdds-inst
                                      world state)))
                   (mv-let (sense lhs rhs)
                           (lit-find-equality (car concl))
                           (declare (ignore sense))
                           (mv lhs rhs state))))
     (t (mv (caar (last cleqs))
            (cdar (last cleqs))
            state)))
    (let*
     ((hyps (if (and instantiate-hyps (car instantiate-hyps))
                (collect-eq-hyps clineqs cl-new-hyps)
                clhyps))
      (hyps (if add-hyps (append (car add-hyps) hyps)
                hyps)))
     (let
      ((res
        (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 "res: ~x0~%" res)
              (value res))))))))