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

author	Tim King <taking@cs.nyu.edu>
	Fri, 26 Apr 2013 21:10:21 +0000 (17:10 -0400)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Fri, 26 Apr 2013 21:10:21 +0000 (17:10 -0400)
commit	9098391fe334d829ec4101f190b8f1fa21c30752
tree	b134fc1fe1c767a50013e1449330ca6a7ee18a3d	tree
parent	a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16	commit \| diff

FCSimplex branch merge

75 files changed:

COPYING		diff \| blob \| history
INSTALL		diff \| blob \| history
Makefile		diff \| blob \| history
config/glpk.m4	[new file with mode: 0644]	blob
configure.ac		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/context/cdhashset.h		diff \| blob \| history
src/context/cdlist.h		diff \| blob \| history
src/main/options_handlers.h		diff \| blob \| history
src/theory/arith/Makefile.am		diff \| blob \| history
src/theory/arith/approx_simplex.cpp	[new file with mode: 0644]	blob
src/theory/arith/approx_simplex.h	[new file with mode: 0644]	blob
src/theory/arith/arith_heuristic_pivot_rule.cpp		diff \| blob \| history
src/theory/arith/arith_heuristic_pivot_rule.h		diff \| blob \| history
src/theory/arith/arith_priority_queue.cpp	[deleted file]	blob \| history
src/theory/arith/arith_priority_queue.h	[deleted file]	blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/arithvar.h		diff \| blob \| history
src/theory/arith/bound_counts.h	[new file with mode: 0644]	blob
src/theory/arith/callbacks.cpp	[new file with mode: 0644]	blob
src/theory/arith/callbacks.h	[new file with mode: 0644]	blob
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/delta_rational.h		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/dio_solver.h		diff \| blob \| history
src/theory/arith/dual_simplex.cpp	[new file with mode: 0644]	blob
src/theory/arith/dual_simplex.h	[new file with mode: 0644]	blob
src/theory/arith/error_set.cpp	[new file with mode: 0644]	blob
src/theory/arith/error_set.h	[new file with mode: 0644]	blob
src/theory/arith/fc_simplex.cpp	[new file with mode: 0644]	blob
src/theory/arith/fc_simplex.h	[new file with mode: 0644]	blob
src/theory/arith/linear_equality.cpp		diff \| blob \| history
src/theory/arith/linear_equality.h		diff \| blob \| history
src/theory/arith/matrix.cpp		diff \| blob \| history
src/theory/arith/matrix.h		diff \| blob \| history
src/theory/arith/options		diff \| blob \| history
src/theory/arith/options_handlers.h		diff \| blob \| history
src/theory/arith/partial_model.cpp		diff \| blob \| history
src/theory/arith/partial_model.h		diff \| blob \| history
src/theory/arith/pure_update_simplex.cpp	[new file with mode: 0644]	blob
src/theory/arith/pure_update_simplex.h	[new file with mode: 0644]	blob
src/theory/arith/simplex-converge.cpp	[new file with mode: 0644]	blob
src/theory/arith/simplex-converge.h	[new file with mode: 0644]	blob
src/theory/arith/simplex.cpp		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/arith/simplex_update.cpp	[new file with mode: 0644]	blob
src/theory/arith/simplex_update.h	[new file with mode: 0644]	blob
src/theory/arith/soi_simplex.cpp	[new file with mode: 0644]	blob
src/theory/arith/soi_simplex.h	[new file with mode: 0644]	blob
src/theory/arith/tableau.cpp	[new file with mode: 0644]	blob
src/theory/arith/tableau.h	[new file with mode: 0644]	blob
src/theory/arith/tableau_sizes.cpp	[new file with mode: 0644]	blob
src/theory/arith/tableau_sizes.h	[new file with mode: 0644]	blob
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp	[new file with mode: 0644]	blob
src/theory/arith/theory_arith_private.h	[new file with mode: 0644]	blob
src/theory/arith/theory_arith_private_forward.h	[new file with mode: 0644]	blob
src/theory/quantifiers/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/configuration.cpp		diff \| blob \| history
src/util/configuration.h		diff \| blob \| history
src/util/configuration_private.h		diff \| blob \| history
src/util/dense_map.h		diff \| blob \| history
src/util/maybe.h	[new file with mode: 0644]	blob
src/util/rational_cln_imp.h		diff \| blob \| history
src/util/rational_gmp_imp.h		diff \| blob \| history
src/util/statistics_registry.h		diff \| blob \| history
test/regress/regress0/arith/integers/Makefile.am		diff \| blob \| history
test/regress/regress0/push-pop/Makefile.am		diff \| blob \| history

RSS Atom