Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
* 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").
|
|
Adds missing override keywords.
|
|
|
|
|
|
|
|
|
|
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
|
|
|
|
* 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.
|
|
|
|
|
|
|
|
|
|
argument.
|
|
|
|
|
|
nodes.
|
|
Generalize previous fix for sets, minor changes to Datatypes.
|
|
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
|
|
improvement to sets.
|
|
minor changes.
|
|
logic, change syntax for empty heap constraint.
|
|
|
|
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
|
|
Fix a few more memory leaks.
|
|
|
|
|
|
|
|
to EPR
|
|
|
|
|
|
breaking in theory sep.
|
|
allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
|
|
|
|
|
|
|
|
|
|
Ensure value of sep.nil is correct in models. Print instantiations as sexprs.
|
|
cleanup.
|
|
|
|
preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.
|
|
|
|
enabled. Fix sep.nil preregistration in TheorySep.
|
|
|
|
|
|
|