Andrew Reynolds [Tue, 25 Sep 2018 02:56:31 +0000 (21:56 -0500)]
Improve non-linear check model error handling (#2497)
Andrew Reynolds [Tue, 25 Sep 2018 02:28:31 +0000 (21:28 -0500)]
Refactor strings equality rewriting (#2513)
This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter.
Mathias Preiner [Tue, 25 Sep 2018 01:42:32 +0000 (18:42 -0700)]
cmake: Fix dependencies for code generation. (#2524)
Mathias Preiner [Tue, 25 Sep 2018 01:15:56 +0000 (18:15 -0700)]
Fix wiki urls. (#2504)
Aina Niemetz [Tue, 25 Sep 2018 00:32:43 +0000 (17:32 -0700)]
cmake: Fix git version info (again). (#2523)
Mathias Preiner [Mon, 24 Sep 2018 23:23:37 +0000 (16:23 -0700)]
cmake: Fix theory order #2. (#2522)
Andres Noetzli [Mon, 24 Sep 2018 21:52:08 +0000 (14:52 -0700)]
Unify rewrites related to (str.contains x y) --> (= x y) (#2512)
Mathias Preiner [Mon, 24 Sep 2018 20:14:13 +0000 (13:14 -0700)]
cmake: Fix theory order. (#2518)
Andres Noetzli [Mon, 24 Sep 2018 19:48:56 +0000 (12:48 -0700)]
Make string rewriter unit tests more robust (#2520)
This commit changes the unit test for the string rewriter to use the
extended rewriter instead of the regular rewriter to make it more
robust, e.g. to different orderings in conjunctions.
Aina Niemetz [Mon, 24 Sep 2018 19:21:14 +0000 (12:21 -0700)]
cmake: Fix and simplify git version info. (#2516)
Mathias Preiner [Mon, 24 Sep 2018 18:44:41 +0000 (11:44 -0700)]
cmake: Add program prefix option. (#2515)
Mathias Preiner [Mon, 24 Sep 2018 15:57:29 +0000 (08:57 -0700)]
Fix generating debug/trace tags.
Aina Niemetz [Sun, 23 Sep 2018 17:55:10 +0000 (10:55 -0700)]
New C++ API: Add checks for Terms/OpTerms. (#2455)
Andrew Reynolds [Sun, 23 Sep 2018 17:16:49 +0000 (12:16 -0500)]
Fix regress2. (#2502)
Mathias Preiner [Sat, 22 Sep 2018 09:02:01 +0000 (02:02 -0700)]
cmake: Add python3 option.
Mathias Preiner [Sat, 22 Sep 2018 06:26:56 +0000 (23:26 -0700)]
cmake: Enable -Wall.
Mathias Preiner [Sat, 22 Sep 2018 01:40:18 +0000 (18:40 -0700)]
cmake: Fix systemtests dependency.
Mathias Preiner [Fri, 21 Sep 2018 23:27:26 +0000 (16:27 -0700)]
cmake: Build fully static binaries with option --static.
Mathias Preiner [Thu, 20 Sep 2018 23:32:27 +0000 (16:32 -0700)]
cmake: Run make coverage in parallel by default.
Mathias Preiner [Thu, 20 Sep 2018 20:31:45 +0000 (13:31 -0700)]
cmake: Add more documentation, some fixes and cleanup.
Aina Niemetz [Thu, 20 Sep 2018 19:30:30 +0000 (12:30 -0700)]
cmake: configure.sh wrapper: Use explicit build directory structure.
We don't create build directories for every build type (and
configuration) anymore. The default build directory is now 'build'
(created where you call the wrapper script from). Option --name allows
to configure an individual name (and path) for the build directory.
Mathias Preiner [Wed, 19 Sep 2018 23:36:22 +0000 (16:36 -0700)]
cmake: configure wrapper: Modify next steps message after configuration.
Since configure.sh is only a wrapper for cmake it prints all the messages from
cmake. At the end we print the next steps after configuration. If configure.sh
is used we add the info to also change into the build directory before calling
make.
Mathias Preiner [Wed, 19 Sep 2018 17:21:54 +0000 (10:21 -0700)]
cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup.
Aina Niemetz [Wed, 19 Sep 2018 16:21:31 +0000 (09:21 -0700)]
cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
Mathias Preiner [Wed, 19 Sep 2018 15:24:11 +0000 (08:24 -0700)]
cmake: Guard GetGitRevisionDescription.
Aina Niemetz [Wed, 19 Sep 2018 00:57:56 +0000 (17:57 -0700)]
cmake: Add target runexamples.
Mathias Preiner [Wed, 19 Sep 2018 00:20:25 +0000 (17:20 -0700)]
cmake: Add support for cross-compiling for Windows.
Mathias Preiner [Mon, 17 Sep 2018 23:32:18 +0000 (16:32 -0700)]
cmake: Require JUnit version 4.
Aina Niemetz [Mon, 17 Sep 2018 21:16:24 +0000 (14:16 -0700)]
cmake: Do not allow dumping with portfolio build.
Aina Niemetz [Mon, 17 Sep 2018 18:07:31 +0000 (11:07 -0700)]
cmake: More documentation, clean up.
Aina Niemetz [Mon, 17 Sep 2018 17:30:56 +0000 (10:30 -0700)]
cmake: Move extracting git information to src/base cmake config file.
Mathias Preiner [Sat, 15 Sep 2018 07:05:44 +0000 (00:05 -0700)]
cmake: Guard examples that require Boost.
Mathias Preiner [Sat, 15 Sep 2018 07:03:27 +0000 (00:03 -0700)]
cmake: Disable unit tests if assertions are not enabled.
Mathias Preiner [Sat, 15 Sep 2018 00:23:30 +0000 (17:23 -0700)]
cmake: FindANTLR: Check if antlr3FileStreamNew is available.
Mathias Preiner [Fri, 14 Sep 2018 23:00:23 +0000 (16:00 -0700)]
cmake: configure.sh wrapper: Fixes for sh.
Mathias Preiner [Fri, 14 Sep 2018 22:08:46 +0000 (15:08 -0700)]
travis: Switch to cmake.
Aina Niemetz [Fri, 14 Sep 2018 21:21:35 +0000 (14:21 -0700)]
cmake: Do not build examples and unit and system tests by default.
Mathias Preiner [Fri, 14 Sep 2018 20:33:44 +0000 (13:33 -0700)]
cmake: configure.sh wrapper: Add --name option.
Aina Niemetz [Fri, 14 Sep 2018 18:50:07 +0000 (11:50 -0700)]
cmake: examples: Configure output directory per target.
Aina Niemetz [Fri, 14 Sep 2018 18:24:15 +0000 (11:24 -0700)]
cmake: Added java examples
Mathias Preiner [Fri, 14 Sep 2018 17:25:49 +0000 (10:25 -0700)]
cmake: configure.sh wrapper: Add --prefix for install directory.
Mathias Preiner [Fri, 14 Sep 2018 00:48:04 +0000 (17:48 -0700)]
cmake: Add some more documentation, cleanup.
Mathias Preiner [Fri, 14 Sep 2018 00:03:54 +0000 (17:03 -0700)]
cmake: Move helper functions to cmake/Helpers.cmake.
Aina Niemetz [Thu, 13 Sep 2018 00:59:57 +0000 (17:59 -0700)]
cmake: Added target examples (currently .cpp examples only)
Mathias Preiner [Wed, 12 Sep 2018 20:58:41 +0000 (13:58 -0700)]
cmake: Simplify build type configuration.
Aina Niemetz [Wed, 12 Sep 2018 20:02:49 +0000 (13:02 -0700)]
cmake: Refactor and clean up build profile printing.
Aina Niemetz [Wed, 12 Sep 2018 16:15:04 +0000 (09:15 -0700)]
cmake: Added target check
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
Mathias Preiner [Wed, 12 Sep 2018 18:10:01 +0000 (11:10 -0700)]
cmake: Add make install rule.
Aina Niemetz [Tue, 11 Sep 2018 22:34:48 +0000 (15:34 -0700)]
cmake: configure.sh wrapper: Fix handling of options with arguments.
Mathias Preiner [Tue, 11 Sep 2018 17:54:20 +0000 (10:54 -0700)]
cmake: Add module finder for Valgrind.
Mathias Preiner [Tue, 11 Sep 2018 17:30:07 +0000 (10:30 -0700)]
cmake: Various CMakeLists.txt fixes/cleanup.
Mathias Preiner [Wed, 12 Sep 2018 07:08:19 +0000 (00:08 -0700)]
cmake: Only build libcvc4 and libcvc4parser as libraries.
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
Mathias Preiner [Mon, 10 Sep 2018 18:35:14 +0000 (11:35 -0700)]
cmake: Move find_package to where it is actually needed.
Aina Niemetz [Tue, 11 Sep 2018 16:11:41 +0000 (09:11 -0700)]
cmake: configure.sh wrapper: Removed env vars help text.
Aina Niemetz [Mon, 10 Sep 2018 16:30:35 +0000 (09:30 -0700)]
cmake: configure.sh wrapper: Configurable build directory
Aina Niemetz [Fri, 7 Sep 2018 23:45:42 +0000 (16:45 -0700)]
cmake: configure.sh wrapper: Create build dirs for configurations
Aina Niemetz [Fri, 7 Sep 2018 21:14:56 +0000 (14:14 -0700)]
cmake: configure.sh wrapper: done (except: configurable build dir)
Aina Niemetz [Fri, 7 Sep 2018 21:13:44 +0000 (14:13 -0700)]
cmake: Updated and prettified configuration printing.
Aina Niemetz [Fri, 7 Sep 2018 00:12:15 +0000 (17:12 -0700)]
cmake: configure.sh wrapper: option parsing
Aina Niemetz [Thu, 6 Sep 2018 22:53:13 +0000 (15:53 -0700)]
cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
Aina Niemetz [Thu, 6 Sep 2018 22:35:55 +0000 (15:35 -0700)]
cmake: Add ENABLE_BEST to enable best configuration of dependencies.
Mathias Preiner [Thu, 6 Sep 2018 23:46:37 +0000 (16:46 -0700)]
cmake: Add Java runtime as required dependency (required for ANTLR).
Mathias Preiner [Thu, 6 Sep 2018 23:16:51 +0000 (16:16 -0700)]
cmake: Add convenience wrappers for tag generation.
Mathias Preiner [Thu, 6 Sep 2018 16:18:07 +0000 (09:18 -0700)]
cmake: Add library versioning for libcvc4.so.
Mathias Preiner [Wed, 5 Sep 2018 21:00:52 +0000 (14:00 -0700)]
cmake: Rebase with current master, add new tests/source files.
Mathias Preiner [Tue, 4 Sep 2018 18:40:46 +0000 (11:40 -0700)]
cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.
Mathias Preiner [Fri, 31 Aug 2018 16:11:23 +0000 (09:11 -0700)]
cmake: Use target specific includes for libcvc4.
Further, print definitions added with add_definitions(...).
Mathias Preiner [Fri, 31 Aug 2018 16:10:50 +0000 (09:10 -0700)]
cmake: Add missing dependency.
Mathias Preiner [Wed, 29 Aug 2018 17:26:10 +0000 (10:26 -0700)]
cmake: Add support for building static binaries/libraries.
Mathias Preiner [Wed, 29 Aug 2018 15:20:31 +0000 (08:20 -0700)]
cmake: Add options for specifying install directories for dependencies.
Mathias Preiner [Sat, 25 Aug 2018 06:14:32 +0000 (23:14 -0700)]
cmake: Add module finder for GLPK-cut-log.
Mathias Preiner [Sat, 25 Aug 2018 02:27:37 +0000 (19:27 -0700)]
cmake: Add module finder for ABC.
Mathias Preiner [Fri, 24 Aug 2018 22:11:03 +0000 (15:11 -0700)]
cmake: Compile Java tests and add to ctest if Java bindings are enabled.
Mathias Preiner [Fri, 24 Aug 2018 19:52:49 +0000 (12:52 -0700)]
cmake: Add SWIG support + Python and Java bindings.
Aina Niemetz [Wed, 22 Aug 2018 15:46:50 +0000 (08:46 -0700)]
cmake: Add dependencies for test targets and support for make coverage.
Mathias Preiner [Tue, 21 Aug 2018 02:39:32 +0000 (19:39 -0700)]
cmake: Various portfolio/default option fixes.
Aina Niemetz [Tue, 21 Aug 2018 01:40:27 +0000 (18:40 -0700)]
cmake: Enable parallel execution for test targets regress, units, systemtests.
Aina Niemetz [Tue, 21 Aug 2018 01:39:10 +0000 (18:39 -0700)]
cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.
Aina Niemetz [Tue, 21 Aug 2018 00:26:56 +0000 (17:26 -0700)]
cmake: Added system tests and target make systemtests.
Aina Niemetz [Sat, 18 Aug 2018 01:25:27 +0000 (18:25 -0700)]
cmake: Added regression tests and target make regress.
Mathias Preiner [Sat, 18 Aug 2018 01:11:26 +0000 (18:11 -0700)]
cmake: Add portfolio support.
Mathias Preiner [Fri, 17 Aug 2018 23:59:09 +0000 (16:59 -0700)]
cmake: Add ASAN support.
Mathias Preiner [Fri, 17 Aug 2018 23:58:27 +0000 (16:58 -0700)]
cmake: Enable shared by default.
Further, force shared builds in case of unit tests.
Mathias Preiner [Fri, 17 Aug 2018 23:57:20 +0000 (16:57 -0700)]
cmake: Disable W-suggest-override for unit tests.
Aina Niemetz [Fri, 17 Aug 2018 18:37:27 +0000 (11:37 -0700)]
cmake: Add target units.
Aina Niemetz [Fri, 17 Aug 2018 18:12:57 +0000 (11:12 -0700)]
cmake: Removed obsolete CMakeLists file in test.
Aina Niemetz [Fri, 17 Aug 2018 01:56:03 +0000 (18:56 -0700)]
cmake: Add support for CxxTest.
Aina Niemetz [Thu, 16 Aug 2018 22:55:25 +0000 (15:55 -0700)]
cmake: Filter through and disable unused HAVE_* variables from autotools.
Mathias Preiner [Fri, 17 Aug 2018 01:07:59 +0000 (18:07 -0700)]
cmake: Do not set global output directories for binaries and libraries.
Mathias Preiner [Fri, 17 Aug 2018 00:57:55 +0000 (17:57 -0700)]
cmake: Fix some includes.
Aina Niemetz [Wed, 15 Aug 2018 23:47:00 +0000 (16:47 -0700)]
cmake: Added support for coverage and profiling.
Aina Niemetz [Wed, 15 Aug 2018 21:00:33 +0000 (14:00 -0700)]
cmake: Added 3-valued option handling (to enable detection of user-set options).
Mathias Preiner [Wed, 15 Aug 2018 19:53:43 +0000 (12:53 -0700)]
cmake: Add module finder for readline.
Mathias Preiner [Wed, 15 Aug 2018 00:43:17 +0000 (17:43 -0700)]
cmake: Generate token headers.
Aina Niemetz [Wed, 15 Aug 2018 01:18:04 +0000 (18:18 -0700)]
cmake: Added licensing options and warnings/errors.
Mathias Preiner [Wed, 15 Aug 2018 00:32:26 +0000 (17:32 -0700)]
cmake: Cleanup CMakeLists.txt files, remove SHARED.
Aina Niemetz [Tue, 14 Aug 2018 20:22:15 +0000 (13:22 -0700)]
cmake: Add build configurations.
Aina Niemetz [Mon, 13 Aug 2018 22:22:07 +0000 (15:22 -0700)]
cmake: Fixed compiler flag macros.
Mathias Preiner [Tue, 14 Aug 2018 00:49:47 +0000 (17:49 -0700)]
cmake: Add module finder for LFSC.
Mathias Preiner [Tue, 14 Aug 2018 00:37:24 +0000 (17:37 -0700)]
cmake: Add module finder for CaDiCaL.