• 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
            • Smtlink-hint
              • Smtlink-hint-p
              • Make-smtlink-hint
              • Func
              • Smtlink-hint-fix
              • Maybe-smtlink-hint
              • Hint-pair
              • Decl
              • Binding
              • Smtlink-hint-equiv
              • Let-binding
              • Change-smtlink-hint
              • Smtlink-hint->expanded-clause-w/-hint
              • Smtlink-hint->type-decl-list
              • Smtlink-hint->fast-functions
              • Smtlink-hint->expanded-g/type
              • Smtlink-hint->smt-params
              • Smtlink-hint->let-binding
              • Smtlink-hint->hypotheses
              • Smtlink-hint->fty-info
              • Smtlink-hint->wrld-fn-len
              • Smtlink-hint->symbols
              • Smtlink-hint->smt-fname
              • Smtlink-hint->smt-dir
              • Smtlink-hint->smt-cnf
              • Smtlink-hint->rm-file
              • Smtlink-hint->main-hint
              • Smtlink-hint->int-to-rat
              • Smtlink-hint->functions
              • Smtlink-hint->fty-types
              • Smtlink-hint->custom-p
              • Smtlink-hint->fty
              • Smtlink-hint->abs
            • Smt-hint
            • Make-alist-fn-lst
            • True-list-fix
          • Function-expansion
          • Smt-config
          • Fty-support
          • Smt-computed-hints
          • Add-hypo-cp
          • Smt-hint-please
          • Type-extract-cp
          • Smt-extract
          • Smtlink-process-user-hint
          • 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

• Smt-hint-interface

Smtlink-hint

This is a product type introduced by defprod.

Fields

functions — func-list

hypotheses — hint-pair-list

main-hint — true-listp

let-binding — let-binding

symbols — ACL2::symbol-list

abs — ACL2::symbol-list

fty — ACL2::symbol-list

fty-info — fty-info-alist

fty-types — fty-types

int-to-rat — booleanp

smt-dir — stringp

rm-file — booleanp

smt-fname — stringp

smt-params — true-listp

fast-functions — func-alist

type-decl-list — pseudo-termp

expanded-clause-w/-hint — hint-pair

expanded-g/type — pseudo-termp

smt-cnf — smtlink-config

wrld-fn-len — natp

custom-p — booleanp

Subtopics

Smtlink-hint-p

Recognizer for smtlink-hint structures.

Make-smtlink-hint

Basic constructor macro for smtlink-hint structures.

Func

Smtlink-hint-fix

Fixing function for smtlink-hint structures.

Maybe-smtlink-hint

Option type; smtlink-hint or nil.

Hint-pair

Decl

Binding

Smtlink-hint-equiv

Basic equivalence relation for smtlink-hint structures.

Let-binding

Change-smtlink-hint

Modifying constructor for smtlink-hint structures.

Smtlink-hint->expanded-clause-w/-hint

Get the expanded-clause-w/-hint field from a smtlink-hint.

Smtlink-hint->type-decl-list

Get the type-decl-list field from a smtlink-hint.

Smtlink-hint->fast-functions

Get the fast-functions field from a smtlink-hint.

Smtlink-hint->expanded-g/type

Get the expanded-g/type field from a smtlink-hint.

Smtlink-hint->smt-params

Get the smt-params field from a smtlink-hint.

Smtlink-hint->let-binding

Get the let-binding field from a smtlink-hint.

Smtlink-hint->hypotheses

Get the hypotheses field from a smtlink-hint.

Smtlink-hint->fty-info

Get the fty-info field from a smtlink-hint.

Smtlink-hint->wrld-fn-len

Get the wrld-fn-len field from a smtlink-hint.

Smtlink-hint->symbols

Get the symbols field from a smtlink-hint.

Smtlink-hint->smt-fname

Get the smt-fname field from a smtlink-hint.

Smtlink-hint->smt-dir

Get the smt-dir field from a smtlink-hint.

Smtlink-hint->smt-cnf

Get the smt-cnf field from a smtlink-hint.

Smtlink-hint->rm-file

Get the rm-file field from a smtlink-hint.

Smtlink-hint->main-hint

Get the main-hint field from a smtlink-hint.

Smtlink-hint->int-to-rat

Get the int-to-rat field from a smtlink-hint.

Smtlink-hint->functions

Get the functions field from a smtlink-hint.

Smtlink-hint->fty-types

Get the fty-types field from a smtlink-hint.

Smtlink-hint->custom-p

Get the custom-p field from a smtlink-hint.

Smtlink-hint->fty

Get the fty field from a smtlink-hint.

Smtlink-hint->abs

Get the abs field from a smtlink-hint.