diff options
author | Tim King <taking@cs.nyu.edu> | 2010-11-03 18:42:28 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-11-03 18:42:28 +0000 |
commit | 1528cf8a04d9ba35e5e78c50aaf6ff5b258fd52d (patch) | |
tree | 1fefec3af551b906c6ee274df324bed91f343c3d /src | |
parent | a7f99ba2844707d1b405e1cd3c01404c9e43850a (diff) |
Adds statistics for the number of Uservariables and Slack variables used by arithmetic.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e691788fa..181632812 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -124,6 +124,7 @@ void TheoryArith::preRegisterTerm(TNode n) { } if(isTheoryLeaf(n) || isStrictlyVarList){ + ++(d_statistics.d_statUserVariables); ArithVar varN = requestArithVar(n,false); setupInitialValue(varN); } @@ -197,6 +198,9 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v void TheoryArith::setupSlack(TNode left){ + + + ++(d_statistics.d_statSlackVariables); TypeNode real_type = NodeManager::currentNM()->realType(); Node slack = NodeManager::currentNM()->mkVar(real_type); left.setAttribute(Slack(), slack); |