projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ea8139d) | patch
- The array type rules were fixed to use isSubtypeOf.
authorTim King <taking@cs.nyu.edu>
Sat, 19 May 2012 17:24:52 +0000 (17:24 +0000)
committerTim King <taking@cs.nyu.edu>
Sat, 19 May 2012 17:24:52 +0000 (17:24 +0000)
commit7a1139538caede03eb279a7b13ef7476bebd4736
tree3d0d8eea13869c7314c3e17fa524a8d1174ae9d9tree
parentea8139dc7b727bf48bd7b7c6b169d763618a1f2acommit | diff
- The array type rules were fixed to use isSubtypeOf.
- The type of (kind::DIVISION x y) is RealType.
- A reference to util/pseudoboolean.i was removed.
- rec5.cvc is disabled for now.  The type of 2 is Integer which is not a subtype of [0..11].
src/cvc4.i diff | blob | history
src/theory/arith/theory_arith_type_rules.h diff | blob | history
src/theory/arrays/theory_arrays_type_rules.h diff | blob | history
test/regress/regress0/datatypes/Makefile.am diff | blob | history