projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 589bf87) | patch
This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and DIVISION...
authorTim King <taking@cs.nyu.edu>
Sat, 29 Sep 2012 07:19:28 +0000 (07:19 +0000)
committerTim King <taking@cs.nyu.edu>
Sat, 29 Sep 2012 07:19:28 +0000 (07:19 +0000)
commit7667b8e139cba6024ebb5e25e280cb15ce1af51a
tree4f7d5a14bdee423a712ac4220690ce92cc1b5a54tree
parent589bf879f00d2d8df4ccdaf3db28674ce3639512commit | diff
This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and DIVISION. Improves support for non-linear monomials in getEqualityStatus(). Fixes bug 405.
src/theory/arith/arith_utilities.h diff | blob | history
src/theory/arith/normal_form.cpp diff | blob | history
src/theory/arith/normal_form.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history