Content

Download and Installation

• Binary Distributions
• Building Yices from Source

Basics

• Overview
• Basic Usage

API Reference

• Version Information
  • __YICES_VERSION
  • __YICES_VERSION_MAJOR
  • __YICES_VERSION_PATCHLEVEL
  • yices_version
  • yices_build_arch
  • yices_build_mode
  • yices_build_date
• MCSAT Support
  • yices_has_mcsat
• Thread-Safe API
  • yices_is_thread_safe
• Global Initialization and Cleanup
  • yices_init
  • yices_exit
  • yices_reset
  • yices_free_string
• Catching “Out of Memory” Errors
  • yices_set_out_of_mem_callback
• Hard-coded Limits
  • YICES_MAX_TYPES
  • YICES_MAX_TERMS
  • YICES_MAX_ARITY
  • YICES_MAX_DEGREE
  • YICES_MAX_VARS
  • YICES_MAX_BVSIZE
• API Types
  • Yices Types
  • Yices Terms
  • Contexts
  • Models
  • Error Reports
• Error Reporting
  • yices_error_code
  • yices_error_report
  • yices_clear_error
  • yices_print_error
  • yices_print_error_fd
  • yices_error_string
• Vectors
  • Type Vectors
  • Term Vectors
  • Vectors of Node Descriptors
• Types
  • Type Constructors
  • Tests on Types
  • Access to Type Components
  • Type Macros
• Terms
  • General Constructors
  • Boolean Terms
  • Arithmetic Terms
  • Bitvector Terms
  • Term Properties
  • Access to Term Components
• Miscellaneous Operations
  • Names
  • Parsing
  • Substitutions
  • Garbage Collection
• Contexts
  • Creation and Configuration
  • Assertions and Satisfiability Checks
  • Push and Pop
  • Check with Assumptions and Unsat Cores
  • Check Modulo a Model and Model Interpolant
  • Check and Compute Interpolant
  • Set a Fixed Variable Ordering for MCSat
  • Set a Initial Variable Ordering for MCSat
  • Search Parameters
• Models
  • Model Construction
  • Value of a Term in a Model
  • Model Assignment
  • Supports
  • Implicants
  • Model Generalization
• Operations on Formulas
  • Checking Satisfiability
  • Export to DIMACS
• Pretty Printing
  • Printing Terms and Types
  • Printing Models and Term Values

Appendix

• Yices Input Language
• SMT Logics
• Heuristic Parameters
• References

Index and Search

• Index

• Search Page