projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7b9c252) | patch
Refactor quantifier macros preprocessing pass (#1840)
authoryoni206 <yoni206@users.noreply.github.com>
Sat, 25 Aug 2018 21:31:32 +0000 (14:31 -0700)
committerAndres Noetzli <andres.noetzli@gmail.com>
Sat, 25 Aug 2018 21:31:32 +0000 (14:31 -0700)
commitc66033a67511b10b5ee22b7072b9ceab45552a79
tree3c313868e6b10ee4caa11bc017e65fde0c0ee11ftree
parent7b9c2529c149a9cd046083af401cbdeadf406804commit | diff
Refactor quantifier macros preprocessing pass (#1840)

Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`,
and added the necessary methods for inheritance from PreprocessingPass.

No need to add a test - regress0 fails when adding Assert(false) when assertions had changed.
src/Makefile.am diff | blob | history
src/preprocessing/passes/quantifier_macros.cpp [new file with mode: 0644] blob
src/preprocessing/passes/quantifier_macros.h [new file with mode: 0644] blob
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/macros.cpp [deleted file] blob | history
src/theory/quantifiers/macros.h [deleted file] blob | history