Adding an option to the equality engine constructor to treat all constants as
authorDejan Jovanovic <dejan.jovanovic@gmail.com>
Sat, 27 Dec 2014 03:15:13 +0000 (19:15 -0800)
committerDejan Jovanovic <dejan.jovanovic@gmail.com>
Sat, 27 Dec 2014 03:15:13 +0000 (19:15 -0800)
commit0c624b4f57c5f1bc3c94058fe5b1da4bdd724041
treed582a79203d9cc8f6ace757b8f9a729102d9f657
parent9e50f189118d5f8bb0f7eb54f19677e52f5a3852
Adding an option to the equality engine constructor to treat all constants as
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.
14 files changed:
.cproject
src/theory/arith/congruence_manager.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/bv_subtheory_core.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/sets/theory_sets_private.cpp
src/theory/shared_terms_database.cpp
src/theory/strings/theory_strings.cpp
src/theory/theory_engine.cpp
src/theory/theory_model.cpp
src/theory/uf/equality_engine.cpp
src/theory/uf/equality_engine.h
src/theory/uf/theory_uf.cpp