Remove obsolete test/api/statistics.cpp. (#6116)

This test shouldn't be an API test and is not portable to the new API
right now statistics are not retrievable via the API. When we add
methods for retrieving statistics to the new API, we'll need thorough
unit tests this, which makes this test obsolete.

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index 8750ff8fe2f6f9816f6914a98378c448f9e5bffd..bc185140f31cad345d824ab67b3300ce7a69bd8d 100644 (file)
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -44,8 +44,6 @@ cvc4_add_api_test(ouroborous)
 cvc4_add_api_test(reset_assertions)
 cvc4_add_api_test(sep_log_api)
 cvc4_add_api_test(smt2_compliance)
-# TODO(cvc4-projects#209): Add methods for retrieving statistics to new API
-# cvc4_add_api_test(statistics)
 cvc4_add_api_test(two_solvers)
 cvc4_add_api_test(issue5074)
 cvc4_add_api_test(issue4889)

diff --git a/test/api/statistics.cpp b/test/api/statistics.cpp
deleted file mode 100644 (file)
index 5a11fc7..0000000
--- a/test/api/statistics.cpp
+++ /dev/null
@@ -1,77 +0,0 @@
-/*********************                                                        */
-/*! \file statistics.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andres Noetzli, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A simple statistics test for CVC4.
- **
- ** This simple test just makes sure that the statistics interface is
- ** minimally functional.
- **/
-
-#include "util/statistics.h"
-
-#include <iostream>
-#include <sstream>
-
-#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
-#include "util/sexpr.h"
-
-using namespace CVC4;
-using namespace std;
-
-int main() {
-  api::Solver slv;
-  ExprManager* em = slv.getExprManager();
-  SmtEngine* smt = slv.getSmtEngine();
-  smt->setOption("incremental", SExpr("true"));
-  Expr x = em->mkVar("x", em->integerType());
-  Expr y = em->mkVar("y", em->integerType());
-  smt->assertFormula(em->mkExpr(
-      kind::GT, em->mkExpr(kind::PLUS, x, y), em->mkConst(Rational(5))));
-  Expr q = em->mkExpr(kind::GT, x, em->mkConst(Rational(0)));
-  Result r = smt->checkEntailed(q);
-
-  if (r != Result::NOT_ENTAILED)
-  {
-    exit(1);
-  }
-
-  Statistics stats = smt->getStatistics();
-  for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) {
-    cout << "stat " << (*i).first << " is " << (*i).second << endl;
-  }
-
-  smt->assertFormula(em->mkExpr(kind::LT, y, em->mkConst(Rational(5))));
-  r = smt->checkEntailed(q);
-  Statistics stats2 = smt->getStatistics();
-  bool different = false;
-  for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
-    cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl;
-    cout << "stat2 " << (*i).first << " is " << (*i).second << endl;
-    if (smt->getStatistic((*i).first) != (*i).second)
-    {
-      cout << "SMT engine reports different value for statistic " << (*i).first
-           << ": " << smt->getStatistic((*i).first) << endl;
-      exit(1);
-    }
-    different = different || stats.getStatistic((*i).first) != (*i).second;
-  }
-
-#ifdef CVC4_STATISTICS_ON
-  if(!different) {
-    cout << "stats are the same!  bailing.." << endl;
-    exit(1);
-  }
-#endif /* CVC4_STATISTICS_ON */
-
-  return r == Result::ENTAILED ? 0 : 1;
-}