projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8b202ba) | patch
Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now suppor...
authorTim King <taking@cs.nyu.edu>
Tue, 29 Nov 2011 21:11:45 +0000 (21:11 +0000)
committerTim King <taking@cs.nyu.edu>
Tue, 29 Nov 2011 21:11:45 +0000 (21:11 +0000)
commite9198d9b99c6037165362870436b45826674303f
treeb5e8d01a53d38d353dae7c16351ff9206e1f96c6tree
parent8b202bab8442c927e9ac18a35c71a82444acf63bcommit | diff
Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
13 files changed:
src/prop/prop_engine.cpp diff | blob | history
src/theory/arith/Makefile.am diff | blob | history
src/theory/arith/arith_prop_manager.cpp diff | blob | history
src/theory/arith/arith_prop_manager.h diff | blob | history
src/theory/arith/delta_rational.h diff | blob | history
src/theory/arith/difference_manager.cpp [new file with mode: 0644] blob
src/theory/arith/difference_manager.h [new file with mode: 0644] blob
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/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history