projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5321d62) | patch
Small fixes to TheoryArith. Added a hack to make Integers a subtype of Real. See...
authorTim King <taking@cs.nyu.edu>
Fri, 21 May 2010 19:27:18 +0000 (19:27 +0000)
committerTim King <taking@cs.nyu.edu>
Fri, 21 May 2010 19:27:18 +0000 (19:27 +0000)
commit4ba56dc24c972afae6137e4dd6a05f3957e48bf5
tree45bde947434108368092d09a355108469b58d524tree
parent5321d62fce6c747fa9d11e9df5b2ef8c4e25de21commit | diff
Small fixes to TheoryArith.  Added a hack to make Integers a subtype of Real. See Bug 127 for a discussion of the hack.  I am also adding a regression test that does not work (bug 128). It is not enabled so make check should still be fine.
src/expr/builtin_type_rules.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/prop/cnf_stream.cpp diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/tableau.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
test/regress/regress0/ite_arith.smt2 [new file with mode: 0644] blob
test/regress/regress0/ite_real_int_type.smt [new file with mode: 0644] blob