| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-10 | Move rewrite to pass (#2128) | Caleb Donovick | |
| 2018-07-06 | Split ext theory to own file and document (#1809) | Andrew Reynolds | |
| 2018-07-04 | Reorganize candidate rewrite rule filtering (#2116) | Andrew Reynolds | |
| 2018-07-04 | Remove unused CDVector (#2139) | Andres Noetzli | |
| 2018-07-02 | Refactor ApplySubsts preprocessing pass. (#2120) | Aina Niemetz | |
| 2018-06-28 | New C++ API: Implementation of Result. (#2112) | Aina Niemetz | |
| 2018-06-28 | Split and document ceg theory instantiators (#2094) | Andrew Reynolds | |
| 2018-06-27 | Synthesize candidate-rewrites from standard inputs (#1918) | Andrew Reynolds | |
| 2018-06-26 | sygusComp2018: Add evaluator (#2090) | Andres Noetzli | |
| This commit adds the Evaluator class that can be used to quickly evaluate terms under a given substitution without going through the rewriter. This has been shown to lead to significant performance improvements on SyGuS PBE problems with a large number of inputs because candidate solutions are evaluated on those inputs. With this commit, the evaluator only gets called from the SyGuS solver but there are potentially other places in the code that could profit from it. | |||
| 2018-06-20 | Resolve CVC4_USE_SYMFPU in headers at config-time (#2077) | Andres Noetzli | |
| As described in issue #2013, we had `#ifdef CVC4_USE_SYMFPU` conditions in floatingpoint.h, which was problematic when installing the header files because the definition of `CVC4_USE_SYMFPU` was a compile-flag and simply including the header files in another project would be missing that definition. This commit moves floatingpoint.h to a template file floatingpoint.h.in and substitutes the value of `CVC4_USE_SYMFPU` at configure-time when generating floatingpoint.h (this is the same solution that integer.h and rational.h use). I have tested the fix with the examples provided in #2013 and they work. | |||
| 2018-05-21 | Refactor sygus eval unfold (#1946) | Andrew Reynolds | |
| 2018-05-15 | Refactor static learning preprocessing pass (#1857) | yoni206 | |
| 2018-05-10 | Sygus repair constants (#1812) | Andrew Reynolds | |
| 2018-05-10 | Refactored BVAckermann preprocessing pass. (#1889) | Aina Niemetz | |
| 2018-05-09 | Add the symmetry breaker module (#1847) | PaulMeng | |
| 2018-05-08 | Refactor bv-abstraction preprocessing pass. (#1860) | Mathias Preiner | |
| 2018-05-03 | Refactor bv-intro-pow2 preprocessing pass. (#1851) | Mathias Preiner | |
| 2018-05-03 | Move Lazy trie datastructure to its own file (#1871) | Haniel Barbosa | |
| Preparation for further developing CegisUnif | |||
| 2018-05-02 | Remove (dummy) SMT1 printer (#1854) | Andres Noetzli | |
| 2018-04-30 | Refactor real2int (#1813) | Haniel Barbosa | |
| This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. | |||
| 2018-04-30 | Remove subsort symmetry breaking (#1807) | Andrew Reynolds | |
| 2018-04-27 | New module for synthesizing functions in a data-driven SyGuS approach (#1819) | Haniel Barbosa | |
| 2018-04-25 | Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788) | yoni206 | |
| 2018-04-25 | Move candidate rewrite code to own file (#1804) | Andrew Reynolds | |
| 2018-04-20 | Symmetry detection module (#1749) | PaulMeng | |
| 2018-04-19 | Refactor pbRewrites preprocessing pass (#1767) | Andres Noetzli | |
| This commit refactors the pbRewrites preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. It also makes use of the AssertionPipeline::replace function to do proper dependency tracking. | |||
| 2018-04-10 | Refactored BVGauss preprocessing pass. (#1766) | Aina Niemetz | |
| 2018-04-03 | Refactor IntToBV preprocessing pass (#1716) | Andres Noetzli | |
| This commit refactors the IntToBV preprocessing pass into the new style. This commit is essentially just a code move, it does not attempt to fix issues (e.g. #1715). | |||
| 2018-04-03 | Option to turn arbitrary input into sygus (#1704) | Andrew Reynolds | |
| Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving. This includes improvements to the robustness of the sygus solver. | |||
| 2018-04-03 | Make sygus unif I/O an subclass of sygus unif (#1741) | Andrew Reynolds | |
| 2018-04-02 | Reorganize bitblaster code. (#1695) | Mathias Preiner | |
| This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the sub-directory bitblast/. | |||
| 2018-03-30 | Split strategy representation from SygusUnif (#1730) | Andrew Reynolds | |
| 2018-03-27 | Make sygus unif utility (#1720) | Andrew Reynolds | |
| 2018-03-23 | Remove unused code (#1700) | Andrew Reynolds | |
| 2018-03-23 | Minor reorganization for ematching (#1701) | Andrew Reynolds | |
| 2018-03-20 | Add support for CaDiCaL as eager BV SAT solver. (#1675) | Mathias Preiner | |
| 2018-03-01 | Create infrastructure for sygus modules (#1632) | Andrew Reynolds | |
| 2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds | |
| 2018-02-13 | Remove unused cd_set_collection.h (#1606) | Andres Noetzli | |
| 2018-02-09 | Class to reduce printing of redundant candidate rewrites (#1588) | Andrew Reynolds | |
| 2018-02-05 | Statically eliminate redundant sygus constructors (#1560) | Andrew Reynolds | |
| 2018-02-01 | Use sygus to synthesize/verify rewrite rules (#1547) | Andrew Reynolds | |
| 2018-01-03 | Global negate (#1466) | Andrew Reynolds | |
| 2017-12-10 | Add new infrastructure for preprocessing passes (#1053) | justinxu421 | |
| This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits). | |||
| 2017-12-08 | Document and clean datatypes rewriter (#1437) | Andrew Reynolds | |
| 2017-12-06 | Remove CDChunkList (#1414) | Andres Noetzli | |
| 2017-11-30 | Add Gaussian Elimination as a preprocessing pass for BV. (#1342) | Aina Niemetz | |
| This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur. | |||
| 2017-11-24 | (Refactor) Instantiate utility (#1387) | Andrew Reynolds | |
| 2017-11-22 | Sygus Lambda Grammars (#1390) | Andrew Reynolds | |
| 2017-11-21 | Adding infrastructure for normalizing SyGuS grammars (#1397) | Haniel Barbosa | |
| * minor Using string previously computed * adding option * starting module for simplifying grammars * more * more * fix * fix * fix * fix * fix * removing unused command * removing unused command * removing unnecessary quantifier engine * adding lambda support * transient * reverting changes * starting normalization of integers * removing unnecessary objects * using for_each * rebuilding given datatypes * recrating types as given * bug fixing * minor * reverting space changes * addressing review * addressing review | |||
 |
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