projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5676b8b) | patch
This commit merges in the branch branches/arithmetic/congruence into trunk. Here...
authorTim King <taking@cs.nyu.edu>
Tue, 24 Apr 2012 18:36:40 +0000 (18:36 +0000)
committerTim King <taking@cs.nyu.edu>
Tue, 24 Apr 2012 18:36:40 +0000 (18:36 +0000)
commitc0f5194dd56c5127c5c6dab5e59997eccc2d78a5
tree080d465b923832f14d67da4431642609d66b921btree
parent5676b8bddcf001ba567ebb6d8e7b42dbd13ac9f3commit | diff
This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:
- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager
13 files changed:
src/context/Makefile.am diff | blob | history
src/context/cdmaybe.h [new file with mode: 0644] blob
src/theory/arith/Makefile.am diff | blob | history
src/theory/arith/congruence_manager.cpp [new file with mode: 0644] blob
src/theory/arith/congruence_manager.h [new file with mode: 0644] blob
src/theory/arith/constraint.cpp diff | blob | history
src/theory/arith/constraint.h diff | blob | history
src/theory/arith/difference_manager.cpp [deleted file] blob | history
src/theory/arith/difference_manager.h [deleted file] blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
test/regress/regress0/uflra/Makefile.am diff | blob | history
test/regress/regress0/uflra/constants0.smt [new file with mode: 0644] blob