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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Thu, 20 Feb 2020 00:59:58 +0000 (16:59 -0800)
committer	GitHub <noreply@github.com>
	Thu, 20 Feb 2020 00:59:58 +0000 (16:59 -0800)
commit	508ecb3007a2b6aa8b76b28dc8282247b5dba957
tree	b80cab956e6b40b4cd783ceb78393006c09782b5	tree
parent	9705504973f6f85c6be4944c615984df7b614f67	commit \| diff

resource manager: Add statistic for every resource. (#3772)

This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).

Fixes #3751.

52 files changed:

src/bindings/java/CMakeLists.txt		diff \| blob \| history
src/cvc4.i		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/expr/expr_manager.i		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/preprocessing/passes/apply_substs.cpp		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.cpp		diff \| blob \| history
src/preprocessing/passes/ite_removal.cpp		diff \| blob \| history
src/preprocessing/passes/ite_simp.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/static_learning.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.h		diff \| blob \| history
src/prop/bv_sat_solver_notify.h		diff \| blob \| history
src/prop/bvminisat/bvminisat.h		diff \| blob \| history
src/prop/bvminisat/core/Solver.cc		diff \| blob \| history
src/prop/bvminisat/core/Solver.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/bv/bitblast/bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_eager_solver.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_test_utils.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/util/resource_manager.cpp		diff \| blob \| history
src/util/resource_manager.h		diff \| blob \| history
src/util/resource_manager.i	[deleted file]	blob \| history
test/unit/theory/theory_white.h		diff \| blob \| history

RSS Atom