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

projects / cvc5.git / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: 2901ee1) | patch

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 19 Nov 2020 12:42:04 +0000 (06:42 -0600)
committer	GitHub <noreply@github.com>
	Thu, 19 Nov 2020 12:42:04 +0000 (06:42 -0600)
commit	b0130a1e032c201fab3c4b19f25871428b761967
tree	f18039906a287a4d55345b1c4bd0ac86cf5232c5	tree
parent	2901ee18f824d1f9e4338ef2853da0ab4ccbff0e	commit \| diff

Use symbol manager for unsat cores (#5468)

This PR uses the symbol manager for handling names for unsat cores.

This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.

14 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/expr/symbol_manager.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/proof/unsat_core.cpp		diff \| blob \| history
src/proof/unsat_core.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/expr_names.cpp	[deleted file]	blob \| history
src/smt/expr_names.h	[deleted file]	blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history