Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-02-15 | Refactor regressions (#1581) | Andrew Reynolds | |
2018-02-15 | Fix context memory manager unit test (#1609) | Andres Noetzli | |
Commit 83f150c727f197c530d6f46a75b516eea52bed29 changed the flag that we use to determine whether to use the context memory manager or the debug version. However, the change was not reflected in the context memory manager unit test. This commit fixes the unit test to check the correct flag. | |||
2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds | |
2018-02-13 | Remove unused cd_set_collection.h (#1606) | Andres Noetzli | |
2018-02-13 | Provide a uniform way to serialize node containers to output stream. (#1604) | Aina Niemetz | |
2018-02-13 | Moved (unrecursified) bv::utils::collectVars. (#1602) | Aina Niemetz | |
2018-02-13 | Skip header for determining top contributors list. (#1603) | Aina Niemetz | |
2018-02-12 | Option to use extended rewriter as a preprocessing pass (#1600) | Andrew Reynolds | |
2018-02-12 | Minor improvements to sygus sampler (#1598) | Andrew Reynolds | |
2018-02-11 | Move (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594) | Aina Niemetz | |
This unrecursifies and moves bv::utils::numNodes to an unnamed namespace in lazy_bitblaster.cpp (only place where it is used). Tested against the recursive implementation (with a temporary Assertion) on regression tests. | |||
2018-02-10 | More minor improvements to synth-rr (#1597) | Andrew Reynolds | |
2018-02-09 | Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589) | Aina Niemetz | |
2018-02-09 | Remove mkNode from bv::utils (#1587) | Aina Niemetz | |
2018-02-09 | Removing an always true comparison (unsigned) >= 0u. (#1582) | Tim King | |
2018-02-09 | Class to reduce printing of redundant candidate rewrites (#1588) | Andrew Reynolds | |
2018-02-09 | Renaming CHECK to CVC4_CHECK. This avoids name collisions with other popular ↵ | Tim King | |
assertion macros. This name is likely temporary while Assert() is deprecated. (#1590) | |||
2018-02-09 | Replacing an incorrect reference to an injected class name when the type was ↵ | Tim King | |
meant. (#1585) | |||
2018-02-08 | Replace CMM flag with debug CMM flag, fix leak in debug CMM (#1586) | Andres Noetzli | |
Previously, we had -DCVC4_CONTEXT_MEMORY_MANAGER that needed to be added as a compile flag to use the context memory manager (which we want by default). This makes compiling with other build systems cumbersome because you have to know about the flag. This commit replaces the -DCVC4_CONTEXT_MEMORY_MANAGER flag with a -DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER flag that does the opposite (in absence of the flag, we use the context memory manager). Additionally, the commit fixes a memory leak in the debug context memory manager (the destructor did not clean up the allocations). | |||
2018-02-08 | Inlining line_buffered_input to avoid warning about unused variables in ↵ | Tim King | |
production builds. (#1584) | |||
2018-02-08 | Clean up bv utils (part one). (#1580) | Aina Niemetz | |
This is part one of an effort to clean up bv utils. It addresses review comments not addressed in #1566 (changes of moved code), removes unused functions and moves a helper to compute the gcd over Index. | |||
2018-02-08 | Adding virtual destructors on classes with virtual functions. (#1583) | Tim King | |
2018-02-08 | Minor improvements to sygus sampling. (#1577) | Andrew Reynolds | |
2018-02-08 | Updated copyright | Aina Niemetz | |
2018-02-08 | Initializing Timer::d_wall_limit (CID 1362899). (#1573) | Tim King | |
2018-02-08 | Simplify and cleanup bv::utils::mkConjunction. (#1571) | Aina Niemetz | |
2018-02-08 | Check whether Cryptominisat4/ABC was installed via get-* script. (#1565) | Mathias Preiner | |
2018-02-08 | Remove invalid regression test (#1579) | Andres Noetzli | |
2018-02-07 | Removing an unused variable. (#1576) | Tim King | |
2018-02-07 | Fixing more inconsistent usages of override. (#1575) | Tim King | |
2018-02-07 | Reduce number of Travis builds. (#1578) | Aina Niemetz | |
2018-02-07 | Fixing line numbers on type_checker_template.cpp (#1574) | Tim King | |
2018-02-07 | Cleanup Cryptominisat header. (#1561) | Mathias Preiner | |
Clang formatted sat_solver_factor.cpp | |||
2018-02-07 | Use template for bv::utils::mkOr. (#1570) | Aina Niemetz | |
2018-02-07 | Adds a new CHECK macro that abort()s on failure. (#1532) | Tim King | |
2018-02-07 | Add remaining transcendental functions (#1551) | Andrew Reynolds | |
2018-02-07 | Use template for bv::utils::mkAnd. (#1569) | Aina Niemetz | |
2018-02-06 | Renamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568) | Aina Niemetz | |
2018-02-06 | Split and document theory_bv_utils. (#1566) | Aina Niemetz | |
This moves the implementation from the header to the .cpp file. It further documents all functions in the header file. | |||
2018-02-06 | Use separate shell script for common get-* script parts. (#1567) | Mathias Preiner | |
2018-02-06 | Fixes two memory leaks coming from Transf. (#1564) | Tim King | |
First, it adds a virtual destructor so the subclasses will get cleaned up. Second, it wraps the returned pointer in a unique_ptr. Should fix ASAN failures in the nightly run. | |||
2018-02-06 | Updated copyright header for bv_inverter.(cpp|h). | Aina Niemetz | |
2018-02-06 | Updated year in update-copyright script. | Aina Niemetz | |
2018-02-06 | Resolving warnings from -Winconsistent-missing-override on clang. (#1563) | Tim King | |
2018-02-06 | Fix two multiply-by-constant corner cases for bv rewriter (#1562) | Andrew Reynolds | |
2018-02-06 | Updated authors list | Aina Niemetz | |
2018-02-06 | Fix rewrite for string replace (#1537) | Andrew Reynolds | |
2018-02-05 | Using getOperator() directly instead of using -1. CID 1172262. (#1559) | Tim King | |
2018-02-05 | Aborting on errors in StatisticsRegistry::unregisterStat() instead of ↵ | Tim King | |
throwing exceptions. This is called from destructors and therefore it is inappropraiate to throw exceptions. This solution is temporary until Assert() is deprecated in favor of an aborting version. (#1539) | |||
2018-02-05 | Statically eliminate redundant sygus constructors (#1560) | Andrew Reynolds | |
2018-02-05 | Cleaning up the printing of theory model representative sets. (#1538) | Tim King | |