Made ~Stat() virtual. Added some additional statistics. And added some documentation.
authorTim King <taking@cs.nyu.edu>
Tue, 22 Jun 2010 17:25:14 +0000 (17:25 +0000)
committerTim King <taking@cs.nyu.edu>
Tue, 22 Jun 2010 17:25:14 +0000 (17:25 +0000)
src/main/main.cpp
src/theory/arith/theory_arith.cpp
src/util/stats.h

index 5c19a995ded6a4a87e85622278e6a11cf7a1efd1..4dc62f8d35fff13117d4ab576ab9c850dad8879d 100644 (file)
@@ -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);
   }
index c16d8f1830009c837f06534b4088765e7e39017c..b3b7f58be10cf198d954a183976881e37a3c77a0 100644 (file)
@@ -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;
index b9f0fdf61c8dd70b59b6e69c2e480d4f6cdd2022..43f84fee6690eb3aa1d971ff841b48679a3864ea 100644 (file)
@@ -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);
   }