Andrew Reynolds [Thu, 27 Sep 2018 03:25:35 +0000 (22:25 -0500)]
Fix bug in getSymbols. (#2544)
Mathias Preiner [Thu, 27 Sep 2018 01:28:15 +0000 (18:28 -0700)]
cmake: Only print dumping warning if not disabled by user. (#2543)
Haniel Barbosa [Wed, 26 Sep 2018 23:13:29 +0000 (18:13 -0500)]
Makes SyGuS parsing more robust in invariant problems (#2509)
Mathias Preiner [Wed, 26 Sep 2018 22:34:58 +0000 (15:34 -0700)]
cmake: Fix test target dependency issues. (#2540)
Andrew Reynolds [Wed, 26 Sep 2018 21:50:51 +0000 (16:50 -0500)]
Enable quantified array regression. (#2539)
Andrew Reynolds [Wed, 26 Sep 2018 19:54:05 +0000 (14:54 -0500)]
Symmetry breaking for variable agnostic enumerators (#2527)
Aina Niemetz [Wed, 26 Sep 2018 04:59:28 +0000 (21:59 -0700)]
cmake: New INSTALL.md for build and testing instructions. (#2536)
Mathias Preiner [Wed, 26 Sep 2018 04:26:06 +0000 (21:26 -0700)]
cmake: Exclude examples for coverage target. (#2535)
Andrew Reynolds [Wed, 26 Sep 2018 03:50:20 +0000 (22:50 -0500)]
Eagerly ensure literal on active guards for sygus enumerators (#2531)
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)
Aina Niemetz [Wed, 26 Sep 2018 00:07:00 +0000 (17:07 -0700)]
examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)
Aina Niemetz [Tue, 25 Sep 2018 20:27:59 +0000 (13:27 -0700)]
cmake: configure.sh wrapper: Removed unused option --gmp.
yoni206 [Tue, 25 Sep 2018 19:52:04 +0000 (14:52 -0500)]
carefully printing trusted assertions in proofs (#2505)
Mathias Preiner [Tue, 25 Sep 2018 16:31:40 +0000 (09:31 -0700)]
cmake: Fix tag code generation dependencies. (#2529)
Andrew Reynolds [Tue, 25 Sep 2018 12:34:54 +0000 (07:34 -0500)]
Fix warnings uncovered by cmake build (#2521)
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
Andrew Reynolds [Tue, 25 Sep 2018 04:50:50 +0000 (23:50 -0500)]
Allow partial models for multiple sygus enumerators (#2499)
Andrew Reynolds [Tue, 25 Sep 2018 04:00:32 +0000 (23:00 -0500)]
Infrastructure for variable agnostic sygus enumerators (#2511)
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.