Public interface review items:
authorMorgan Deters <mdeters@gmail.com>
Fri, 28 Sep 2012 17:29:01 +0000 (17:29 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 28 Sep 2012 17:29:01 +0000 (17:29 +0000)
commit65f720aac2d497c6e829d9c76638073a10060e7d
tree357035797e31f96a37dce30cb97ddb0aaf8f3bb7
parentc0c351a89871e0a6881668fa1a8d87349ab8af8e
Public interface review items:

* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
  or a public exception type.
* auto-generated documentation for Smt options and internal options

Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
85 files changed:
Makefile.am
configure.ac
doc/SmtEngine.3cvc4_template.in [new file with mode: 0644]
doc/cvc4.1_template.in
doc/cvc4.5.in
doc/libcvc4.3_template.in
doc/libcvc4compat.3.in
doc/libcvc4parser.3.in
doc/options.3cvc4_template.in [new file with mode: 0644]
src/compat/cvc3_compat.cpp
src/compat/cvc3_compat.h
src/expr/kind_template.h
src/expr/symbol_table.cpp
src/expr/symbol_table.h
src/expr/type.cpp
src/expr/type.h
src/main/driver_unified.cpp
src/main/interactive_shell.cpp
src/main/main.cpp
src/main/util.cpp
src/options/Makefile.am
src/options/mkoptions
src/parser/antlr_input.cpp
src/parser/antlr_input.h
src/parser/antlr_input_imports.cpp
src/parser/antlr_line_buffered_input.cpp
src/parser/bounded_token_buffer.cpp
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/parser.cpp
src/parser/parser.h
src/parser/parser_builder.cpp
src/parser/parser_builder.h
src/parser/smt1/Smt1.g
src/parser/smt1/smt1.cpp
src/parser/smt1/smt1_input.cpp
src/parser/smt1/smt1_input.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2_input.cpp
src/parser/smt2/smt2_input.h
src/parser/tptp/tptp.cpp
src/parser/tptp/tptp.h
src/parser/tptp/tptp_input.cpp
src/parser/tptp/tptp_input.h
src/printer/dagification_visitor.cpp
src/prop/cnf_stream.cpp
src/smt/options
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/logic_info.cpp
src/theory/logic_info.h
src/util/Assert.cpp
src/util/Assert.h
src/util/Makefile.am
src/util/ascription_type.h
src/util/bitvector.h
src/util/cardinality.h
src/util/datatype.cpp
src/util/datatype.h
src/util/exception.cpp [new file with mode: 0644]
src/util/exception.h
src/util/integer_cln_imp.h
src/util/integer_gmp_imp.h
src/util/predicate.h
src/util/rational_cln_imp.h
src/util/rational_gmp_imp.h
src/util/result.h
src/util/sexpr.h
src/util/statistics_registry.cpp
src/util/statistics_registry.h
src/util/subrange_bound.h
test/system/ouroborous.cpp
test/unit/expr/expr_manager_public.h
test/unit/expr/expr_public.h
test/unit/expr/kind_map_black.h
test/unit/expr/node_black.h
test/unit/expr/type_cardinality_public.h
test/unit/theory/logic_info_white.h
test/unit/util/assert_white.h
test/unit/util/boolean_simplification_black.h