summaryrefslogtreecommitdiff
path: root/examples/README
blob: cc3c23f26ed1fbba83f3280bf80e74264b28ea98 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
Examples
--------

This directory contains usage examples of CVC4's different language
bindings, library APIs, and also tutorial examples from the tutorials
available at http://cvc4.cs.stanford.edu/wiki/Tutorials

### SimpleVC*, simple_vc*

These are examples of how to use CVC4 with each of its library
interfaces (APIs) and language bindings.  They are essentially "hello
world" examples, and do not fully demonstrate the interfaces, but
function as a starting point to using simple expressions and solving
functionality through each library.

### Targeted examples

The "api" directory contains some more specifically-targeted
examples (for bitvectors, for arithmetic, etc.).  The "api/java"
directory contains the same examples in Java.

### Building Examples

The examples provided in this directory are not built by default.

    make examples                      # build all examples
    make runexamples                   # build and run all examples
    make <example>                     # build examples/<subdir>/<example>.<ext>
    ctest example//<subdir>/<example>  # run examples/<subdir>/<example>.<ext>

The examples binaries are built into `<build_dir>/bin/examples`.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback