Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.

1 files changed, 20 insertions, 0 deletions

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 331fd2bcb..52aa5a5ce 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -485,6 +485,15 @@ public:
   void setEqualityEngineProof();
   bool hasEqualityEngineProof() const;
 
+
+  /**
+   * There cannot be a literal associated with this constraint.
+   * The explanation is the constant true.
+   * explainInto() does nothing.
+   */
+  //void setPsuedoConstraint();
+  //bool isPsuedoConstraint() const;
+
   /**
    * Returns a explanation of the constraint that is appropriate for conflicts.
    *
@@ -694,6 +703,14 @@ private:
    */
   ProofId d_equalityEngineProof;
 
+  /**
+   * Marks a node as being true always.
+   * This is only okay for purely internal things.
+   *
+   * This is a special proof that is always a member of the list.
+   */
+  //ProofId d_psuedoConstraintProof;
+
   typedef context::CDList<Constraint, ConstraintValue::ProofCleanup> ProofCleanupList;
   typedef context::CDList<Constraint, ConstraintValue::CanBePropagatedCleanup> CBPList;
   typedef context::CDList<Constraint, ConstraintValue::AssertionOrderCleanup> AOList;
@@ -817,6 +834,7 @@ public:
 
   void addVariable(ArithVar v);
   bool variableDatabaseIsSetup(ArithVar v) const;
+  void removeVariable(ArithVar v);
 
   Node eeExplain(ConstConstraint c) const;
   void eeExplain(ConstConstraint c, NodeBuilder<>& nb) const;
@@ -881,6 +899,8 @@ public:
 private:
   void raiseUnateConflict(Constraint ant, Constraint cons);
 
+  DenseSet d_reclaimable;
+
   class Statistics {
   public:
     IntStat d_unatePropagateCalls;