Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-08-20 | Fix initialization of d_smt in ValidityChecker for changes from #2240. (#2343) | Aina Niemetz | |
2018-08-20 | Remove disabled system test cvc3_george. (#2342) | Aina Niemetz | |
Disabled since 6 years, @mdeters commented when disabling it that it takes a very long time to build, see 868ee6d. | |||
2018-08-20 | More unused code elimination (#2339) | Andrew Reynolds | |
2018-08-20 | Remove support for prototype (non-sygus) synthesis (#2338) | Andrew Reynolds | |
2018-08-20 | Add regressions that increase coverage (#2337) | Andrew Reynolds | |
2018-08-20 | Minor improvements to the interface for sygus sampler (#2326) | Andrew Reynolds | |
2018-08-20 | Make sygus inference a preprocessing pass (#2334) | Andrew Reynolds | |
2018-08-18 | run-regress script: Exit with exit code > 0 on failure. (#2336) | Aina Niemetz | |
This is in preparation for migration to cmake since ctest determines failure via exit code. | |||
2018-08-17 | Remove support for flipDecision (#2319) | Andrew Reynolds | |
2018-08-17 | Remove miscellaneous unused code (#2333) | Andrew Reynolds | |
2018-08-17 | Add sygus stream regressions (#2330) | Andrew Reynolds | |
2018-08-17 | Split sygus grammar to its own ANTLR grammar (#2307) | Andrew Reynolds | |
2018-08-17 | Fix spurious warning in sort inference (#2331) | Andrew Reynolds | |
2018-08-17 | Fix arithmetic division by zero in sygus repair constant module (#2329) | Andrew Reynolds | |
2018-08-17 | Eliminate partial operators in sygus grammar normalization (#2323) | Andrew Reynolds | |
This corrects a bug that was introduced in #2266 (the hack removed there was necessary). This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus. This also enables total semantics for BV div-by-zero for sygus. | |||
2018-08-16 | Initialize inputAssertions only when proofRecipe is non-null (#2325) | Tim King | |
Most of the PR is clang-format cruft from picking up the contents of a PROOF({ ... }); | |||
2018-08-16 | Refactor eager atoms preprocessing pass. (#2318) | Mathias Preiner | |
2018-08-17 | cleaning unnecessary timers/dumps (#2327) | Haniel Barbosa | |
2018-08-16 | Adding support for bitvector SyGuS problems without grammars (#2328) | Haniel Barbosa | |
2018-08-16 | Make quantifiers-preprocess preprocessing pass (#2322) | Caleb Donovick | |
2018-08-16 | Removing coverity warnings from theory_sep.cpp (#2320) | Tim King | |
2018-08-16 | Refactor IteRemoval preprocessing pass (#1793) | Andres Noetzli | |
This commit refactors the IteRemoval pass to follow the new format. In addition to moving the code, this entails the following changes: - The timer for the ITE removal is now called differently (the default timer of PreprocessingPass is used) and measures just the preprocessing pass without applySubstitutions(). It also measures the time used by both invocations of the ITE removal pass. - Debug output will be slightly different because we now just rely on the default functionality of PreprocessingPass. - d_iteRemover is now passed into the PreprocessingPassContext. - AssertionPipeline now owns the d_iteSkolemMap, which makes it accessible by preprocessing passes. The idea behind this is that the preprocessing passes collect information in AssertionPipeline and d_iteSkolemMap fits that pattern. | |||
2018-08-16 | Move node algorithms to separate file (#2311) | Andres Noetzli | |
2018-08-16 | Minor fixes and improvement for sygus to builtin. (#2306) | Andrew Reynolds | |
2018-08-16 | Refactor extended rewriter preprocessing pass (#2324) | Haniel Barbosa | |
2018-08-16 | Refactor apply2const (#2316) | Haniel Barbosa | |
2018-08-15 | Switching an Assert to a CVC4_CHECK to test if it resolves CID 1459595. (#2315) | Tim King | |
2018-08-15 | Removing attribute cleanups. (#2300) | Tim King | |
* Removing attribute cleanups. | |||
2018-08-15 | Add contrib/get-gmp script. (#2292) | Mathias Preiner | |
2018-08-15 | Remove unused tuple classes (#2313) | Andres Noetzli | |
Since we are using C++11, we can replace the triple and quad classes with std::tuple. | |||
2018-08-15 | Remove unused class DynamicArray (#2312) | Andres Noetzli | |
2018-08-15 | Make sort inference a preprocessing pass (#2309) | Andrew Reynolds | |
2018-08-15 | Fix dumping of get-unsat-assumptions (#2302) | Andres Noetzli | |
When dumping a `get-unsat-assumptions` command, CVC4 was instead dumping two `get-unsat-cores` commands. This commit splits `SmtEngine::getUnsatCores()` into a part that does the dumping and an internal part that actually gets the unsat core without dumping. `SmtEngine::getUnsatAssumptions()` now calls the internal version to avoid the redundant dumping of a `get-unsat-cores` command and changes the command that gets dumped in `SmtEngine::getUnsatAssumptions()`. | |||
2018-08-14 | Remove unused declaration (#2310) | Andres Noetzli | |
2018-08-14 | autotools: Remove personal builds, rename build 'default' to 'testing'. (#2303) | Aina Niemetz | |
2018-08-13 | Fix get-unsat-assumptions output (#2301) | Andres Noetzli | |
Fixes #2298. The `get-unsat-assumptions` command was printing the result with square brackets and commas instead of parentheses and spaces between the assumptions. | |||
2018-08-13 | Removing support for T* and const T* attributes. (#2297) | Tim King | |
* Removing support for T* and const T* attributes. These are unused. | |||
2018-08-11 | Make attributes robust to static init orderings (#2295) | Andres Noetzli | |
@taking pointed out that part of the issue fixed in #2293 is also that we should be more robust to different (de-)initialization orders. A common, portable way to achieve this is to allocate the object in question on the heap and make the pointer to it static [0]. This commit fixes the variable in question. I have tested this fix in ASAN (without using --no-static-init flag for CxxTest) and it works. [0] https://isocpp.org/wiki/faq/ctors#construct-on-first-use-v2 | |||
2018-08-10 | Fix portfolio command executor for changes from #2240. (#2294) | Aina Niemetz | |
2018-08-10 | Do not use static initialization in CxxTest runner (#2293) | Andres Noetzli | |
The static initialization in the CxxTest runner was causing problems when having `std::unique_ptr`s in test classes. When the ExprManager's deconstructor is called, we count on certain static objects to be around (e.g. https://github.com/CVC4/CVC4/blob/0a02fd2b69c0c0f454fc33d8028b24f4fcf431de/src/expr/attribute_internals.h#L508). If the ExprManager is (indirectly) owned by a `std::unique_ptr` in a static class, however, there are no such guarantees as the destruction order of static objects is not defined. This commit adds a flag for CxxTest to not use static initialization in the test runner, which solves the issue. Additionally, the commit fixes a warning about a missing virtual deconstructor in ParserBlack that came up after using the new flags. This fixes an issue reported in the nightly builds. | |||
2018-08-09 | Fix char overflow issues in regular expression solver (#2275) | Andrew Reynolds | |
2018-08-09 | Fix documentation of regression tests (#2290) | Andres Noetzli | |
2018-08-08 | Plug solver API object into parser. (#2240) | Aina Niemetz | |
2018-08-08 | Fixing documentation nit from PR#2232. (#2289) | Tim King | |
2018-08-08 | Proposal for adding map utility functions to CVC4. (#2232) | Tim King | |
* Proposal for adding map utility functions to CVC4. | |||
2018-08-08 | Disable argument relevance for sygus by default (#2288) | Andrew Reynolds | |
2018-08-08 | Add debug test for sygus subcall verify calls. (#2287) | Andrew Reynolds | |
2018-08-08 | Move uf model code from uf to quantifiers (#2095) | Andrew Reynolds | |
2018-08-08 | Do beta-reduction in expandDefinitions (#2286) | Andrew Reynolds | |
2018-08-07 | Require Swig 3 (#2283) | Andres Noetzli | |
Removes some hacks due to Swig 2's incomplete C++11 support and adds checks for version 3 at configuration time as well as in swig.h |