cvc5
  • Installation
  • Binary Documentation
  • API Documentation
  • Options
  • Output tags
  • Proof production
  • Resource limits
  • 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 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: Grammars
    • SyGuS: Invariants
  • 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 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: Grammars
  • SyGuS: Invariants
Previous Next

© Copyright 2022, the authors of cvc5.

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