| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-03-22 | Collect statistics about normal form inferences (#4127) | Andres Noetzli | |
| This commit adds code to count the number of inferences made of each inference type for normal form inferences. It extends the Inference enum in `infer_info.h` and adds two new `sendInference()` methods in the `InferenceManager` to send and count inferences that have a corresonding entry in the `Inference` enum. | |||
| 2020-03-02 | Split collect model info by types in strings (#3847) | Andrew Reynolds | |
| Towards a theory of sequences. We will need to do similar splits per type for most of the functions throughout strings. | |||
| 2020-02-22 | Minor refactoring of equality notifications (#3798) | Andrew Reynolds | |
| Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver. | |||
| 2020-02-22 | Move check memberships to reg exp solver (#3793) | Andrew Reynolds | |
| There was previously a function in TheoryStrings to make the proper call to checkMembership. In the refactored code, this is no longer necessary and the interface to RegExp can be simplified. | |||
| 2020-02-21 | Move cardinality inference scheme to base solver in strings (#3792) | Andrew Reynolds | |
| Moves handling of cardinality to the base solver, refactors how cardinality is accessed. No intended behavior change in this commit. | |||
| 2020-02-21 | Split extended functions solver in strings (#3768) | Andrew Reynolds | |
| 2020-02-15 | Move proxy variables to InferenceManager in strings (#3758) | Andrew Reynolds | |
| 2020-02-07 | Split strings finite model finding strategy (#3727) | Andrew Reynolds | |
| 2020-02-07 | Split core solver from the theory of strings (#3713) | Andrew Reynolds | |
| This splits the main procedure from Liang et al CAV 2014 to its own file, the "core solver" of theory of strings. I have intentionally not updated or clang-formatted the code in core_solver.cpp since I would prefer this PR to involve as little change to behavior as possible (it is copied verbatim from theory_strings.cpp). Future PRs will clean this code up. | |||
| 2020-02-04 | Split base solver from the theory of strings (#3680) | Andrew Reynolds | |
| 2020-01-30 | Move disequality list to solver state in strings (#3678) | Andrew Reynolds | |
| 2020-01-29 | Modularize more steps in the strings strategy (#3676) | Andrew Reynolds | |
| 2020-01-29 | Minor updates to string utilities (#3675) | Andrew Reynolds | |
| 2019-11-06 | Move more string utility functions (#3398) | Andrew Reynolds | |
| This is work towards splitting a "core solver" object from TheoryStrings. This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects. It also corrects an issue where we were maintaining two `d_conflict` fields. | |||
| 2019-11-01 | Fix and refactor TheoryStrings::checkFlatForms() (#3326) | Andres Noetzli | |
| This commit fixes some minor (performance) issues in `TheoryStrings::checkFlatForms()`: The `inelig` vector was initialized with copies of the `start` element instead of all the elements before `start` and the `else` branch of `count == asize` was looping over all elements from `1` instead of `start + 1`. Additionally, this commit refactors the code to be a bit more readable. | |||
| 2019-10-16 | Solver state for theory of strings (#3181) | Andrew Reynolds | |
| This refactors the theory of strings to use a solver state object, which manages state information regarding assertions. It also deletes some unused/undefined functions in theory_strings.h. There are no major changes to the behavior of the code or its documentation in this PR. This is work towards #1881. | |||
| 2019-08-22 | Local substitutions for context-depdendent simplification in strings (#3204) | Andrew Reynolds | |
| 2019-07-31 | Eager conflict detection in strings based on constant prefix/suffix (#3110) | Andrew Reynolds | |
| 2019-07-25 | Split infer info data structure in strings (#3107) | Andrew Reynolds | |
| 2019-07-05 | Refactor strings to use an inference manager object (#3076) | Andrew Reynolds | |
| 2019-04-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
| Fixes 2887. | |||
| 2019-04-23 | Refactor normal forms in strings (#2897) | Andrew Reynolds | |
| 2019-03-26 | Update copyright headers. | Aina Niemetz | |
| 2019-03-24 | Split regular expression solver (#2891) | Andrew Reynolds | |
| 2019-03-22 | Revisit strings extended function decomposition (#2892) | Andrew Reynolds | |
| 2019-01-15 | Strings: Add option to change loop process mode (#2794) | Andres Noetzli | |
| This commit adds an option `--strings-process-loop-mode` that allows finer-grained control over CVC4 processes looping word equation. In particular, performing normal loop breaking sometimes leads to worse performance. The "simple" mode disables that inference. | |||
| 2018-11-27 | Make (T)NodeTrie a general utility (#2489) | Andrew Reynolds | |
| This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it. | |||
| 2018-10-16 | Improve strings reductions including skolem caching for contains (#2641) | Andrew Reynolds | |
| 2018-10-10 | Fix compiler warnings (#2602) | Andres Noetzli | |
| 2018-09-30 | Add rewrite for solving stoi (#2532) | Andrew Reynolds | |
| 2018-09-18 | Refactor strings extended functions inferences (#2480) | Andrew Reynolds | |
| This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type. This is in preparation for working on solving equations and further inferences in this style. | |||
| 2018-09-18 | Decision strategy: incorporate strings fmf. (#2485) | Andrew Reynolds | |
| 2018-09-17 | Make strings model construction robust to lengths that are not propagated ↵ | Andrew Reynolds | |
| equal (#2444) This fixes #2429. This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment. We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this. Regardless, the strings model construction should be robust to handle this case, which this PR does. | |||
| 2018-09-14 | Add Skolem cache for strings, refactor length registration (#2457) | Andrew Reynolds | |
| This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor). It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled. | |||
| 2018-08-30 | Add regular expression elimination module (#2400) | Andrew Reynolds | |
| 2018-08-26 | Use uniform length limit for String constants (#2381) | Andres Noetzli | |
| 2018-08-26 | Fix unsigned integer type issues in strings (#2380) | Andrew Reynolds | |
| * Fix unsigned integer types in strings. * Format | |||
| 2018-07-05 | Make string length lemmas more robust to rewriting (#2150) | Andrew Reynolds | |
| 2018-07-02 | Remove some dead code from theory strings (#2125) | Andrew Reynolds | |
| 2018-06-25 | Updated copyright headers. | Aina Niemetz | |
| 2018-05-21 | Infrastructure for strings strategies (#1883) | Andrew Reynolds | |
| 2018-05-08 | Support for str.<= and str.< (#1882) | Andrew Reynolds | |
| 2018-05-07 | Add support for str.code (#1821) | Andrew Reynolds | |
| 2018-04-15 | Make strings fmf apply to all but internally generated Skolems (#1780) | Andrew Reynolds | |
| 2018-03-23 | Remove unused code (#1700) | Andrew Reynolds | |
| 2018-03-19 | Document inferences for strings (#1642) | Andrew Reynolds | |
| 2018-03-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
| Adds missing override keywords. | |||
| 2018-02-06 | Resolving warnings from -Winconsistent-missing-override on clang. (#1563) | Tim King | |
| 2018-01-02 | Improve rewriter for string equality (#1427) | Andrew Reynolds | |
| 2017-12-08 | Make collect model info return a Bool (#1421) | 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