projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3075a8e) | patch
Function definition fmf preprocessing pass (#5064)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 24 Sep 2020 20:02:04 +0000 (15:02 -0500)
committerGitHub <noreply@github.com>
Thu, 24 Sep 2020 20:02:04 +0000 (15:02 -0500)
commit3538f6f4700b3fa357e1c767ee6cd42be87a78b8
treecbc571c8a41e7ec330b6679b7f64b2920f1a939ftree
parent3075a8e20dba6a784316714543c8a1b262459d9acommit | diff
 Function definition fmf preprocessing pass (#5064)

This defines the function definition finite model finding as a proper preprocessing pass.

This is required for cleaning/fixing bugs in the preprocessor on proof-new.

There are no intended behavior changes in this PR, although the code for the pass was updated to the new style guidelines.
src/CMakeLists.txt diff | blob | history
src/preprocessing/passes/fun_def_fmf.cpp [new file with mode: 0644] blob
src/preprocessing/passes/fun_def_fmf.h [new file with mode: 0644] blob
src/preprocessing/preprocessing_pass_registry.cpp diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
src/smt/process_assertions.h diff | blob | history
src/theory/quantifiers/fmf/model_builder.cpp diff | blob | history
src/theory/quantifiers/fun_def_process.cpp [deleted file] blob | history
src/theory/quantifiers/fun_def_process.h [deleted file] blob | history
src/theory/quantifiers/quantifiers_attributes.h diff | blob | history