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

author	Tianyi Liang <tianyi-liang@uiowa.edu>
	Wed, 11 Sep 2013 15:23:19 +0000 (11:23 -0400)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Wed, 11 Sep 2013 22:15:18 +0000 (18:15 -0400)
commit	c3a959b3112af83492694b8f0919381b1c467fb8
tree	62ae7f49087bfb61a439161b5bc1cb5c8c691f21	tree
parent	f49c16dd1169d3de4bbfcdca22af1269bbd0a005	commit \| diff

Theory of strings.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

43 files changed:

NEWS		diff \| blob \| history
src/compat/cvc3_compat.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/options/Makefile.am		diff \| blob \| history
src/parser/smt1/smt1.cpp		diff \| blob \| history
src/parser/smt1/smt1.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/smt2/smt2.h		diff \| blob \| history
src/theory/Makefile.am		diff \| blob \| history
src/theory/builtin/kinds		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/strings/Makefile	[new file with mode: 0644]	blob
src/theory/strings/Makefile.am	[new file with mode: 0644]	blob
src/theory/strings/kinds	[new file with mode: 0644]	blob
src/theory/strings/options	[new file with mode: 0644]	blob
src/theory/strings/theory_strings.cpp	[new file with mode: 0644]	blob
src/theory/strings/theory_strings.h	[new file with mode: 0644]	blob
src/theory/strings/theory_strings_rewriter.cpp	[new file with mode: 0644]	blob
src/theory/strings/theory_strings_rewriter.h	[new file with mode: 0644]	blob
src/theory/strings/theory_strings_type_rules.h	[new file with mode: 0644]	blob
src/theory/strings/type_enumerator.h	[new file with mode: 0644]	blob
src/util/Makefile.am		diff \| blob \| history
src/util/regexp.h	[new file with mode: 0644]	blob
test/Makefile.am		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/strings/Makefile	[new file with mode: 0644]	blob
test/regress/regress0/strings/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress0/strings/cardinality.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/loop001.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/loop002.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/loop003.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/loop004.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/loop005.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/loop006.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/str001.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/str002.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/str003.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/str004.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/str005.smt2	[new file with mode: 0644]	blob
test/unit/theory/logic_info_white.h		diff \| blob \| history

RSS Atom