Remove support for CVC3 language. (#6369)

diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index c4b99a56a24d715c06ccd03b7da490c794461f96..d47897a7cc838e524b054596ae649b5664a0e86d 100644 (file)
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A simple demonstration of the capabilities of CVC4
+ * A simple demonstration of the capabilities of cvc5
  *
  * A simple demonstration of how to use uninterpreted functions, combining this
  * with arithmetic, and extracting a model at the end of a satisfiable query.
@@ -38,7 +38,7 @@ int main()
 {
   Solver slv;
   slv.setOption("produce-models", "true");  // Produce Models
-  slv.setOption("output-language", "cvc4"); // Set the output-language to CVC's
+  slv.setOption("output-language", "cvc"); // Set the output-language to CVC's
   slv.setOption("dag-thresh", "0"); // Disable dagifying the output
   slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
   slv.setLogic(string("QF_UFLIRA"));
@@ -84,13 +84,13 @@ int main()
        << assertions << endl << endl;
 
   cout << "Prove x /= y is entailed. " << endl
-       << "CVC4: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "."
+       << "cvc5: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "."
        << endl
        << endl;
 
   cout << "Call checkSat to show that the assertions are satisfiable. "
        << endl
-       << "CVC4: "
+       << "cvc5: "
        << slv.checkSat() << "."<< endl << endl;
 
   cout << "Call slv.getValue(...) on terms of interest."

diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index eb40f6ba3a00d2c680e1a432f23736e71ffd86c4..adeba3a3c4e1b253fc1b073e8992e008a2c227f6 100644 (file)
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -27,7 +27,7 @@ def prefixPrintGetValue(slv, t, level=0):
 if __name__ == "__main__":
     slv = pycvc4.Solver()
     slv.setOption("produce-models", "true")  # Produce Models
-    slv.setOption("output-language", "cvc4") # Set the output-language to CVC's
+    slv.setOption("output-language", "cvc") # Set the output-language to CVC's
     slv.setOption("dag-thresh", "0") # Disable dagifying the output
     slv.setOption("output-language", "smt2") # use smt-lib v2 as output language
     slv.setLogic("QF_UFLIRA")
@@ -71,11 +71,11 @@ if __name__ == "__main__":
     slv.assertFormula(assertions)
 
     print("Given the following assertions:", assertions, "\n")
-    print("Prove x /= y is entailed.\nCVC4: ",
+    print("Prove x /= y is entailed.\ncvc5: ",
           slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n")
 
     print("Call checkSat to show that the assertions are satisfiable")
-    print("CVC4:", slv.checkSat(), "\n")
+    print("cvc5:", slv.checkSat(), "\n")
 
     print("Call slv.getValue(...) on terms of interest")
     print("slv.getValue({}): {}".format(f_x, slv.getValue(f_x)))

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 13384164ad630e992ea58575ff79d0d431ba09ab..bf17e91f907886431caf5efffcce052fe1d05999 100644 (file)
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -111,23 +111,22 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   }/* switch(language) */
 }/* toOutputLanguage() */
 
-OutputLanguage toOutputLanguage(std::string language) {
-  if (language == "cvc4" || language == "pl" || language == "presentation"
+OutputLanguage toOutputLanguage(std::string language)
+{
+  if (language == "cvc" || language == "pl" || language == "presentation"
       || language == "native" || language == "LANG_CVC")
   {
     return output::LANG_CVC;
   }
-  else if (language == "cvc3" || language == "LANG_CVC3")
-  {
-    return output::LANG_CVC3;
-  }
   else if (language == "smtlib" || language == "smt" || language == "smtlib2"
            || language == "smt2" || language == "smtlib2.6"
            || language == "smt2.6" || language == "LANG_SMTLIB_V2_6"
            || language == "LANG_SMTLIB_V2")
   {
     return output::LANG_SMTLIB_V2_6;
-  } else if(language == "tptp" || language == "LANG_TPTP") {
+  }
+  else if (language == "tptp" || language == "LANG_TPTP")
+  {
     return output::LANG_TPTP;
   }
   else if (language == "sygus" || language == "LANG_SYGUS"
@@ -144,11 +143,12 @@ OutputLanguage toOutputLanguage(std::string language) {
     return output::LANG_AUTO;
   }
 
-  throw OptionException(std::string("unknown output language `" + language + "'"));
-}/* toOutputLanguage() */
+  throw OptionException(
+      std::string("unknown output language `" + language + "'"));
+}
 
 InputLanguage toInputLanguage(std::string language) {
-  if (language == "cvc4" || language == "pl" || language == "presentation"
+  if (language == "cvc" || language == "pl" || language == "presentation"
       || language == "native" || language == "LANG_CVC")
   {
     return input::LANG_CVC;

diff --git a/src/options/language.h b/src/options/language.h
index 413ef59edb5398507b1e4f802492485fba678973..54e0e9dfa7f6e53747c9ed0908eaf9bf65bb3875 100644 (file)
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -114,8 +114,6 @@ enum CVC4_EXPORT Language
 
   /** The AST output language */
   LANG_AST = 10,
-  /** The CVC3-compatibility output language */
-  LANG_CVC3,
 
   /** LANG_MAX is > any valid OutputLanguage id */
   LANG_MAX
@@ -133,9 +131,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_AST:
     out << "LANG_AST";
     break;
-  case LANG_CVC3:
-    out << "LANG_CVC3";
-    break;
   default:
     out << "undefined_output_language";
   }

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index c06a7aab3f8e5a6d96d568058a313a72c89e11cb..91d06dec2ce0b46036385b89c96159d6b50a0752 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -290,7 +290,7 @@ static const std::string languageDescription =
     "\
 Languages currently supported as arguments to the -L / --lang option:\n\
   auto                           attempt to automatically determine language\n\
-  cvc4 | presentation | pl       cvc5 presentation language\n\
+  cvc | presentation | pl        CVC presentation language\n\
   smt | smtlib | smt2 |\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format (cnf, fof and tff)\n\
@@ -298,8 +298,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
   auto                           match output language to input language\n\
-  cvc4 | presentation | pl       cvc5 presentation language\n\
-  cvc3                           CVC3 presentation language\n\
+  cvc | presentation | pl        CVC presentation language\n\
   smt | smtlib | smt2 |\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format\n\

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 6237c874496b88b754ebfa062b3e99fa05ea2dfc..6ab419b8526c4d70a9265cad40628f6796d16ded 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -56,10 +56,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
   case LANG_AST:
     return unique_ptr<Printer>(new printer::ast::AstPrinter());
 
-  case LANG_CVC3:
-    return unique_ptr<Printer>(
-        new printer::cvc::CvcPrinter(/* cvc3-mode = */ true));
-
   default: Unhandled() << lang;
   }
 }

diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index 3f1fa67332f4e00ea3fad73c1b0164b0693a1221..b51982d59bf693d91b9316624689b4b9d76e93ac 100644 (file)
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -10,10 +10,10 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * "Ouroborous" test: does CVC4 read its own output?
+ * "Ouroborous" test: does cvc5 read its own output?
  *
  * The "Ouroborous" test, named after the serpent that swallows its
- * own tail, ensures that CVC4 can parse some input, output it again
+ * own tail, ensures that cvc5 can parse some input, output it again
  * (in any of its languages) and then parse it again.  The result of
  * the first parse must be equal to the result of the second parse;
  * both strings and expressions are compared for equality.
@@ -57,7 +57,7 @@ int main()
   }
   catch (...)
   {
-    std::cerr << "non-cvc4 exception thrown" << std::endl;
+    std::cerr << "non-cvc5 exception thrown" << std::endl;
   }
   return 1;
 }
@@ -66,8 +66,8 @@ std::string parse(std::string instr,
                   std::string input_language,
                   std::string output_language)
 {
-  assert(input_language == "smt2" || input_language == "cvc4");
-  assert(output_language == "smt2" || output_language == "cvc4");
+  assert(input_language == "smt2" || input_language == "cvc");
+  assert(output_language == "smt2" || output_language == "cvc");
 
   std::string declarations;
 
@@ -125,8 +125,8 @@ std::string translate(std::string instr,
                       std::string input_language,
                       std::string output_language)
 {
-  assert(input_language == "smt2" || input_language == "cvc4");
-  assert(output_language == "smt2" || output_language == "cvc4");
+  assert(input_language == "smt2" || input_language == "cvc");
+  assert(output_language == "smt2" || output_language == "cvc");
 
   std::cout << "==============================================" << std::endl
             << "translating from "
@@ -159,9 +159,9 @@ void runTestString(std::string instr, std::string instr_language)
             << "   in language " << input::LANG_SMTLIB_V2 << std::endl;
   std::string smt2str = translate(instr, instr_language, "smt2");
   std::cout << "in SMT2      : " << smt2str << std::endl;
-  std::string cvcstr = translate(smt2str, "smt2", "cvc4");
+  std::string cvcstr = translate(smt2str, "smt2", "cvc");
   std::cout << "in CVC       : " << cvcstr << std::endl;
-  std::string outstr = translate(cvcstr, "cvc4", "smt2");
+  std::string outstr = translate(cvcstr, "cvc", "smt2");
   std::cout << "back to SMT2 : " << outstr << std::endl << std::endl;
 
   assert(outstr == smt2str);  // differences in output
@@ -170,8 +170,8 @@ void runTestString(std::string instr, std::string instr_language)
 int32_t runTest()
 {
   runTestString("(= (f (f y)) x)", "smt2");
-  runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", "cvc4");
-  runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", "cvc4");
-  runTestString("a[x][y] = a[y][x]", "cvc4");
+  runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", "cvc");
+  runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", "cvc");
+  runTestString("a[x][y] = a[y][x]", "cvc");
   return 0;
 }