summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-15Fix 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-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-13Remove unused cd_set_collection.h (#1606)Andres Noetzli
2018-02-13Provide a uniform way to serialize node containers to output stream. (#1604)Aina Niemetz
2018-02-13Moved (unrecursified) bv::utils::collectVars. (#1602)Aina Niemetz
2018-02-13Skip header for determining top contributors list. (#1603)Aina Niemetz
2018-02-12Option to use extended rewriter as a preprocessing pass (#1600)Andrew Reynolds
2018-02-12Minor improvements to sygus sampler (#1598)Andrew Reynolds
2018-02-11Move (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-10More minor improvements to synth-rr (#1597)Andrew Reynolds
2018-02-09Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)Aina Niemetz
2018-02-09Remove mkNode from bv::utils (#1587)Aina Niemetz
2018-02-09Removing an always true comparison (unsigned) >= 0u. (#1582)Tim King
2018-02-09Class to reduce printing of redundant candidate rewrites (#1588)Andrew Reynolds
2018-02-09Renaming 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-09Replacing an incorrect reference to an injected class name when the type was ↵Tim King
meant. (#1585)
2018-02-08Replace 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-08Inlining line_buffered_input to avoid warning about unused variables in ↵Tim King
production builds. (#1584)
2018-02-08Clean 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-08Adding virtual destructors on classes with virtual functions. (#1583)Tim King
2018-02-08Minor improvements to sygus sampling. (#1577)Andrew Reynolds
2018-02-08Updated copyrightAina Niemetz
2018-02-08Initializing Timer::d_wall_limit (CID 1362899). (#1573)Tim King
2018-02-08Simplify and cleanup bv::utils::mkConjunction. (#1571)Aina Niemetz
2018-02-08Check whether Cryptominisat4/ABC was installed via get-* script. (#1565)Mathias Preiner
2018-02-08Remove invalid regression test (#1579)Andres Noetzli
2018-02-07Removing an unused variable. (#1576)Tim King
2018-02-07Fixing more inconsistent usages of override. (#1575)Tim King
2018-02-07Reduce number of Travis builds. (#1578)Aina Niemetz
2018-02-07Fixing line numbers on type_checker_template.cpp (#1574)Tim King
2018-02-07Cleanup Cryptominisat header. (#1561)Mathias Preiner
Clang formatted sat_solver_factor.cpp
2018-02-07Use template for bv::utils::mkOr. (#1570)Aina Niemetz
2018-02-07Adds a new CHECK macro that abort()s on failure. (#1532)Tim King
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-02-07Use template for bv::utils::mkAnd. (#1569)Aina Niemetz
2018-02-06Renamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568)Aina Niemetz
2018-02-06Split 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-06Use separate shell script for common get-* script parts. (#1567)Mathias Preiner
2018-02-06Fixes 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-06Updated copyright header for bv_inverter.(cpp|h).Aina Niemetz
2018-02-06Updated year in update-copyright script.Aina Niemetz
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-02-06Fix two multiply-by-constant corner cases for bv rewriter (#1562)Andrew Reynolds
2018-02-06Updated authors listAina Niemetz
2018-02-06Fix rewrite for string replace (#1537)Andrew Reynolds
2018-02-05Using getOperator() directly instead of using -1. CID 1172262. (#1559)Tim King
2018-02-05Aborting 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-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-05Cleaning up the printing of theory model representative sets. (#1538)Tim King
2018-02-05Removing references to __gnu_cxx. (#1541)Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback