| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | New C++ API: Add checks for Sorts. (#2519) | Aina Niemetz | |
| 2018-10-04 | Infrastructure for string length entailments via approximations (#2514) | Andrew Reynolds | |
| 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-04 | Clean remaining references to getNextDecisionRequest and simplify (#2500) | Andrew Reynolds | |
| 2018-10-03 | Fix mem leak in sha1_collision example. (#2588) | Aina Niemetz | |
| 2018-10-03 | Fix mem leak in sets_translate example. (#2589) | Aina Niemetz | |
| 2018-10-03 | Simplify datatypes printing (#2573) | Andrew Reynolds | |
| 2018-10-03 | Fix compiler warnings. (#2585) | Aina Niemetz | |
| 2018-10-03 | Fix regress (#2575) | Andrew Reynolds | |
| 2018-10-03 | Add actively generated sygus enumerators (#2552) | Andrew Reynolds | |
| 2018-10-03 | Make CegisUnif with condition independent robust to var agnostic (#2565) | Haniel Barbosa | |
| 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 | Make registration of preprocessing passes explicit (#2564) | Andres Noetzli | |
| As it turns out, self-registering types are problematic with static linkage [0]. Instead of fixing the issue with linker flags, which seems possible but also brittle (e.g. the flags may be different for different linkers), this commit adds an explicit registration of each preprocessing pass. [0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html | |||
| 2018-10-02 | Fix documentation for `make regress`. (#2557) | Alex Ozdemir | |
| 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: Generate compile_commands.json on configure. (#2559) | Mathias Preiner | |
| 2018-10-01 | cmake: Add build target build-tests to build all test dependencies. (#2558) | Mathias Preiner | |
| 2018-10-01 | init scalar class members (coverity issues 1473720 and 1473721) (#2554) | Haniel Barbosa | |
| 2018-10-01 | Fix compiler warnings. (#2555) | Aina Niemetz | |
| 2018-10-01 | Fix dumping pre/post preprocessing passes (#2469) | Andres Noetzli | |
| This commit changes the hard-coded list of checks for preprocessing-related dump tags to take advantage of the new preprocessing pass registration mechanism from PR #2468. It also fixes a typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()` and adds a list of available passes to the `--dump help` output. | |||
| 2018-10-01 | Refactor preprocessing pass registration (#2468) | Andres Noetzli | |
| This commit refactors how preprocessing pass registration works, inspired by LLVM's approach [0]. The basic idea is that every preprocessing pass declares a static variable of type `RegisterPass` in its source file that registers the pass with the `PreprocessingPassRegistry` when starting the program. The registry is a singleton that keeps track of all the available passes and allows other code to create instances of the passes (note: previously the registry itself was owning the passes but this is no longer the case). One of the advantages of this solution is that we have a list of available passes directly at the beginning of the program, which is useful for example when parsing options. As a side effect, this commit also fixes the SortInference pass, which was expecting arguments other than the preprocessing pass context in its constructor. This commit is required for fixing dumping pre/post preprocessing passes. It is also the ground work for allowing the user to specify a preprocessing pipeline using command-line arguments. [0] https://llvm.org/docs/WritingAnLLVMPass.html | |||
| 2018-09-30 | Add rewrite for solving stoi (#2532) | Andrew Reynolds | |
| 2018-09-29 | cmake: Ignore ctest exit code for coverage reports. | Mathias Preiner | |
| 2018-09-29 | Stream concrete values for variable agnostic enumerators (#2526) | Haniel Barbosa | |
| 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 | Remove assertion. (#2549) | Andrew Reynolds | |
| 2018-09-27 | Infrastructure for using active enumerators in sygus modules (#2547) | Andrew Reynolds | |
| 2018-09-27 | Incorporate all unification enumerators into getTermList. (#2541) | Andrew Reynolds | |
| 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 | Fix bug in getSymbols. (#2544) | Andrew Reynolds | |
| 2018-09-26 | cmake: Only print dumping warning if not disabled by user. (#2543) | Mathias Preiner | |
| 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-26 | Symmetry breaking for variable agnostic enumerators (#2527) | Andrew Reynolds | |
| 2018-09-25 | cmake: New INSTALL.md for build and testing instructions. (#2536) | Aina Niemetz | |
| 2018-09-25 | cmake: Exclude examples for coverage target. (#2535) | Mathias Preiner | |
| 2018-09-25 | Eagerly ensure literal on active guards for sygus enumerators (#2531) | Andrew Reynolds | |
| 2018-09-25 | cmake: Add check for GCC 4.5.1 and warn user. (#2533) | Mathias Preiner | |
| 2018-09-25 | examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534) | Aina Niemetz | |
| 2018-09-25 | cmake: configure.sh wrapper: Removed unused option --gmp. | 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