projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7f079d6) | patch
Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiat...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 26 May 2016 19:51:01 +0000 (14:51 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 26 May 2016 19:51:11 +0000 (14:51 -0500)
commit28b20948a3b236bf32ca399e2cd85b09c1e57e67
tree54319cbb8b27a94240ef5cfcd53bc0d7fb0c9fe4tree
parent7f079d6d88fc6e7e5c73eb4bfa9cb42e6930c224commit | diff
Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
contrib/run-script-smtcomp2016 diff | blob | history
src/theory/quantifiers/alpha_equivalence.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 [new file with mode: 0644] blob