cvc5.git
6 years agoInfrastructure for variable agnostic sygus enumerators (#2511)
Andrew Reynolds [Tue, 25 Sep 2018 04:00:32 +0000 (23:00 -0500)]
Infrastructure for variable agnostic sygus enumerators (#2511)

6 years ago Improve non-linear check model error handling (#2497)
Andrew Reynolds [Tue, 25 Sep 2018 02:56:31 +0000 (21:56 -0500)]
 Improve non-linear check model error handling (#2497)

6 years agoRefactor strings equality rewriting (#2513)
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.

6 years agocmake: Fix dependencies for code generation. (#2524)
Mathias Preiner [Tue, 25 Sep 2018 01:42:32 +0000 (18:42 -0700)]
cmake: Fix dependencies for code generation. (#2524)

6 years agoFix wiki urls. (#2504)
Mathias Preiner [Tue, 25 Sep 2018 01:15:56 +0000 (18:15 -0700)]
Fix wiki urls. (#2504)

6 years agocmake: Fix git version info (again). (#2523)
Aina Niemetz [Tue, 25 Sep 2018 00:32:43 +0000 (17:32 -0700)]
cmake: Fix git version info (again). (#2523)

6 years agocmake: Fix theory order #2. (#2522)
Mathias Preiner [Mon, 24 Sep 2018 23:23:37 +0000 (16:23 -0700)]
cmake: Fix theory order #2. (#2522)

6 years agoUnify rewrites related to (str.contains x y) --> (= x y) (#2512)
Andres Noetzli [Mon, 24 Sep 2018 21:52:08 +0000 (14:52 -0700)]
Unify rewrites related to (str.contains x y) --> (= x y) (#2512)

6 years agocmake: Fix theory order. (#2518)
Mathias Preiner [Mon, 24 Sep 2018 20:14:13 +0000 (13:14 -0700)]
cmake: Fix theory order. (#2518)

6 years agoMake string rewriter unit tests more robust (#2520)
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.

6 years agocmake: Fix and simplify git version info. (#2516)
Aina Niemetz [Mon, 24 Sep 2018 19:21:14 +0000 (12:21 -0700)]
cmake: Fix and simplify git version info. (#2516)

6 years agocmake: Add program prefix option. (#2515)
Mathias Preiner [Mon, 24 Sep 2018 18:44:41 +0000 (11:44 -0700)]
cmake: Add program prefix option. (#2515)

6 years agoFix generating debug/trace tags.
Mathias Preiner [Mon, 24 Sep 2018 15:57:29 +0000 (08:57 -0700)]
Fix generating debug/trace tags.

6 years ago New C++ API: Add checks for Terms/OpTerms. (#2455)
Aina Niemetz [Sun, 23 Sep 2018 17:55:10 +0000 (10:55 -0700)]
 New C++ API: Add checks for Terms/OpTerms. (#2455)

6 years agoFix regress2. (#2502)
Andrew Reynolds [Sun, 23 Sep 2018 17:16:49 +0000 (12:16 -0500)]
Fix regress2. (#2502)

6 years agocmake: Add python3 option.
Mathias Preiner [Sat, 22 Sep 2018 09:02:01 +0000 (02:02 -0700)]
cmake: Add python3 option.

6 years agocmake: Enable -Wall.
Mathias Preiner [Sat, 22 Sep 2018 06:26:56 +0000 (23:26 -0700)]
cmake: Enable -Wall.

6 years agocmake: Fix systemtests dependency.
Mathias Preiner [Sat, 22 Sep 2018 01:40:18 +0000 (18:40 -0700)]
cmake: Fix systemtests dependency.

6 years agocmake: Build fully static binaries with option --static.
Mathias Preiner [Fri, 21 Sep 2018 23:27:26 +0000 (16:27 -0700)]
cmake: Build fully static binaries with option --static.

6 years agocmake: Run make coverage in parallel by default.
Mathias Preiner [Thu, 20 Sep 2018 23:32:27 +0000 (16:32 -0700)]
cmake: Run make coverage in parallel by default.

6 years agocmake: Add more documentation, some fixes and cleanup.
Mathias Preiner [Thu, 20 Sep 2018 20:31:45 +0000 (13:31 -0700)]
cmake: Add more documentation, some fixes and cleanup.

6 years agocmake: configure.sh wrapper: Use explicit build directory structure.
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.

6 years agocmake: configure wrapper: Modify next steps message after configuration.
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.

6 years agocmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup.
Mathias Preiner [Wed, 19 Sep 2018 17:21:54 +0000 (10:21 -0700)]
cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup.

6 years agocmake: Refactor cvc4_add_unit_test macro to support test names with '/'.
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.

6 years agocmake: Guard GetGitRevisionDescription.
Mathias Preiner [Wed, 19 Sep 2018 15:24:11 +0000 (08:24 -0700)]
cmake: Guard GetGitRevisionDescription.

6 years agocmake: Add target runexamples.
Aina Niemetz [Wed, 19 Sep 2018 00:57:56 +0000 (17:57 -0700)]
cmake: Add target runexamples.

6 years agocmake: Add support for cross-compiling for Windows.
Mathias Preiner [Wed, 19 Sep 2018 00:20:25 +0000 (17:20 -0700)]
cmake: Add support for cross-compiling for Windows.

6 years agocmake: Require JUnit version 4.
Mathias Preiner [Mon, 17 Sep 2018 23:32:18 +0000 (16:32 -0700)]
cmake: Require JUnit version 4.

6 years agocmake: Do not allow dumping with portfolio build.
Aina Niemetz [Mon, 17 Sep 2018 21:16:24 +0000 (14:16 -0700)]
cmake: Do not allow dumping with portfolio build.

6 years agocmake: More documentation, clean up.
Aina Niemetz [Mon, 17 Sep 2018 18:07:31 +0000 (11:07 -0700)]
cmake: More documentation, clean up.

6 years agocmake: Move extracting git information to src/base cmake config file.
Aina Niemetz [Mon, 17 Sep 2018 17:30:56 +0000 (10:30 -0700)]
cmake: Move extracting git information to src/base cmake config file.

6 years agocmake: Guard examples that require Boost.
Mathias Preiner [Sat, 15 Sep 2018 07:05:44 +0000 (00:05 -0700)]
cmake: Guard examples that require Boost.

6 years agocmake: Disable unit tests if assertions are not enabled.
Mathias Preiner [Sat, 15 Sep 2018 07:03:27 +0000 (00:03 -0700)]
cmake: Disable unit tests if assertions are not enabled.

6 years agocmake: FindANTLR: Check if antlr3FileStreamNew is available.
Mathias Preiner [Sat, 15 Sep 2018 00:23:30 +0000 (17:23 -0700)]
cmake: FindANTLR: Check if antlr3FileStreamNew is available.

6 years agocmake: configure.sh wrapper: Fixes for sh.
Mathias Preiner [Fri, 14 Sep 2018 23:00:23 +0000 (16:00 -0700)]
cmake: configure.sh wrapper: Fixes for sh.

6 years agotravis: Switch to cmake.
Mathias Preiner [Fri, 14 Sep 2018 22:08:46 +0000 (15:08 -0700)]
travis: Switch to cmake.

6 years agocmake: Do not build examples and unit and system tests by default.
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.

6 years agocmake: configure.sh wrapper: Add --name option.
Mathias Preiner [Fri, 14 Sep 2018 20:33:44 +0000 (13:33 -0700)]
cmake: configure.sh wrapper: Add --name option.

6 years agocmake: examples: Configure output directory per target.
Aina Niemetz [Fri, 14 Sep 2018 18:50:07 +0000 (11:50 -0700)]
cmake: examples: Configure output directory per target.

6 years agocmake: Added java examples
Aina Niemetz [Fri, 14 Sep 2018 18:24:15 +0000 (11:24 -0700)]
cmake: Added java examples

6 years agocmake: configure.sh wrapper: Add --prefix for install directory.
Mathias Preiner [Fri, 14 Sep 2018 17:25:49 +0000 (10:25 -0700)]
cmake: configure.sh wrapper: Add --prefix for install directory.

6 years agocmake: Add some more documentation, cleanup.
Mathias Preiner [Fri, 14 Sep 2018 00:48:04 +0000 (17:48 -0700)]
cmake: Add some more documentation, cleanup.

6 years agocmake: Move helper functions to cmake/Helpers.cmake.
Mathias Preiner [Fri, 14 Sep 2018 00:03:54 +0000 (17:03 -0700)]
cmake: Move helper functions to cmake/Helpers.cmake.

6 years agocmake: Added target examples (currently .cpp examples only)
Aina Niemetz [Thu, 13 Sep 2018 00:59:57 +0000 (17:59 -0700)]
cmake: Added target examples (currently .cpp examples only)

6 years agocmake: Simplify build type configuration.
Mathias Preiner [Wed, 12 Sep 2018 20:58:41 +0000 (13:58 -0700)]
cmake: Simplify build type configuration.

6 years agocmake: Refactor and clean up build profile printing.
Aina Niemetz [Wed, 12 Sep 2018 20:02:49 +0000 (13:02 -0700)]
cmake: Refactor and clean up build profile printing.

6 years agocmake: Added target check
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.

6 years agocmake: Add make install rule.
Mathias Preiner [Wed, 12 Sep 2018 18:10:01 +0000 (11:10 -0700)]
cmake: Add make install rule.

6 years agocmake: configure.sh wrapper: Fix handling of options with arguments.
Aina Niemetz [Tue, 11 Sep 2018 22:34:48 +0000 (15:34 -0700)]
cmake: configure.sh wrapper: Fix handling of options with arguments.

6 years agocmake: Add module finder for Valgrind.
Mathias Preiner [Tue, 11 Sep 2018 17:54:20 +0000 (10:54 -0700)]
cmake: Add module finder for Valgrind.

6 years agocmake: Various CMakeLists.txt fixes/cleanup.
Mathias Preiner [Tue, 11 Sep 2018 17:30:07 +0000 (10:30 -0700)]
cmake: Various CMakeLists.txt fixes/cleanup.

6 years agocmake: Only build libcvc4 and libcvc4parser as libraries.
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.

6 years agocmake: Move find_package to where it is actually needed.
Mathias Preiner [Mon, 10 Sep 2018 18:35:14 +0000 (11:35 -0700)]
cmake: Move find_package to where it is actually needed.

6 years agocmake: configure.sh wrapper: Removed env vars help text.
Aina Niemetz [Tue, 11 Sep 2018 16:11:41 +0000 (09:11 -0700)]
cmake: configure.sh wrapper: Removed env vars help text.

6 years agocmake: configure.sh wrapper: Configurable build directory
Aina Niemetz [Mon, 10 Sep 2018 16:30:35 +0000 (09:30 -0700)]
cmake: configure.sh wrapper: Configurable build directory

6 years agocmake: configure.sh wrapper: Create build dirs for configurations
Aina Niemetz [Fri, 7 Sep 2018 23:45:42 +0000 (16:45 -0700)]
cmake: configure.sh wrapper: Create build dirs for configurations

6 years agocmake: configure.sh wrapper: done (except: configurable build dir)
Aina Niemetz [Fri, 7 Sep 2018 21:14:56 +0000 (14:14 -0700)]
cmake: configure.sh wrapper: done (except: configurable build dir)

6 years agocmake: Updated and prettified configuration printing.
Aina Niemetz [Fri, 7 Sep 2018 21:13:44 +0000 (14:13 -0700)]
cmake: Updated and prettified configuration printing.

6 years agocmake: configure.sh wrapper: option parsing
Aina Niemetz [Fri, 7 Sep 2018 00:12:15 +0000 (17:12 -0700)]
cmake: configure.sh wrapper: option parsing

6 years agocmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
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.

6 years agocmake: Add ENABLE_BEST to enable best configuration of dependencies.
Aina Niemetz [Thu, 6 Sep 2018 22:35:55 +0000 (15:35 -0700)]
cmake: Add ENABLE_BEST to enable best configuration of dependencies.

6 years agocmake: Add Java runtime as required dependency (required for ANTLR).
Mathias Preiner [Thu, 6 Sep 2018 23:46:37 +0000 (16:46 -0700)]
cmake: Add Java runtime as required dependency (required for ANTLR).

6 years agocmake: Add convenience wrappers for tag generation.
Mathias Preiner [Thu, 6 Sep 2018 23:16:51 +0000 (16:16 -0700)]
cmake: Add convenience wrappers for tag generation.

6 years agocmake: Add library versioning for libcvc4.so.
Mathias Preiner [Thu, 6 Sep 2018 16:18:07 +0000 (09:18 -0700)]
cmake: Add library versioning for libcvc4.so.

6 years agocmake: Rebase with current master, add new tests/source files.
Mathias Preiner [Wed, 5 Sep 2018 21:00:52 +0000 (14:00 -0700)]
cmake: Rebase with current master, add new tests/source files.

6 years agocmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.
Mathias Preiner [Tue, 4 Sep 2018 18:40:46 +0000 (11:40 -0700)]
cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.

6 years agocmake: Use target specific includes for libcvc4.
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(...).

6 years agocmake: Add missing dependency.
Mathias Preiner [Fri, 31 Aug 2018 16:10:50 +0000 (09:10 -0700)]
cmake: Add missing dependency.

6 years agocmake: Add support for building static binaries/libraries.
Mathias Preiner [Wed, 29 Aug 2018 17:26:10 +0000 (10:26 -0700)]
cmake: Add support for building static binaries/libraries.

6 years agocmake: Add options for specifying install directories for dependencies.
Mathias Preiner [Wed, 29 Aug 2018 15:20:31 +0000 (08:20 -0700)]
cmake: Add options for specifying install directories for dependencies.

6 years agocmake: Add module finder for GLPK-cut-log.
Mathias Preiner [Sat, 25 Aug 2018 06:14:32 +0000 (23:14 -0700)]
cmake: Add module finder for GLPK-cut-log.

6 years agocmake: Add module finder for ABC.
Mathias Preiner [Sat, 25 Aug 2018 02:27:37 +0000 (19:27 -0700)]
cmake: Add module finder for ABC.

6 years agocmake: Compile Java tests and add to ctest if Java bindings are enabled.
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.

6 years agocmake: Add SWIG support + Python and Java bindings.
Mathias Preiner [Fri, 24 Aug 2018 19:52:49 +0000 (12:52 -0700)]
cmake: Add SWIG support + Python and Java bindings.

6 years agocmake: Add dependencies for test targets and support for make coverage.
Aina Niemetz [Wed, 22 Aug 2018 15:46:50 +0000 (08:46 -0700)]
cmake: Add dependencies for test targets and support for make coverage.

6 years agocmake: Various portfolio/default option fixes.
Mathias Preiner [Tue, 21 Aug 2018 02:39:32 +0000 (19:39 -0700)]
cmake: Various portfolio/default option fixes.

6 years agocmake: Enable parallel execution for test targets regress, units, systemtests.
Aina Niemetz [Tue, 21 Aug 2018 01:40:27 +0000 (18:40 -0700)]
cmake: Enable parallel execution for test targets regress, units, systemtests.

6 years agocmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.
Aina Niemetz [Tue, 21 Aug 2018 01:39:10 +0000 (18:39 -0700)]
cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.

6 years agocmake: Added system tests and target make systemtests.
Aina Niemetz [Tue, 21 Aug 2018 00:26:56 +0000 (17:26 -0700)]
cmake: Added system tests and target make systemtests.

6 years agocmake: Added regression tests and target make regress.
Aina Niemetz [Sat, 18 Aug 2018 01:25:27 +0000 (18:25 -0700)]
cmake: Added regression tests and target make regress.

6 years agocmake: Add portfolio support.
Mathias Preiner [Sat, 18 Aug 2018 01:11:26 +0000 (18:11 -0700)]
cmake: Add portfolio support.

6 years agocmake: Add ASAN support.
Mathias Preiner [Fri, 17 Aug 2018 23:59:09 +0000 (16:59 -0700)]
cmake: Add ASAN support.

6 years agocmake: Enable shared by default.
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.

6 years agocmake: Disable W-suggest-override for unit tests.
Mathias Preiner [Fri, 17 Aug 2018 23:57:20 +0000 (16:57 -0700)]
cmake: Disable W-suggest-override for unit tests.

6 years agocmake: Add target units.
Aina Niemetz [Fri, 17 Aug 2018 18:37:27 +0000 (11:37 -0700)]
cmake: Add target units.

6 years agocmake: Removed obsolete CMakeLists file in test.
Aina Niemetz [Fri, 17 Aug 2018 18:12:57 +0000 (11:12 -0700)]
cmake: Removed obsolete CMakeLists file in test.

6 years agocmake: Add support for CxxTest.
Aina Niemetz [Fri, 17 Aug 2018 01:56:03 +0000 (18:56 -0700)]
cmake: Add support for CxxTest.

6 years agocmake: Filter through and disable unused HAVE_* variables from autotools.
Aina Niemetz [Thu, 16 Aug 2018 22:55:25 +0000 (15:55 -0700)]
cmake: Filter through and disable unused HAVE_* variables from autotools.

6 years agocmake: Do not set global output directories for binaries and libraries.
Mathias Preiner [Fri, 17 Aug 2018 01:07:59 +0000 (18:07 -0700)]
cmake: Do not set global output directories for binaries and libraries.

6 years agocmake: Fix some includes.
Mathias Preiner [Fri, 17 Aug 2018 00:57:55 +0000 (17:57 -0700)]
cmake: Fix some includes.

6 years agocmake: Added support for coverage and profiling.
Aina Niemetz [Wed, 15 Aug 2018 23:47:00 +0000 (16:47 -0700)]
cmake: Added support for coverage and profiling.

6 years agocmake: Added 3-valued option handling (to enable detection of user-set options).
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).

6 years agocmake: Add module finder for readline.
Mathias Preiner [Wed, 15 Aug 2018 19:53:43 +0000 (12:53 -0700)]
cmake: Add module finder for readline.

6 years agocmake: Generate token headers.
Mathias Preiner [Wed, 15 Aug 2018 00:43:17 +0000 (17:43 -0700)]
cmake: Generate token headers.

6 years agocmake: Added licensing options and warnings/errors.
Aina Niemetz [Wed, 15 Aug 2018 01:18:04 +0000 (18:18 -0700)]
cmake: Added licensing options and warnings/errors.

6 years agocmake: Cleanup CMakeLists.txt files, remove SHARED.
Mathias Preiner [Wed, 15 Aug 2018 00:32:26 +0000 (17:32 -0700)]
cmake: Cleanup CMakeLists.txt files, remove SHARED.

6 years agocmake: Add build configurations.
Aina Niemetz [Tue, 14 Aug 2018 20:22:15 +0000 (13:22 -0700)]
cmake: Add build configurations.

6 years agocmake: Fixed compiler flag macros.
Aina Niemetz [Mon, 13 Aug 2018 22:22:07 +0000 (15:22 -0700)]
cmake: Fixed compiler flag macros.

6 years agocmake: Add module finder for LFSC.
Mathias Preiner [Tue, 14 Aug 2018 00:49:47 +0000 (17:49 -0700)]
cmake: Add module finder for LFSC.