Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.

1 files changed, 8 insertions, 1 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e8d920084..6255efbbc 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -39,6 +39,7 @@
 #include "theory/arith/arith_prop_manager.h"
 #include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/dio_solver.h"
+#include "theory/arith/difference_manager.h"
 
 #include "util/stats.h"
 
@@ -196,9 +197,11 @@ private:
   /** This manager keeps track of information needed to propagate. */
   ArithPropManager d_propManager;
 
+  /** This keeps track of difference equalities. Mostly for sharing. */
+  DifferenceManager d_differenceManager;
+
   /** This implements the Simplex decision procedure. */
   SimplexDecisionProcedure d_simplex;
-
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
   virtual ~TheoryArith();
@@ -228,6 +231,8 @@ public:
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  void addSharedTerm(TNode n);
+
 private:
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;
@@ -329,6 +334,8 @@ private:
     IntStat d_permanentlyRemovedVariables;
     TimerStat d_presolveTime;
 
+    IntStat d_externalBranchAndBounds;
+
     IntStat d_initialTableauSize;
     IntStat d_currSetToSmaller;
     IntStat d_smallerSetToCurr;