projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: daf2eca) | patch
Infrastructure for storing and printing heap models for separation logic. Ensure...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 20 Jul 2016 18:28:01 +0000 (13:28 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 20 Jul 2016 18:28:01 +0000 (13:28 -0500)
commitf827fb06c949d421fb32f6629c2c353ca7bd026e
tree04b3563aa2467784517193dd22ef95f2ce1e612atree
parentdaf2eca9a4bb32680cbf35945bb09cfd13be76a7commit | diff
Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/model.h diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/sep/theory_sep.h diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history