• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
          • Uninterpreted-fn-cp
          • Smt-hint-interface
          • Function-expansion
          • Smt-config
          • Fty-support
          • Smt-computed-hints
          • Add-hypo-cp
          • Smt-hint-please
          • Type-extract-cp
          • Smt-extract
          • Smtlink-process-user-hint
            • Process-smtlink-hints
              • Combine-hints
              • Merge-functions
              • Make-merge-function-option-lst
              • Remove-duplicate-from-decl-list
              • Process-hint
              • Merge-hypothesis
              • Make-merge-more-returns
              • Make-merge-returns-helper
              • Make-merge-returns
              • Make-merge-formals-helper
              • Make-merge-formals
              • Set-smt-solver-params
              • Set-int-to-rat
              • Merge-main-hint
              • Make-merge-guard
              • Make-merge-function
              • Set-wrld-len
              • Set-smt-dir
              • Set-rm-file
              • Set-fty-types
              • Set-fname
              • Set-custom-p
              • Set-abstract-types
              • Make-merge-hypothesis
            • Function-syntax
            • Smtlink-hint-syntax
            • Argument-lst-syntax
            • Hypothesis-lst-syntax
            • Translate-cmp-smtlink
            • Process-hint-clause-processor
            • Smt-solver-params
            • Hints-syntax
            • True-set-equiv-relation
          • Smt-basics
          • Smt-type-hyp
          • Smt-magic-fix
        • Trusted
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Smtlink-process-user-hint

Process-smtlink-hints

Definitions and Theorems

Function: make-merge-formals-helper

(defun make-merge-formals-helper (content)
 (declare (xargs :guard (argument-lst-syntax-p content)))
 (let ((acl2::__function__ 'make-merge-formals-helper))
  (declare (ignorable acl2::__function__))
  (b* ((content (argument-lst-syntax-fix content))
       ((unless (consp content)) nil)
       ((cons first rest) content)
       ((list* argname type & hints) first)
       (new-formal (make-decl :name argname
                              :type (make-hint-pair :thm type
                                                    :hints hints))))
    (cons new-formal
          (make-merge-formals-helper rest)))))

Theorem: decl-listp-of-make-merge-formals-helper

(defthm decl-listp-of-make-merge-formals-helper
  (b* ((decls (make-merge-formals-helper content)))
    (decl-listp decls))
  :rule-classes :rewrite)

Function: remove-duplicate-from-decl-list

(defun remove-duplicate-from-decl-list (decls seen)
 (declare (xargs :guard (and (decl-listp decls)
                             (symbol-listp seen))))
 (let ((acl2::__function__ 'remove-duplicate-from-decl-list))
  (declare (ignorable acl2::__function__))
  (b* ((decls (decl-list-fix decls))
       ((unless (consp decls)) nil)
       ((cons first rest) decls)
       ((decl d) first)
       (seen? (member-equal d.name seen))
       ((if seen?)
        (remove-duplicate-from-decl-list rest seen)))
   (cons
       first
       (remove-duplicate-from-decl-list rest (cons d.name seen))))))

Theorem: decl-listp-of-remove-duplicate-from-decl-list

(defthm decl-listp-of-remove-duplicate-from-decl-list
  (b* ((simple-decls (remove-duplicate-from-decl-list decls seen)))
    (decl-listp simple-decls))
  :rule-classes :rewrite)

Function: make-merge-formals

(defun make-merge-formals (content smt-func)
 (declare (xargs :guard (and (argument-lst-syntax-p content)
                             (func-p smt-func))))
 (let ((acl2::__function__ 'make-merge-formals))
  (declare (ignorable acl2::__function__))
  (b*
   ((new-formals (make-merge-formals-helper content))
    ((func f) smt-func)
    (all-formals
     (remove-duplicate-from-decl-list (append new-formals f.formals)
                                      nil)))
   (change-func f :formals all-formals))))

Theorem: func-p-of-make-merge-formals

(defthm func-p-of-make-merge-formals
  (b* ((func (make-merge-formals content smt-func)))
    (func-p func))
  :rule-classes :rewrite)

Function: make-merge-returns-helper

(defun make-merge-returns-helper (content)
 (declare (xargs :guard (argument-lst-syntax-p content)))
 (let ((acl2::__function__ 'make-merge-returns-helper))
   (declare (ignorable acl2::__function__))
   (b* ((content (argument-lst-syntax-fix content))
        ((unless (consp content)) nil)
        ((cons first rest) content)
        ((cons argname (cons type (cons & hints)))
         first)
        (new-return
             (make-decl :name argname
                        :type (make-hint-pair :thm type
                                              :hints (car hints)))))
     (cons new-return
           (make-merge-returns-helper rest)))))

Theorem: decl-listp-of-make-merge-returns-helper

(defthm decl-listp-of-make-merge-returns-helper
  (b* ((decls (make-merge-returns-helper content)))
    (decl-listp decls))
  :rule-classes :rewrite)

Function: make-merge-returns

(defun make-merge-returns (content smt-func)
 (declare (xargs :guard (and (argument-lst-syntax-p content)
                             (func-p smt-func))))
 (let ((acl2::__function__ 'make-merge-returns))
  (declare (ignorable acl2::__function__))
  (b*
   ((new-return (make-merge-returns-helper content))
    ((func f) smt-func)
    (all-returns
      (remove-duplicate-from-decl-list (append new-return f.returns)
                                       nil)))
   (change-func f :returns all-returns))))

Theorem: func-p-of-make-merge-returns

(defthm func-p-of-make-merge-returns
  (b* ((func (make-merge-returns content smt-func)))
    (func-p func))
  :rule-classes :rewrite)

Function: make-merge-guard

(defun make-merge-guard (content smt-func)
  (declare (xargs :guard (and (hypothesis-syntax-p content)
                              (func-p smt-func))))
  (let ((acl2::__function__ 'make-merge-guard))
    (declare (ignorable acl2::__function__))
    (b* ((content (hypothesis-syntax-fix content))
         (smt-func (func-fix smt-func))
         ((cons thm (cons & hints-lst)) content)
         (hints (car hints-lst))
         (new-guard (make-hint-pair :thm thm :hints hints)))
      (change-func smt-func
                   :guard new-guard))))

Theorem: func-p-of-make-merge-guard

(defthm func-p-of-make-merge-guard
  (b* ((func (make-merge-guard content smt-func)))
    (func-p func))
  :rule-classes :rewrite)

Function: make-merge-more-returns

(defun make-merge-more-returns (content smt-func)
 (declare (xargs :guard (and (hypothesis-lst-syntax-p content)
                             (func-p smt-func))))
 (let ((acl2::__function__ 'make-merge-more-returns))
  (declare (ignorable acl2::__function__))
  (b*
   ((content (hypothesis-lst-syntax-fix content))
    (smt-func (func-fix smt-func))
    ((func f) smt-func)
    ((unless (consp content)) smt-func)
    ((cons first rest) content)
    ((cons thm (cons & hints-lst)) first)
    (hints (car hints-lst))
    (new-more-return (make-hint-pair :thm thm :hints hints))
    (new-func
         (change-func
              smt-func
              :more-returns (cons new-more-return f.more-returns))))
   (make-merge-more-returns rest new-func))))

Theorem: func-p-of-make-merge-more-returns

(defthm func-p-of-make-merge-more-returns
  (b* ((func (make-merge-more-returns content smt-func)))
    (func-p func))
  :rule-classes :rewrite)

Function: make-merge-function-option-lst

(defun make-merge-function-option-lst (fun-opt-lst smt-func)
 (declare
      (xargs :guard (and (function-option-lst-syntax-p fun-opt-lst)
                         (func-p smt-func))))
 (let ((acl2::__function__ 'make-merge-function-option-lst))
  (declare (ignorable acl2::__function__))
  (b*
   ((fun-opt-lst (function-option-lst-syntax-fix fun-opt-lst))
    (smt-func (func-fix smt-func))
    ((unless (consp fun-opt-lst)) smt-func)
    ((cons option (cons content rest))
     fun-opt-lst)
    (new-func
     (case option
       (:formals (make-merge-formals content smt-func))
       (:returns (make-merge-returns content smt-func))
       (:level (change-func smt-func
                            :expansion-depth content))
       (:guard (make-merge-guard content smt-func))
       (:more-returns (make-merge-more-returns content smt-func)))))
   (make-merge-function-option-lst rest new-func))))

Theorem: func-p-of-make-merge-function-option-lst

(defthm func-p-of-make-merge-function-option-lst
  (b* ((func (make-merge-function-option-lst fun-opt-lst smt-func)))
    (func-p func))
  :rule-classes :rewrite)

Function: make-merge-function

(defun make-merge-function (func smt-func)
  (declare (xargs :guard (and (function-syntax-p func)
                              (func-p smt-func))))
  (let ((acl2::__function__ 'make-merge-function))
    (declare (ignorable acl2::__function__))
    (b* ((func (function-syntax-fix func))
         ((cons fun-name fun-opt-lst) func)
         (name fun-name))
      (make-merge-function-option-lst
           fun-opt-lst
           (change-func smt-func :name name)))))

Theorem: func-p-of-make-merge-function

(defthm func-p-of-make-merge-function
  (b* ((func (make-merge-function func smt-func)))
    (func-p func))
  :rule-classes :rewrite)

Function: merge-functions

(defun merge-functions (content hint)
  (declare (xargs :guard (and (function-lst-syntax-p content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'merge-functions))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (content (function-lst-syntax-fix content))
         ((unless (consp content)) hint)
         ((cons first rest) content)
         (name (car first))
         ((smtlink-hint h) hint)
         (exist? (hons-get name h.fast-functions))
         (smt-func (if exist? (cdr exist?) (make-func)))
         (new-func-lst (cons (make-merge-function first smt-func)
                             h.functions))
         (new-hint (change-smtlink-hint hint
                                        :functions new-func-lst)))
      (merge-functions rest new-hint))))

Theorem: smtlink-hint-p-of-merge-functions

(defthm smtlink-hint-p-of-merge-functions
  (b* ((new-hint (merge-functions content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: make-merge-hypothesis

(defun make-merge-hypothesis (hypo)
  (declare (xargs :guard (hypothesis-syntax-p hypo)))
  (let ((acl2::__function__ 'make-merge-hypothesis))
    (declare (ignorable acl2::__function__))
    (b* ((hypo (hypothesis-syntax-fix hypo))
         ((list* thm & rest) hypo))
      (make-hint-pair :thm thm
                      :hints (car rest)))))

Theorem: hint-pair-p-of-make-merge-hypothesis

(defthm hint-pair-p-of-make-merge-hypothesis
  (b* ((hp (make-merge-hypothesis hypo)))
    (hint-pair-p hp))
  :rule-classes :rewrite)

Function: merge-hypothesis

(defun merge-hypothesis (content hint)
  (declare (xargs :guard (and (hypothesis-lst-syntax-p content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'merge-hypothesis))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (content (hypothesis-lst-syntax-fix content))
         ((unless (consp content)) hint)
         ((cons first rest) content)
         ((smtlink-hint h) hint)
         (new-hypo-lst (cons (make-merge-hypothesis first)
                             h.hypotheses))
         (new-hint (change-smtlink-hint hint
                                        :hypotheses new-hypo-lst)))
      (merge-hypothesis rest new-hint))))

Theorem: smtlink-hint-p-of-merge-hypothesis

(defthm smtlink-hint-p-of-merge-hypothesis
  (b* ((new-hint (merge-hypothesis content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: merge-main-hint

(defun merge-main-hint (content hint)
  (declare (xargs :guard (and (hints-syntax-p content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'merge-main-hint))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (content (hints-syntax-fix content))
         (new-hint (change-smtlink-hint hint
                                        :main-hint content)))
      new-hint)))

Theorem: smtlink-hint-p-of-merge-main-hint

(defthm smtlink-hint-p-of-merge-main-hint
  (b* ((new-hint (merge-main-hint content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-abstract-types

(defun set-abstract-types (content hint)
  (declare (xargs :guard (and (symbol-listp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-abstract-types))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :abs content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-abstract-types

(defthm smtlink-hint-p-of-set-abstract-types
  (b* ((new-hint (set-abstract-types content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-fty-types

(defun set-fty-types (content hint)
  (declare (xargs :guard (and (symbol-listp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-fty-types))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :fty content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-fty-types

(defthm smtlink-hint-p-of-set-fty-types
  (b* ((new-hint (set-fty-types content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-int-to-rat

(defun set-int-to-rat (content hint)
  (declare (xargs :guard (and (booleanp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-int-to-rat))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :int-to-rat content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-int-to-rat

(defthm smtlink-hint-p-of-set-int-to-rat
  (b* ((new-hint (set-int-to-rat content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-fname

(defun set-fname (content hint)
  (declare (xargs :guard (and (stringp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-fname))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :smt-fname content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-fname

(defthm smtlink-hint-p-of-set-fname
  (b* ((new-hint (set-fname content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-smt-dir

(defun set-smt-dir (content hint)
  (declare (xargs :guard (and (stringp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-smt-dir))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :smt-dir content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-smt-dir

(defthm smtlink-hint-p-of-set-smt-dir
  (b* ((new-hint (set-smt-dir content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-rm-file

(defun set-rm-file (content hint)
  (declare (xargs :guard (and (booleanp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-rm-file))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :rm-file content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-rm-file

(defthm smtlink-hint-p-of-set-rm-file
  (b* ((new-hint (set-rm-file content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-custom-p

(defun set-custom-p (content hint)
  (declare (xargs :guard (and (booleanp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-custom-p))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :custom-p content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-custom-p

(defthm smtlink-hint-p-of-set-custom-p
  (b* ((new-hint (set-custom-p content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-wrld-len

(defun set-wrld-len (content hint)
  (declare (xargs :guard (and (natp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-wrld-len))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :wrld-fn-len content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-wrld-len

(defthm smtlink-hint-p-of-set-wrld-len
  (b* ((new-hint (set-wrld-len content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: set-smt-solver-params

(defun set-smt-solver-params (content hint)
  (declare (xargs :guard (and (smt-solver-params-p content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-smt-solver-params))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (content (smt-solver-params-fix content))
         (new-hint (change-smtlink-hint hint
                                        :smt-params content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-smt-solver-params

(defthm smtlink-hint-p-of-set-smt-solver-params
  (b* ((new-hint (set-smt-solver-params content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)

Function: combine-hints

(defun combine-hints (user-hint hint)
 (declare (xargs :guard (and (smtlink-hint-syntax-p user-hint)
                             (smtlink-hint-p hint))))
 (let ((acl2::__function__ 'combine-hints))
  (declare (ignorable acl2::__function__))
  (b*
   ((hint (smtlink-hint-fix hint))
    (user-hint (smtlink-hint-syntax-fix user-hint))
    ((unless (consp user-hint)) hint)
    ((cons option (cons second rest))
     user-hint)
    ((smtlink-hint h) hint)
    (fast-funcs (make-alist-fn-lst h.functions))
    (new-hint
     (case option
      (:functions
       (with-fast-alist
            fast-funcs
            (merge-functions
                 second
                 (change-smtlink-hint hint
                                      :fast-functions fast-funcs))))
      (:hypotheses (merge-hypothesis second hint))
      (:main-hint (merge-main-hint second hint))
      (:abstract (set-abstract-types second hint))
      (:fty (set-fty-types second hint))
      (:int-to-rat (set-int-to-rat second hint))
      (:smt-fname (set-fname second hint))
      (:smt-dir (set-smt-dir second hint))
      (:rm-file (set-rm-file second hint))
      (:custom-p (set-custom-p second hint))
      (:smt-solver-params (set-smt-solver-params second hint))
      (t (set-wrld-len second hint)))))
   (combine-hints rest new-hint))))

Theorem: smtlink-hint-p-of-combine-hints

(defthm smtlink-hint-p-of-combine-hints
  (b* ((combined-hint (combine-hints user-hint hint)))
    (smtlink-hint-p combined-hint))
  :rule-classes :rewrite)

Function: process-hint

(defun process-hint (cl user-hint)
 (declare (xargs :guard (pseudo-term-listp cl)))
 (let ((acl2::__function__ 'process-hint))
  (declare (ignorable acl2::__function__))
  (b*
   ((cl (pseudo-term-list-fix cl))
    ((unless (smtlink-hint-syntax-p user-hint))
     (prog2$
      (cw
       "User provided Smtlink hint can't be applied because of ~
    syntax error in the hints: ~q0Therefore proceed without Smtlink...~%"
       user-hint)
      (list cl)))
    (combined-hint (combine-hints user-hint (smt-hint)))
    (next-cp (cdr (assoc-equal 'process-hint
                               *smt-architecture*)))
    ((if (null next-cp)) (list cl))
    (cp-hint
     (cons
      ':clause-processor
      (cons
           (cons next-cp
                 (cons 'clause
                       (cons (cons 'quote (cons combined-hint 'nil))
                             'nil)))
           'nil)))
    (subgoal-lst (cons (cons 'hint-please
                             (cons (cons 'quote (cons cp-hint 'nil))
                                   'nil))
                       cl)))
   (list subgoal-lst))))

Theorem: pseudo-term-list-listp-of-process-hint

(defthm pseudo-term-list-listp-of-process-hint
  (b* ((subgoal-lst (process-hint cl user-hint)))
    (pseudo-term-list-listp subgoal-lst))
  :rule-classes :rewrite)

Subtopics

Combine-hints

Combining user-hints into smt-hint.

Merge-functions

Merging function hints into smt-hint.

Make-merge-function-option-lst

Add option information into func.

Remove-duplicate-from-decl-list

Remove shadowed decls from decl-list

Process-hint

Merge-hypothesis

Merge hypothesis into hint

Make-merge-more-returns

Adding user-defined more-return theorems.

Make-merge-returns-helper

Adding user defined returns to overwrite what's already in smt-func.

Make-merge-returns

Adding user defined returns to overwrite what's already in smt-func.

Make-merge-formals-helper

Adding user defined formals to overwrite what's already in smt-func.

Make-merge-formals

Adding user defined formals to overwrite what's already in smt-func.

Set-smt-solver-params

Set :smt-params

Set-int-to-rat

Set :int-to-rat based on user hint.

Merge-main-hint

Merge main-hint

Make-merge-guard

Adding user defined guard to smt-func.

Make-merge-function

Function for generating func-p of a single function hint.

Set-wrld-len

Set :wrld-fn-len

Set-smt-dir

Set :smt-dir

Set-rm-file

Set :rm-file

Set-fty-types

set fty types

Set-fname

Set :smt-fname.

Set-custom-p

Set :custom-p

Set-abstract-types

set fty types

Make-merge-hypothesis

Generate a hint-pair for hypo