make smtlib-model-format default for yices-smt2

Author: ahmed-irfan

doc/manual/manual.tex

@@ -3707,7 +3707,7 @@ \subsubsection*{Model Format}
 To use this format, you must invoke \texttt{yices-smt2} as follows
 \begin{small}
 \begin{lstlisting}[language=sh]
-   yices-smt2 --smt2-model-format
+   yices-smt2 --yices-model-format
 \end{lstlisting}
 \end{small}
 
@@ -3860,7 +3860,7 @@ \subsubsection*{All Command-line Options}
   after all commands have been executed (i.e., after reaching the
   command \texttt{(exit)} or the end of the input file).
 
-\item[--smt2-model-format] Display models in the SMT-LIB~2 format.
+\item[--yices-model-format] Display models in the Yices model format.
 
 \item[--bvconst-in-decimal] Prints bit-vector constants as numbers
   (using the SMT-LIB~2 decimal syntax), instead of constants in binary

doc/yices-smt2.1

@@ -53,8 +53,8 @@ to true.
 .B \-\-mcsat
 Force use of the MCSAT solver.
 .TP
-.B \-\-smt2-model-format
-Print models in the SMT-LIB format (instead of the default Yices format)..
+.B \-\-yices-model-format
+Print models in the Yices model format (instead of the SMT-LIB format)..
 .TP
 .B \-\-bvconst-in-decimal
 Print bitvector constants using the SMT-LIB decimal format, instead of the binary format.

src/frontend/yices_smt2.c

@@ -153,7 +153,7 @@ typedef enum optid {
   verbosity_opt,           // set verbosity on the command line
   incremental_opt,         // enable incremental mode
   interactive_opt,         // enable interactive mode
-  smt2format_opt,          // use SMT-LIB2 format for models
+  yicesformat_opt,         // use the Yices model format for models
   bvdecimal_opt,           // use (_ bv<xxx> n) for bit-vector constants
   timeout_opt,             // give a timeout
   delegate_opt,            // use an external sat solver
@@ -201,7 +201,7 @@ static option_desc_t options[NUM_OPTIONS] = {
   { "timeout", 't', MANDATORY_INT, timeout_opt },
   { "incremental", '\0', FLAG_OPTION, incremental_opt },
   { "interactive", '\0', FLAG_OPTION, interactive_opt },
-  { "smt2-model-format", '\0', FLAG_OPTION, smt2format_opt },
+  { "yices-model-format", '\0', FLAG_OPTION, yicesformat_opt },
   { "bvconst-in-decimal", '\0', FLAG_OPTION, bvdecimal_opt },
   { "delegate", '\0', MANDATORY_STRING, delegate_opt },
   { "dimacs", '\0', MANDATORY_STRING, dimacs_opt },
@@ -264,7 +264,7 @@ static void print_help(const char *progname) {
          "    --stats, -s               Print statistics once all commands have been processed\n"
          "    --incremental             Enable support for push/pop\n"
          "    --interactive             Run in interactive mode (ignored if a filename is given)\n"
-         "    --smt2-model-format       Display models in the SMT-LIB 2 format (default = false)\n"
+         "    --yices-model-format      Display models in the Yices model format (default = false)\n"
          "    --bvconst-in-decimal      Display bit-vector constants as decimal numbers (default = false)\n"
          "    --delegate=<satsolver>    Use an external SAT solver (can be cadical, cryptominisat, kissat, or y2sat)\n"
          "    --dimacs=<filename>       Bitblast and export to a file (in DIMACS format)\n"
@@ -369,7 +369,7 @@ static void parse_command_line(int argc, char *argv[]) {
   filename = NULL;
   incremental = false;
   interactive = false;
-  smt2_model_format = false;
+  smt2_model_format = true;
   bvdecimal = false;
   show_stats = false;
   verbosity = 0;
@@ -505,8 +505,8 @@ static void parse_command_line(int argc, char *argv[]) {
         }
         break;
 
-      case smt2format_opt:
-        smt2_model_format = true;
+      case yicesformat_opt:
+        smt2_model_format = false;
         break;
 
       case bvdecimal_opt:

tests/regress/coverage/smtlib/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking09.smt2.options

@@ -1 +1 @@
---mcsat --trace mcsat::interpolant::check
+--mcsat --yices-model-format --trace mcsat::interpolant::check

tests/regress/coverage/smtlib/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-03.smt2.options

@@ -1 +1 @@
---mcsat --trace mcsat::interpolant::check
+--mcsat --yices-model-format --trace mcsat::interpolant::check

tests/regress/mcsat/bool/assumptions/test01.smt2.options

@@ -1 +1 @@
---mcsat --incremental --trace mcsat::interpolant::check
+--mcsat --incremental --yices-model-format --trace mcsat::interpolant::check

tests/regress/mcsat/bool/assumptions/test01m.smt2.options

@@ -1 +1 @@
---mcsat --trace mcsat::interpolant::check
+--mcsat --yices-model-format --trace mcsat::interpolant::check

tests/regress/mcsat/bv/assumptions/issue233.smt2.options

@@ -1 +1 @@
---mcsat --trace mcsat::interpolant::check
+--mcsat --yices-model-format --trace mcsat::interpolant::check