summaryrefslogtreecommitdiff
path: root/src/theory/sep/theory_sep.h
AgeCommit message (Collapse)Author
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-09-18Decision strategy: incorporate separation logic. (#2494)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-07-07Update copyright headers.Mathias Preiner
2017-07-07Use new copyright header format.Mathias Preiner
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵ajreynol
argument.
2017-03-27Making ppNotifyAssertions take a const vector.Tim King
2016-12-06Improve bounds for global heap in sep, refactor preprocessing. Minor ↵ajreynol
improvement to sets.
2016-11-03Make data points accurate in sep logic models.ajreynol
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + ↵ajreynol
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-11-02Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ajreynol
Fix a few more memory leaks.
2016-09-14Lemma cache in theory sep. Minor optimization for sets. Minor improvements ↵ajreynol
to EPR
2016-09-12Prefer non-cardinality constants in term models for sep logic.ajreynol
2016-09-12Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry ↵ajreynol
breaking in theory sep.
2016-09-09Support 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-08Refactor seplog preprocess. Handle case where sep data type cannot be inferred.ajreynol
2016-08-25Minor cleanup preprocessing, add ppNotifyAssertions.ajreynol
2016-07-20Infrastructure for storing and printing heap models for separation logic. ↵ajreynol
Ensure value of sep.nil is correct in models. Print instantiations as sexprs.
2016-07-20Infer conflicts in strings based on abstracting equality as contains. Minor ↵ajreynol
cleanup.
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-07-05Refactor last call for theories, only create one model when quantifiers are ↵ajreynol
enabled. Fix sep.nil preregistration in TheorySep.
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback