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
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.