summaryrefslogtreecommitdiff
path: root/src/theory/sep/kinds
AgeCommit message (Collapse)Author
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2020-08-21Remove spurious theory methods calls (#4931)Andrew Reynolds
This PR removes spurious theory method calls that are not implemented. It also renames a common "propagate(TNode lit)" pattern to "propagateLit(TNode lit)" to avoid confusion with "propagate(Effort e)".
2018-09-18Decision strategy: incorporate separation logic. (#2494)Andrew Reynolds
2017-04-12Add nullary operator metakind.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil ↵ajreynol
nodes.
2016-12-01Improvement and bug fix for str.indexof reduction, add regression. Other ↵ajreynol
minor changes.
2016-11-08Add a few options to separation logic and sets. Minor changes to separation ↵ajreynol
logic, change syntax for empty heap constraint.
2016-06-20Minor change to sep/kindsajreynol
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