Adding support for a master equality engine. Each theory gets the master equality...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Mon, 26 Nov 2012 17:07:46 +0000 (17:07 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Mon, 26 Nov 2012 17:07:46 +0000 (17:07 +0000)
commit2a731b9164bb178f1232a9af0babc7dd84450cea
tree57d14d55f1bae93737dbee34c737771858572fad
parent164163c9c8fd255947cf3e8d236a5b9da1a1fdab
Adding support for a master equality engine. Each theory gets the master equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit().
22 files changed:
src/smt/smt_engine.cpp
src/theory/arith/congruence_manager.cpp
src/theory/arith/congruence_manager.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/bv/bv_subtheory_eq.cpp
src/theory/bv/bv_subtheory_eq.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
src/theory/uf/equality_engine.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h