Some work on the dump infrastructure to support portfolio work.
authorMorgan Deters <mdeters@gmail.com>
Fri, 9 Mar 2012 21:10:17 +0000 (21:10 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 9 Mar 2012 21:10:17 +0000 (21:10 +0000)
commit84f26af22566f7c10dea45b399b944cb50b5e317
tree68fbe22665cc09f46c321c6132e49dabbc15c337
parentf29ea80fb3e238278a721d79077c9087bccbac0b
Some work on the dump infrastructure to support portfolio work.

  Dump("foo") << FooCommand(...);

now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.

If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run.  This is done even if the muzzle is on.

This commit also cleans up some code that used the dump feature (in arrays,
particularly).
22 files changed:
configure.ac
src/expr/command.cpp
src/expr/command.h
src/main/driver.cpp
src/main/driver_portfolio.cpp
src/prop/cnf_stream.cpp
src/prop/minisat/core/Solver.cc
src/prop/minisat/core/Solver.h
src/prop/prop_engine.cpp
src/smt/smt_engine.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/util/Makefile.am
src/util/dump.cpp [new file with mode: 0644]
src/util/dump.h [new file with mode: 0644]
src/util/ite_removal.cpp
src/util/ite_removal.h
src/util/options.cpp
src/util/output.cpp
src/util/output.h