projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ff70395) | patch
Added the division symbol to the parser, and minimal support for it in TheoryArith...
authorTim King <taking@cs.nyu.edu>
Thu, 20 May 2010 22:51:48 +0000 (22:51 +0000)
committerTim King <taking@cs.nyu.edu>
Thu, 20 May 2010 22:51:48 +0000 (22:51 +0000)
commit5321d62fce6c747fa9d11e9df5b2ef8c4e25de21
tree87685c6a9f32d99f09de28a02fc80378a94b6ec9tree
parentff70395fd3dcde9f68eda1c6a8bd70e6491f7458commit | diff
Added the division symbol to the parser, and minimal support for it in TheoryArith.  Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real.
src/parser/smt/Smt.g diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/kinds diff | blob | history
src/theory/arith/partial_model.cpp diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/theory_engine.h diff | blob | history
test/regress/regress0/ite.smt2 diff | blob | history