From: Aina Niemetz Date: Wed, 26 Sep 2018 04:59:28 +0000 (-0700) Subject: cmake: New INSTALL.md for build and testing instructions. (#2536) X-Git-Tag: cvc5-1.0.0~4500 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e954e0ee501ecf9489ce43775c0c3c6b7123ac89;p=cvc5.git cmake: New INSTALL.md for build and testing instructions. (#2536) --- diff --git a/INSTALL b/INSTALL deleted file mode 100644 index 655c0e005..000000000 --- a/INSTALL +++ /dev/null @@ -1,259 +0,0 @@ -CVC4 prerelease version 1.7. - -** Quick-start instructions - -*** Supported operating systems - -CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled -using Mingw-w64. We recommend a 64-bit operating system. - -On macOS, we recommend using Homebrew (https://brew.sh/) to install the -dependencies. We also have a Homebrew Tap available at -https://github.com/CVC4/homebrew-cvc4 . - -*** Build dependencies - -The following tools and libraries are required to build and run CVC4. -Versions given are minimum versions; more recent versions should be -compatible. - - GNU C and C++ (gcc and g++) or Clang, reasonably recent versions - GNU Make - GNU Bash - GMP v4.2 (GNU Multi-Precision arithmetic library) - libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library) - The Boost C++ base libraries - -Some features, such as the theory of floating-point numbers, require optional -dependencies, please refer to the section "Optional dependencies" below for -details. - -If "make" is non-GNU on your system, make sure to invoke "gmake" (or -whatever GNU Make is installed as). If your usual shell is not Bash, -the configure script should auto-correct this. If it does not, you'll -see strange shell syntax errors, and you may need to explicitly set -SHELL or CONFIG_SHELL to the location of bash on your system. - -*** Installing libantlr3c: ANTLR parser generator C support library - -For libantlr3c, you can use the convenience script in -contrib/get-antlr-3.4. This will download, patch, and install -libantlr3c. On a 32-bit machine, or if you have difficulty building -libantlr3c (or difficulty getting CVC4 to link against it later), you -may need to remove the --enable-64bit part in the script. (If you're -curious, the manual instructions are at -http://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#ANTLR3 .) - -*** Installing the Boost C++ base libraries - -A Boost package is available on most Linux distributions and Homebrew; check -yours for a package named something like libboost-dev or boost-devel. There -are a number of additional Boost packages in some distributions, but this -"basic" one should be sufficient for building CVC4. - -Should you want to install Boost manually, or to learn more about the -Boost project, please visit http://www.boost.org/. - -*** Optional dependencies - -None of these is required, but can improve CVC4 as described below: - - Optional: SymFPU (an implementation of SMT-LIB/IEEE-754 floating-point - operations in terms of bit-vector operations) - Optional: CaDiCaL (optional SAT solver) - Optional: CryptoMiniSat (optional SAT solver) - Optional: LFSC (the LFSC proof checker) - Optional: SWIG 3.0.x (Simplified Wrapper and Interface Generator) - Optional: CLN v1.3 or newer (Class Library for Numbers) - Optional: glpk-cut-log (A fork of the GNU Linear Programming Kit) - Optional: ABC library (for improved bitvector support) - Optional: GNU Readline library (for an improved interactive experience) - Optional: The Boost C++ threading library (libboost_thread) - Optional: CxxTest unit testing framework - -SymFPU is required for supporting the theory of floating-point numbers. It can -be installed using the contrib/get-symfpu script. Use --with-symfpu when -configuring CVC4 to build with the dependency. - -CaDiCaL is a SAT solver that can be used for solving non-incremental bit-vector -problems when using eager bit-blasting. This dependency may improve -performance. It can be installed using the contrib/get-cadical script. Use ---with-cadical when configuring CVC4 to build with this dependency. - -CryptoMiniSat is a SAT solver that can be used for solving bit-vector problems -when using eager bit-blasting. This dependency may improve performance. It can -be installed using the contrib/get-cryptominisat script. Use ---with-cryptominisat when configuring CVC4 to build with this dependency. - -LFSC is required to check proofs internally with --check-proofs. It can be -installed using the contrib/get-lfsc script. Use --with-lfsc when configuring -CVC4 to build with this dependency. - -SWIG is necessary to build the Java API (and of course a JDK is -necessary, too). SWIG 1.x/2.x won't work; you'll need 3.0, and the more -recent the better. See "Language bindings" below for build instructions. - -CLN is an alternative multiprecision arithmetic package that can offer -better performance and memory footprint than GMP. CLN is covered by -the GNU General Public License, version 3; so if you choose to use -CVC4 with CLN support, you are licensing CVC4 under that same license. -(Usually CVC4's license is more permissive than GPL is; see the file -COPYING in the CVC4 source distribution for details.) Please visit -http://www.ginac.de/CLN/ for more details about CLN. - -glpk-cut-log is a fork of GLPK (the GNU Linear Programming Kit). -This can be used to speed up certain classes of problems for the arithmetic -implementation in CVC4. (This is not recommended for most users.) The source -code for glpk-cut-log is available at: -https://github.com/timothy-king/glpk-cut-log/ -The only option for installation of glpk-cut-log is downloading the library, -compiling and installing it manually. CVC4 is no longer compatible with the -main GLPK library. GLPK and glpk-cut-log are covered by the GNU General Public -License, version 3; so if you choose to use CVC4 with GLPK support, you are -licensing CVC4 under that same license. -(Usually CVC4's license is more permissive; see above discussion.) -Please visit http://www.gnu.org/software/glpk/ for more details about GLPK. - -ABC: A System for Sequential Synthesis and Verification is a library -for synthesis and verification of logic circuits. This can be used to -speed up the eager bit-vector solver by first encoding the bit-blasted -formula into AIG format and then using ABC to simplify the AIG. To -install abc run the contrib/get-abc script which will download and -install a compatible version of ABC in the cvc4 directory. To configure -CVC4 to use abc configure with --with-abc and --with-abc-dir=PATH, where -PATH corresponds to the install path of ABC. To run CVC4 using ABC use -the --bitblast-aig command line argument. -Please visit http://www.eecs.berkeley.edu/~alanmi/abc/ for more details -on ABC. - -The GNU Readline library is optionally used to provide command -editing, tab completion, and history functionality at the CVC prompt -(when running in interactive mode). Check your distribution for a -package named "libreadline-dev" or "readline-devel" or similar. This -library is covered by the GNU General Public License, version 3. Like -the above-mentioned libraries, if you choose to use CVC4 with readline -support, you are licensing CVC4 under that same license. (Please visit -http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more -details about readline.) - -The Boost C++ threading library (often packaged independently of the -Boost base library) is needed to run CVC4 in "portfolio" -(multithreaded) mode. Check your distribution for a package named -"libboost-thread-dev" or similar. - -CxxTest is necessary to run CVC4's unit tests (included with the -distribution). Running these is not really required for users of -CVC4; "make check" will skip unit tests if CxxTest isn't available, -and go on to run the extensive system- and regression-tests in the -source tree. However, if you're interested, you can download CxxTest -at http://cxxtest.com/ . - -*** Building CVC4 - -Once the build dependencies are satisfied, you should be able to configure, -make, make check, and make install without incident: - - ./autogen.sh [not required when building from a source distribution] - ./configure [use --prefix to specify a prefix; default /usr/local - use --with-* to use optional dependencies] - make - make check [optional but a good idea!] - -To build from a repository checkout (rather than a distributed CVC4 -tarball), there are additional dependencies; see below. - -You can then "make install" to install in the prefix you gave to -the configure script (/usr/local by default). ** You should run -"make check" ** before installation to ensure that CVC4 has been -built correctly. In particular, GCC version 4.5.1 seems to have a -bug in the optimizer that results in incorrect behavior (and wrong -results) in many builds. This is a known problem for MiniSat, and -since MiniSat is at the core of CVC4, a problem for CVC4. "make check" -easily detects this problem (by showing a number of FAILed test cases). -It is ok if the unit tests aren't run as part of "make check", but all -system tests and regression tests should pass without incident. - -To build API documentation, use "make doc". Documentation is produced -under doc/ but is not installed by "make install". - -Examples and tutorials are not installed with "make install." You may -want to "make install-examples". See below. - -For more information about the build system itself (probably not -necessary for casual users), see the Appendix at the bottom of this -file. - -*** Language bindings - -There are several options available for using CVC4 from the API. - -First, CVC4 offers a complete and flexible API for manipulating -expressions, maintaining a stack of assertions, and checking -satisfiability, and related things. The C++ libraries (libcvc4.so and -libcvc4parser.so) and required headers are installed normally via a -"make install". This API is also available from Java (via CVC4.jar -and libcvc4jni.so) by configuring with --enable-language-bindings=java. -You'll also need SWIG 2.0 installed (and you might need to help -configure find it if you installed it in a nonstandard place with ---with-swig-dir=/path/to/swig/installation). You may also need to -give the configure script the path to your Java headers (in -particular, jni.h). You might do so with (for example): - - ./configure --enable-language-bindings=java \ - JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include - -The examples/ directory includes some basic examples (the "simple vc" family of -examples) of all these interfaces. - -In principle, since we use SWIG to generate the native Java API, we -could support other languages as well. However, using CVC4 from other -languages is not supported, nor expected to work, at this time. If -you're interested in helping to develop, maintain, and test a language -binding, please contact one of the project leaders. - -*** Building CVC4 from a repository checkout - -CVC4's main repository is kept on GitHub at: - - https://github.com/CVC4/CVC4 - -and there are numerous experimental forks housed on GitHub as well, -by different developers, implementing various features. - -The following tools and libraries are additionally required to build -CVC4 from from a repository checkout rather than from a prepared -source tarball. - - Automake v1.11 or later - Autoconf v2.61 or later - Libtool v2.2 or later - ANTLR3 v3.2 or v3.4 - Python (2.x or 3.x) - -First, use "./autogen.sh" to create the configure script. Then proceed as -normal for any distribution tarball. The parsers are pre-generated for the -tarballs, but don't exist in the repository; hence the extra ANTLR3 requirement -to generate the source code for the parsers, when building from the repository. -Similarly, Python is required for generating some of the code. - -*** Examples and tutorials are not built or installed - -Examples are not built by "make" or "make install". See -examples/README for information on what to find in the examples/ -directory, as well as information about building and installing them. - -*** Appendix: Build architecture - -The build system is generated by automake, libtool, and autoconf. It -is somewhat nonstandard, though, which (for one thing) requires that -GNU Make be used. If you ./configure in the top-level source -directory, the objects will actually all appear in -builds/${arch}/${build_id}. This is to allow multiple, separate -builds in the same place (e.g., an assertions-enabled debugging build -alongside a production build), without changing directories at the -shell. The "current" build is maintained until you re-configure. - -You can also create your own build directory inside or outside of the -source tree and configure from there. All objects will then be built -in that directory, and you'll ultimately find the "cvc4" binary in -src/main/, and the libraries under src/ and src/parser/. diff --git a/INSTALL.md b/INSTALL.md new file mode 100644 index 000000000..2f0c7a051 --- /dev/null +++ b/INSTALL.md @@ -0,0 +1,325 @@ +CVC4 prerelease version 1.7. +============================ + +## Supported Operating Systems + +CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled +using Mingw-w64. We recommend a 64-bit operating system. + +On macOS, we recommend using Homebrew (https://brew.sh/) to install the +dependencies. We also have a Homebrew Tap available at +https://github.com/CVC4/homebrew-cvc4 . + +## Build dependencies + +The following tools and libraries are required to build and run CVC4. +Versions given are minimum versions; more recent versions should be +compatible. + +- [GNU C and C++ (gcc and g++)](https://gcc.gnu.org) + or [Clang](https://clang.llvm.org) (reasonably recent versions) +- [CMake >= 3.1](https://cmake.org) +- [GNU Bash](https://www.gnu.org/software/bash/) +- [Python >= 2.7](https://www.python.org) +- [GMP v4.2 (GNU Multi-Precision arithmetic library)](https://gmplib.org) +- [libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)](http://www.antlr3.org/) + +Some features, such as the theory of floating-point numbers, require +[optional dependencies](optional-dependencies) (see below). + +### Installing libantlr3c: ANTLR parser generator C support library + +For libantlr3c, you can use the script contrib/get-antlr-3.4. +This will download, patch, and install libantlr3c. + +If you're on a 32-bit machine, or if you have difficulty building +libantlr3c (or difficulty getting CVC4 to link against it), you +may need to remove the configure option `--enable-64bit` in the script. + +### Warning: GCC 4.5.1 + +GCC version 4.5.1 seems to have a bug in the optimizer that may result in +incorrect behavior (and wrong results) in many builds. This is a known problem +for MiniSat, and since MiniSat is at the core of CVC4, a problem for CVC4. +We recommend using a GCC version > 4.5.1. + +## Optional Dependencies + +### SymFPU (Support for the Theory of Floating Point Numbers) + +[SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4) +is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms +of bit-vector operations. +It is required for supporting the theory of floating-point numbers and +can be installed using the `contrib/get-symfpu` script. +Configure CVC4 with `configure.sh --symfpu` to build with this dependency. + +### CaDiCaL (Optional SAT solver) + +[CaDiCaL](https://github.com/arminbiere/cadical) +is a SAT solver that can be used for solving non-incremental bit-vector +problems with eager bit-blasting. This dependency may improve performance. +It can be installed using the `contrib/get-cadical script`. +Configure CVC4 with `configure.sh --cadical` to build with this dependency. + +### CryptoMiniSat (Optional SAT solver) + +[CryptoMinisat](https://github.com/msoos/cryptominisat) +is a SAT solver that can be used for solving bit-vector problems with eager +bit-blasting. This dependency may improve performance. +It can be installed using the `contrib/get-cryptominisat` script. +Configure CVC4 with `configure.sh --cryptominisat` to build with this +dependency. + +### LFSC (The LFSC Proof Checker) + +[LFSC](https://github.com/CVC4/LFSC) is required to check proofs internally +with --check-proofs. It can be installed using the `contrib/get-lfsc` script. +Configure CVC4 with `configure.sh --lfsc` to build with this dependency. + +### SWIG >= 3.0.x (Simplified Wrapper and Interface Generator) + +SWIG 3.0.x (and a JDK) is necessary to build the Java API. +See [Language Bindings](language-bindings) below for build instructions. + +### CLN >= v1.3 (Class Library for Numbers) + +[CLN](http://www.ginac.de/CLN) +is an alternative multiprecision arithmetic package that may offer better +performance and memory footprint than GMP. +Configure CVC4 with `configure.sh --cln` to build with this dependency. + +Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). +If you choose to use CVC4 with CLN support, you are licensing CVC4 under that +same license. +(Usually CVC4's license is more permissive than GPL, see the file `COPYING` in +the CVC4 source distribution for details.) + +### glpk-cut-log (A fork of the GNU Linear Programming Kit) + +[glpk-cut-log](https://github.com/timothy-king/glpk-cut-log/) is a fork of +[GLPK](http://www.gnu.org/software/glpk/) (the GNU Linear Programming Kit). +This can be used to speed up certain classes of problems for the arithmetic +implementation in CVC4. (This is not recommended for most users.) + +glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script. +Note that the only installation option is manual installation via this script. +CVC4 is no longer compatible with the main GLPK library. +Configure CVC4 with `configure.sh --glpk` to build with this dependency. + +Note that GLPK and glpk-cut-log are covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). +If you choose to use CVC4 with GLPK support, you are licensing CVC4 under that +same license. +(Usually CVC4's license is more permissive; see above discussion.) + +### ABC library (Improved Bit-Vector Support) + +[ABC](http://www.eecs.berkeley.edu/~alanmi/abc/) (A System for Sequential +Synthesis and Verification) is a library for synthesis and verification of +logic circuits. This dependency may improve performance of the eager +bit-vector solver. When enabled, the bit-blasted formula is encoded into +and-inverter-graphs (AIG) and ABC is used to simplify these AIGs. + +ABC can be installed using the `contrib/get-abc` script. +Configure CVC4 with `configure.sh --abc` to build with this dependency. + +### GNU Readline library (Improved Interactive Experience) + +The [GNU Readline](http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html) +library is optionally used to provide command editing, tab completion, and +history functionality at the CVC4 prompt (when running in interactive mode). +Check your distribution for a package named "libreadline-dev" or +"readline-devel" or similar. + +Note that GNU Readline is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). +If you choose to use CVC4 with GNU Readline support, you are licensing CVC4 +under that same license. +(Usually CVC4's license is more permissive; see above discussion.) + +### libboost_thread: The Boost C++ threading library (Portfolio Builds) + +The [Boost](http://www.boost.org) C++ threading library (often packaged +independently of the Boost base library) is needed to run CVC4 in "portfolio" +(multithreaded) mode. +Check your distribution for a package named "libboost-thread-dev" or similar. + +### Boost C++ base libraries (Examples) + +The [Boost](http://www.boost.org) C++ base library is needed for some examples +provided with CVC4. + +### CxxTest Unit Testing Framework (Unit Tests) + +[CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests +(included with the distribution). See [Testing](testing) below for more details. + + +## Building CVC4 + + ./configure.sh # use --prefix to specify a prefix (default: /usr/local) + # use --name= for custom build directory + cd # default is ./build + make # use -jN for parallel build with N threads + make check # to run default set of tests + make install # to install into the prefix specified above + +All binaries are built into `/bin`, the CVC4 library is built into +`/src`. + +## Language bindings + +CVC4 provides a complete and flexible C++ API (see `examples/api` for examples). +It further provides Java (see `examples/SimpleVC.java` and `examples/api/java`) +and Python (see `examples/SimpleVC.py`) API bindings. + +Configure CVC4 with `configure.sh --language-bindings=[java,python,all]` +to build with language bindings. +Note that this requires SWIG >= 3.0.x. + +In principle, since we use SWIG to generate the native Java and PythonAPI, +we could support other languages as well. However, using CVC4 from other +languages is not supported, nor expected to work, at this time. +If you're interested in helping to develop, maintain, and test a language +binding, please contact one of the project leaders. + +## Building the Examples + +The examples provided in directory `examples` are not built by default. + + make examples # build all examples + make runexamples # build and run all examples + make # build examples//. + ctest example// # run test example// + +All examples binaries are built into `/bin/examples`. + +See `examples/README` for more detailed information on what to find in the +`examples` directory. + +## Testing CVC4 + +We use `ctest` as test infrastructure, for all command-line options of ctest, +see `ctest -h`. Some useful options are: + + ctest -R # run all tests with names matching + ctest -E # exclude tests with names matching + ctest -L # run all tests with labels matching + ctest -LE # exclude tests with labels matching + ctest # run all tests + ctest -jN # run all tests in parallel with N threads + ctest --output-on-failure # run all tests and print output of failed tests + +We have 4 categories of tests: +- **examples** in directory `examples` + (label: **example**) +- **regression tests** (5 levels) in directory `test/regress` + (label: **regressN** with N the regression level) +- **system tests** in directory `test/system` + (label: **system**) +- **unit tests** in directory `test/unit` + (label: **unit**) + +### Testing Examples + +For building instructions, see [Building the Examples](building-the-examples). + +We use prefix `example/` + `/` + `` (for `` in +`example//`) as test target name. + + make bitvectors # build example/api/bitvectors.cpp + ctest -R bitvectors # run all tests that match '*bitvectors*' + # > runs example/api/bitvectors + # > example/api/bitvectors_and_arrays + # > ... + ctest -R bitvectors$ # run all tests that match '*bitvectors' + # > runs example/api/bitvectors + ctest -R example/api/bitvectors$ # run all tests that match '*example/api/bitvectors' + # > runs example/api/bitvectors + + +### Testing System Tests + +The system tests are not built by default. + + make systemtests # build and run all system tests + make # build test/system/. + ctest system/ # run test/system/. + +All system test binaries are built into `/bin/test/system`. + +We use prefix `system/` + `` (for `` in `test/system`) +as test target name. + + make ouroborous # build test/system/ouroborous.cpp + ctest -R ouroborous # run all tests that match '*ouroborous*' + # > runs system/ouroborous + ctest -R ouroborous$ # run all tests that match '*ouroborous' + # > runs system/ouroborous + ctest -R system/ouroborous$ # run all tests that match '*system/ouroborous' + # > runs system/ouroborous +### Testing Unit Tests + +The unit tests are not built by default. + + make units # build and run all unit tests + make # build test/unit//. + ctest unit// # run test/unit//. + +All unit test binaries are built into `/bin/test/unit`. + +We use prefix `unit/` + `/` + `` (for `` in +`test/unit/`) as test target name. + + make map_util_black # build test/unit/base/map_util_black.cpp + ctest -R map_util_black # run all tests that match '*map_util_black*' + # > runs unit/base/map_util_black + ctest -R base/map_util_black$ # run all tests that match '*base/map_util_black' + # > runs unit/base/map_util_black + ctest -R unit/base/map_util_black$ # run all tests that match '*unit/base/map_util_black' + # > runs unit/base/map_util_black + +### Testing Regression Tests + +We use prefix `regressN/` + `/` + `` (for `` +in level `N` in `test/regress/regressN/`) as test target name. + + ctest -L regress # run all regression tests + ctest -L regress0 # run all regression tests in level 0 + ctest -L regress[0-1] # run all regression tests in level 0 and 1 + ctest -R regress # run all regression tests + ctest -R regress0 # run all regression tests in level 0 + ctest -R regress[0-1] # run all regression tests in level 0 and 1 + ctest -R regress0/bug288b # run all tests that match '*regress0/bug288b*' + # > runs regress0/bug288b +### Custom Targets + +All custom test targets build and run a preconfigured set of tests. + +- `make check [-jN] [ARGS=-jN]` + The default build-and-test target for CVC4, builds and runs all examples, + all system and unit tests, and regression tests from levels 0 and 1. + +- `make systemtests [-jN] [ARGS=-jN]` + Build and run all system tests. + +- `make units [-jN] [ARGS=-jN]` + Build and run all unit tests. + +- `make regress [-jN] [ARGS=-jN]` + Build and run all regression tests. + +- `make runexamples [-jN] [ARGS=-jN]` + Build and run all examples. + +- `make coverage [-jN] [ARGS=-jN]` + Build and run all tests (system and unit tests, regression tests level 0-4) + with gcov to determine code coverage. + +We use `ctest` as test infrastructure, and by default all test targets +are configured to **run** in parallel with the maximum number of threads +available on the system. Override with `ARGS=-jN`. + +Use `-jN` for parallel **building** with `N` threads. + + + diff --git a/examples/README b/examples/README index df8cffe73..cc3c23f26 100644 --- a/examples/README +++ b/examples/README @@ -1,8 +1,11 @@ +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 -*** Files named SimpleVC*, simple_vc* +### 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 @@ -10,24 +13,19 @@ 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 +### 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. -*** Installing example source code - -Examples are not automatically installed by "make install". If you -wish to install them, use "make install-examples" after you configure -your CVC4 source tree. They'll appear in your documentation -directory, under the "examples" subdirectory (so, by default, -in /usr/local/share/doc/cvc4/examples). +### Building Examples -*** Building examples +The examples provided in this directory are not built by default. -Examples can be built as a separate step, after building CVC4 from -source. After building CVC4, you can run "make examples". You'll -find the built binaries in builds/examples (or just in "examples" if -you configured a build directory outside of the source tree). + make examples # build all examples + make runexamples # build and run all examples + make # build examples//. + ctest example/// # run examples//. +The examples binaries are built into `/bin/examples`.