cvc5
  • Installation
  • Binary Documentation
  • API Documentation
  • Options
  • Output tags
  • Proof Production
  • Resource limits
  • Skolem Identifiers
  • Statistics
  • Examples
    • Hello World
    • Exception Handling
    • Theory of Bags
    • Theory of Bit-Vectors
    • Theory of Bit-Vectors and Arrays
    • Theory of Bit-Vectors: extract
    • Theory of Datatypes
    • Theory of Finite Fields
    • Theory of Floating-Points
    • Theory of Linear Arithmetic
    • Quickstart Example
    • Theory of Relations
    • Theory of Sequences
    • Theory of Sets
    • Theory of Strings
    • Theory Combination
    • SyGuS: Functions
    • SyGuS: Invariants
    • Parser
    • Parser with Shared Symbol Manager
    • Theory of Uninterpreted Functions
  • Theory References
  • References
  • Index
Other versions
cvc5-main
cvc5-1.2.1
cvc5-1.2.0
cvc5-1.1.2
cvc5-1.1.1
cvc5-1.1.0
cvc5-1.0.9
cvc5-1.0.8
cvc5-1.0.7
cvc5-1.0.2
cvc5-1.0.1
cvc5-1.0.0
cvc5
  • Examples

Examples 

The following examples show how the APIs ( C++ API , Java API , Python API ) and input languages can be used. For every example, the same problem is constructed and solved using different input mechanisms.

  • Hello World
  • Exception Handling
  • Theory of Bags
  • Theory of Bit-Vectors
  • Theory of Bit-Vectors and Arrays
  • Theory of Bit-Vectors: extract
  • Theory of Datatypes
  • Theory of Finite Fields
  • Theory of Floating-Points
  • Theory of Linear Arithmetic
  • Quickstart Example
  • Theory of Relations
  • Theory of Sequences
  • Theory of Sets
  • Theory of Strings
  • Theory Combination
  • SyGuS: Functions
  • SyGuS: Invariants
  • Parser
  • Parser with Shared Symbol Manager
  • Theory of Uninterpreted Functions
Previous Next

© Copyright 2025, the authors of cvc5.

Built with Sphinx using a theme provided by Read the Docs .