projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2b2c656) | patch
Add ability to provide theory-specific proof rules to EqualityEngine, extends enumera...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Mar 2014 16:50:28 +0000 (11:50 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Mar 2014 16:50:28 +0000 (11:50 -0500)
commit2ad315a59ad2bd7f69ba7a975874aab12f0fa605
tree1798365a3194ff1eb4cb9b741449475ccff7a760tree
parent2b2c656543cc4ee7051ff00211a56f45331a763ccommit | diff
Add ability to provide theory-specific proof rules to EqualityEngine, extends enumeration of MergeReasonType.  Add initial use in TheoryArrays.
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history
src/theory/uf/equality_engine_types.h diff | blob | history