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

author	Tim King <taking@cs.nyu.edu>
	Fri, 7 Mar 2014 23:00:37 +0000 (18:00 -0500)
committer	Tim King <taking@cs.nyu.edu>
	Fri, 7 Mar 2014 23:00:52 +0000 (18:00 -0500)
commit	9ccdea06edbc72e3ecd282e9e015f6fc4b2e7173
tree	cde6138cb9ab6ef0b7c15edf42e3e8cc53637002	tree
parent	42be934ef4d4430944ae9074c7202a7d130c75bb	commit \| diff

Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

48 files changed:

config/glpk.m4		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.h		diff \| blob \| history
src/theory/arith/arith_ite_utils.cpp	[new file with mode: 0644]	blob
src/theory/arith/arith_ite_utils.h	[new file with mode: 0644]	blob
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.h		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/callbacks.cpp		diff \| blob \| history
src/theory/arith/callbacks.h		diff \| blob \| history
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/constraint_forward.h		diff \| blob \| history
src/theory/arith/cut_log.cpp	[new file with mode: 0644]	blob
src/theory/arith/cut_log.h	[new file with mode: 0644]	blob
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/dio_solver.h		diff \| blob \| history
src/theory/arith/error_set.cpp		diff \| blob \| history
src/theory/arith/error_set.h		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/linear_equality.cpp		diff \| blob \| history
src/theory/arith/linear_equality.h		diff \| blob \| history
src/theory/arith/matrix.h		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/options		diff \| blob \| history
src/theory/arith/partial_model.cpp		diff \| blob \| history
src/theory/arith/partial_model.h		diff \| blob \| history
src/theory/arith/simplex.cpp		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/arith/simplex_update.cpp		diff \| blob \| history
src/theory/arith/simplex_update.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/soi_simplex.h		diff \| blob \| history
src/theory/arith/tableau.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/util/rational_cln_imp.cpp		diff \| blob \| history
src/util/rational_cln_imp.h		diff \| blob \| history
src/util/rational_gmp_imp.cpp		diff \| blob \| history
src/util/rational_gmp_imp.h		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history

RSS Atom