From 7d9d562bb560cb4b83ffaaf94918f834916dad2f Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 28 May 2010 20:17:48 +0000 Subject: Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit. --- src/expr/node_manager.cpp | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/expr') diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7c8fb229a..a1b5b771f 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -229,6 +229,9 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) { case kind::UMINUS: typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n); break; + case kind::DIVISION: + typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n); + break; case kind::CONST_RATIONAL: typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n); break; -- cgit v1.2.3