projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4fc1fe1) | patch
Adding evaluation of constant terms to the equality engine. Evaluation on a particula...
authorDejan Jovanović <dejan@cs.nyu.edu>
Wed, 20 Mar 2013 01:10:27 +0000 (21:10 -0400)
committerDejan Jovanović <dejan@cs.nyu.edu>
Wed, 20 Mar 2013 01:10:27 +0000 (21:10 -0400)
commit66175a0f0e8d9cf3bc89c3d422ef5b18b217a7da
tree5c92ac3c2785e6d84e50f87988404d3624b45209tree
parent4fc1fe120fd570f8e49da2fefa7b8a0bfed9df48commit | diff
Adding evaluation of constant terms to the equality engine. Evaluation on a particular kind can be set by setting interpreted = true when calling addFunctionKind.
.cproject diff | blob | history
src/theory/bv/bv_subtheory_eq.cpp diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history