| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-05 | Add uniform way to serialize containers of Expr to stream. (#1638) | Aina Niemetz | |
| 2018-03-02 | Fixed typo. | Aina Niemetz | |
| 2018-03-02 | Optimization for sygus streaming mode (#1636) | Andrew Reynolds | |
| 2018-03-02 | Simplify sygus wrt miniscoping (#1634) | Andrew Reynolds | |
| 2018-03-02 | Fixed comments in smt_engine.h. | Aina Niemetz | |
| 2018-03-02 | Print candidate rewrites in terms of original grammar (#1635) | Andrew Reynolds | |
| 2018-03-01 | Create infrastructure for sygus modules (#1632) | Andrew Reynolds | |
| 2018-02-28 | SmtEngine::getAssignment now returns a vector of assignments. (#1628) | Aina Niemetz | |
| 2018-02-27 | Minor fixes for rec-fun (#1616) | Andrew Reynolds | |
| 2018-02-27 | Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627) | Aina Niemetz | |
| 2018-02-27 | Improve rewriter for string indexof (#1592) | Andrew Reynolds | |
| 2018-02-27 | Option to not use partial function semantics for arithmetic div by zero (#1620) | Andrew Reynolds | |
| 2018-02-27 | Improvements to sygus sampling (#1621) | Andrew Reynolds | |
| 2018-02-23 | Add unit tests for BitVector, minor BV rewrite fix (#1622) | Andres Noetzli | |
| This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low. | |||
| 2018-02-23 | Split and document bitvector.h. (#1615) | Aina Niemetz | |
| 2018-02-23 | Fix cd-simplification for strings (#1624) | Andrew Reynolds | |
| 2018-02-22 | Minor improvements to string rewriter (#1572) | Andrew Reynolds | |
| 2018-02-22 | Fixed disabling the BV equality slicer for quantifiers. (#1623) | Aina Niemetz | |
| This fixes an incorrect condition introduced in #1619 to disable the BV equality slicer. | |||
| 2018-02-21 | Disable BV equality slicer if not pure QF_BV. (#1619) | Aina Niemetz | |
| 2018-02-20 | Improve documentation of bv::utils::isCoreTerm (#1617) | Aina Niemetz | |
| 2018-02-20 | Moved and simplified bv::utils::intersect. (#1614) | Aina Niemetz | |
| Tested against the recursive implementation with a temporary assertion on regression tests with --bv-eq-slicer=auto. | |||
| 2018-02-20 | Minor fixes and additions for transcendental functions (#1612) | Andrew Reynolds | |
| Also adds parsing support for PI in smt2 with syntax "real.pi". | |||
| 2018-02-20 | Unrecursified and merged bv::utils::is(Core|Equality)Term. (#1605) | Aina Niemetz | |
| This unrecursifies and merges bv::utils::isCoreTerm and bv::utils::isEqualityTerm to avoid code duplication. In the best case, the recursive implementation visits less nodes. This can be achieved with the non-recursive implementation, however, at the cost of increased code complexity. In practice, on QF_BV the new implementation slightly improves performance. Tested against the recursive implementation with a temporary assertion on regression tests (bv::utils::isCoreTerm was tested with --bv-eq-slicer=auto). Further tested on QF_BV with a TO of 300s (slight performance improvement). | |||
| 2018-02-16 | bv::utils::mk(And|Or) Do not return true if size of vector is 0. (#1613) | Aina Niemetz | |
| 2018-02-16 | Make regress1 default, only test regress0 on Travis. (#1611) | Aina Niemetz | |
| 2018-02-15 | Removed bv::utils::mkConjunction (redundant). (#1610) | Aina Niemetz | |
| 2018-02-15 | Fix corner case for rewrite of mult by pow 2 (#1601) | Andrew Reynolds | |
| 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 | |
 |
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