This commit merges into trunk the branch branches/arithmetic/integers2 from r2650...
authorTim King <taking@cs.nyu.edu>
Wed, 15 Feb 2012 21:52:16 +0000 (21:52 +0000)
committerTim King <taking@cs.nyu.edu>
Wed, 15 Feb 2012 21:52:16 +0000 (21:52 +0000)
commit9a0a59d5c85c4a1d2469f43e9d2b433e156810ba
treeba66b1c5cdeec062ce4144a463ec0b61a83e3cc6
parent093fa1757392e7bfc18493f2daa87ff540aeea86
This commit merges into trunk the branch branches/arithmetic/integers2 from r2650 to r2779.
- This excludes revision 2777.  This revision had some strange performance implications and was delaying the merge.
- This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts.
- The DioSolver can be disabled at command line using --disable-dio-solver.
- This includes a number of changes to the arithmetic normal form.
- The Integer class features a number of new number theoretic function.
- This commit includes a few rather loud warning. I will do my best to take care of them today.
22 files changed:
src/theory/arith/arith_rewriter.cpp
src/theory/arith/arith_utilities.h
src/theory/arith/delta_rational.h
src/theory/arith/dio_solver.cpp
src/theory/arith/dio_solver.h
src/theory/arith/normal_form.cpp
src/theory/arith/normal_form.h
src/theory/arith/partial_model.cpp
src/theory/arith/partial_model.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/util/bitvector.h
src/util/integer_cln_imp.h
src/util/integer_gmp_imp.h
src/util/rational_cln_imp.h
src/util/rational_gmp_imp.h
test/regress/regress0/Makefile.am
test/regress/regress0/bug288b.smt [new file with mode: 0644]
test/regress/regress0/bug288c.smt [new file with mode: 0644]
test/regress/regress1/arith/Makefile.am
test/regress/regress1/arith/lpsat-goal-9.smt2 [new file with mode: 0644]
test/regress/regress1/arith/qlock-4-10-9.base.cvc.smt2 [new file with mode: 0644]