diff options
Diffstat (limited to 'src/theory/arith/linear_equality.h')
-rw-r--r-- | src/theory/arith/linear_equality.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 607ee6244..293a0ddad 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -243,11 +243,6 @@ public: /** Specialization of update if the module is not tracking yet (for Simplex). */ void updateTracked(ArithVar x_i, const DeltaRational& v); - /** - * Updates every non-basic to reflect the assignment in many. - * For use with ApproximateSimplex. - */ - void updateMany(const DenseMap<DeltaRational>& many); /** * Updates the value of a basic variable x_i to v, @@ -259,7 +254,14 @@ public: ArithVariables& getVariables() const{ return d_variables; } Tableau& getTableau() const{ return d_tableau; } + /** + * Updates every non-basic to reflect the assignment in many. + * For use with ApproximateSimplex. + */ + void updateMany(const DenseMap<DeltaRational>& many); void forceNewBasis(const DenseSet& newBasis); + void applySolution(const DenseSet& newBasis, const DenseMap<DeltaRational>& newValues); + /** * Returns a pointer to the first Tableau entry on the row ridx that does not @@ -689,6 +691,7 @@ private: IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings; TimerStat d_weakenTime; + TimerStat d_forceTime; Statistics(); ~Statistics(); |