From b1200db566d19132a3f0861eeef35f3c0aaa0a08 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 29 Jun 2010 22:01:30 +0000
Subject: This commit merges the decaying-rows branch into the main trunk.

---
 src/theory/arith/theory_arith.h | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/theory/arith/theory_arith.h')

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index c76923bee..ba9b5329d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -232,6 +232,10 @@ private:
    */
   bool assertionCases(TNode original, TNode assertion);
 
+  TNode findBasicRow(TNode variable);
+  bool shouldEject(TNode var);
+  void ejectInactiveVariables();
+  void reinjectVariable(TNode x);
 
   //TODO get rid of this!
   Node simulatePreprocessing(TNode n);
@@ -249,6 +253,7 @@ private:
 
   Statistics d_statistics;
 
+
 };
 
 }/* CVC4::theory::arith namespace */
-- 
cgit v1.2.3