projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 082ffea) | patch
Implement -o subs to show learned top-level substitutions (#7944)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Jan 2022 22:17:57 +0000 (16:17 -0600)
committerGitHub <noreply@github.com>
Fri, 14 Jan 2022 22:17:57 +0000 (22:17 +0000)
commit7c0191f914405b6f88eba838af101e045de2d933
tree2bd23ebb6e3b3d8102311bf8e2ed9b4ca2dfa2a2tree
parent082ffeaffc2975da6da574e0f0ed65a007691a18commit | diff
Implement -o subs to show learned top-level substitutions (#7944)

Also adds substitutions as part of the output of -o learned-lits for completeness.
src/options/base_options.toml diff | blob | history
src/preprocessing/passes/non_clausal_simp.cpp diff | blob | history
src/preprocessing/preprocessing_pass_context.cpp diff | blob | history
src/preprocessing/preprocessing_pass_context.h diff | blob | history
src/theory/substitutions.cpp diff | blob | history
src/theory/substitutions.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/printer/print_subs.smt2 [new file with mode: 0644] blob