Support for having two SmtEngines with the same ExprManager.
authorMorgan Deters <mdeters@gmail.com>
Mon, 16 Jul 2012 15:53:22 +0000 (15:53 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 16 Jul 2012 15:53:22 +0000 (15:53 +0000)
commit36615c5e7332e26645b33ce9b6bab25439a5108e
tree166efefced107009f4a68ff3d0c6623540dfa435
parent25396f93b7df85c80a39ed207483e28a8c86ff26
Support for having two SmtEngines with the same ExprManager.

Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine.  Otherwise, theories register the
same statistic twice.  This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed.  Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).
22 files changed:
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/node_manager.h
src/main/driver.cpp
src/main/driver_portfolio.cpp
src/smt/Makefile.am
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/smt_engine_scope.cpp [new file with mode: 0644]
src/smt/smt_engine_scope.h [new file with mode: 0644]
src/util/stats.cpp
src/util/stats.h
test/system/Makefile.am
test/system/boilerplate.cpp
test/system/two_smt_engines.cpp [new file with mode: 0644]
test/unit/Makefile.am
test/unit/prop/cnf_stream_black.h [deleted file]
test/unit/prop/cnf_stream_white.h [new file with mode: 0644]
test/unit/theory/theory_arith_white.h
test/unit/theory/theory_black.h [deleted file]
test/unit/theory/theory_engine_white.h
test/unit/theory/theory_white.h [new file with mode: 0644]