diff options
author | anwu1219 <haozewu@stanford.edu> | 2018-09-25 23:43:13 -0700 |
---|---|---|
committer | anwu1219 <haozewu@stanford.edu> | 2018-09-25 23:43:13 -0700 |
commit | a1e86adf59555c204e2b3058141ad6f41175be1d (patch) | |
tree | 412a8207c745469cdec53bafddef66648911c1e6 | |
parent | 7bc41fcca9b4b02e77b02934a40a7d4100cd4d5b (diff) | |
parent | e954e0ee501ecf9489ce43775c0c3c6b7123ac89 (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
-rw-r--r-- | CMakeLists.txt | 21 | ||||
-rw-r--r-- | INSTALL | 259 | ||||
-rw-r--r-- | INSTALL.md | 325 | ||||
-rwxr-xr-x | configure.sh | 1 | ||||
-rw-r--r-- | examples/README | 26 | ||||
-rw-r--r-- | examples/hashsmt/sha1_inversion.cpp | 6 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 17 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 5 |
9 files changed, 384 insertions, 282 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 453f1bcf7..921396e21 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -217,6 +217,24 @@ endif() enable_testing() #-----------------------------------------------------------------------------# +# Check GCC version. +# +# GCC version 4.5.1 builds MiniSat incorrectly with -O2, which results in +# incorrect answers. + +if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU") + execute_process( + COMMAND ${CMAKE_CXX_COMPILER} -dumpversion + OUTPUT_VARIABLE GCC_VERSION + OUTPUT_STRIP_TRAILING_WHITESPACE) + if(GCC_VERSION VERSION_EQUAL "4.5.1") + message(FATAL_ERROR + "GCC 4.5.1's optimizer is known to build MiniSat incorrectly " + "(and by extension CVC4).") + endif() +endif() + +#-----------------------------------------------------------------------------# # Check options, find packages and configure build. if(USE_PYTHON2) @@ -252,7 +270,8 @@ if(ENABLE_COVERAGE) add_definitions(-DCVC4_COVERAGE) setup_target_for_coverage_lcov( NAME coverage - EXECUTABLE ctest -j${CTEST_NTHREADS} $(ARGS) + EXECUTABLE + ctest -j${CTEST_NTHREADS} -LE "example" --output-on-failure $(ARGS) DEPENDENCIES cvc4-bin) endif() 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=<PATH> for custom build directory + cd <build_dir> # 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 `<build_dir>/bin`, the CVC4 library is built into +`<build_dir>/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 <example> # build examples/<subdir>/<example>.<ext> + ctest example/<subdir>/<example> # run test example/<subdir>/<example> + +All examples binaries are built into `<build_dir>/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 <regex> # run all tests with names matching <regex> + ctest -E <regex> # exclude tests with names matching <regex> + ctest -L <regex> # run all tests with labels matching <regex> + ctest -LE <regex> # exclude tests with labels matching <regex> + 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/` + `<subdir>/` + `<example>` (for `<example>` in +`example/<subdir>/`) 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 <system_test> # build test/system/<system_test>.<ext> + ctest system/<system_test> # run test/system/<system_test>.<ext> + +All system test binaries are built into `<build_dir>/bin/test/system`. + +We use prefix `system/` + `<system_test>` (for `<system_test>` 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 <unit_test> # build test/unit/<subdir>/<unit_test>.<ext> + ctest unit/<subdir>/<unit_test> # run test/unit/<subdir>/<unit_test>.<ext> + +All unit test binaries are built into `<build_dir>/bin/test/unit`. + +We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in +`test/unit/<subdir>`) 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/` + `<subdir>/` + `<regress_test>` (for `<regress_test>` +in level `N` in `test/regress/regressN/<subdir>`) 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/configure.sh b/configure.sh index 16764dd8a..0740ce396 100755 --- a/configure.sh +++ b/configure.sh @@ -50,7 +50,6 @@ The following options configure parameterized features. Optional Packages: The following flags enable optional packages (disable with --no-<option name>). --cln use CLN instead of GMP - --gmp use GMP instead of CLN --glpk use GLPK simplex solver --abc use the ABC AIG library --cadical use the CaDiCaL SAT solver 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 <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`. diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index 652fc4e5b..ef5191cb7 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -22,7 +22,13 @@ * Author: dejan */ +#include <boost/version.hpp> +#if BOOST_VERSION > 106700 +#include <boost/uuid/detail/sha1.hpp> +#else #include <boost/uuid/sha1.hpp> +#endif + #include <fstream> #include <iostream> #include <sstream> diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index cc5332cfd..e7b00068a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -808,8 +808,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap); os << " "; - ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); - + ProofManager::currentPM()->printTrustedTerm(*it, os, globalLetMap); os << "))"; os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; paren << "))"; @@ -832,9 +831,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, //TODO os << "(trust_f "; - if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << "(p_app "; - ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); - if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << ")"; + ProofManager::currentPM()->printTrustedTerm(*it, os, globalLetMap); os << ") "; os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; @@ -1063,5 +1060,13 @@ void ProofManager::printGlobalLetMap(std::set<Node>& atoms, void ProofManager::ensureLiteral(Node node) { d_cnfProof->ensureLiteral(node); } - +void ProofManager::printTrustedTerm(Node term, + std::ostream& os, + ProofLetMap& globalLetMap) +{ + TheoryProofEngine* tpe = ProofManager::currentPM()->getTheoryProofEngine(); + if (tpe->printsAsBool(term)) os << "(p_app "; + tpe->printTheoryTerm(term.toExpr(), os, globalLetMap); + if (tpe->printsAsBool(term)) os << ")"; +} } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 89aa66c2d..0342288fe 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -239,6 +239,12 @@ public: // for SMT variable names that have spaces and other things static std::string sanitize(TNode var); + // wrap term with (p_app ... ) if the term is printed as a boolean, and print + // used for "trust" assertions + static void printTrustedTerm(Node term, + std::ostream& os, + ProofLetMap& globalLetMap); + /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/ void addAssertion(Expr formula); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index a10ecc566..18e9619cb 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -482,7 +482,10 @@ void TermDbSygus::registerEnumerator(Node e, NodeManager* nm = NodeManager::currentNM(); if( mkActiveGuard ){ // make the guard - d_enum_to_active_guard[e] = nm->mkSkolem("eG", nm->booleanType()); + Node ag = nm->mkSkolem("eG", nm->booleanType()); + // must ensure it is a literal immediately here + ag = d_quantEngine->getValuation().ensureLiteral(ag); + d_enum_to_active_guard[e] = ag; } Trace("sygus-db") << " registering symmetry breaking clauses..." |