| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-08-07 | New C++ API: Add checks and tests for push/pop. (#3121) | Aina Niemetz | |
| 2019-08-07 | New C++ API: Introduce macros for try-catch blocks in Solver. (#3121) | Aina Niemetz | |
| 2019-08-06 | New C++ API: Fix branch prediction in CHECK macros. (#3161) | Aina Niemetz | |
| 2019-08-06 | Properly parse qualified identifiers (#3111) | Andrew Reynolds | |
| 2019-08-05 | Remove forward declarations in quantifiers engine (#3156) | Andrew Reynolds | |
| 2019-08-03 | Fix printing issue related to nested quotes (#3154) | Andrew Reynolds | |
| 2019-08-03 | Collapse @ chains in SMT2 printer (#3140) | Haniel Barbosa | |
| 2019-08-02 | Update CaDiCaL to version 1.0.3. (#3137) | Mathias Preiner | |
| * Removes incremental API check (#3011) * Fixes toSatValueLit to use the new semantics of CaDiCaL's val() Fixes #3011 | |||
| 2019-08-02 | Flip the polarity of the argument of get-abduct (#3153) | Andrew Reynolds | |
| 2019-08-02 | Move basic sygus enumerator to its own file (#3149) | Andrew Reynolds | |
| 2019-08-02 | Remove simplification specialized for sygus si solution reconstruction (#3147) | Andrew Reynolds | |
| 2019-08-02 | Support default sygus grammar for strings (#3148) | Andrew Reynolds | |
| 2019-08-02 | Throw option exception when track inst lemmas is not used (#3145) | Andrew Reynolds | |
| 2019-08-02 | Fix solution filtering for streaming abducts (#3143) | Andrew Reynolds | |
| 2019-08-01 | Fix BVGauss unit tests. (#3142) | Mathias Preiner | |
| pass_bv_gauss_white.h included bv_gauss.cpp to test the functions in the anonymous namespace, which resulted in ODR (one definition rule) violations reported by ASAN. This commit exposes the functionality required in the unit tests as private static members of the BVGauss class. Since this is a white unit test, we can access private members in the tests. | |||
| 2019-08-01 | Enable sygus logic when produce-abducts is true (#3144) | Andrew Reynolds | |
| 2019-08-01 | Fix memory leak in rewriter (debug mode). (#3141) | Mathias Preiner | |
| s_rewriteStack in rewriter.cpp was not properly cleaned up. This commit wraps s_rewriteStack in a std::unique_ptr to automatically free the memory. | |||
| 2019-08-01 | Move some generic utilities out of quantifiers (#3139) | Andrew Reynolds | |
| 2019-08-01 | Regular expression intersection modes (#3134) | Andrew Reynolds | |
| 2019-07-31 | Parsing THF and adding several regressions (#3131) | Haniel Barbosa | |
| 2019-07-31 | Add some missing cases in evaluator (#3133) | Andrew Reynolds | |
| 2019-07-31 | Eager conflict detection in strings based on constant prefix/suffix (#3110) | Andrew Reynolds | |
| 2019-07-30 | Track solver execution mode (#3132) | Andrew Reynolds | |
| 2019-07-30 | Code to activate hoelim preprocessing pass (#3129) | Haniel Barbosa | |
| 2019-07-30 | Minor improvement for rewriter for str.replace (#3124) | Andrew Reynolds | |
| 2019-07-30 | Handle RE intersections modulo equality (#3120) | Andrew Reynolds | |
| 2019-07-29 | Model blocker feature (#3112) | Andrew Reynolds | |
| 2019-07-29 | Support get-abduct smt2 command (#3122) | Andrew Reynolds | |
| 2019-07-29 | Fix match trie for polymorphic operators (#3125) | Andrew Reynolds | |
| 2019-07-29 | Refactoring of bit-vector elimination rules (#3105) | yoni206 | |
| This commit makes the following minor refactors to src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h: - Including options/bv_options.h: this is needed because this header file is being used. - Marking all functions as inline: details in a discussion inside the PR. | |||
| 2019-07-27 | Minor improvement to term canonizer (#3123) | Andrew Reynolds | |
| 2019-07-25 | Input user grammar in sygus abduct (#3119) | Andrew Reynolds | |
| 2019-07-25 | Split infer info data structure in strings (#3107) | Andrew Reynolds | |
| 2019-07-24 | Minor refactoring of regexp operation (#3116) | Andrew Reynolds | |
| 2019-07-24 | Fix null node when using no-strings-lazy-pp (#3114) | Andrew Reynolds | |
| 2019-07-24 | Move string util functions (#3115) | Andrew Reynolds | |
| 2019-07-23 | Fix sygus datatype parsing in sygus v1 format (#3113) | Andrew Reynolds | |
| 2019-07-23 | Fix help messages (#3096) | Andrew Reynolds | |
| 2019-07-22 | Get operators in node (#3094) | yoni206 | |
| This commit adds a function to node_algorithm.{h,cpp} that returns the operators that occur in a given node. | |||
| 2019-07-22 | Avoid move constructor of std::fstream for GCC < 5 (#3098) | Andres Noetzli | |
| GCC < 5 does not support the move constructor of `std::fstream` (see https://gcc.gnu.org/bugzilla/show_bug.cgi?id=54316 for details). This commit wraps the `std::fstream` in an `std::unique_ptr` to work around that issue. | |||
| 2019-07-19 | SyGuS grammar refactor (#3100) | yoni206 | |
| 2019-07-19 | Fixes for sygus with datatypes (#3103) | Andrew Reynolds | |
| 2019-07-19 | Fix case of unfolding negative membership in reg exp concatenation (#3101) | Andrew Reynolds | |
| 2019-07-18 | Removing forward-declaration of undefined function ↵ | Andrew V. Jones | |
| 'registerForceLogicListener' (#3086) | |||
| 2019-07-18 | Basic rewrites for tolower/toupper (#3095) | Andrew Reynolds | |
| 2019-07-17 | Minor clean in strings. (#3093) | Andrew Reynolds | |
| 2019-07-16 | Add support for str.tolower and str.toupper (#3092) | Andrew Reynolds | |
| 2019-07-15 | Add string rewrite to distribute character stars over concatenation (#3091) | Andrew Reynolds | |
| 2019-07-08 | Towards refactoring relations (#3078) | Andrew Reynolds | |
| 2019-07-05 | Refactor strings to use an inference manager object (#3076) | Andrew Reynolds | |
 |
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