cvc5.git
6 years agocmake: Only do Java tests when unit testing on (#2551)
Andres Noetzli [Fri, 28 Sep 2018 15:21:32 +0000 (08:21 -0700)]
cmake: Only do Java tests when unit testing on (#2551)

Right now, we are adding the Java tests even when we are not building
unit tests. This commit changes the build system to only add the Java
tests when unit tests are enabled. There are two reasons for this
change:

- building a production version of CVC4 should not require JUnit
- it seems more intuitive (to me at least) to disable JUnit tests when
  unit tests are disabled

This change also simplifies building the Java bindings in our homebrew
formula.

6 years agocmake: Add CxxTest finder module to allow custom paths. (#2542)
Mathias Preiner [Fri, 28 Sep 2018 02:47:25 +0000 (19:47 -0700)]
cmake: Add CxxTest finder module to allow custom paths. (#2542)

6 years agoRemove assertion. (#2549)
Andrew Reynolds [Thu, 27 Sep 2018 19:40:06 +0000 (14:40 -0500)]
Remove assertion. (#2549)

6 years agoInfrastructure for using active enumerators in sygus modules (#2547)
Andrew Reynolds [Thu, 27 Sep 2018 18:57:17 +0000 (13:57 -0500)]
Infrastructure for using active enumerators in sygus modules (#2547)

6 years agoIncorporate all unification enumerators into getTermList. (#2541)
Andrew Reynolds [Thu, 27 Sep 2018 12:09:18 +0000 (07:09 -0500)]
Incorporate all unification enumerators into getTermList. (#2541)

6 years agoFix Taylor overapproximation for large exponentials (#2538)
Andrew Reynolds [Thu, 27 Sep 2018 05:36:24 +0000 (00:36 -0500)]
Fix Taylor overapproximation for large exponentials (#2538)

6 years ago Fix homogeneous string constant rewrite (#2545)
Andrew Reynolds [Thu, 27 Sep 2018 04:25:14 +0000 (23:25 -0500)]
 Fix homogeneous string constant rewrite (#2545)

6 years agoFix bug in getSymbols. (#2544)
Andrew Reynolds [Thu, 27 Sep 2018 03:25:35 +0000 (22:25 -0500)]
Fix bug in getSymbols. (#2544)

6 years agocmake: Only print dumping warning if not disabled by user. (#2543)
Mathias Preiner [Thu, 27 Sep 2018 01:28:15 +0000 (18:28 -0700)]
cmake: Only print dumping warning if not disabled by user. (#2543)

6 years agoMakes SyGuS parsing more robust in invariant problems (#2509)
Haniel Barbosa [Wed, 26 Sep 2018 23:13:29 +0000 (18:13 -0500)]
Makes SyGuS parsing more robust in invariant problems (#2509)

6 years agocmake: Fix test target dependency issues. (#2540)
Mathias Preiner [Wed, 26 Sep 2018 22:34:58 +0000 (15:34 -0700)]
cmake: Fix test target dependency issues. (#2540)

6 years agoEnable quantified array regression. (#2539)
Andrew Reynolds [Wed, 26 Sep 2018 21:50:51 +0000 (16:50 -0500)]
Enable quantified array regression. (#2539)

6 years agoSymmetry breaking for variable agnostic enumerators (#2527)
Andrew Reynolds [Wed, 26 Sep 2018 19:54:05 +0000 (14:54 -0500)]
Symmetry breaking for variable agnostic enumerators (#2527)

6 years agocmake: New INSTALL.md for build and testing instructions. (#2536)
Aina Niemetz [Wed, 26 Sep 2018 04:59:28 +0000 (21:59 -0700)]
cmake: New INSTALL.md for build and testing instructions. (#2536)

6 years agocmake: Exclude examples for coverage target. (#2535)
Mathias Preiner [Wed, 26 Sep 2018 04:26:06 +0000 (21:26 -0700)]
cmake: Exclude examples for coverage target. (#2535)

6 years agoEagerly ensure literal on active guards for sygus enumerators (#2531)
Andrew Reynolds [Wed, 26 Sep 2018 03:50:20 +0000 (22:50 -0500)]
Eagerly ensure literal on active guards for sygus enumerators (#2531)

6 years agocmake: Add check for GCC 4.5.1 and warn user. (#2533)
Mathias Preiner [Wed, 26 Sep 2018 00:33:48 +0000 (17:33 -0700)]
cmake: Add check for GCC 4.5.1 and warn user. (#2533)

6 years agoexamples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)
Aina Niemetz [Wed, 26 Sep 2018 00:07:00 +0000 (17:07 -0700)]
examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)

6 years agocmake: configure.sh wrapper: Removed unused option --gmp.
Aina Niemetz [Tue, 25 Sep 2018 20:27:59 +0000 (13:27 -0700)]
cmake: configure.sh wrapper: Removed unused option --gmp.

6 years agocarefully printing trusted assertions in proofs (#2505)
yoni206 [Tue, 25 Sep 2018 19:52:04 +0000 (14:52 -0500)]
carefully printing trusted assertions in proofs (#2505)

6 years agocmake: Fix tag code generation dependencies. (#2529)
Mathias Preiner [Tue, 25 Sep 2018 16:31:40 +0000 (09:31 -0700)]
cmake: Fix tag code generation dependencies. (#2529)

6 years agoFix warnings uncovered by cmake build (#2521)
Andrew Reynolds [Tue, 25 Sep 2018 12:34:54 +0000 (07:34 -0500)]
Fix warnings uncovered by cmake build (#2521)

6 years agoFix quantifiers selector over store rewrite (#2510)
Andrew Reynolds [Tue, 25 Sep 2018 05:24:20 +0000 (00:24 -0500)]
Fix quantifiers selector over store rewrite (#2510)

Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.

After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581

6 years agoAllow partial models for multiple sygus enumerators (#2499)
Andrew Reynolds [Tue, 25 Sep 2018 04:50:50 +0000 (23:50 -0500)]
Allow partial models for multiple sygus enumerators (#2499)

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.