AC_SUBST(cvc4_LDFLAGS)
AC_SUBST(pcvc4_LDFLAGS)
+AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
+
# remember the command line used for configure
AC_SUBST(cvc4_config_cmdline)
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 \
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)( \
-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)
+
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 = \
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 = \
+++ /dev/null
-topdir = ../..
-srcdir = src/context
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
+++ /dev/null
-topdir = ../..
-srcdir = src/decision
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
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 \
}/* 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 */
#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>
**/
#include "expr/node.h"
+#include "expr/attribute.h"
#include "util/output.h"
#include <iostream>
" 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 */
* 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
#include <ext/hash_map>
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
#include "expr/node_manager.h"
#include "expr/type_checker.h"
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 {
**/
#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"
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),
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),
init();
}
-inline void NodeManager::init() {
+void NodeManager::init() {
poolInsert( &expr::NodeValue::s_null );
for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
{
ScopedBool dontGC(d_inReclaimZombies);
- d_attrManager.deleteAllAttributes();
+ d_attrManager->deleteAllAttributes();
}
for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
}
delete d_statisticsRegistry;
+ delete d_attrManager;
delete d_options;
}
d_nodeUnderDeletion = nv;
// remove attributes
- d_attrManager.deleteAllAttributes(nv);
+ d_attrManager->deleteAllAttributes(nv);
// decr ref counts of children
nv->decrRefCounts();
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 */
#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"
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 */
/**
size_t next_id;
- expr::attr::AttributeManager d_attrManager;
+ expr::attr::AttributeManager* d_attrManager;
/** The associated ExprManager */
ExprManager* d_exprManager;
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
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
}
};/* 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));
}
}
-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);
}
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);
--- /dev/null
+/********************* */
+/*! \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 */
#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"
#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 {
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();
${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;
switch(n.getKind()) {
${construles}
-#line 72 "${template}"
+#line 73 "${template}"
default:;
}
#include <vector>
+#include "expr/node_manager_attributes.h"
#include "expr/type_node.h"
#include "expr/type_properties.h"
}
}
+/** 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 */
( 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;
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 \
@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 = \
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 \
+++ /dev/null
-topdir = ../..
-srcdir = src/printer
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
#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"
#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"
#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"
+++ /dev/null
-topdir = ../..
-srcdir = src/proof
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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 =
+++ /dev/null
-topdir = ../..
-srcdir = src/prop
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
-
+++ /dev/null
-topdir = ../../..
-srcdir = src/prop/bvminisat
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-topdir = ../../..
-srcdir = src/prop/minisat
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-topdir = ../..
-srcdir = src/smt
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
#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>
#include "smt/model_postprocessor.h"
#include "smt/boolean_terms.h"
+#include "expr/node_manager_attributes.h"
using namespace std;
using namespace CVC4;
+++ /dev/null
-topdir = ../..
-srcdir = src/theory
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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)
-$(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; \
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/arith
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/arrays
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
--- /dev/null
+/********************* */
+/*! \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 */
#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);
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
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
(compare == Cardinality::EQUAL && (!(defaultValue < mostFrequentValue)))) {
return false;
}
- n.setAttribute(ArrayConstantMostFrequentValueAttr(), mostFrequentValue);
- n.setAttribute(ArrayConstantMostFrequentValueCountAttr(), mostFrequentValueCount);
+ setMostFrequentValue(n, mostFrequentValue);
+ setMostFrequentValueCount(n, mostFrequentValueCount);
return true;
}
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/bool
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/builtin
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/bv
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/datatypes
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
#include "theory/rewriter.h"
#include "theory/datatypes/options.h"
#include "theory/type_enumerator.h"
+#include "expr/node_manager_attributes.h"
namespace CVC4 {
namespace theory {
#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
#include "util/matcher.h"
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
namespace CVC4 {
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/example
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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 =
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/idl
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/quantifiers
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
#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 {
#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#include "expr/attribute.h"
#include "theory/theory.h"
#include <map>
#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"
#pragma once
#include "expr/node.h"
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
namespace CVC4 {
namespace theory {
#pragma once
+#include "expr/attribute.h"
+
namespace CVC4 {
namespace theory {
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/rewriterules
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/strings
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
#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"
+++ /dev/null
-topdir = ../../..
-srcdir = src/theory/uf
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
#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"
#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"
** \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"
#include "context/context.h"
#include "context/context_mm.h"
+#include "context/cdhashmap.h"
#include "context/cdchunk_list.h"
#include "util/statistics_registry.h"
#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"
# All unit tests
UNIT_TESTS = \
+ expr/expr_public \
+ expr/expr_manager_public \
+ expr/type_cardinality_public \
+ util/cardinality_public
+if WHITE_AND_BLACK_TESTS
+UNIT_TESTS += \
theory/logic_info_white \
theory/theory_engine_white \
theory/theory_black \
theory/theory_arith_white \
theory/theory_bv_white \
theory/type_enumerator_white \
- expr/expr_public \
- expr/expr_manager_public \
expr/node_white \
expr/node_black \
expr/kind_black \
expr/attribute_black \
expr/symbol_table_black \
expr/node_self_iterator_black \
- expr/type_cardinality_public \
expr/type_node_white \
parser/parser_black \
parser/parser_builder_black \
util/trans_closure_black \
util/boolean_simplification_black \
util/subrange_bound_white \
- util/cardinality_public \
util/recursion_breaker_black \
main/interactive_shell_black
+endif
export VERBOSE = 1
AM_LDFLAGS_PUBLIC =
AM_LIBADD_WHITE = \
@abs_top_builddir@/src/main/libmain.a \
- @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
- @abs_top_builddir@/src/libcvc4_noinst.la
+ @abs_top_builddir@/src/parser/libcvc4parser.la \
+ @abs_top_builddir@/src/libcvc4.la
AM_LIBADD_BLACK = \
@abs_top_builddir@/src/main/libmain.a \
- @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
- @abs_top_builddir@/src/libcvc4_noinst.la
+ @abs_top_builddir@/src/parser/libcvc4parser.la \
+ @abs_top_builddir@/src/libcvc4.la
AM_LIBADD_PUBLIC = \
@abs_top_builddir@/src/parser/libcvc4parser.la \
@abs_top_builddir@/src/libcvc4.la
#include "expr/node_builder.h"
#include "expr/node_manager.h"
#include "expr/attribute.h"
+#include "expr/node_manager_attributes.h"
#include "expr/node.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
// TS_ASSERT_DIFFERS(theory::PreRewriteCacheTop::s_id, theory::PostRewriteCacheTop::s_id);
lastId = attr::LastAttributeId<TypeNode, false>::getId();
- TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
+ TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId);
}
#include <vector>
#include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
#include "context/context.h"
#include "util/rational.h"
projects / cvc5.git / commitdiff