From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 11 Mar 2021 02:29:57 +0000 (-0800)
Subject: Remove obsolete test/api/statistics.cpp. (#6116)
X-Git-Tag: cvc5-1.0.0~2103
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98abdd354351cdf3d8fb64a4eeca38db63cbbeea;p=cvc5.git

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 8750ff8fe..bc185140f 100644
--- 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
index 5a11fc74d..000000000
--- 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;
-}