Small fixes to TheoryArith. Added a hack to make Integers a subtype of Real. See...

diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h
index 2a6b43b22615f06a0fdc27a9f65b1c0b9a089b65..e0ad0b038c1fcb5c298201b433c704f98841638e 100644 (file)
--- 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 da16000cef417ae9fbe39d6dfa64dcf4807941a1..821349b45bb60169775207032084a34658e2534a 100644 (file)
--- 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<TypeConstant>() == REAL_TYPE;
+  return getKind() == kind::TYPE_CONSTANT
+    && (getConst<TypeConstant>() == REAL_TYPE || getConst<TypeConstant>() == INTEGER_TYPE);
 }
 
 /** Is this a function type? */

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 1d32fffda7345a80ba02244609cf490f468d5982..f7b1a6b9e7a816236e83dfb60006d3c09e2f4938 100644 (file)
--- 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 eb77b0d54ef0d1d4cc5b8ee9af7d1fccd4a841ca..31afa986c94ecc27964f3db80cc1253b30487499 100644 (file)
--- 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 13ee9183f34ec7cb582ed1dd1ff554b3bd207220..6f1df59580bdc7764608887835b318864b0febf8 100644 (file)
--- 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 5d94d20a9e5065cdf52c71649a456ac52add05be..184844dbc3e563a1a2ab397e4bd86c31b9cdd7cd 100644 (file)
--- 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 2ab94c1953e5b5239d872c4e6e99503284c9c27b..7237c3a5476f8f9a32806060ed2d955255c881c4 100644 (file)
--- 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 66883161ebad61bd579506079cadd2706253336b..6ca447ea5c5a61516d60eb9dd260737280dad5de 100644 (file)
--- 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 (file)
index 0000000..0e17166
--- /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 (file)
index 0000000..5141a0b
--- /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)) )
+)