summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-06-29 00:49:38 +0000
committerMorgan Deters <mdeters@gmail.com>2010-06-29 00:49:38 +0000
commite7e9c10006b5b243a73832ed97c5dec79df6c90a (patch)
treea2826c3f4407e9b9dbf12f6c8bb246dd7302b412 /src/theory/uf
parentc53cd044fa8c172f11e79c94669c1e08419051d5 (diff)
* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"
data into a CDMap. Such a key doesn't disappear from the map on pop, but rather returns to its "initializing" state, set by insertAtContextLevelZero(). This can be used for lazy assignment, among other things, and has been added to support some exploratory coding by Tim in arithmetic. * Made internal CDOmap<> copy constructor private (it should always have been). This is necessary to avoid CxxTest (or others) doing nasty generic programming things that cause context invariants to be broken. * Added unit testing for this feature, and in general beef up the unit testing for CDMap<>. * src/expr/node_manager.cpp: Better output for unhandled cases in getType().
Diffstat (limited to 'src/theory/uf')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback