Changing default language (#4561)

Useful to avoid issues when a language is not set and it cannot be easily inferred (for example via the API). Since the language that covers most operators in CVC4 is the SMT one we use that as default now.

diff --git a/NEWS b/NEWS
index 92cd3ee80bf4a6aa24fd1788cc8805c5f3409623..a7d6d3f40195a3e6f1dca447b95bdfd0e4866449 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -9,6 +9,9 @@ Changes:
   `Result::Entailment` along with corresponding changes to the enum values.
 * Java API change: The name of CVC4's package is now `edu.stanford.CVC4`
   instead of `edu.nyu.acsys.CVC4`.
+* The default output language is changed from CVC to SMT-LIB 2.6. The
+  default output language is used when the problem language cannot be
+  easily inferred (for example when CVC4 is used from the API).
 * Printing of BV constants: previously CVC4 would print BV constant
   values as indexed symbols by default and in binary notation with the
   option --bv-print-consts-in-binary. To be SMT-LIB compliant the

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index f8d62a8be6e31a3aebbfbf0705868989be36165f..332af6e48c8d2902b8a99ec61938c30647e473eb 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -122,9 +122,10 @@ Printer* Printer::getPrinter(OutputLanguage lang)
       lang = language::toOutputLanguage(options::inputLanguage());
      }
    }
-   if(lang == language::output::LANG_AUTO) {
-      lang = language::output::LANG_CVC4; // default
-    }
+   if (lang == language::output::LANG_AUTO)
+   {
+     lang = language::output::LANG_SMTLIB_V2_6;  // default
+   }
   }
   if(d_printers[lang] == NULL) {
     d_printers[lang] = makePrinter(lang);

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 43554088f27ff8d776077428c6f4a76e0b3dfa24..3dcf18f788177246d12247b94149ffeb75cfc6d5 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -416,9 +416,8 @@ void SolverBlack::testMkBitVector()
   TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2),
                    d_solver->mkBitVector("a", 16));
   TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "01010101", 2).toString(),
-                   "0bin01010101");
-  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(),
-                   "0bin00001111");
+                   "#b01010101");
+  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(), "#b00001111");
   TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "-1", 10),
                    d_solver->mkBitVector(8, "FF", 16));
 }