diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-06 16:58:16 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-10 18:47:35 -0600 |
commit | 726603e0e5a5482cf98538079790747e43313276 (patch) | |
tree | 12e41e99a21a16cf9cff7374a84d9a6527f03c8b /src/theory/quantifiers | |
parent | 6c6f44c32a6bb957c1e82ae75fbf62db2e286595 (diff) |
Flatten libcvc4 build structure; remove some #include interdependences
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/Makefile | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/Makefile.am | 62 | ||||
-rwxr-xr-x | src/theory/quantifiers/symmetry_breaking.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 1 |
5 files changed, 3 insertions, 66 deletions
diff --git a/src/theory/quantifiers/Makefile b/src/theory/quantifiers/Makefile deleted file mode 100644 index 8ffdfb575..000000000 --- a/src/theory/quantifiers/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/quantifiers - -include $(topdir)/Makefile.subdir diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am deleted file mode 100644 index be24d6c67..000000000 --- a/src/theory/quantifiers/Makefile.am +++ /dev/null @@ -1,62 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libquantifiers.la - -libquantifiers_la_SOURCES = \ - theory_quantifiers_type_rules.h \ - theory_quantifiers.h \ - quantifiers_rewriter.h \ - quantifiers_rewriter.cpp \ - theory_quantifiers.cpp \ - instantiation_engine.h \ - instantiation_engine.cpp \ - trigger.h \ - trigger.cpp \ - candidate_generator.h \ - candidate_generator.cpp \ - inst_match.h \ - inst_match.cpp \ - model_engine.h \ - model_engine.cpp \ - modes.cpp \ - modes.h \ - term_database.h \ - term_database.cpp \ - first_order_model.h \ - first_order_model.cpp \ - model_builder.h \ - model_builder.cpp \ - quantifiers_attributes.h \ - quantifiers_attributes.cpp \ - inst_gen.h \ - inst_gen.cpp \ - quant_util.h \ - quant_util.cpp \ - inst_match_generator.h \ - inst_match_generator.cpp \ - macros.h \ - macros.cpp \ - inst_strategy_e_matching.h \ - inst_strategy_e_matching.cpp \ - inst_strategy_cbqi.h \ - inst_strategy_cbqi.cpp \ - full_model_check.h \ - full_model_check.cpp \ - bounded_integers.h \ - bounded_integers.cpp \ - first_order_reasoning.h \ - first_order_reasoning.cpp \ - rewrite_engine.h \ - rewrite_engine.cpp \ - relevant_domain.h \ - relevant_domain.cpp \ - symmetry_breaking.h \ - symmetry_breaking.cpp - - -EXTRA_DIST = \ - kinds \ - options_handlers.h diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index 05461d378..7f6855fea 100755 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -29,6 +29,7 @@ #include "util/sort_inference.h" #include "context/context.h" #include "context/context_mm.h" +#include "context/cdhashmap.h" #include "context/cdchunk_list.h" namespace CVC4 { diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 1688479f3..177d8b230 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -17,6 +17,7 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H +#include "expr/attribute.h" #include "theory/theory.h" #include <map> diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index fb599e2a0..8ebde136d 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -19,6 +19,7 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H +#include "context/cdhashmap.h" #include "theory/theory.h" #include "util/hash.h" #include "util/statistics_registry.h" |