projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 68237f7) | patch
This merges in the branch cvc4/branches/arithmetic/matrix into trunk.
authorTim King <taking@cs.nyu.edu>
Fri, 27 Apr 2012 14:47:10 +0000 (14:47 +0000)
committerTim King <taking@cs.nyu.edu>
Fri, 27 Apr 2012 14:47:10 +0000 (14:47 +0000)
commitf813ed144b0945334e03bfd769ea3c2cf8b75843
treee70c9bddf5445aac50b5080c2b1719e6ffb478e0tree
parent68237f7d39a03905be4cc133a42083fc3342adb4commit | diff
This merges in the branch cvc4/branches/arithmetic/matrix into trunk.
- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!
21 files changed:
src/context/Makefile.am diff | blob | history
src/context/cddense_set.h [new file with mode: 0644] blob
src/theory/arith/Makefile.am diff | blob | history
src/theory/arith/arith_priority_queue.h diff | blob | history
src/theory/arith/arithvar.h diff | blob | history
src/theory/arith/arithvar_set.h [deleted file] blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/dio_solver.h 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.cpp [new file with mode: 0644] blob
src/theory/arith/matrix.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/tableau.cpp [deleted file] blob | history
src/theory/arith/tableau.h [deleted file] blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/util/Makefile.am diff | blob | history
src/util/dense_map.h [new file with mode: 0644] blob
src/util/index.h [new file with mode: 0644] blob