git.libre-soc.org Git - cvc5.git/commit

author	Christopher L. Conway <christopherleeconway@gmail.com>
	Wed, 28 Jul 2010 22:57:36 +0000 (22:57 +0000)
committer	Christopher L. Conway <christopherleeconway@gmail.com>
	Wed, 28 Jul 2010 22:57:36 +0000 (22:57 +0000)
commit	88766918615793536224bf50d0bb70ec9f9efd93
tree	5a038bb2c17199f43d7a422063751bc3839b7388	tree
parent	d2787f41e72184fbdf2619d3c0466bed9b6211be	commit \| diff

Forcing a type check on Node construction in debug mode (Fixes: #188)
NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions

15 files changed:

src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/parser/cvc/cvc_input.cpp		diff \| blob \| history
src/parser/cvc/cvc_input.h		diff \| blob \| history
src/parser/input.h		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
test/regress/regress0/precedence/not-eq.cvc		diff \| blob \| history
test/unit/expr/expr_public.h		diff \| blob \| history
test/unit/expr/node_black.h		diff \| blob \| history
test/unit/expr/node_builder_black.h		diff \| blob \| history
test/unit/parser/parser_black.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history
test/unit/theory/theory_uf_white.h		diff \| blob \| history