git.libre-soc.org Git - cvc5.git/commit

author	Mathias Preiner <mathias.preiner@gmail.com>
	Wed, 7 Mar 2018 00:54:06 +0000 (16:54 -0800)
committer	GitHub <noreply@github.com>
	Wed, 7 Mar 2018 00:54:06 +0000 (16:54 -0800)
commit	c6b2e085d4eb2c232a528a96e13fc7b65fd98fea
tree	632708f158acc6a3b5b3201212fa2ba1a0606c30	tree
parent	612bb0013f180a7d414f0a4b1e770aaa7ed09152	commit \| diff

Make statistics output consistent. (#1647)

* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").

36 files changed:

examples/sets-translate/sets_translate.cpp		diff \| blob \| history
src/expr/kind_template.cpp		diff \| blob \| history
src/expr/kind_template.h		diff \| blob \| history
src/expr/mkkind		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/proof/array_proof.cpp		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/theory_proof.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arrays/kinds		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/bv/abstraction.cpp		diff \| blob \| history
src/theory/bv/bv_quick_check.cpp		diff \| blob \| history
src/theory/bv/bv_quick_check.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_to_bool.cpp		diff \| blob \| history
src/theory/bv/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/slicer.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/util/statistics.cpp		diff \| blob \| history

RSS Atom