projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9ac1cb1) | patch
Added map from skolem variables to new ite formulas in ite removal.
authorClark Barrett <barrett@cs.nyu.edu>
Mon, 30 Apr 2012 14:42:28 +0000 (14:42 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Mon, 30 Apr 2012 14:42:28 +0000 (14:42 +0000)
commit97555307af3415d6fbbac3fc9dccdafec51056b7
tree56b47f809268d5b8ae21594d22cbec7ced8f46aatree
parent9ac1cb18f03a5edf4b50532d29e195f74d6a83c2commit | diff
Added map from skolem variables to new ite formulas in ite removal.
d_sharedTermsExist is now set based on logicInfo instead of dynamically when
shared terms are found.
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/util/ite_removal.cpp diff | blob | history
src/util/ite_removal.h diff | blob | history