• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
          • Defunc
          • Cgen
            • Defdata
            • Test?
            • ACL2s-defaults
            • Prove/cgen
            • Register-type
            • With-timeout
            • Defdata-attach
            • Testing-enabled
            • Defdata-aliasing-enabled
            • Cgen-single-test-timeout
            • Verbosity-level
            • Search-strategy
            • Num-print-counterexamples
            • Cgen-timeout
            • Cgen-local-timeout
            • Num-witnesses
            • Num-trials
            • Num-print-witnesses
            • Test-then-skip-proofs
            • Sampling-method
            • Recursively-fix
            • Num-counterexamples
            • Backtrack-limit
            • Print-cgen-summary
            • Cgen::flush
            • Backtrack-bad-generalizations
            • Use-fixers
            • Thm-no-test
            • Defthmd-no-test
            • Defthm-no-test
          • Ccg
          • Defdata
          • ACL2s-user-guide
          • ACL2s-tutorial
          • ACL2s-implementation-notes
          • Match
          • ACL2s-faq
          • ACL2s-intro
          • ACL2s-defaults
          • Definec
          • ACL2s-utilities
          • ACL2s-interface
          • ACL2s-installation
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Cgen
• ACL2s-defaults

Sampling-method

Specify sampling method to be used to instantiate variables

Specify which of the following methods to use for instantiating free variables of the conjecture under test: :be or :random or :uniform-random or :mixed By default this parameter is set to the symbol :random

Usage: 
(acl2s-defaults :set sampling-method :random) 
(acl2s-defaults :get sampling-method) 
:doc sampling-method