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.

4 files changed, 22 insertions, 4 deletions

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 {