From 232042b3e2e265dbfe9c693d018d48388be91018 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 17 Mar 2011 20:38:32 +0000 Subject: - Removes arith_constants.h - Adds ArithStaticLearner. Consolidates and cleans up the code for static learning in arithmetic. Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick. The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node. - This commit contains miscellaneous other arithmetic cleanup. --- src/theory/arith/simplex.h | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) (limited to 'src/theory/arith/simplex.h') diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index c6bc3c434..6f3ff073f 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -25,9 +25,6 @@ namespace arith { class SimplexDecisionProcedure { private: - /** Stores system wide constants to avoid unnessecary reconstruction. */ - const ArithConstants& d_constants; - /** * Manages information about the assignment and upper and lower bounds on * variables. @@ -44,23 +41,22 @@ private: std::vector d_delayedLemmas; uint32_t d_delayedLemmasPos; + Rational d_ZERO; + public: - SimplexDecisionProcedure(const ArithConstants& constants, - ArithPartialModel& pm, + SimplexDecisionProcedure(ArithPartialModel& pm, OutputChannel* out, Tableau& tableau) : - d_constants(constants), d_partialModel(pm), d_out(out), d_tableau(tableau), d_queue(pm, tableau), d_numVariables(0), d_delayedLemmas(), - d_delayedLemmasPos(0) + d_delayedLemmasPos(0), + d_ZERO(0) {} - -public: /** * Assert*(n, orig) takes an bound n that is implied by orig. * and asserts that as a new bound if it is tighter than the current bound -- cgit v1.2.3