Made ~Stat() virtual. Added some additional statistics. And added some documentation.

3 files changed, 24 insertions, 6 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 5c19a995d..4dc62f8d3 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -112,12 +112,15 @@ int runCvc4(int argc, char* argv[]) {
   SmtEngine smt(&exprMgr, &options);
 
   // If no file supplied we read from standard input
-  bool inputFromStdin = 
+  bool inputFromStdin =
     firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
 
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
+  ReferenceStat< const char* > s_statFilename("filename",filename);
+  StatisticsRegistry::registerStat(&s_statFilename);
+
   if(options.lang == parser::LANG_AUTO) {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
@@ -160,7 +163,7 @@ int runCvc4(int argc, char* argv[]) {
       ParserBuilder(exprMgr, filename)
         .withInputLanguage(options.lang)
         .withMmap(options.memoryMap)
-        .withChecks(options.semanticChecks && 
+        .withChecks(options.semanticChecks &&
                     !Configuration::isMuzzledBuild() )
         .withStrictMode( options.strictParsing );
 
@@ -185,6 +188,10 @@ int runCvc4(int argc, char* argv[]) {
   // Remove the parser
   delete parser;
 
+  Result asSatResult = lastResult.asSatisfiabilityResult();
+  ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult);
+  StatisticsRegistry::registerStat(&s_statSatResult);
+
   if(options.statistics){
     StatisticsRegistry::flushStatistics(cerr);
   }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c16d8f183..b3b7f58be 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -267,10 +267,10 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
 
 
-  if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){
+  if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
     return false; //sat
   }
-  if(d_partialModel.belowLowerBound(x_i, c_i, true)){
+  if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
diff --git a/src/util/stats.h b/src/util/stats.h
index b9f0fdf61..43f84fee6 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -66,6 +66,7 @@ public:
       AlwaysAssert(d_name.find(s_delim) == std::string::npos);
     }
   }
+  virtual ~Stat() {}
 
   virtual void flushInformation(std::ostream& out) const = 0;
 
@@ -96,6 +97,11 @@ inline void StatisticsRegistry::registerStat(Stat* s) throw (AssertionException)
 }
 
 
+
+/**
+ *  class T must have stream insertion operation defined.
+ * std::ostream& operator<<(std::ostream&, const T&);
+ */
 template<class T>
 class DataStat : public Stat{
 public:
@@ -111,15 +117,20 @@ public:
   }
 };
 
+/** T must have an assignment operator=(). */
 template <class T>
 class ReferenceStat: public DataStat<T>{
 private:
   const T* d_data;
 
 public:
-  ReferenceStat(const std::string& s): DataStat<T>(s), d_data(NULL){}
+  ReferenceStat(const std::string& s):
+    DataStat<T>(s), d_data(NULL)
+  {}
 
-  ReferenceStat(const std::string& s, const T& data):ReferenceStat<T>(s){
+  ReferenceStat(const std::string& s, const T& data):
+    DataStat<T>(s),d_data(NULL)
+  {
     setData(data);
   }