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

projects / cvc5.git / commit

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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 12 Jan 2022 23:28:02 +0000 (17:28 -0600)
committer	GitHub <noreply@github.com>
	Wed, 12 Jan 2022 23:28:02 +0000 (23:28 +0000)
commit	14155a4a00177a496eb48df0d50e38e2190908c3
tree	f4d3b53c2fbd0994dbead4785f549070681c4a95	tree
parent	defb0de81171b6633e5ef745f927217614a4fe54	commit \| diff

Add -o learned-lits to output learned literals (#7934)

Prints both literals learned during preprocessing, and during search.

This feature was recently requested by Cetora.

14 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/options/base_options.toml		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/prop/zero_level_learner.cpp	[new file with mode: 0644]	blob
src/prop/zero_level_learner.h	[new file with mode: 0644]	blob
src/smt/preprocessor.cpp		diff \| blob \| history
src/smt/preprocessor.h		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/theory/substitutions.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/printer/learned-lit-output.smt2	[new file with mode: 0644]	blob