From e322681d960a2fe26a968f6bb16d1d7b10b5215f Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 23 Mar 2012 23:06:29 +0000 Subject: Removed the variableRemovalEnabled option and d_removedRows from TheoryArith. This had been disabled for several months. --- src/theory/arith/theory_arith.h | 14 -------------- 1 file changed, 14 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 ec2df3e17..4f111d350 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -169,13 +169,6 @@ private: Comparison mkIntegerEqualityFromAssignment(ArithVar v); - /** - * If ArithVar v maps to the node n in d_removednode, - * then n = (= asNode(v) rhs) where rhs is a term that - * can be used to determine the value of n using getValue(). - */ - std::map d_removedRows; - /** * List of all of the inequalities asserted in the current context. */ @@ -424,12 +417,6 @@ private: */ bool entireStateIsConsistent(); - /** - * Permanently removes a variable from the problem. - * The caller guarentees the saftey of this removal! - */ - void permanentlyRemoveVariable(ArithVar v); - bool isImpliedUpperBound(ArithVar var, Node exp); bool isImpliedLowerBound(ArithVar var, Node exp); @@ -456,7 +443,6 @@ private: TimerStat d_simplifyTimer; TimerStat d_staticLearningTimer; - IntStat d_permanentlyRemovedVariables; TimerStat d_presolveTime; IntStat d_externalBranchAndBounds; -- cgit v1.2.3