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

author	Morgan Deters <mdeters@gmail.com>
	Sat, 23 Apr 2011 05:15:56 +0000 (05:15 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Sat, 23 Apr 2011 05:15:56 +0000 (05:15 +0000)
commit	57b8c4c8581d2d3ffcf3d3a1bb228271cb4d074a
tree	1c1781cc83118e4bbd2ad6939b16734c30a69f1a	tree
parent	673d0e86b91094a58433c3ca71591fb0a0c60f84	commit \| diff

* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work

31 files changed:

contrib/switch-config		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/expr_template.h		diff \| blob \| history
src/parser/Makefile.am		diff \| blob \| history
src/parser/Makefile.antlr_tracing	[new file with mode: 0644]	blob
src/parser/antlr_tracing.h	[new file with mode: 0644]	blob
src/parser/bounded_token_buffer.cpp		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/cvc/Makefile.am		diff \| blob \| history
src/parser/cvc/README	[new file with mode: 0644]	blob
src/parser/cvc/cvc_input.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/smt/Makefile.am		diff \| blob \| history
src/parser/smt/Smt.g		diff \| blob \| history
src/parser/smt2/Makefile.am		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/util/Assert.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/boolean_simplification.cpp	[new file with mode: 0644]	blob
src/util/boolean_simplification.h		diff \| blob \| history
src/util/output.h		diff \| blob \| history
src/util/subrange_bound.h	[new file with mode: 0644]	blob
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/subranges.cvc	[new file with mode: 0644]	blob
test/regress/run_regression		diff \| blob \| history
test/unit/Makefile.am		diff \| blob \| history
test/unit/expr/expr_manager_public.h		diff \| blob \| history
test/unit/parser/parser_black.h		diff \| blob \| history
test/unit/util/boolean_simplification_black.h	[new file with mode: 0644]	blob
test/unit/util/subrange_bound_white.h	[new file with mode: 0644]	blob

RSS Atom