projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7bc8ebe) | patch
Refactor quantifiers macros (#6348)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 13 Apr 2021 20:38:36 +0000 (15:38 -0500)
committerGitHub <noreply@github.com>
Tue, 13 Apr 2021 20:38:36 +0000 (20:38 +0000)
commitf7dcb4875bba33b7712732a874581639681926f8
treea9591152675088a259d0c6ebb7c832df62246a99tree
parent7bc8ebe940cf092d66265040db48c1e4b486c73fcommit | diff
Refactor quantifiers macros (#6348)

This does some refactoring of quantifiers macros preprocessing pass to use up-to-date utility methods, including lambdas, substitutions, methods for getting free variables.

This is work towards adding proofs for macros.
src/preprocessing/passes/quantifier_macros.cpp diff | blob | history
src/preprocessing/passes/quantifier_macros.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 [new file with mode: 0644] blob