From: Tim King <taking@cs.nyu.edu>
Date: Wed, 3 Nov 2010 18:42:28 +0000 (+0000)
Subject: Adds statistics for the number of Uservariables and Slack variables used by arithmetic.
X-Git-Tag: cvc5-1.0.0~8751
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1528cf8a04d9ba35e5e78c50aaf6ff5b258fd52d;p=cvc5.git

Adds statistics for the number of Uservariables and Slack variables used by arithmetic.
---

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);