Content

Download and Installation

• Binary Distributions
• Building Yices from Source

Basics

• Overview
• Basic Usage

API Reference

• Version Information
• MCSAT Support
• Thread-Safe API
• Global Initialization and Cleanup
• Catching “Out of Memory” Errors
• Hard-coded Limits
• API Types
  • Yices Types
  • Yices Terms
  • Contexts
  • Models
  • Error Reports
• Error Reporting
• Vectors
  • Type Vectors
  • Term Vectors
  • Vectors of Node Descriptors
• Types
  • Type Constructors
  • Tests on Types
  • Access to Type Components
• 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
  • 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