diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2018-08-25 14:31:32 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-25 14:31:32 -0700 |
| commit | c66033a67511b10b5ee22b7072b9ceab45552a79 (patch) | |
| tree | 3c313868e6b10ee4caa11bc017e65fde0c0ee11f /src/Makefile.am | |
| parent | 7b9c2529c149a9cd046083af401cbdeadf406804 (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.
Diffstat (limited to 'src/Makefile.am')
| -rw-r--r-- | src/Makefile.am | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index d399602cb..e0a9fb807 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -95,6 +95,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bv_to_bool.h \ preprocessing/passes/quantifiers_preprocess.cpp \ preprocessing/passes/quantifiers_preprocess.h \ + preprocessing/passes/quantifier_macros.cpp \ + preprocessing/passes/quantifier_macros.h \ preprocessing/passes/real_to_int.cpp \ preprocessing/passes/real_to_int.h \ preprocessing/passes/rewrite.cpp \ @@ -482,8 +484,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/lazy_trie.h \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/local_theory_ext.h \ - theory/quantifiers/macros.cpp \ - theory/quantifiers/macros.h \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/quant_conflict_find.h \ theory/quantifiers/quant_epr.cpp \ |