Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-26 | Fix -Wshadow warnings in common headers | Andres Noetzli | |
2020-02-19 | resource manager: Add statistic for every resource. (#3772) | Mathias Preiner | |
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`). Fixes #3751. | |||
2019-12-09 | Make theory rewriters non-static (#3547) | Andres Noetzli | |
This commit changes theory rewriters to be non-static. This refactoring is needed as a stepping stone to making our rewriter configurable: If we have multiple solver objects with different rewrite configurations, we cannot use `static` variables for the rewriter table in the BV rewriter for example. It is also in line with our goal of getting rid of singletons in general. Note that the `Rewriter` class is still a singleton, which will be changed in a future commit. | |||
2019-10-30 | Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366) | Mathias Preiner | |
2019-04-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
Fixes 2887. | |||
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-09-22 | cmake: Remove unused CMakeLists.txt | Mathias Preiner | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-09-18 | Decision strategy: incorporate separation logic. (#2494) | Andrew Reynolds | |
2018-08-22 | Fix invalid iterator comparisons (#2349) | Andrew Reynolds | |
2018-08-16 | Removing coverity warnings from theory_sep.cpp (#2320) | Tim King | |
2018-07-17 | Refactor sep-pre-skolem-emp preprocessing pass | yoni206 | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-03-06 | Make statistics output consistent. (#1647) | Mathias Preiner | |
* Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv"). | |||
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-10 | Removing throw specifiers for TypeRules. (#1501) | Tim King | |
2017-12-08 | Make collect model info return a Bool (#1421) | Andrew Reynolds | |
2017-12-06 | Remove CDChunkList (#1414) | Andres Noetzli | |
2017-11-01 | (Move-only) Split quant util (#1306) | Andrew Reynolds | |
* Initial draft of splitting quant util. * Minor * Document recursive term builder. * Rename file, minor. * Clang format | |||
2017-10-30 | Remove include (#1298) | Andrew Reynolds | |
2017-10-09 | Split term database (#1206) | Andrew Reynolds | |
* Move equality query to own file, move equality inference to quantifiers engine. * Move quantifiers attributes out of TermDb and into QuantAttribute. * Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header. * Split term database into term util. * Partial fix for #1205 that eliminates need for dependency in node.cpp. * Add more references to github issues. | |||
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2017-07-07 | Use new copyright header format. | Mathias Preiner | |
2017-04-14 | Fix nullary operator printers, minor. | ajreynol | |
2017-04-12 | Add nullary operator metakind. | ajreynol | |
2017-04-04 | Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵ | ajreynol | |
argument. | |||
2017-03-27 | Making ppNotifyAssertions take a const vector. | Tim King | |
2017-03-22 | Fix more cases of rewritten explanations in strings for bug 784. Minor. | ajreynol | |
2017-03-06 | Support for set compliment and universe set. Simplify approach for sep.nil ↵ | ajreynol | |
nodes. | |||
2017-03-03 | Fix for collectModelInfo related to finite types + preregistration. ↵ | ajreynol | |
Generalize previous fix for sets, minor changes to Datatypes. | |||
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ | ajreynol | |
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. | |||
2016-12-06 | Improve bounds for global heap in sep, refactor preprocessing. Minor ↵ | ajreynol | |
improvement to sets. | |||
2016-12-01 | Improvement and bug fix for str.indexof reduction, add regression. Other ↵ | ajreynol | |
minor changes. | |||
2016-11-08 | Add a few options to separation logic and sets. Minor changes to separation ↵ | ajreynol | |
logic, change syntax for empty heap constraint. | |||
2016-11-03 | Make data points accurate in sep logic models. | ajreynol | |
2016-11-03 | Add priorities to getNextDecision. Properly handle case for finite types + ↵ | ajreynol | |
unbounded heaps in sep logic. Fix another simple memory leak in sygus. | |||
2016-11-02 | Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ | ajreynol | |
Fix a few more memory leaks. | |||
2016-11-02 | Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat. | ajreynol | |
2016-09-15 | Make sep pto a trigger kind, track in equality engines and term database. | ajreynol | |
2016-09-14 | Support for unique variable generation in node manager. | ajreynol | |
2016-09-14 | Lemma cache in theory sep. Minor optimization for sets. Minor improvements ↵ | ajreynol | |
to EPR | |||
2016-09-13 | Minor changes to sep logic, epr, quantifier splitting. | ajreynol | |
2016-09-12 | Prefer non-cardinality constants in term models for sep logic. | ajreynol | |
2016-09-12 | Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry ↵ | ajreynol | |
breaking in theory sep. | |||
2016-09-09 | Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵ | ajreynol | |
allow sep disequal card constants when type is monotonic. Update logics on sep regressions. | |||
2016-09-08 | Refactor seplog preprocess. Handle case where sep data type cannot be inferred. | ajreynol | |
2016-08-25 | Minor cleanup preprocessing, add ppNotifyAssertions. | ajreynol | |
2016-08-09 | Fixes for sep star rewrite. | ajreynol | |
2016-07-22 | Minor, error handling for polymorphism + sep logic. | ajreynol | |