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 | |
| parent | 6c6f44c32a6bb957c1e82ae75fbf62db2e286595 (diff) | |
Flatten libcvc4 build structure; remove some #include interdependences
Diffstat (limited to 'src')
77 files changed, 871 insertions, 1152 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index e6d5f80ed..0bbc49e13 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -14,70 +14,410 @@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ 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) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = lib options expr util context theory prop decision smt printer proof . parser compat bindings main +SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main +THEORIES = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules idl strings lib_LTLIBRARIES = libcvc4.la -if HAVE_CXXTESTGEN -check_LTLIBRARIES = libcvc4_noinst.la -endif libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) # This "tricks" automake into linking us as a C++ library (rather than # as a C library, which messes up exception handling support) -nodist_EXTRA_libcvc4_noinst_la_SOURCES = dummy.cpp nodist_EXTRA_libcvc4_la_SOURCES = dummy.cpp -libcvc4_noinst_la_SOURCES = git_versioninfo.cpp svn_versioninfo.cpp -libcvc4_la_SOURCES = git_versioninfo.cpp svn_versioninfo.cpp +libcvc4_la_SOURCES = \ + git_versioninfo.cpp \ + svn_versioninfo.cpp \ + context/context.cpp \ + context/context.h \ + context/context_mm.cpp \ + context/context_mm.h \ + context/cdo.h \ + context/cdlist.h \ + context/cdchunk_list.h \ + context/cdlist_forward.h \ + context/cdqueue.h \ + context/cdtrail_queue.h \ + context/cdtrail_hashmap.h \ + context/cdtrail_hashmap_forward.h \ + context/cdinsert_hashmap.h \ + context/cdinsert_hashmap_forward.h \ + context/cdhashmap.h \ + context/cdhashmap_forward.h \ + context/cdhashset.h \ + context/cdhashset_forward.h \ + context/cdvector.h \ + context/cdmaybe.h \ + context/stacking_map.h \ + context/stacking_vector.h \ + context/cddense_set.h \ + decision/decision_mode.h \ + decision/decision_mode.cpp \ + decision/decision_engine.h \ + decision/decision_engine.cpp \ + decision/decision_strategy.h \ + decision/justification_heuristic.h \ + decision/justification_heuristic.cpp \ + decision/options_handlers.h \ + printer/printer.h \ + printer/printer.cpp \ + printer/dagification_visitor.h \ + printer/dagification_visitor.cpp \ + printer/model_format_mode.h \ + printer/model_format_mode.cpp \ + printer/ast/ast_printer.h \ + printer/ast/ast_printer.cpp \ + printer/smt1/smt1_printer.h \ + printer/smt1/smt1_printer.cpp \ + printer/smt2/smt2_printer.h \ + printer/smt2/smt2_printer.cpp \ + printer/cvc/cvc_printer.h \ + printer/cvc/cvc_printer.cpp \ + printer/tptp/tptp_printer.h \ + printer/tptp/tptp_printer.cpp \ + printer/options_handlers.h \ + proof/proof.h \ + proof/sat_proof.h \ + proof/sat_proof.cpp \ + proof/cnf_proof.h \ + proof/cnf_proof.cpp \ + proof/theory_proof.h \ + proof/theory_proof.cpp \ + proof/proof_manager.h \ + proof/proof_manager.cpp \ + prop/registrar.h \ + prop/prop_engine.cpp \ + prop/prop_engine.h \ + prop/theory_proxy.h \ + prop/theory_proxy.cpp \ + prop/cnf_stream.h \ + prop/cnf_stream.cpp \ + prop/sat_solver.h \ + prop/sat_solver_types.h \ + prop/sat_solver_factory.h \ + prop/sat_solver_factory.cpp \ + prop/sat_solver_registry.h \ + prop/sat_solver_registry.cpp \ + prop/options_handlers.h \ + smt/smt_engine.cpp \ + smt/smt_engine.h \ + smt/model_postprocessor.cpp \ + smt/model_postprocessor.h \ + smt/smt_engine_scope.cpp \ + smt/smt_engine_scope.h \ + smt/command_list.cpp \ + smt/command_list.h \ + smt/modal_exception.h \ + smt/boolean_terms.h \ + smt/boolean_terms.cpp \ + smt/logic_exception.h \ + smt/simplification_mode.h \ + smt/simplification_mode.cpp \ + smt/options_handlers.h \ + theory/decision_attributes.h \ + theory/logic_info.h \ + theory/logic_info.cpp \ + theory/output_channel.h \ + theory/interrupted.h \ + theory/type_enumerator.h \ + theory/theory_engine.h \ + theory/theory_engine.cpp \ + theory/theory_test_utils.h \ + theory/theory.h \ + theory/theory.cpp \ + theory/theoryof_mode.h \ + theory/theory_registrar.h \ + theory/rewriter.h \ + theory/rewriter_attributes.h \ + theory/rewriter.cpp \ + theory/substitutions.h \ + theory/substitutions.cpp \ + theory/valuation.h \ + theory/valuation.cpp \ + theory/shared_terms_database.h \ + theory/shared_terms_database.cpp \ + theory/term_registration_visitor.h \ + theory/term_registration_visitor.cpp \ + theory/ite_simplifier.h \ + theory/ite_simplifier.cpp \ + theory/unconstrained_simplifier.h \ + theory/unconstrained_simplifier.cpp \ + theory/quantifiers_engine.h \ + theory/quantifiers_engine.cpp \ + theory/model.h \ + theory/model.cpp \ + theory/rep_set.h \ + theory/rep_set.cpp \ + theory/atom_requests.h \ + theory/atom_requests.cpp \ + theory/options_handlers.h \ + theory/uf/theory_uf.h \ + theory/uf/theory_uf.cpp \ + theory/uf/theory_uf_type_rules.h \ + theory/uf/theory_uf_rewriter.h \ + theory/uf/equality_engine.h \ + theory/uf/equality_engine_types.h \ + theory/uf/equality_engine.cpp \ + theory/uf/symmetry_breaker.h \ + theory/uf/symmetry_breaker.cpp \ + theory/uf/theory_uf_strong_solver.h \ + theory/uf/theory_uf_strong_solver.cpp \ + theory/uf/theory_uf_model.h \ + theory/uf/theory_uf_model.cpp \ + theory/uf/options_handlers.h \ + theory/bv/theory_bv_utils.h \ + theory/bv/type_enumerator.h \ + theory/bv/bitblaster.h \ + theory/bv/bitblaster.cpp \ + theory/bv/bv_to_bool.h \ + theory/bv/bv_to_bool.cpp \ + theory/bv/bv_subtheory.h \ + theory/bv/bv_subtheory_core.h \ + theory/bv/bv_subtheory_core.cpp \ + theory/bv/bv_subtheory_bitblast.h \ + theory/bv/bv_subtheory_bitblast.cpp \ + theory/bv/bv_subtheory_inequality.h \ + theory/bv/bv_subtheory_inequality.cpp \ + theory/bv/bv_inequality_graph.h \ + theory/bv/bv_inequality_graph.cpp \ + theory/bv/bitblast_strategies.h \ + theory/bv/bitblast_strategies.cpp \ + theory/bv/slicer.h \ + theory/bv/slicer.cpp \ + theory/bv/theory_bv.h \ + theory/bv/theory_bv.cpp \ + theory/bv/theory_bv_rewrite_rules.h \ + theory/bv/theory_bv_rewrite_rules_core.h \ + theory/bv/theory_bv_rewrite_rules_operator_elimination.h \ + theory/bv/theory_bv_rewrite_rules_constant_evaluation.h \ + theory/bv/theory_bv_rewrite_rules_normalization.h \ + theory/bv/theory_bv_rewrite_rules_simplification.h \ + theory/bv/theory_bv_type_rules.h \ + theory/bv/theory_bv_rewriter.h \ + theory/bv/theory_bv_rewriter.cpp \ + theory/bv/cd_set_collection.h \ + theory/idl/idl_model.h \ + theory/idl/idl_model.cpp \ + theory/idl/idl_assertion.h \ + theory/idl/idl_assertion.cpp \ + theory/idl/idl_assertion_db.h \ + theory/idl/idl_assertion_db.cpp \ + theory/idl/theory_idl.h \ + theory/idl/theory_idl.cpp \ + theory/builtin/theory_builtin_type_rules.h \ + theory/builtin/type_enumerator.h \ + theory/builtin/theory_builtin_rewriter.h \ + theory/builtin/theory_builtin_rewriter.cpp \ + theory/builtin/theory_builtin.h \ + theory/builtin/theory_builtin.cpp \ + theory/datatypes/theory_datatypes_type_rules.h \ + theory/datatypes/type_enumerator.h \ + theory/datatypes/theory_datatypes.h \ + theory/datatypes/datatypes_rewriter.h \ + theory/datatypes/theory_datatypes.cpp \ + theory/strings/theory_strings.h \ + theory/strings/theory_strings.cpp \ + theory/strings/theory_strings_rewriter.h \ + theory/strings/theory_strings_rewriter.cpp \ + theory/strings/theory_strings_type_rules.h \ + theory/strings/type_enumerator.h \ + theory/strings/theory_strings_preprocess.h \ + theory/strings/theory_strings_preprocess.cpp \ + theory/strings/regexp_operation.cpp \ + theory/strings/regexp_operation.h \ + theory/arrays/theory_arrays_type_rules.h \ + theory/arrays/type_enumerator.h \ + theory/arrays/theory_arrays_rewriter.h \ + theory/arrays/theory_arrays_rewriter.cpp \ + theory/arrays/theory_arrays.h \ + theory/arrays/theory_arrays.cpp \ + theory/arrays/union_find.h \ + theory/arrays/union_find.cpp \ + theory/arrays/array_info.h \ + theory/arrays/array_info.cpp \ + theory/arrays/static_fact_manager.h \ + theory/arrays/static_fact_manager.cpp \ + theory/quantifiers/theory_quantifiers_type_rules.h \ + theory/quantifiers/theory_quantifiers.h \ + theory/quantifiers/quantifiers_rewriter.h \ + theory/quantifiers/quantifiers_rewriter.cpp \ + theory/quantifiers/theory_quantifiers.cpp \ + theory/quantifiers/instantiation_engine.h \ + theory/quantifiers/instantiation_engine.cpp \ + theory/quantifiers/trigger.h \ + theory/quantifiers/trigger.cpp \ + theory/quantifiers/candidate_generator.h \ + theory/quantifiers/candidate_generator.cpp \ + theory/quantifiers/inst_match.h \ + theory/quantifiers/inst_match.cpp \ + theory/quantifiers/model_engine.h \ + theory/quantifiers/model_engine.cpp \ + theory/quantifiers/modes.cpp \ + theory/quantifiers/modes.h \ + theory/quantifiers/term_database.h \ + theory/quantifiers/term_database.cpp \ + theory/quantifiers/first_order_model.h \ + theory/quantifiers/first_order_model.cpp \ + theory/quantifiers/model_builder.h \ + theory/quantifiers/model_builder.cpp \ + theory/quantifiers/quantifiers_attributes.h \ + theory/quantifiers/quantifiers_attributes.cpp \ + theory/quantifiers/inst_gen.h \ + theory/quantifiers/inst_gen.cpp \ + theory/quantifiers/quant_util.h \ + theory/quantifiers/quant_util.cpp \ + theory/quantifiers/inst_match_generator.h \ + theory/quantifiers/inst_match_generator.cpp \ + theory/quantifiers/macros.h \ + theory/quantifiers/macros.cpp \ + theory/quantifiers/inst_strategy_e_matching.h \ + theory/quantifiers/inst_strategy_e_matching.cpp \ + theory/quantifiers/inst_strategy_cbqi.h \ + theory/quantifiers/inst_strategy_cbqi.cpp \ + theory/quantifiers/full_model_check.h \ + theory/quantifiers/full_model_check.cpp \ + theory/quantifiers/bounded_integers.h \ + theory/quantifiers/bounded_integers.cpp \ + theory/quantifiers/first_order_reasoning.h \ + theory/quantifiers/first_order_reasoning.cpp \ + theory/quantifiers/rewrite_engine.h \ + theory/quantifiers/rewrite_engine.cpp \ + theory/quantifiers/relevant_domain.h \ + theory/quantifiers/relevant_domain.cpp \ + theory/quantifiers/symmetry_breaking.h \ + theory/quantifiers/symmetry_breaking.cpp \ + theory/quantifiers/options_handlers.h \ + theory/rewriterules/theory_rewriterules_rules.h \ + theory/rewriterules/theory_rewriterules_rules.cpp \ + theory/rewriterules/theory_rewriterules.h \ + theory/rewriterules/theory_rewriterules.cpp \ + theory/rewriterules/theory_rewriterules_rewriter.h \ + theory/rewriterules/theory_rewriterules_type_rules.h \ + theory/rewriterules/theory_rewriterules_preprocess.h \ + theory/rewriterules/theory_rewriterules_params.h \ + theory/rewriterules/rr_inst_match.h \ + theory/rewriterules/rr_inst_match_impl.h \ + theory/rewriterules/rr_inst_match.cpp \ + theory/rewriterules/rr_trigger.h \ + theory/rewriterules/rr_trigger.cpp \ + theory/rewriterules/rr_candidate_generator.h \ + theory/rewriterules/rr_candidate_generator.cpp \ + theory/rewriterules/efficient_e_matching.h \ + theory/rewriterules/efficient_e_matching.cpp \ + theory/arith/theory_arith_type_rules.h \ + theory/arith/type_enumerator.h \ + theory/arith/arithvar.h \ + theory/arith/arithvar.cpp \ + theory/arith/bound_counts.h \ + theory/arith/arith_rewriter.h \ + theory/arith/arith_rewriter.cpp \ + theory/arith/arith_static_learner.h \ + theory/arith/arith_static_learner.cpp \ + theory/arith/constraint_forward.h \ + theory/arith/constraint.h \ + theory/arith/constraint.cpp \ + theory/arith/congruence_manager.h \ + theory/arith/congruence_manager.cpp \ + theory/arith/normal_form.h\ + theory/arith/normal_form.cpp \ + theory/arith/arith_utilities.h \ + theory/arith/delta_rational.h \ + theory/arith/delta_rational.cpp \ + theory/arith/partial_model.h \ + theory/arith/partial_model.cpp \ + theory/arith/linear_equality.h \ + theory/arith/linear_equality.cpp \ + theory/arith/simplex_update.h \ + theory/arith/simplex_update.cpp \ + theory/arith/callbacks.h \ + theory/arith/callbacks.cpp \ + theory/arith/matrix.h \ + theory/arith/matrix.cpp \ + theory/arith/tableau.h \ + theory/arith/tableau.cpp \ + theory/arith/tableau_sizes.h \ + theory/arith/tableau_sizes.cpp \ + theory/arith/error_set.h \ + theory/arith/error_set.cpp \ + theory/arith/simplex.h \ + theory/arith/simplex.cpp \ + theory/arith/dual_simplex.h \ + theory/arith/dual_simplex.cpp \ + theory/arith/fc_simplex.h \ + theory/arith/fc_simplex.cpp \ + theory/arith/soi_simplex.h \ + theory/arith/soi_simplex.cpp \ + theory/arith/approx_simplex.h \ + theory/arith/approx_simplex.cpp \ + theory/arith/attempt_solution_simplex.h \ + theory/arith/attempt_solution_simplex.cpp \ + theory/arith/theory_arith.h \ + theory/arith/theory_arith.cpp \ + theory/arith/theory_arith_private_forward.h \ + theory/arith/theory_arith_private.h \ + theory/arith/theory_arith_private.cpp \ + theory/arith/dio_solver.h \ + theory/arith/dio_solver.cpp \ + theory/arith/arith_heuristic_pivot_rule.h \ + theory/arith/arith_heuristic_pivot_rule.cpp \ + theory/arith/arith_unate_lemma_mode.h \ + theory/arith/arith_unate_lemma_mode.cpp \ + theory/arith/arith_propagation_mode.h \ + theory/arith/arith_propagation_mode.cpp \ + theory/arith/options_handlers.h \ + theory/booleans/type_enumerator.h \ + theory/booleans/theory_bool.h \ + theory/booleans/theory_bool.cpp \ + theory/booleans/theory_bool_type_rules.h \ + theory/booleans/theory_bool_rewriter.h \ + theory/booleans/theory_bool_rewriter.cpp \ + theory/booleans/circuit_propagator.h \ + theory/booleans/circuit_propagator.cpp \ + theory/booleans/boolean_term_conversion_mode.h \ + theory/booleans/boolean_term_conversion_mode.cpp \ + theory/booleans/options_handlers.h + +nodist_libcvc4_la_SOURCES = \ + smt/smt_options.cpp \ + theory/rewriter_tables.h \ + theory/theory_traits.h \ + theory/type_enumerator.cpp + libcvc4_la_LIBADD = \ @builddir@/options/liboptions.la \ @builddir@/util/libutil.la \ @builddir@/expr/libexpr.la \ - @builddir@/context/libcontext.la \ - @builddir@/proof/libproof.la \ - @builddir@/prop/libprop.la \ - @builddir@/prop/minisat/libminisat.la \ - @builddir@/prop/bvminisat/libbvminisat.la \ - @builddir@/printer/libprinter.la \ - @builddir@/smt/libsmt.la \ - @builddir@/theory/libtheory.la \ - @builddir@/decision/libdecision.la -libcvc4_noinst_la_LIBADD = \ - @builddir@/options/liboptions.la \ - @builddir@/util/libutil.la \ - @builddir@/expr/libexpr.la \ - @builddir@/context/libcontext.la \ - @builddir@/proof/libproof.la \ - @builddir@/prop/libprop.la \ @builddir@/prop/minisat/libminisat.la \ - @builddir@/prop/bvminisat/libbvminisat.la \ - @builddir@/printer/libprinter.la \ - @builddir@/smt/libsmt.la \ - @builddir@/theory/libtheory.la \ - @builddir@/decision/libdecision.la + @builddir@/prop/bvminisat/libbvminisat.la if CVC4_NEEDS_REPLACEMENT_FUNCTIONS libcvc4_la_LIBADD += \ @builddir@/lib/libreplacements.la -libcvc4_noinst_la_LIBADD += \ - @builddir@/lib/libreplacements.la endif if CVC4_USE_GLPK libcvc4_la_LIBADD += $(GLPK_LIBS) -libcvc4_noinst_la_LIBADD += $(GLPK_LIBS) endif +BUILT_SOURCES = \ + theory/rewriter_tables.h \ + theory/theory_traits.h \ + theory/type_enumerator.cpp + CLEANFILES = \ svn_versioninfo.cpp \ svninfo.tmp \ svninfo \ git_versioninfo.cpp \ gitinfo.tmp \ - gitinfo + gitinfo \ + theory/rewriter_tables.h \ + theory/theory_traits.h \ + theory/type_enumerator.cpp EXTRA_DIST = \ include/cvc4_private_library.h \ @@ -86,7 +426,33 @@ EXTRA_DIST = \ include/cvc4_private.h \ include/cvc4_public.h \ include/cvc4.h \ - cvc4.i + cvc4.i \ + smt/smt_options_template.cpp \ + smt/modal_exception.i \ + smt/logic_exception.i \ + smt/smt_engine.i \ + theory/logic_info.i \ + theory/rewriter_tables_template.h \ + theory/theory_traits_template.h \ + theory/type_enumerator_template.cpp \ + theory/mktheorytraits \ + theory/mkrewriter \ + theory/Makefile.subdirs \ + theory/uf/kinds \ + theory/bv/kinds \ + theory/idl/kinds \ + theory/builtin/kinds \ + theory/datatypes/kinds \ + theory/strings/kinds \ + theory/arrays/kinds \ + theory/quantifiers/kinds \ + theory/rewriterules/kinds \ + theory/arith/kinds \ + theory/booleans/kinds \ + theory/example/ecdata.h \ + theory/example/ecdata.cpp \ + theory/example/theory_uf_tim.h \ + theory/example/theory_uf_tim.cpp svn_versioninfo.cpp: svninfo $(AM_V_GEN)( \ @@ -199,3 +565,30 @@ uninstall-local: -rmdir "$(DESTDIR)$(includedir)/cvc4/bindings" -rmdir "$(DESTDIR)$(includedir)/cvc4" -rmdir "$(DESTDIR)$(libdir)/ocaml/cvc4" + +include @top_srcdir@/src/theory/Makefile.subdirs + +theory/rewriter_tables.h: theory/rewriter_tables_template.h theory/mkrewriter @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/theory/mkrewriter + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/theory/mkrewriter \ + $< \ + `cat @top_builddir@/src/theory/.subdirs` \ + > $@) || (rm -f $@ && exit 1) + +theory/theory_traits.h: theory/theory_traits_template.h theory/mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/theory/mktheorytraits + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/theory/mktheorytraits \ + $< \ + `cat @top_builddir@/src/theory/.subdirs` \ + > $@) || (rm -f $@ && exit 1) + +theory/type_enumerator.cpp: theory/type_enumerator_template.cpp theory/mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/theory/mktheorytraits + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/theory/mktheorytraits \ + $< \ + `cat @top_builddir@/src/theory/.subdirs` \ + > $@) || (rm -f $@ && exit 1) + diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am index 11dffe9f0..5a8bd454e 100644 --- a/src/compat/Makefile.am +++ b/src/compat/Makefile.am @@ -20,26 +20,17 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas if CVC4_BUILD_LIBCOMPAT lib_LTLIBRARIES = libcvc4compat.la -if HAVE_CXXTESTGEN -check_LTLIBRARIES = libcvc4compat_noinst.la -endif libcvc4compat_la_LDFLAGS = \ -version-info $(LIBCVC4COMPAT_VERSION) -libcvc4compat_noinst_la_LDFLAGS = libcvc4compat_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser -libcvc4compat_noinst_la_LIBADD = \ - -L@builddir@/.. -lcvc4 \ - -L@builddir@/../parser -lcvc4parser if CVC4_NEEDS_REPLACEMENT_FUNCTIONS libcvc4compat_la_LIBADD += \ @builddir@/../lib/libreplacements.la -libcvc4compat_noinst_la_LIBADD += \ - @builddir@/../lib/libreplacements.la endif libcvc4compat_la_SOURCES = \ @@ -47,11 +38,6 @@ libcvc4compat_la_SOURCES = \ cvc3_compat.cpp libcvc4compat_la_CXXFLAGS = -fno-strict-aliasing -libcvc4compat_noinst_la_SOURCES = \ - cvc3_compat.h \ - cvc3_compat.cpp -libcvc4compat_noinst_la_CXXFLAGS = -fno-strict-aliasing - else EXTRA_DIST = \ diff --git a/src/context/Makefile b/src/context/Makefile deleted file mode 100644 index 44ac0f2e6..000000000 --- a/src/context/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/context - -include $(topdir)/Makefile.subdir diff --git a/src/context/Makefile.am b/src/context/Makefile.am deleted file mode 100644 index 524bd5ffc..000000000 --- a/src/context/Makefile.am +++ /dev/null @@ -1,31 +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 = libcontext.la - -libcontext_la_SOURCES = \ - context.cpp \ - context.h \ - context_mm.cpp \ - context_mm.h \ - cdo.h \ - cdlist.h \ - cdchunk_list.h \ - cdlist_forward.h \ - cdqueue.h \ - cdtrail_queue.h \ - cdtrail_hashmap.h \ - cdtrail_hashmap_forward.h \ - cdinsert_hashmap.h \ - cdinsert_hashmap_forward.h \ - cdhashmap.h \ - cdhashmap_forward.h \ - cdhashset.h \ - cdhashset_forward.h \ - cdvector.h \ - cdmaybe.h \ - stacking_map.h \ - stacking_vector.h \ - cddense_set.h diff --git a/src/decision/Makefile b/src/decision/Makefile deleted file mode 100644 index 27978f85f..000000000 --- a/src/decision/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/decision - -include $(topdir)/Makefile.subdir diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am deleted file mode 100644 index f75a17a69..000000000 --- a/src/decision/Makefile.am +++ /dev/null @@ -1,18 +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 = libdecision.la - -libdecision_la_SOURCES = \ - decision_mode.h \ - decision_mode.cpp \ - decision_engine.h \ - decision_engine.cpp \ - decision_strategy.h \ - justification_heuristic.h \ - justification_heuristic.cpp - -EXTRA_DIST = \ - options_handlers.h diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index bf52da184..16ee454c8 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -15,13 +15,14 @@ libexpr_la_SOURCES = \ type.h \ type.cpp \ node_value.h \ + node_value.cpp \ node_manager.h \ + node_manager.cpp \ + node_manager_attributes.h \ type_checker.h \ attribute.h \ attribute_internals.h \ attribute.cpp \ - node_manager.cpp \ - node_value.cpp \ command.h \ command.cpp \ symbol_table.h \ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 721a09403..f9939fa90 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -587,6 +587,85 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ + +template <class AttrKind> +inline typename AttrKind::value_type +NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const { + return d_attrManager->getAttribute(nv, AttrKind()); +} + +template <class AttrKind> +inline bool NodeManager::hasAttribute(expr::NodeValue* nv, + const AttrKind&) const { + return d_attrManager->hasAttribute(nv, AttrKind()); +} + +template <class AttrKind> +inline bool +NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&, + typename AttrKind::value_type& ret) const { + return d_attrManager->getAttribute(nv, AttrKind(), ret); +} + +template <class AttrKind> +inline void +NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&, + const typename AttrKind::value_type& value) { + d_attrManager->setAttribute(nv, AttrKind(), value); +} + +template <class AttrKind> +inline typename AttrKind::value_type +NodeManager::getAttribute(TNode n, const AttrKind&) const { + return d_attrManager->getAttribute(n.d_nv, AttrKind()); +} + +template <class AttrKind> +inline bool +NodeManager::hasAttribute(TNode n, const AttrKind&) const { + return d_attrManager->hasAttribute(n.d_nv, AttrKind()); +} + +template <class AttrKind> +inline bool +NodeManager::getAttribute(TNode n, const AttrKind&, + typename AttrKind::value_type& ret) const { + return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret); +} + +template <class AttrKind> +inline void +NodeManager::setAttribute(TNode n, const AttrKind&, + const typename AttrKind::value_type& value) { + d_attrManager->setAttribute(n.d_nv, AttrKind(), value); +} + +template <class AttrKind> +inline typename AttrKind::value_type +NodeManager::getAttribute(TypeNode n, const AttrKind&) const { + return d_attrManager->getAttribute(n.d_nv, AttrKind()); +} + +template <class AttrKind> +inline bool +NodeManager::hasAttribute(TypeNode n, const AttrKind&) const { + return d_attrManager->hasAttribute(n.d_nv, AttrKind()); +} + +template <class AttrKind> +inline bool +NodeManager::getAttribute(TypeNode n, const AttrKind&, + typename AttrKind::value_type& ret) const { + return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret); +} + +template <class AttrKind> +inline void +NodeManager::setAttribute(TypeNode n, const AttrKind&, + const typename AttrKind::value_type& value) { + d_attrManager->setAttribute(n.d_nv, AttrKind(), value); +} + }/* CVC4 namespace */ #endif /* __CVC4__EXPR__ATTRIBUTE_H */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index ad9ec49ac..32a1d73e1 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -19,6 +19,7 @@ #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" #include "util/cvc4_assert.h" +#include "expr/node_manager_attributes.h" #include <vector> #include <iterator> diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 30f7ce8b9..b1614f31b 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -15,6 +15,7 @@ **/ #include "expr/node.h" +#include "expr/attribute.h" #include "util/output.h" #include <iostream> @@ -51,4 +52,42 @@ UnknownTypeException::UnknownTypeException(TNode n) throw() : " its type cannot be computed until it is substituted away") { } +/** Is this node constant? (and has that been computed yet?) */ +struct IsConstTag { }; +struct IsConstComputedTag { }; +typedef expr::Attribute<IsConstTag, bool> IsConstAttr; +typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr; + +template <bool ref_count> +bool NodeTemplate<ref_count>::isConst() const { + assertTNodeNotExpired(); + Debug("isConst") << "Node::isConst() for: " << *this << std::endl; + if(isNull()) { + return false; + } + switch(getMetaKind()) { + case kind::metakind::CONSTANT: + Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl; + return true; + case kind::metakind::VARIABLE: + Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl; + return false; + default: + if(getAttribute(IsConstComputedAttr())) { + bool bval = getAttribute(IsConstAttr()); + Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl; + return bval; + } else { + bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this); + Debug("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl; + const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval); + const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true); + return bval; + } + } +} + +template bool NodeTemplate<true>::isConst() const; +template bool NodeTemplate<false>::isConst() const; + }/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index e6a163a8b..3c058c924 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -443,7 +443,7 @@ public: * Returns true if this node represents a constant * @return true if const */ - inline bool isConst() const; + bool isConst() const; /** * Returns true if this node represents a constant @@ -921,7 +921,7 @@ inline std::ostream& operator<<(std::ostream& out, #include <ext/hash_map> -#include "expr/attribute.h" +//#include "expr/attribute.h" #include "expr/node_manager.h" #include "expr/type_checker.h" @@ -1271,42 +1271,6 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const return NodeManager::currentNM()->getType(*this, check); } -/** Is this node constant? (and has that been computed yet?) */ -struct IsConstTag { }; -struct IsConstComputedTag { }; -typedef expr::Attribute<IsConstTag, bool> IsConstAttr; -typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr; - -template <bool ref_count> -inline bool -NodeTemplate<ref_count>::isConst() const { - assertTNodeNotExpired(); - Debug("isConst") << "Node::isConst() for: " << *this << std::endl; - if(isNull()) { - return false; - } - switch(getMetaKind()) { - case kind::metakind::CONSTANT: - Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl; - return true; - case kind::metakind::VARIABLE: - Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl; - return false; - default: - if(getAttribute(IsConstComputedAttr())) { - bool bval = getAttribute(IsConstAttr()); - Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl; - return bval; - } else { - bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this); - Debug("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl; - const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval); - const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true); - return bval; - } - } -} - template <bool ref_count> inline Node NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index cc890b9b9..f6424cfe0 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -17,7 +17,9 @@ **/ #include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" +#include "expr/attribute.h" #include "util/cvc4_assert.h" #include "options/options.h" #include "util/statistics_registry.h" @@ -83,7 +85,7 @@ NodeManager::NodeManager(context::Context* ctxt, d_options(new Options()), d_statisticsRegistry(new StatisticsRegistry()), next_id(0), - d_attrManager(ctxt), + d_attrManager(new expr::attr::AttributeManager(ctxt)), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false), @@ -97,7 +99,7 @@ NodeManager::NodeManager(context::Context* ctxt, d_options(new Options(options)), d_statisticsRegistry(new StatisticsRegistry()), next_id(0), - d_attrManager(ctxt), + d_attrManager(new expr::attr::AttributeManager(ctxt)), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false), @@ -105,7 +107,7 @@ NodeManager::NodeManager(context::Context* ctxt, init(); } -inline void NodeManager::init() { +void NodeManager::init() { poolInsert( &expr::NodeValue::s_null ); for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { @@ -125,7 +127,7 @@ NodeManager::~NodeManager() { { ScopedBool dontGC(d_inReclaimZombies); - d_attrManager.deleteAllAttributes(); + d_attrManager->deleteAllAttributes(); } for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { @@ -153,6 +155,7 @@ NodeManager::~NodeManager() { } delete d_statisticsRegistry; + delete d_attrManager; delete d_options; } @@ -216,7 +219,7 @@ void NodeManager::reclaimZombies() { d_nodeUnderDeletion = nv; // remove attributes - d_attrManager.deleteAllAttributes(nv); + d_attrManager->deleteAllAttributes(nv); // decr ref counts of children nv->decrRefCounts(); @@ -432,4 +435,155 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { return dtt; } +TypeNode NodeManager::mkSort(uint32_t flags) { + NodeBuilder<1> nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + nb << sortTag; + TypeNode tn = nb.constructTypeNode(); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewSort(tn, flags); + } + return tn; +} + +TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) { + NodeBuilder<1> nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + nb << sortTag; + TypeNode tn = nb.constructTypeNode(); + setAttribute(tn, expr::VarNameAttr(), name); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewSort(tn, flags); + } + return tn; +} + +TypeNode NodeManager::mkSort(TypeNode constructor, + const std::vector<TypeNode>& children, + uint32_t flags) { + Assert(constructor.getKind() == kind::SORT_TYPE && + constructor.getNumChildren() == 0, + "expected a sort constructor"); + Assert(children.size() > 0, "expected non-zero # of children"); + Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) && + hasAttribute(constructor.d_nv, expr::VarNameAttr()), + "expected a sort constructor" ); + std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr()); + Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(), + "arity mismatch in application of sort constructor"); + NodeBuilder<> nb(this, kind::SORT_TYPE); + Node sortTag = Node(constructor.d_nv->d_children[0]); + nb << sortTag; + nb.append(children); + TypeNode type = nb.constructTypeNode(); + setAttribute(type, expr::VarNameAttr(), name); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags); + } + return type; +} + +TypeNode NodeManager::mkSortConstructor(const std::string& name, + size_t arity) { + Assert(arity > 0); + NodeBuilder<> nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + nb << sortTag; + TypeNode type = nb.constructTypeNode(); + setAttribute(type, expr::VarNameAttr(), name); + setAttribute(type, expr::SortArityAttr(), arity); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewSortConstructor(type); + } + return type; +} + +Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) { + Node n = NodeBuilder<0>(this, kind::VARIABLE); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); + setAttribute(n, expr::VarNameAttr(), name); + setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewVar(n, flags); + } + return n; +} + +Node* NodeManager::mkVarPtr(const std::string& name, + const TypeNode& type, uint32_t flags) { + Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); + setAttribute(*n, TypeAttr(), type); + setAttribute(*n, TypeCheckedAttr(), true); + setAttribute(*n, expr::VarNameAttr(), name); + setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewVar(*n, flags); + } + return n; +} + +Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) { + Node n = mkBoundVar(type); + setAttribute(n, expr::VarNameAttr(), name); + return n; +} + +Node* NodeManager::mkBoundVarPtr(const std::string& name, + const TypeNode& type) { + Node* n = mkBoundVarPtr(type); + setAttribute(*n, expr::VarNameAttr(), name); + return n; +} + +Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) { + Node n = NodeBuilder<0>(this, kind::VARIABLE); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); + setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewVar(n, flags); + } + return n; +} + +Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) { + Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); + setAttribute(*n, TypeAttr(), type); + setAttribute(*n, TypeCheckedAttr(), true); + setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewVar(*n, flags); + } + return n; +} + +Node NodeManager::mkBoundVar(const TypeNode& type) { + Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); + return n; +} + +Node* NodeManager::mkBoundVarPtr(const TypeNode& type) { + Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr(); + setAttribute(*n, TypeAttr(), type); + setAttribute(*n, TypeCheckedAttr(), true); + return n; +} + +Node NodeManager::mkInstConstant(const TypeNode& type) { + Node n = NodeBuilder<0>(this, kind::INST_CONSTANT); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + +Node NodeManager::mkAbstractValue(const TypeNode& type) { + Node n = mkConst(AbstractValue(++d_abstractValueCount)); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 31f6d75d9..51ed1f94d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -19,7 +19,7 @@ #include "cvc4_private.h" /* circular dependency; force node.h first */ -#include "expr/attribute.h" +//#include "expr/attribute.h" #include "expr/node.h" #include "expr/type_node.h" #include "expr/expr.h" @@ -45,27 +45,11 @@ namespace CVC4 { class StatisticsRegistry; namespace expr { + namespace attr { + class AttributeManager; + }/* CVC4::expr::attr namespace */ -class TypeChecker; - -// Definition of an attribute for the variable name. -// TODO: hide this attribute behind a NodeManager interface. -namespace attr { - struct VarNameTag { }; - struct GlobalVarTag { }; - struct SortArityTag { }; - struct DatatypeTupleTag { }; - struct DatatypeRecordTag { }; -}/* CVC4::expr::attr namespace */ - -typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; -typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr; -typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; -/** Attribute true for datatype types that are replacements for tuple types */ -typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr; -/** Attribute true for datatype types that are replacements for record types */ -typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr; - + class TypeChecker; }/* CVC4::expr namespace */ /** @@ -117,7 +101,7 @@ class NodeManager { size_t next_id; - expr::attr::AttributeManager d_attrManager; + expr::attr::AttributeManager* d_attrManager; /** The associated ExprManager */ ExprManager* d_exprManager; @@ -274,15 +258,6 @@ class NodeManager { expr::NodeValue* child[N]; };/* struct NodeManager::NVStorage<N> */ - // attribute tags - struct TypeTag { }; - struct TypeCheckedTag { }; - - // NodeManager's attributes. These aren't exposed outside of this - // class; use the getters. - typedef expr::Attribute<TypeTag, TypeNode> TypeAttr; - typedef expr::Attribute<TypeCheckedTag, bool> TypeCheckedAttr; - /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. * * It has been decided for now to hold off on implementations of @@ -781,18 +756,18 @@ public: inline TypeNode mkTesterType(TypeNode domain); /** Make a new (anonymous) sort of arity 0. */ - inline TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE); + TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort with the given name of arity 0. */ - inline TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE); + TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort by parameterizing the given sort constructor. */ - inline TypeNode mkSort(TypeNode constructor, - const std::vector<TypeNode>& children, - uint32_t flags = ExprManager::SORT_FLAG_NONE); + TypeNode mkSort(TypeNode constructor, + const std::vector<TypeNode>& children, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort with the given name and arity. */ - inline TypeNode mkSortConstructor(const std::string& name, size_t arity); + TypeNode mkSortConstructor(const std::string& name, size_t arity); /** * Make a predicate subtype type defined by the given LAMBDA @@ -933,86 +908,6 @@ public: } };/* class NodeManagerScope */ - -template <class AttrKind> -inline typename AttrKind::value_type -NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const { - return d_attrManager.getAttribute(nv, AttrKind()); -} - -template <class AttrKind> -inline bool NodeManager::hasAttribute(expr::NodeValue* nv, - const AttrKind&) const { - return d_attrManager.hasAttribute(nv, AttrKind()); -} - -template <class AttrKind> -inline bool -NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&, - typename AttrKind::value_type& ret) const { - return d_attrManager.getAttribute(nv, AttrKind(), ret); -} - -template <class AttrKind> -inline void -NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&, - const typename AttrKind::value_type& value) { - d_attrManager.setAttribute(nv, AttrKind(), value); -} - -template <class AttrKind> -inline typename AttrKind::value_type -NodeManager::getAttribute(TNode n, const AttrKind&) const { - return d_attrManager.getAttribute(n.d_nv, AttrKind()); -} - -template <class AttrKind> -inline bool -NodeManager::hasAttribute(TNode n, const AttrKind&) const { - return d_attrManager.hasAttribute(n.d_nv, AttrKind()); -} - -template <class AttrKind> -inline bool -NodeManager::getAttribute(TNode n, const AttrKind&, - typename AttrKind::value_type& ret) const { - return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret); -} - -template <class AttrKind> -inline void -NodeManager::setAttribute(TNode n, const AttrKind&, - const typename AttrKind::value_type& value) { - d_attrManager.setAttribute(n.d_nv, AttrKind(), value); -} - -template <class AttrKind> -inline typename AttrKind::value_type -NodeManager::getAttribute(TypeNode n, const AttrKind&) const { - return d_attrManager.getAttribute(n.d_nv, AttrKind()); -} - -template <class AttrKind> -inline bool -NodeManager::hasAttribute(TypeNode n, const AttrKind&) const { - return d_attrManager.hasAttribute(n.d_nv, AttrKind()); -} - -template <class AttrKind> -inline bool -NodeManager::getAttribute(TypeNode n, const AttrKind&, - typename AttrKind::value_type& ret) const { - return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret); -} - -template <class AttrKind> -inline void -NodeManager::setAttribute(TypeNode n, const AttrKind&, - const typename AttrKind::value_type& value) { - d_attrManager.setAttribute(n.d_nv, AttrKind(), value); -} - - /** Get the (singleton) type for booleans. */ inline TypeNode NodeManager::booleanType() { return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE)); @@ -1229,69 +1124,6 @@ inline bool NodeManager::hasOperator(Kind k) { } } -inline TypeNode NodeManager::mkSort(uint32_t flags) { - NodeBuilder<1> nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); - nb << sortTag; - TypeNode tn = nb.constructTypeNode(); - for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSort(tn, flags); - } - return tn; -} - -inline TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) { - NodeBuilder<1> nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); - nb << sortTag; - TypeNode tn = nb.constructTypeNode(); - setAttribute(tn, expr::VarNameAttr(), name); - for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSort(tn, flags); - } - return tn; -} - -inline TypeNode NodeManager::mkSort(TypeNode constructor, - const std::vector<TypeNode>& children, - uint32_t flags) { - Assert(constructor.getKind() == kind::SORT_TYPE && - constructor.getNumChildren() == 0, - "expected a sort constructor"); - Assert(children.size() > 0, "expected non-zero # of children"); - Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) && - hasAttribute(constructor.d_nv, expr::VarNameAttr()), - "expected a sort constructor" ); - std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr()); - Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(), - "arity mismatch in application of sort constructor"); - NodeBuilder<> nb(this, kind::SORT_TYPE); - Node sortTag = Node(constructor.d_nv->d_children[0]); - nb << sortTag; - nb.append(children); - TypeNode type = nb.constructTypeNode(); - setAttribute(type, expr::VarNameAttr(), name); - for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags); - } - return type; -} - -inline TypeNode NodeManager::mkSortConstructor(const std::string& name, - size_t arity) { - Assert(arity > 0); - NodeBuilder<> nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); - nb << sortTag; - TypeNode type = nb.constructTypeNode(); - setAttribute(type, expr::VarNameAttr(), name); - setAttribute(type, expr::SortArityAttr(), arity); - for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSortConstructor(type); - } - return type; -} - inline Kind NodeManager::operatorToKind(TNode n) { return kind::operatorToKind(n.d_nv); } @@ -1540,95 +1372,6 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, return NodeBuilder<>(this, kind).append(children).constructTypeNode(); } - -inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) { - Node n = NodeBuilder<0>(this, kind::VARIABLE); - setAttribute(n, TypeAttr(), type); - setAttribute(n, TypeCheckedAttr(), true); - setAttribute(n, expr::VarNameAttr(), name); - setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); - for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n, flags); - } - return n; -} - -inline Node* NodeManager::mkVarPtr(const std::string& name, - const TypeNode& type, uint32_t flags) { - Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); - setAttribute(*n, TypeAttr(), type); - setAttribute(*n, TypeCheckedAttr(), true); - setAttribute(*n, expr::VarNameAttr(), name); - setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); - for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(*n, flags); - } - return n; -} - -inline Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) { - Node n = mkBoundVar(type); - setAttribute(n, expr::VarNameAttr(), name); - return n; -} - -inline Node* NodeManager::mkBoundVarPtr(const std::string& name, - const TypeNode& type) { - Node* n = mkBoundVarPtr(type); - setAttribute(*n, expr::VarNameAttr(), name); - return n; -} - -inline Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) { - Node n = NodeBuilder<0>(this, kind::VARIABLE); - setAttribute(n, TypeAttr(), type); - setAttribute(n, TypeCheckedAttr(), true); - setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); - for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n, flags); - } - return n; -} - -inline Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) { - Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); - setAttribute(*n, TypeAttr(), type); - setAttribute(*n, TypeCheckedAttr(), true); - setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); - for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(*n, flags); - } - return n; -} - -inline Node NodeManager::mkBoundVar(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE); - setAttribute(n, TypeAttr(), type); - setAttribute(n, TypeCheckedAttr(), true); - return n; -} - -inline Node* NodeManager::mkBoundVarPtr(const TypeNode& type) { - Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr(); - setAttribute(*n, TypeAttr(), type); - setAttribute(*n, TypeCheckedAttr(), true); - return n; -} - -inline Node NodeManager::mkInstConstant(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::INST_CONSTANT); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); - return n; -} - -inline Node NodeManager::mkAbstractValue(const TypeNode& type) { - Node n = mkConst(AbstractValue(++d_abstractValueCount)); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); - return n; -} - template <class T> Node NodeManager::mkConst(const T& val) { return mkConstInternal<Node, T>(val); diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h new file mode 100644 index 000000000..ab55baa6e --- /dev/null +++ b/src/expr/node_manager_attributes.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file node_manager_attributes.h + ** \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 + **/ + +#pragma once + +#include "expr/attribute.h" + +namespace CVC4 { +namespace expr { + +// Definition of an attribute for the variable name. +// TODO: hide this attribute behind a NodeManager interface. +namespace attr { + struct VarNameTag { }; + struct GlobalVarTag { }; + struct SortArityTag { }; + struct DatatypeTupleTag { }; + struct DatatypeRecordTag { }; + struct TypeTag { }; + struct TypeCheckedTag { }; +}/* CVC4::expr::attr namespace */ + +typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; +typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr; +typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; +/** Attribute true for datatype types that are replacements for tuple types */ +typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr; +/** Attribute true for datatype types that are replacements for record types */ +typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr; +typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr; +typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr; + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index f3cf992ba..672fc6aae 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -19,6 +19,7 @@ #include <vector> #include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" #include "expr/type.h" #include "expr/type_node.h" #include "util/exception.h" diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index aa7039f52..b2138c9a1 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -18,10 +18,11 @@ #include "expr/type_checker.h" #include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" ${typechecker_includes} -#line 25 "${template}" +#line 26 "${template}" namespace CVC4 { namespace expr { @@ -34,7 +35,7 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) switch(n.getKind()) { case kind::VARIABLE: case kind::SKOLEM: - typeNode = nodeManager->getAttribute(n, NodeManager::TypeAttr()); + typeNode = nodeManager->getAttribute(n, TypeAttr()); break; case kind::BUILTIN: typeNode = nodeManager->builtinOperatorType(); @@ -45,16 +46,16 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) ${typerules} -#line 49 "${template}" +#line 50 "${template}" default: Debug("getType") << "FAILURE" << std::endl; Unhandled(n.getKind()); } - nodeManager->setAttribute(n, NodeManager::TypeAttr(), typeNode); - nodeManager->setAttribute(n, NodeManager::TypeCheckedAttr(), - check || nodeManager->getAttribute(n, NodeManager::TypeCheckedAttr())); + nodeManager->setAttribute(n, TypeAttr(), typeNode); + nodeManager->setAttribute(n, TypeCheckedAttr(), + check || nodeManager->getAttribute(n, TypeCheckedAttr())); return typeNode; @@ -68,7 +69,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) switch(n.getKind()) { ${construles} -#line 72 "${template}" +#line 73 "${template}" default:; } diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 2fc380224..54fd2f3e8 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -16,6 +16,7 @@ #include <vector> +#include "expr/node_manager_attributes.h" #include "expr/type_node.h" #include "expr/type_properties.h" @@ -482,4 +483,15 @@ TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){ } } +/** Is this a sort kind */ +bool TypeNode::isSort() const { + return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || + ( isPredicateSubtype() && getSubtypeParentType().isSort() ); +} + +/** Is this a sort constructor kind */ +bool TypeNode::isSortConstructor() const { + return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); +} + }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 145ca2aba..75d6d8063 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -916,17 +916,6 @@ inline bool TypeNode::isSExpr() const { ( isPredicateSubtype() && getSubtypeParentType().isSExpr() ); } -/** Is this a sort kind */ -inline bool TypeNode::isSort() const { - return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || - ( isPredicateSubtype() && getSubtypeParentType().isSort() ); -} - -/** Is this a sort constructor kind */ -inline bool TypeNode::isSortConstructor() const { - return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); -} - /** Is this a predicate subtype */ inline bool TypeNode::isPredicateSubtype() const { return getKind() == kind::SUBTYPE_TYPE; diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 7ead35abd..a178f8dd5 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -20,13 +20,9 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = smt1 smt2 cvc tptp lib_LTLIBRARIES = libcvc4parser.la -if HAVE_CXXTESTGEN -check_LTLIBRARIES = libcvc4parser_noinst.la -endif libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \ -version-info $(LIBCVC4PARSER_VERSION) -libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS) libcvc4parser_la_LIBADD = \ @builddir@/smt1/libparsersmt1.la \ @@ -34,18 +30,10 @@ libcvc4parser_la_LIBADD = \ @builddir@/tptp/libparsertptp.la \ @builddir@/cvc/libparsercvc.la \ -L@builddir@/.. -lcvc4 -libcvc4parser_noinst_la_LIBADD = \ - @builddir@/smt1/libparsersmt1.la \ - @builddir@/smt2/libparsersmt2.la \ - @builddir@/tptp/libparsertptp.la \ - @builddir@/cvc/libparsercvc.la \ - @builddir@/../libcvc4_noinst.la if CVC4_NEEDS_REPLACEMENT_FUNCTIONS libcvc4parser_la_LIBADD += \ @builddir@/../lib/libreplacements.la -libcvc4parser_noinst_la_LIBADD += \ - @builddir@/../lib/libreplacements.la endif libcvc4parser_la_SOURCES = \ @@ -69,27 +57,6 @@ libcvc4parser_la_SOURCES = \ parser_exception.h \ antlr_tracing.h -libcvc4parser_noinst_la_SOURCES = \ - antlr_input.h \ - antlr_input.cpp \ - antlr_input_imports.cpp \ - antlr_line_buffered_input.h \ - antlr_line_buffered_input.cpp \ - bounded_token_buffer.h \ - bounded_token_buffer.cpp \ - bounded_token_factory.h \ - bounded_token_factory.cpp \ - input.h \ - input.cpp \ - memory_mapped_input_buffer.h \ - memory_mapped_input_buffer.cpp \ - parser.h \ - parser.cpp \ - parser_builder.h \ - parser_builder.cpp \ - parser_exception.h \ - antlr_tracing.h - EXTRA_DIST = \ Makefile.antlr_tracing \ cvc4parser.i \ diff --git a/src/printer/Makefile b/src/printer/Makefile deleted file mode 100644 index 72baefbd9..000000000 --- a/src/printer/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/printer - -include $(topdir)/Makefile.subdir diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am deleted file mode 100644 index cd938088e..000000000 --- a/src/printer/Makefile.am +++ /dev/null @@ -1,27 +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 = libprinter.la - -libprinter_la_SOURCES = \ - printer.h \ - printer.cpp \ - dagification_visitor.h \ - dagification_visitor.cpp \ - model_format_mode.h \ - model_format_mode.cpp \ - ast/ast_printer.h \ - ast/ast_printer.cpp \ - smt1/smt1_printer.h \ - smt1/smt1_printer.cpp \ - smt2/smt2_printer.h \ - smt2/smt2_printer.cpp \ - cvc/cvc_printer.h \ - cvc/cvc_printer.cpp \ - tptp/tptp_printer.h \ - tptp/tptp_printer.cpp - -EXTRA_DIST = \ - options_handlers.h diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 88c769f26..8ab5c121d 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -17,7 +17,7 @@ #include "printer/ast/ast_printer.h" #include "expr/expr.h" // for ExprSetDepth etc.. #include "util/language.h" // for LANG_AST -#include "expr/node_manager.h" // for VarNameAttr +#include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/command.h" #include "printer/dagification_visitor.h" #include "util/node_visitor.h" diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 513ff7276..e0375e6e1 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -17,7 +17,7 @@ #include "printer/cvc/cvc_printer.h" #include "expr/expr.h" // for ExprSetDepth etc.. #include "util/language.h" // for LANG_AST -#include "expr/node_manager.h" // for VarNameAttr +#include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/command.h" #include "theory/substitutions.h" #include "smt/smt_engine.h" diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 756e521a6..d086caf38 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -28,6 +28,7 @@ #include "util/language.h" #include "smt/smt_engine.h" #include "smt/options.h" +#include "expr/node_manager_attributes.h" #include "theory/model.h" #include "theory/arrays/theory_arrays_rewriter.h" diff --git a/src/proof/Makefile b/src/proof/Makefile deleted file mode 100644 index b0985ba84..000000000 --- a/src/proof/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/proof - -include $(topdir)/Makefile.subdir diff --git a/src/proof/Makefile.am b/src/proof/Makefile.am deleted file mode 100644 index e996ddb60..000000000 --- a/src/proof/Makefile.am +++ /dev/null @@ -1,21 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ - -I@builddir@/.. -I@srcdir@/../prop/minisat -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libproof.la - -libproof_la_SOURCES = \ - proof.h \ - sat_proof.h \ - sat_proof.cpp \ - cnf_proof.h \ - cnf_proof.cpp \ - theory_proof.h \ - theory_proof.cpp \ - proof_manager.h \ - proof_manager.cpp - -EXTRA_DIST = diff --git a/src/prop/Makefile b/src/prop/Makefile deleted file mode 100644 index 08f0c693c..000000000 --- a/src/prop/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/prop - -include $(topdir)/Makefile.subdir diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am deleted file mode 100644 index 6b8221443..000000000 --- a/src/prop/Makefile.am +++ /dev/null @@ -1,29 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ - -I@builddir@/.. -I@srcdir@/minisat -I@srcdir@/bvminisat -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libprop.la - -libprop_la_SOURCES = \ - registrar.h \ - prop_engine.cpp \ - prop_engine.h \ - theory_proxy.h \ - theory_proxy.cpp \ - cnf_stream.h \ - cnf_stream.cpp \ - sat_solver.h \ - sat_solver_types.h \ - sat_solver_factory.h \ - sat_solver_factory.cpp \ - sat_solver_registry.h \ - sat_solver_registry.cpp - -EXTRA_DIST = \ - options_handlers.h - -SUBDIRS = minisat bvminisat - diff --git a/src/prop/bvminisat/Makefile b/src/prop/bvminisat/Makefile deleted file mode 100644 index 71888016d..000000000 --- a/src/prop/bvminisat/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/prop/bvminisat - -include $(topdir)/Makefile.subdir diff --git a/src/prop/minisat/Makefile b/src/prop/minisat/Makefile deleted file mode 100644 index e8b442ac1..000000000 --- a/src/prop/minisat/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/prop/minisat - -include $(topdir)/Makefile.subdir diff --git a/src/smt/Makefile b/src/smt/Makefile deleted file mode 100644 index 7103b6d21..000000000 --- a/src/smt/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/smt - -include $(topdir)/Makefile.subdir diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am deleted file mode 100644 index 45c2e4924..000000000 --- a/src/smt/Makefile.am +++ /dev/null @@ -1,32 +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 = libsmt.la - -libsmt_la_SOURCES = \ - smt_engine.cpp \ - smt_engine.h \ - model_postprocessor.cpp \ - model_postprocessor.h \ - smt_engine_scope.cpp \ - smt_engine_scope.h \ - command_list.cpp \ - command_list.h \ - modal_exception.h \ - boolean_terms.h \ - boolean_terms.cpp \ - logic_exception.h \ - simplification_mode.h \ - simplification_mode.cpp - -nodist_libsmt_la_SOURCES = \ - smt_options.cpp - -EXTRA_DIST = \ - options_handlers.h \ - smt_options_template.cpp \ - modal_exception.i \ - logic_exception.i \ - smt_engine.i diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 9f1b9c1a6..1157c464e 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -22,8 +22,7 @@ #include "theory/booleans/boolean_term_conversion_mode.h" #include "theory/booleans/options.h" #include "expr/kind.h" -#include "util/hash.h" -#include "util/bool.h" +#include "expr/node_manager_attributes.h" #include "util/ntuple.h" #include <string> #include <algorithm> diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index c61a61940..686ecbbe6 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -16,6 +16,7 @@ #include "smt/model_postprocessor.h" #include "smt/boolean_terms.h" +#include "expr/node_manager_attributes.h" using namespace std; using namespace CVC4; 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<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr; +typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> 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<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr; -typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> 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 <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" 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" diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 8db91da69..1c5dd3e07 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -24,6 +24,7 @@ #include "expr/expr_manager_scope.h" #include "expr/node_manager.h" #include "expr/node.h" +#include "expr/attribute.h" #include "util/recursion_breaker.h" #include "util/matcher.h" #include "util/cvc4_assert.h" |