| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-10 | Add length-based rewrites for (str.substr _ _ _)substrsubstr | Andres Noetzli | |
| This commit adds two rewrites for `(str.substr _ _ _)` that use length-based reasoning: - `(str.substr (str.substr x a b) c d) ---> ""` if `c >= b` - `(str.substr s x x) ---> ""` if `(str.len s) <= 1` | |||
| 2018-10-09 | Support for basic actively-generated enumerators (#2606) | Andrew Reynolds | |
| 2018-10-08 | BV instantiator: Factor out util functions. (#2604) | Aina Niemetz | |
| Previously, all util functions for the BV instantiator were static functions in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h). Asan reported errors for the corresponing unit test because of this. | |||
| 2018-10-08 | BV inverter: Factor out util functions. (#2603) | Aina Niemetz | |
| Previously, all invertibility condition functions were static functions in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/bv_inverter_utils.(cpp|h). | |||
| 2018-10-08 | Address slow sygus regressions (#2598) | Andrew Reynolds | |
| 2018-10-05 | Fix cache for sygus post-condition inference (#2592) | Andrew Reynolds | |
| 2018-10-05 | Update default options for sygus (#2586) | Andrew Reynolds | |
| 2018-10-04 | New C++ API: Add checks for Sorts. (#2519) | Aina Niemetz | |
| 2018-10-04 | Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590) | Andres Noetzli | |
| With older versions of CMake, skipped tests are reported as failures, which is undesirable. This commit changes the CMakeLists file to only use the `SKIP_RETURN_CODE` property if a newer version of CMake is used. | |||
| 2018-10-04 | Fix end constraint for regexp elimination (#2571) | Andrew Reynolds | |
| 2018-10-03 | Fix regress (#2575) | Andrew Reynolds | |
| 2018-10-03 | Fix stale op list in sets (#2572) | Andrew Reynolds | |
| 2018-10-03 | Eliminate partial operators within lambdas during grammar normalization (#2570) | Andrew Reynolds | |
| 2018-10-02 | cmake: Display skipped tests as not run (#2567) | Andres Noetzli | |
| Currently, the run_regression.py script just returns 0 when we skip a test due to a feature not supported by the current configuration. Returning 0 marks those tests as passed. To make it more clear which tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property to the regression tests and changes the regression script to return 77 for skipped tests. The feature is supported since at least CMake 3.0 [0]. For backwards compatibility with autotools, returning 77 for skipped tests is only active when `--cmake` is passed to the run_regression.py script. [0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html | |||
| 2018-10-02 | Allow (_ to_fp ...) in strict parsing mode (#2566) | Andres Noetzli | |
| When parsing with `--strict-parsing`, we are checking whether the operators that we encounter have been explicitly added to the `d_logicOperators` set in the `Parser` class. We did not do that for the indexed operator `(_ to_fp ...)` (which is represented by the kind `FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator. | |||
| 2018-10-02 | unit: Fix ASAN detection for GCC. (#2561) | Mathias Preiner | |
| 2018-10-02 | cmake: Add examples to build-tests, add warning for disabling static build. ↵ | Mathias Preiner | |
| (#2562) | |||
| 2018-10-02 | Fix "catching polymorphic type by value" warnings (#2556) | Andres Noetzli | |
| When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make sure that we use a reference type for the exception, otherwise the unit test tries to catch the exception by value, resulting in "catching polymorphic type by value" warnings. | |||
| 2018-10-01 | cmake: Add build target build-tests to build all test dependencies. (#2558) | Mathias Preiner | |
| 2018-09-30 | Add rewrite for solving stoi (#2532) | Andrew Reynolds | |
| 2018-09-28 | Rewrites for (= "" _) and (= (str.replace _) _) (#2546) | Andres Noetzli | |
| 2018-09-28 | cmake: Only do Java tests when unit testing on (#2551) | Andres Noetzli | |
| 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. | |||
| 2018-09-27 | cmake: Add CxxTest finder module to allow custom paths. (#2542) | Mathias Preiner | |
| 2018-09-27 | Fix Taylor overapproximation for large exponentials (#2538) | Andrew Reynolds | |
| 2018-09-26 | Fix homogeneous string constant rewrite (#2545) | Andrew Reynolds | |
| 2018-09-26 | Makes SyGuS parsing more robust in invariant problems (#2509) | Haniel Barbosa | |
| 2018-09-26 | cmake: Fix test target dependency issues. (#2540) | Mathias Preiner | |
| 2018-09-26 | Enable quantified array regression. (#2539) | Andrew Reynolds | |
| 2018-09-24 | Fix quantifiers selector over store rewrite (#2510) | Andrew Reynolds | |
| 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 | |||
| 2018-09-24 | Unify rewrites related to (str.contains x y) --> (= x y) (#2512) | Andres Noetzli | |
| 2018-09-24 | Make string rewriter unit tests more robust (#2520) | Andres Noetzli | |
| 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. | |||
| 2018-09-23 | Fix regress2. (#2502) | Andrew Reynolds | |
| 2018-09-22 | cmake: Fix systemtests dependency. | Mathias Preiner | |
| 2018-09-22 | cmake: Run make coverage in parallel by default. | Mathias Preiner | |
| 2018-09-22 | cmake: Refactor cvc4_add_unit_test macro to support test names with '/'. | Aina Niemetz | |
| 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. | |||
| 2018-09-22 | cmake: Require JUnit version 4. | Mathias Preiner | |
| 2018-09-22 | cmake: More documentation, clean up. | Aina Niemetz | |
| 2018-09-22 | cmake: Disable unit tests if assertions are not enabled. | Mathias Preiner | |
| 2018-09-22 | cmake: Do not build examples and unit and system tests by default. | Aina Niemetz | |
| 2018-09-22 | cmake: Added target check | Aina Niemetz | |
| 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. | |||
| 2018-09-22 | cmake: Only build libcvc4 and libcvc4parser as libraries. | Mathias Preiner | |
| 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. | |||
| 2018-09-22 | cmake: Rebase with current master, add new tests/source files. | Mathias Preiner | |
| 2018-09-22 | cmake: Compile Java tests and add to ctest if Java bindings are enabled. | Mathias Preiner | |
| 2018-09-22 | cmake: Add dependencies for test targets and support for make coverage. | Aina Niemetz | |
| 2018-09-22 | cmake: Enable parallel execution for test targets regress, units, systemtests. | Aina Niemetz | |
| 2018-09-22 | cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON. | Aina Niemetz | |
| 2018-09-22 | cmake: Added system tests and target make systemtests. | Aina Niemetz | |
| 2018-09-22 | cmake: Added regression tests and target make regress. | Aina Niemetz | |
| 2018-09-22 | cmake: Disable W-suggest-override for unit tests. | Mathias Preiner | |
| 2018-09-22 | cmake: Add target units. | Aina Niemetz | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback