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

author	Martin Brain <martin.brain@cs.ox.ac.uk>
	Thu, 4 Dec 2014 02:29:43 +0000 (21:29 -0500)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Thu, 4 Dec 2014 02:58:28 +0000 (21:58 -0500)
commit	cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7
tree	582afecddf7d64953d8562ab57dd915db6cc852f	tree
parent	2121eaac7e63875f1e6ba53076535d25fd561c04	commit \| diff

Floating point infrastructure.

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

31 files changed:

src/Makefile.am		diff \| blob \| history
src/cvc4.i		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/expr_manager_template.cpp.orig	[new file with mode: 0644]	blob
src/expr/expr_manager_template.h		diff \| blob \| history
src/expr/expr_manager_template.h.orig	[new file with mode: 0644]	blob
src/expr/node_manager.h		diff \| blob \| history
src/expr/node_manager.h.orig	[new file with mode: 0644]	blob
src/expr/type.cpp		diff \| blob \| history
src/expr/type.h		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/options/Makefile.am		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/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/boolean_terms.cpp		diff \| blob \| history
src/theory/fp/kinds	[new file with mode: 0644]	blob
src/theory/fp/options	[new file with mode: 0644]	blob
src/theory/fp/options_handlers.h	[new file with mode: 0644]	blob
src/theory/fp/theory_fp.cpp	[new file with mode: 0644]	blob
src/theory/fp/theory_fp.h	[new file with mode: 0644]	blob
src/theory/fp/theory_fp_rewriter.cpp	[new file with mode: 0644]	blob
src/theory/fp/theory_fp_rewriter.h	[new file with mode: 0644]	blob
src/theory/fp/theory_fp_type_rules.h	[new file with mode: 0644]	blob
src/theory/logic_info.cpp		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/floatingpoint.cpp	[new file with mode: 0644]	blob
src/util/floatingpoint.h	[new file with mode: 0644]	blob
src/util/floatingpoint.i	[new file with mode: 0644]	blob
test/unit/theory/logic_info_white.h		diff \| blob \| history

RSS Atom