From 4ba56dc24c972afae6137e4dd6a05f3957e48bf5 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 21 May 2010 19:27:18 +0000 Subject: [PATCH] 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 | 2 +- src/expr/type_node.cpp | 3 ++- src/expr/type_node.h | 4 ++-- src/prop/cnf_stream.cpp | 1 + src/theory/arith/arith_rewriter.cpp | 3 +++ src/theory/arith/arith_rewriter.h | 1 + src/theory/arith/tableau.h | 2 +- src/theory/arith/theory_arith.cpp | 20 +++++++++++++++++--- test/regress/regress0/ite_arith.smt2 | 6 ++++++ test/regress/regress0/ite_real_int_type.smt | 8 ++++++++ 10 files changed, 42 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/ite_arith.smt2 create mode 100644 test/regress/regress0/ite_real_int_type.smt diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h index 2a6b43b22..e0ad0b038 100644 --- a/src/expr/builtin_type_rules.h +++ b/src/expr/builtin_type_rules.h @@ -23,7 +23,7 @@ namespace CVC4 { class EqualityTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) { if (n[0].getType() != n[1].getType()) { throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type"); } diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index da16000ce..821349b45 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -28,7 +28,8 @@ bool TypeNode::isInteger() const { } bool TypeNode::isReal() const { - return getKind() == kind::TYPE_CONSTANT && getConst() == REAL_TYPE; + return getKind() == kind::TYPE_CONSTANT + && (getConst() == REAL_TYPE || getConst() == INTEGER_TYPE); } /** Is this a function type? */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1d32fffda..f7b1a6b9e 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -110,7 +110,7 @@ public: * @return true if expressions are equal, false otherwise */ bool operator==(const TypeNode& typeNode) const { - return d_nv == typeNode.d_nv; + return d_nv == typeNode.d_nv || (typeNode.isReal() && this->isReal()); } /** @@ -119,7 +119,7 @@ public: * @return true if expressions are equal, false otherwise */ bool operator!=(const TypeNode& typeNode) const { - return d_nv != typeNode.d_nv; + return !(*this == typeNode); } /** diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index eb77b0d54..31afa986c 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -338,6 +338,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) { if(node.getKind() == ITE) { Assert( node.getNumChildren() == 3 ); + //TODO should this be a skolem? Node skolem = nodeManager->mkVar(node.getType()); Node newAssertion = nodeManager->mkNode( diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 13ee9183f..6f1df5958 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -417,6 +417,9 @@ Node ArithRewriter::rewriteTerm(TNode t){ return rewritePlus(t); }else if(t.getKind() == kind::DIVISION){ return rewriteConstantDiv(t); + }else if(t.getKind() == kind::MINUS){ + Node sub = makeSubtractionNode(t[0],t[1]); + return rewrite(sub); }else{ Unreachable(); return Node::null(); diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 5d94d20a9..184844dbc 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -75,6 +75,7 @@ private: Node rewriteTerm(TNode t); Node rewriteMult(TNode t); Node rewritePlus(TNode t); + Node rewriteMinus(TNode t); Node makeSubtractionNode(TNode l, TNode r); diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 2ab94c195..7237c3a54 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -94,7 +94,7 @@ public: void subsitute(Row& row_s){ TNode x_s = row_s.basicVar(); - Assert(!has(x_s)); + Assert(has(x_s)); Assert(x_s != d_x_i); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 66883161e..6ca447ea5 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -99,6 +99,7 @@ void TheoryArith::registerTerm(TNode tn){ if(tn.getKind() == kind::BUILTIN) return; if(tn.getMetaKind() == metakind::VARIABLE){ + setupVariable(tn); } @@ -419,12 +420,25 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){ Node TheoryArith::simulatePreprocessing(TNode n){ if(n.getKind() == NOT){ Node sub = simulatePreprocessing(n[0]); - return NodeManager::currentNM()->mkNode(NOT,sub); + if(sub.getKind() == NOT){ + return sub[0]; + }else{ + return NodeManager::currentNM()->mkNode(NOT,sub); + } }else{ Node rewritten = rewrite(n); Kind k = rewritten.getKind(); - if(!isRelationOperator(k)){ - return rewritten; + bool negate = false; + + if(rewritten.getKind() == NOT){ + Node sub = simulatePreprocessing(rewritten[0]); + if(sub.getKind() == NOT){ + return sub[0]; + }else{ + return NodeManager::currentNM()->mkNode(NOT,sub); + } + } else if(!isRelationOperator(k)){ + Unreachable("Slack must be have been created!"); }else if(rewritten[0].getMetaKind() == metakind::VARIABLE){ return rewritten; }else { diff --git a/test/regress/regress0/ite_arith.smt2 b/test/regress/regress0/ite_arith.smt2 new file mode 100644 index 000000000..0e171666f --- /dev/null +++ b/test/regress/regress0/ite_arith.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LRA) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (not (= x (ite true x y)))) +(check-sat) diff --git a/test/regress/regress0/ite_real_int_type.smt b/test/regress/regress0/ite_real_int_type.smt new file mode 100644 index 000000000..5141a0b42 --- /dev/null +++ b/test/regress/regress0/ite_real_int_type.smt @@ -0,0 +1,8 @@ +(benchmark ite_real_int_type +:logic QF_LRA +:status sat +:extrafuns ((x Real)) +:extrafuns ((y Real)) +:formula + (and (= 0 (ite true x 1)) (= 0 (ite (= x 0) 0 1)) (= x (ite true y 0)) (= 0 (ite true 0 0)) ) +) -- 2.30.2