From bd0a6c39c56c6ad2bf12e7b9fd41db1772fed9cd Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 5 Dec 2012 21:45:12 +0000 Subject: Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex. --- src/theory/arith/theory_arith.h | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) (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 b791186cf..7d1150fb1 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -89,17 +89,20 @@ private: /** Static learner. */ ArithStaticLearner d_learner; - /** - * List of the variables in the system. - * This is needed to keep a positive ref count on slack variables. - */ - std::vector d_variables; + + ArithVar d_numberOfVariables; + inline ArithVar getNumberOfVariables() const { return d_numberOfVariables; } + std::vector d_pool; + void releaseArithVar(ArithVar v); /** * The map between arith variables to nodes. */ ArithVarNodeMap d_arithvarNodeMap; + typedef ArithVarNodeMap::var_iterator var_iterator; + var_iterator var_begin() const { return d_arithvarNodeMap.var_begin(); } + var_iterator var_end() const { return d_arithvarNodeMap.var_end(); } NodeSet d_setupNodes; bool isSetup(Node n) const { @@ -273,6 +276,18 @@ private: void outputConflicts(); + class TempVarMalloc : public ArithVarMalloc { + private: + TheoryArith& d_ta; + public: + TempVarMalloc(TheoryArith& ta) : d_ta(ta) {} + ArithVar request(){ + Node skolem = mkRealSkolem("tmpVar"); + return d_ta.requestArithVar(skolem, false); + } + void release(ArithVar v){ d_ta.releaseArithVar(v); } + } d_tempVarMalloc; + /** * A copy of the tableau. * This is equivalent to the original tableau if d_tableauSizeHasBeenModified @@ -433,7 +448,7 @@ private: ArithVar requestArithVar(TNode x, bool slack); /** Initial (not context dependent) sets up for a variable.*/ - void setupInitialValue(ArithVar x); + void setupBasicValue(ArithVar x); /** Initial (not context dependent) sets up for a new slack variable.*/ void setupSlack(TNode left); -- cgit v1.2.3