** Don't fear the files-changed list, almost all changes are in the **
authorMorgan Deters <mdeters@gmail.com>
Fri, 4 Jun 2010 18:55:22 +0000 (18:55 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 4 Jun 2010 18:55:22 +0000 (18:55 +0000)
commita460f751e8345e61c4989386765d84bb76fe37d6
tree08bc3c035b5bd8f220853e06dc90fb939c55b2ed
parentfebba49895125f4f3489e7dff283a000ae9965b3
** Don't fear the files-changed list, almost all changes are in the **
** file-level documentation at the top of the sources.              **

This is the "make bugzilla stop bugging me" bugfix commit.

* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
  Updated documentation in the file.  Resolves bug #99.

* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
  moved into a separate file.  Partially resolves bug #100.

* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
  namespace) instead of metakind.h (where it was in CVC4::metakind).
  This clears up a warning (private #inclusion) from the SMT and SMT2
  parsers, and maybe makes more sense anyways, since this is based on
  the kind (and not the metakind) of an operator.

* Documentation improvement; doxygen top-level \file gestures, \brief
  gestures for files, etc.  Changed contrib/update-copyright.pl for
  this change, and post-processed to add \brief.  Resolves bug #98.

* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
  They no longer made sense.  Resolves bug #91.
172 files changed:
contrib/update-copyright.pl
src/context/cdlist.h
src/context/cdmap.h
src/context/cdo.h
src/context/cdset.h
src/context/context.cpp
src/context/context.h
src/context/context_mm.cpp
src/context/context_mm.h
src/expr/Makefile.am
src/expr/attribute.cpp
src/expr/attribute.h
src/expr/attribute_internals.h
src/expr/builtin_type_rules.h
src/expr/command.cpp
src/expr/command.h
src/expr/convenience_node_builders.h [new file with mode: 0644]
src/expr/declaration_scope.cpp
src/expr/declaration_scope.h
src/expr/expr_manager_scope.h
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/expr_template.cpp
src/expr/expr_template.h
src/expr/kind_template.h
src/expr/metakind_template.h
src/expr/node.cpp
src/expr/node.h
src/expr/node_builder.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/node_value.cpp
src/expr/node_value.h
src/expr/type.cpp
src/expr/type.h
src/expr/type_constant.h
src/expr/type_node.cpp
src/expr/type_node.h
src/include/cvc4_private.h
src/include/cvc4_public.h
src/include/cvc4parser_private.h
src/include/cvc4parser_public.h
src/main/getopt.cpp
src/main/main.cpp
src/main/main.h
src/main/usage.h
src/main/util.cpp
src/parser/antlr_input.cpp
src/parser/antlr_input.h
src/parser/antlr_input_imports.cpp
src/parser/bounded_token_buffer.cpp
src/parser/bounded_token_buffer.h
src/parser/bounded_token_factory.cpp
src/parser/bounded_token_factory.h
src/parser/cvc/Cvc.g
src/parser/cvc/cvc_input.cpp
src/parser/cvc/cvc_input.h
src/parser/input.cpp
src/parser/input.h
src/parser/memory_mapped_input_buffer.cpp
src/parser/memory_mapped_input_buffer.h
src/parser/parser.cpp
src/parser/parser.h
src/parser/parser_builder.cpp
src/parser/parser_builder.h
src/parser/parser_exception.h
src/parser/parser_options.h
src/parser/smt/Smt.g
src/parser/smt/smt_input.cpp
src/parser/smt/smt_input.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/parser/smt2/smt2_input.cpp
src/parser/smt2/smt2_input.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/sat.cpp
src/prop/sat.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/arith/arith_constants.h
src/theory/arith/arith_rewriter.cpp
src/theory/arith/arith_rewriter.h
src/theory/arith/arith_utilities.h
src/theory/arith/basic.h
src/theory/arith/delta_rational.cpp
src/theory/arith/delta_rational.h
src/theory/arith/normal.h
src/theory/arith/partial_model.cpp
src/theory/arith/partial_model.h
src/theory/arith/slack.h
src/theory/arith/tableau.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_type_rules.h
src/theory/arrays/theory_arrays.h
src/theory/booleans/theory_bool.h
src/theory/booleans/theory_bool_type_rules.h
src/theory/bv/theory_bv.h
src/theory/bv/theory_bv_type_rules.h
src/theory/interrupted.h
src/theory/output_channel.h
src/theory/theory.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theoryof_table_template.h
src/theory/uf/ecdata.cpp
src/theory/uf/ecdata.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
src/theory/uf/theory_uf_type_rules.h
src/util/Assert.cpp
src/util/Assert.h
src/util/bitvector.cpp
src/util/bitvector.h
src/util/bool.h
src/util/configuration.cpp
src/util/configuration.h
src/util/debug.h
src/util/decision_engine.cpp
src/util/decision_engine.h
src/util/exception.h
src/util/gmp_util.h
src/util/hash.h
src/util/integer.cpp
src/util/integer.h
src/util/model.h
src/util/options.h
src/util/output.cpp
src/util/output.h
src/util/rational.cpp
src/util/rational.h
src/util/result.h
src/util/sexpr.h
src/util/unique_id.h
test/unit/context/cdlist_black.h
test/unit/context/cdmap_black.h
test/unit/context/cdmap_white.h
test/unit/context/cdo_black.h
test/unit/context/context_black.h
test/unit/context/context_mm_black.h
test/unit/context/context_white.h
test/unit/expr/attribute_black.h
test/unit/expr/attribute_white.h
test/unit/expr/declaration_scope_black.h
test/unit/expr/expr_manager_public.h
test/unit/expr/expr_public.h
test/unit/expr/kind_black.h
test/unit/expr/node_black.h
test/unit/expr/node_builder_black.h
test/unit/expr/node_manager_black.h
test/unit/expr/node_manager_white.h
test/unit/expr/node_white.h
test/unit/memory.h
test/unit/parser/parser_black.h
test/unit/parser/parser_builder_black.h
test/unit/prop/cnf_stream_black.h
test/unit/theory/theory_black.h
test/unit/theory/theory_uf_white.h
test/unit/util/assert_white.h
test/unit/util/bitvector_black.h
test/unit/util/configuration_black.h
test/unit/util/exception_black.h
test/unit/util/integer_black.h
test/unit/util/integer_white.h
test/unit/util/output_black.h
test/unit/util/rational_black.h
test/unit/util/rational_white.h