projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dce6be1) | patch
ensure that get-value and get-model are consistent, rewrite function value bodies...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 13 Sep 2012 20:39:13 +0000 (20:39 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 13 Sep 2012 20:39:13 +0000 (20:39 +0000)
commit01dfa806851502267e1032483fec48e8b4373634
tree8103a5a5a763fecfc42793bf5c3c88290bff775btree
parentdce6be13f8eb90006c7ceb8d43a8a78da23ca838commit | diff
ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output
src/smt/smt_engine.cpp diff | blob | history
src/theory/model.cpp diff | blob | history
src/theory/model.h diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/first_order_model.h diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf_model.h diff | blob | history