From ad4298296a1d0a93e63fbfdbdc1cc7d0032fafd8 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 6 Nov 2013 16:58:16 -0500 Subject: Flatten libcvc4 build structure; remove some #include interdependences --- src/theory/Makefile | 4 - src/theory/Makefile.am | 111 --------------------- src/theory/Makefile.subdirs | 4 +- src/theory/arith/Makefile | 4 - src/theory/arith/Makefile.am | 72 ------------- src/theory/arrays/Makefile | 4 - src/theory/arrays/Makefile.am | 22 ---- src/theory/arrays/theory_arrays_rewriter.cpp | 49 +++++++++ src/theory/arrays/theory_arrays_rewriter.h | 16 ++- src/theory/arrays/theory_arrays_type_rules.h | 8 +- src/theory/booleans/Makefile | 4 - src/theory/booleans/Makefile.am | 22 ---- src/theory/builtin/Makefile | 4 - src/theory/builtin/Makefile.am | 17 ---- src/theory/bv/Makefile | 4 - src/theory/bv/Makefile.am | 44 -------- src/theory/datatypes/Makefile | 4 - src/theory/datatypes/Makefile.am | 16 --- src/theory/datatypes/datatypes_rewriter.h | 1 + src/theory/datatypes/theory_datatypes_type_rules.h | 2 +- src/theory/example/Makefile | 4 - src/theory/example/Makefile.am | 14 --- src/theory/idl/Makefile | 4 - src/theory/idl/Makefile.am | 19 ---- src/theory/quantifiers/Makefile | 4 - src/theory/quantifiers/Makefile.am | 62 ------------ src/theory/quantifiers/symmetry_breaking.h | 1 + src/theory/quantifiers/term_database.h | 1 + src/theory/quantifiers/theory_quantifiers.h | 1 + src/theory/rewriter.h | 2 +- src/theory/rewriter_attributes.h | 2 + src/theory/rewriterules/Makefile | 4 - src/theory/rewriterules/Makefile.am | 28 ------ src/theory/strings/Makefile | 4 - src/theory/strings/Makefile.am | 21 ---- src/theory/theory.h | 2 +- src/theory/uf/Makefile | 4 - src/theory/uf/Makefile.am | 25 ----- src/theory/uf/equality_engine.h | 1 + src/theory/uf/theory_uf.h | 2 +- src/theory/uf/theory_uf_model.cpp | 1 + src/theory/uf/theory_uf_strong_solver.h | 1 + 42 files changed, 74 insertions(+), 545 deletions(-) delete mode 100644 src/theory/Makefile delete mode 100644 src/theory/Makefile.am delete mode 100644 src/theory/arith/Makefile delete mode 100644 src/theory/arith/Makefile.am delete mode 100644 src/theory/arrays/Makefile delete mode 100644 src/theory/arrays/Makefile.am create mode 100644 src/theory/arrays/theory_arrays_rewriter.cpp delete mode 100644 src/theory/booleans/Makefile delete mode 100644 src/theory/booleans/Makefile.am delete mode 100644 src/theory/builtin/Makefile delete mode 100644 src/theory/builtin/Makefile.am delete mode 100644 src/theory/bv/Makefile delete mode 100644 src/theory/bv/Makefile.am delete mode 100644 src/theory/datatypes/Makefile delete mode 100644 src/theory/datatypes/Makefile.am delete mode 100644 src/theory/example/Makefile delete mode 100644 src/theory/example/Makefile.am delete mode 100644 src/theory/idl/Makefile delete mode 100644 src/theory/idl/Makefile.am delete mode 100644 src/theory/quantifiers/Makefile delete mode 100644 src/theory/quantifiers/Makefile.am delete mode 100644 src/theory/rewriterules/Makefile delete mode 100644 src/theory/rewriterules/Makefile.am delete mode 100644 src/theory/strings/Makefile delete mode 100644 src/theory/strings/Makefile.am delete mode 100644 src/theory/uf/Makefile delete mode 100644 src/theory/uf/Makefile.am (limited to 'src/theory') diff --git a/src/theory/Makefile b/src/theory/Makefile deleted file mode 100644 index da7d0e6b9..000000000 --- a/src/theory/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/theory - -include $(topdir)/Makefile.subdir diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am deleted file mode 100644 index 860075aa8..000000000 --- a/src/theory/Makefile.am +++ /dev/null @@ -1,111 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules idl strings -DIST_SUBDIRS = $(SUBDIRS) example - -noinst_LTLIBRARIES = libtheory.la - -libtheory_la_SOURCES = \ - decision_attributes.h \ - logic_info.h \ - logic_info.cpp \ - output_channel.h \ - interrupted.h \ - type_enumerator.h \ - theory_engine.h \ - theory_engine.cpp \ - theory_test_utils.h \ - theory.h \ - theory.cpp \ - theoryof_mode.h \ - theory_registrar.h \ - rewriter.h \ - rewriter_attributes.h \ - rewriter.cpp \ - substitutions.h \ - substitutions.cpp \ - valuation.h \ - valuation.cpp \ - shared_terms_database.h \ - shared_terms_database.cpp \ - term_registration_visitor.h \ - term_registration_visitor.cpp \ - ite_simplifier.h \ - ite_simplifier.cpp \ - unconstrained_simplifier.h \ - unconstrained_simplifier.cpp \ - quantifiers_engine.h \ - quantifiers_engine.cpp \ - model.h \ - model.cpp \ - rep_set.h \ - rep_set.cpp \ - atom_requests.h \ - atom_requests.cpp - -nodist_libtheory_la_SOURCES = \ - rewriter_tables.h \ - theory_traits.h \ - type_enumerator.cpp - -libtheory_la_LIBADD = \ - @builddir@/builtin/libbuiltin.la \ - @builddir@/booleans/libbooleans.la \ - @builddir@/uf/libuf.la \ - @builddir@/arith/libarith.la \ - @builddir@/arrays/libarrays.la \ - @builddir@/bv/libbv.la \ - @builddir@/datatypes/libdatatypes.la \ - @builddir@/quantifiers/libquantifiers.la \ - @builddir@/rewriterules/librewriterules.la \ - @builddir@/idl/libidl.la \ - @builddir@/strings/libstrings.la - -EXTRA_DIST = \ - logic_info.i \ - options_handlers.h \ - rewriter_tables_template.h \ - theory_traits_template.h \ - type_enumerator_template.cpp \ - mktheorytraits \ - mkrewriter \ - Makefile.subdirs - -BUILT_SOURCES = \ - rewriter_tables.h \ - theory_traits.h \ - type_enumerator.cpp - -CLEANFILES = \ - rewriter_tables.h \ - theory_traits.h \ - type_enumerator.cpp - -include @top_srcdir@/src/theory/Makefile.subdirs - -rewriter_tables.h: rewriter_tables_template.h mkrewriter @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkrewriter - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkrewriter \ - $< \ - `cat @top_builddir@/src/theory/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mktheorytraits - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mktheorytraits \ - $< \ - `cat @top_builddir@/src/theory/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -type_enumerator.cpp: type_enumerator_template.cpp mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mktheorytraits - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mktheorytraits \ - $< \ - `cat @top_builddir@/src/theory/.subdirs` \ - > $@) || (rm -f $@ && exit 1) diff --git a/src/theory/Makefile.subdirs b/src/theory/Makefile.subdirs index 99adc7d0d..9dbe458df 100644 --- a/src/theory/Makefile.subdirs +++ b/src/theory/Makefile.subdirs @@ -1,5 +1,5 @@ -$(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/theory/Makefile.am - $(AM_V_at)grep '^SUBDIRS = ' $(top_srcdir)/src/theory/Makefile.am | cut -d' ' -f3- | tr ' ' "\n" | xargs -I__D__ echo $(top_srcdir)/src/theory/__D__/kinds >$(top_builddir)/src/theory/.subdirs.tmp +$(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/Makefile.am + $(AM_V_at)grep '^THEORIES = ' $(top_srcdir)/src/Makefile.am | cut -d' ' -f3- | tr ' ' "\n" | xargs -I__D__ echo $(top_srcdir)/src/theory/__D__/kinds >$(top_builddir)/src/theory/.subdirs.tmp @if ! diff -q $(top_builddir)/src/theory/.subdirs $(top_builddir)/src/theory/.subdirs.tmp &>/dev/null; then \ echo " GEN " $@; \ $(am__mv) $(top_builddir)/src/theory/.subdirs.tmp $(top_builddir)/src/theory/.subdirs; \ diff --git a/src/theory/arith/Makefile b/src/theory/arith/Makefile deleted file mode 100644 index 5016522e8..000000000 --- a/src/theory/arith/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/arith - -include $(topdir)/Makefile.subdir diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am deleted file mode 100644 index 620b8a121..000000000 --- a/src/theory/arith/Makefile.am +++ /dev/null @@ -1,72 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libarith.la - -libarith_la_SOURCES = \ - theory_arith_type_rules.h \ - type_enumerator.h \ - arithvar.h \ - arithvar.cpp \ - bound_counts.h \ - arith_rewriter.h \ - arith_rewriter.cpp \ - arith_static_learner.h \ - arith_static_learner.cpp \ - constraint_forward.h \ - constraint.h \ - constraint.cpp \ - congruence_manager.h \ - congruence_manager.cpp \ - normal_form.h\ - normal_form.cpp \ - arith_utilities.h \ - delta_rational.h \ - delta_rational.cpp \ - partial_model.h \ - partial_model.cpp \ - linear_equality.h \ - linear_equality.cpp \ - simplex_update.h \ - simplex_update.cpp \ - callbacks.h \ - callbacks.cpp \ - matrix.h \ - matrix.cpp \ - tableau.h \ - tableau.cpp \ - tableau_sizes.h \ - tableau_sizes.cpp \ - error_set.h \ - error_set.cpp \ - simplex.h \ - simplex.cpp \ - dual_simplex.h \ - dual_simplex.cpp \ - fc_simplex.h \ - fc_simplex.cpp \ - soi_simplex.h \ - soi_simplex.cpp \ - approx_simplex.h \ - approx_simplex.cpp \ - attempt_solution_simplex.h \ - attempt_solution_simplex.cpp \ - theory_arith.h \ - theory_arith.cpp \ - theory_arith_private_forward.h \ - theory_arith_private.h \ - theory_arith_private.cpp \ - dio_solver.h \ - dio_solver.cpp \ - arith_heuristic_pivot_rule.h \ - arith_heuristic_pivot_rule.cpp \ - arith_unate_lemma_mode.h \ - arith_unate_lemma_mode.cpp \ - arith_propagation_mode.h \ - arith_propagation_mode.cpp - -EXTRA_DIST = \ - kinds \ - options_handlers.h diff --git a/src/theory/arrays/Makefile b/src/theory/arrays/Makefile deleted file mode 100644 index bce529db0..000000000 --- a/src/theory/arrays/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/arrays - -include $(topdir)/Makefile.subdir diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am deleted file mode 100644 index 77f102cf8..000000000 --- a/src/theory/arrays/Makefile.am +++ /dev/null @@ -1,22 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libarrays.la - -libarrays_la_SOURCES = \ - theory_arrays_type_rules.h \ - type_enumerator.h \ - theory_arrays_rewriter.h \ - theory_arrays.h \ - theory_arrays.cpp \ - union_find.h \ - union_find.cpp \ - array_info.h \ - array_info.cpp \ - static_fact_manager.h \ - static_fact_manager.cpp - -EXTRA_DIST = \ - kinds diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp new file mode 100644 index 000000000..d926cd7a2 --- /dev/null +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -0,0 +1,49 @@ +/********************* */ +/*! \file theory_arrays_rewriter.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "expr/attribute.h" +#include "theory/arrays/theory_arrays_rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +namespace attr { + struct ArrayConstantMostFrequentValueTag { }; + struct ArrayConstantMostFrequentValueCountTag { }; +}/* CVC4::theory::arrays::attr namespace */ + +typedef expr::Attribute ArrayConstantMostFrequentValueCountAttr; +typedef expr::Attribute ArrayConstantMostFrequentValueAttr; + +Node getMostFrequentValue(TNode store) { + return store.getAttribute(ArrayConstantMostFrequentValueAttr()); +} +uint64_t getMostFrequentValueCount(TNode store) { + return store.getAttribute(ArrayConstantMostFrequentValueCountAttr()); +} + +void setMostFrequentValue(TNode store, TNode value) { + return store.setAttribute(ArrayConstantMostFrequentValueAttr(), value); +} +void setMostFrequentValueCount(TNode store, uint64_t count) { + return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count); +} + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 5df06bda8..388769412 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -22,19 +22,15 @@ #include "theory/rewriter.h" #include "theory/type_enumerator.h" -#include "expr/attribute.h" namespace CVC4 { namespace theory { namespace arrays { -namespace attr { - struct ArrayConstantMostFrequentValueTag { }; - struct ArrayConstantMostFrequentValueCountTag { }; -}/* CVC4::theory::arrays::attr namespace */ - -typedef expr::Attribute ArrayConstantMostFrequentValueCountAttr; -typedef expr::Attribute ArrayConstantMostFrequentValueAttr; +Node getMostFrequentValue(TNode store); +uint64_t getMostFrequentValueCount(TNode store); +void setMostFrequentValue(TNode store, TNode value); +void setMostFrequentValueCount(TNode store, uint64_t count); static inline Node mkEqNode(Node a, Node b) { return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b); @@ -132,8 +128,8 @@ public: unsigned mostFrequentValueCount = 0; store = node[0]; if (store.getKind() == kind::STORE) { - mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr()); - mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr()); + mostFrequentValue = getMostFrequentValue(store); + mostFrequentValueCount = getMostFrequentValueCount(store); } // Compute the most frequently written value for n diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index b16b62f69..9f7bdfd4a 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -127,8 +127,8 @@ struct ArrayStoreTypeRule { unsigned mostFrequentValueCount = 0; store = n[0]; if (store.getKind() == kind::STORE) { - mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr()); - mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr()); + mostFrequentValue = getMostFrequentValue(store); + mostFrequentValueCount = getMostFrequentValueCount(store); } // Compute the most frequently written value for n @@ -145,8 +145,8 @@ struct ArrayStoreTypeRule { (compare == Cardinality::EQUAL && (!(defaultValue < mostFrequentValue)))) { return false; } - n.setAttribute(ArrayConstantMostFrequentValueAttr(), mostFrequentValue); - n.setAttribute(ArrayConstantMostFrequentValueCountAttr(), mostFrequentValueCount); + setMostFrequentValue(n, mostFrequentValue); + setMostFrequentValueCount(n, mostFrequentValueCount); return true; } diff --git a/src/theory/booleans/Makefile b/src/theory/booleans/Makefile deleted file mode 100644 index a74a72d83..000000000 --- a/src/theory/booleans/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/bool - -include $(topdir)/Makefile.subdir diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am deleted file mode 100644 index 9d58ffa75..000000000 --- a/src/theory/booleans/Makefile.am +++ /dev/null @@ -1,22 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libbooleans.la - -libbooleans_la_SOURCES = \ - type_enumerator.h \ - theory_bool.h \ - theory_bool.cpp \ - theory_bool_type_rules.h \ - theory_bool_rewriter.h \ - theory_bool_rewriter.cpp \ - circuit_propagator.h \ - circuit_propagator.cpp \ - boolean_term_conversion_mode.h \ - boolean_term_conversion_mode.cpp - -EXTRA_DIST = \ - kinds \ - options_handlers.h diff --git a/src/theory/builtin/Makefile b/src/theory/builtin/Makefile deleted file mode 100644 index 1dfd8a113..000000000 --- a/src/theory/builtin/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/builtin - -include $(topdir)/Makefile.subdir diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am deleted file mode 100644 index 6ff00feb6..000000000 --- a/src/theory/builtin/Makefile.am +++ /dev/null @@ -1,17 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libbuiltin.la - -libbuiltin_la_SOURCES = \ - theory_builtin_type_rules.h \ - type_enumerator.h \ - theory_builtin_rewriter.h \ - theory_builtin_rewriter.cpp \ - theory_builtin.h \ - theory_builtin.cpp - -EXTRA_DIST = \ - kinds diff --git a/src/theory/bv/Makefile b/src/theory/bv/Makefile deleted file mode 100644 index 797408368..000000000 --- a/src/theory/bv/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/bv - -include $(topdir)/Makefile.subdir diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am deleted file mode 100644 index 8651f280b..000000000 --- a/src/theory/bv/Makefile.am +++ /dev/null @@ -1,44 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libbv.la - -libbv_la_SOURCES = \ - theory_bv_utils.h \ - type_enumerator.h \ - bitblaster.h \ - bitblaster.cpp \ - bv_to_bool.h \ - bv_to_bool.cpp \ - bv_subtheory.h \ - bv_subtheory_core.h \ - bv_subtheory_core.cpp \ - bv_subtheory_bitblast.h \ - bv_subtheory_bitblast.cpp \ - bv_subtheory_inequality.h \ - bv_subtheory_inequality.cpp \ - bv_inequality_graph.h \ - bv_inequality_graph.cpp \ - bitblast_strategies.h \ - bitblast_strategies.cpp \ - slicer.h \ - slicer.cpp \ - theory_bv.h \ - theory_bv.cpp \ - theory_bv_rewrite_rules.h \ - theory_bv_rewrite_rules_core.h \ - theory_bv_rewrite_rules_operator_elimination.h \ - theory_bv_rewrite_rules_constant_evaluation.h \ - theory_bv_rewrite_rules_normalization.h \ - theory_bv_rewrite_rules_simplification.h \ - theory_bv_type_rules.h \ - theory_bv_rewriter.h \ - theory_bv_rewriter.cpp \ - cd_set_collection.h - -EXTRA_DIST = \ - kinds diff --git a/src/theory/datatypes/Makefile b/src/theory/datatypes/Makefile deleted file mode 100644 index cb3da4be3..000000000 --- a/src/theory/datatypes/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/datatypes - -include $(topdir)/Makefile.subdir diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am deleted file mode 100644 index 8b788b73b..000000000 --- a/src/theory/datatypes/Makefile.am +++ /dev/null @@ -1,16 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libdatatypes.la - -libdatatypes_la_SOURCES = \ - theory_datatypes_type_rules.h \ - type_enumerator.h \ - theory_datatypes.h \ - datatypes_rewriter.h \ - theory_datatypes.cpp - -EXTRA_DIST = \ - kinds diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 0bbef1601..37a656555 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -22,6 +22,7 @@ #include "theory/rewriter.h" #include "theory/datatypes/options.h" #include "theory/type_enumerator.h" +#include "expr/node_manager_attributes.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index d3efc636f..527d110e0 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -20,7 +20,7 @@ #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H #include "util/matcher.h" -#include "expr/attribute.h" +//#include "expr/attribute.h" namespace CVC4 { diff --git a/src/theory/example/Makefile b/src/theory/example/Makefile deleted file mode 100644 index be6721f80..000000000 --- a/src/theory/example/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/example - -include $(topdir)/Makefile.subdir diff --git a/src/theory/example/Makefile.am b/src/theory/example/Makefile.am deleted file mode 100644 index 801a048a8..000000000 --- a/src/theory/example/Makefile.am +++ /dev/null @@ -1,14 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libexample.la - -libexample_la_SOURCES = \ - ecdata.h \ - ecdata.cpp \ - theory_uf_tim.h \ - theory_uf_tim.cpp - -EXTRA_DIST = diff --git a/src/theory/idl/Makefile b/src/theory/idl/Makefile deleted file mode 100644 index 75ae33c7e..000000000 --- a/src/theory/idl/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/idl - -include $(topdir)/Makefile.subdir diff --git a/src/theory/idl/Makefile.am b/src/theory/idl/Makefile.am deleted file mode 100644 index 4297e3bdb..000000000 --- a/src/theory/idl/Makefile.am +++ /dev/null @@ -1,19 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libidl.la - -libidl_la_SOURCES = \ - idl_model.h \ - idl_model.cpp \ - idl_assertion.h \ - idl_assertion.cpp \ - idl_assertion_db.h \ - idl_assertion_db.cpp \ - theory_idl.h \ - theory_idl.cpp - -EXTRA_DIST = \ - kinds 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 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" diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 4245ad6f9..e05d97c05 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -19,7 +19,7 @@ #pragma once #include "expr/node.h" -#include "expr/attribute.h" +//#include "expr/attribute.h" namespace CVC4 { namespace theory { diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index 45e83aa63..4c4e33fc6 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -18,6 +18,8 @@ #pragma once +#include "expr/attribute.h" + namespace CVC4 { namespace theory { diff --git a/src/theory/rewriterules/Makefile b/src/theory/rewriterules/Makefile deleted file mode 100644 index 4b1d4fc55..000000000 --- a/src/theory/rewriterules/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/rewriterules - -include $(topdir)/Makefile.subdir diff --git a/src/theory/rewriterules/Makefile.am b/src/theory/rewriterules/Makefile.am deleted file mode 100644 index a1e5771b9..000000000 --- a/src/theory/rewriterules/Makefile.am +++ /dev/null @@ -1,28 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = librewriterules.la - -librewriterules_la_SOURCES = \ - theory_rewriterules_rules.h \ - theory_rewriterules_rules.cpp \ - theory_rewriterules.h \ - theory_rewriterules.cpp \ - theory_rewriterules_rewriter.h \ - theory_rewriterules_type_rules.h \ - theory_rewriterules_preprocess.h \ - theory_rewriterules_params.h \ - rr_inst_match.h \ - rr_inst_match_impl.h \ - rr_inst_match.cpp \ - rr_trigger.h \ - rr_trigger.cpp \ - rr_candidate_generator.h \ - rr_candidate_generator.cpp \ - efficient_e_matching.h \ - efficient_e_matching.cpp - -EXTRA_DIST = \ - kinds diff --git a/src/theory/strings/Makefile b/src/theory/strings/Makefile deleted file mode 100644 index e92c24ab7..000000000 --- a/src/theory/strings/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/strings - -include $(topdir)/Makefile.subdir diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am deleted file mode 100644 index d5e5d1a23..000000000 --- a/src/theory/strings/Makefile.am +++ /dev/null @@ -1,21 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. -AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libstrings.la - -libstrings_la_SOURCES = \ - theory_strings.h \ - theory_strings.cpp \ - theory_strings_rewriter.h \ - theory_strings_rewriter.cpp \ - theory_strings_type_rules.h \ - type_enumerator.h \ - theory_strings_preprocess.h \ - theory_strings_preprocess.cpp \ - regexp_operation.h \ - regexp_operation.cpp - -EXTRA_DIST = \ - kinds diff --git a/src/theory/theory.h b/src/theory/theory.h index 21a5aacf5..fdd2d0518 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -20,7 +20,7 @@ #define __CVC4__THEORY__THEORY_H #include "expr/node.h" -#include "expr/attribute.h" +//#include "expr/attribute.h" #include "expr/command.h" #include "theory/valuation.h" #include "theory/output_channel.h" diff --git a/src/theory/uf/Makefile b/src/theory/uf/Makefile deleted file mode 100644 index c3c641384..000000000 --- a/src/theory/uf/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/uf - -include $(topdir)/Makefile.subdir diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am deleted file mode 100644 index 50c508092..000000000 --- a/src/theory/uf/Makefile.am +++ /dev/null @@ -1,25 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libuf.la - -libuf_la_SOURCES = \ - theory_uf.h \ - theory_uf.cpp \ - theory_uf_type_rules.h \ - theory_uf_rewriter.h \ - equality_engine.h \ - equality_engine_types.h \ - equality_engine.cpp \ - symmetry_breaker.h \ - symmetry_breaker.cpp \ - theory_uf_strong_solver.h \ - theory_uf_strong_solver.cpp \ - theory_uf_model.h \ - theory_uf_model.cpp - -EXTRA_DIST = \ - kinds \ - options_handlers.h diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 8d1b6f1d9..a9294dc69 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -27,6 +27,7 @@ #include "expr/node.h" #include "expr/kind_map.h" #include "context/cdo.h" +#include "context/cdhashmap.h" #include "util/output.h" #include "util/statistics_registry.h" #include "theory/rewriter.h" diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 9ca146bde..2c9b4b7d5 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -21,7 +21,7 @@ #define __CVC4__THEORY__UF__THEORY_UF_H #include "expr/node.h" -#include "expr/attribute.h" +//#include "expr/attribute.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 284212ba9..bf41a256d 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -12,6 +12,7 @@ ** \brief Implementation of Theory UF Model **/ +#include "expr/attribute.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf_model.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 9111ec6a7..079a03c36 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -21,6 +21,7 @@ #include "context/context.h" #include "context/context_mm.h" +#include "context/cdhashmap.h" #include "context/cdchunk_list.h" #include "util/statistics_registry.h" -- cgit v1.2.3