compatibility work, documentation

diff --git a/library_versions b/library_versions
index 2ff79047971428b99632349d1667784a99ddc2ed..4e5a7b82651d6f996196ada38dc64d0d5a128b08 100644 (file)
--- a/library_versions
+++ b/library_versions
@@ -20,5 +20,12 @@
 # CVC4 release numbers and the corresponding interface version
 # information of libraries.
 #
+# For now, libcvc4bindings' version info is used for all language
+# bindings libraries, and _also_ for all "compatibility" bindings
+# libraries (i.e., the old CVC3-esque C and Java bindings).  This
+# may need to be split out in future, if some bindings (particularly
+# the compatibility ones) change more(/less) frequently than the
+# others.
+#
 0\..* libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0
 1\.0 libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 896a1368195d93e92a56a809407d7669e1d838c3..25901f872d533db5ee15cf5e49839d76b31c38a2 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -648,11 +648,30 @@ void CLFlags::setFlag(const std::string& name,
   (*i).second = sv;
 }
 
+void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflags) {
+  // always incremental and model-producing in CVC3 compatibility mode
+  options.incrementalSolving = true;
+  options.produceModels = true;
+
+  options.statistics = clflags["stats"].getBool();
+  options.satRandomSeed = double(clflags["seed"].getInt());
+  options.interactive = clflags["interactive"].getBool();
+  if(options.interactive) {
+    options.interactiveSetByUser = true;
+  }
+  options.parseOnly = clflags["parse-only"].getBool();
+  options.setInputLanguage(clflags["lang"].getString().c_str());
+  if(clflags["output-lang"].getString() == "") {
+    options.outputLanguage = CVC4::language::toOutputLanguage(options.inputLanguage);
+  } else {
+    options.setOutputLanguage(clflags["output-lang"].getString().c_str());
+  }
+}
+
 ValidityChecker::ValidityChecker() :
   d_clflags(new CLFlags()),
   d_options() {
-  d_options.incrementalSolving = true;
-#warning fixme other options from clflags ??
+  setUpOptions(d_options, *d_clflags);
   d_em = new CVC4::ExprManager(d_options);
   d_smt = new CVC4::SmtEngine(d_em);
 }
@@ -660,8 +679,7 @@ ValidityChecker::ValidityChecker() :
 ValidityChecker::ValidityChecker(const CLFlags& clflags) :
   d_clflags(new CLFlags(clflags)),
   d_options() {
-  d_options.incrementalSolving = true;
-#warning fixme other options from clflags ??
+  setUpOptions(d_options, *d_clflags);
   d_em = new CVC4::ExprManager(d_options);
   d_smt = new CVC4::SmtEngine(d_em);
 }
@@ -696,7 +714,7 @@ CLFlags ValidityChecker::createFlags() {
   flags.addFlag("version",CLFlag(true, "print version information and exit"));
   flags.addFlag("interactive", CLFlag(false, "Interactive mode"));
   flags.addFlag("stats", CLFlag(false, "Print run-time statistics"));
-  flags.addFlag("seed", CLFlag(1, "Set the seed for random sequence"));
+  flags.addFlag("seed", CLFlag(91648253, "Set the seed for random sequence"));
   flags.addFlag("printResults", CLFlag(true, "Print results of interactive commands."));
   flags.addFlag("dump-log", CLFlag("", "Dump API call log in CVC3 input "
                                    "format to given file "
@@ -1905,6 +1923,7 @@ void ValidityChecker::loadFile(const std::string& fileName,
   CVC4::Options opts = *d_em->getOptions();
   opts.inputLanguage = lang;
   opts.interactive = interactive;
+  opts.interactiveSetByUser = true;
   CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts);
   CVC4::parser::Parser* parser = parserBuilder.build();
   doCommands(parser, d_smt, opts);
@@ -1917,6 +1936,7 @@ void ValidityChecker::loadFile(std::istream& is,
   CVC4::Options opts = *d_em->getOptions();
   opts.inputLanguage = lang;
   opts.interactive = interactive;
+  opts.interactiveSetByUser = true;
   CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts);
   CVC4::parser::Parser* parser = parserBuilder.withStreamInput(is).build();
   doCommands(parser, d_smt, opts);

diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 81ac3a6aa4ecd3c90c0161ea61463ae4b9905751..63df75a68bfaa10d940d0b93bab8e0f446a5264a 100644 (file)
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -464,6 +464,8 @@ class CVC4_PUBLIC ValidityChecker {
 
   ValidityChecker(const CLFlags& clflags);
 
+  void setUpOptions(CVC4::Options& options, const CLFlags& clflags);
+
 public:
   //! Constructor
   ValidityChecker();

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 009bc73b895b3b7f9e445d82cc73324c3f0f055f..6b79a84bf747b0c88d74409bec951e5a12cadc26 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -393,33 +393,29 @@ throw(OptionException) {
   }
   binary_name = string(progName);
 
-  // The strange string in this call is the short option string.  The
+  // The strange string in this call is the short option string.  An
   // initial '+' means that option processing stops as soon as a
-  // non-option argument is encountered.  The initial ':' indicates
-  // that getopt_long() should return ':' instead of '?' for a missing
-  // option argument.  Then, each letter is a valid short option for
-  // getopt_long(), and if it's encountered, getopt_long() returns
-  // that character.  A ':' after an option character means an
-  // argument is required; two colons indicates an argument is
-  // optional; no colons indicate an argument is not permitted.
-  // cmdlineOptions specifies all the long-options and the return
-  // value for getopt_long() should they be encountered.
+  // non-option argument is encountered (it is not present, by design).
+  // The initial ':' indicates that getopt_long() should return ':'
+  // instead of '?' for a missing option argument.  Then, each letter
+  // is a valid short option for getopt_long(), and if it's encountered,
+  // getopt_long() returns that character.  A ':' after an option
+  // character means an argument is required; two colons indicates an
+  // argument is optional; no colons indicate an argument is not
+  // permitted.  cmdlineOptions specifies all the long-options and the
+  // return value for getopt_long() should they be encountered.
   while((c = getopt_long(argc, argv,
-                         "+:hVvqL:d:t:",
+                         ":hVvqL:d:t:",
                          cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
     case 'h':
       help = true;
       break;
-      // options.printUsage(usage);
-      // exit(1);
 
     case 'V':
       version = true;
       break;
-      // fputs(Configuration::about().c_str(), stdout);
-      // exit(0);
 
     case 'v':
       ++verbosity;
@@ -430,52 +426,11 @@ throw(OptionException) {
       break;
 
     case 'L':
-      if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
-        inputLanguage = language::input::LANG_CVC4;
-        break;
-      } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
-        inputLanguage = language::input::LANG_SMTLIB;
-        break;
-      } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) {
-        inputLanguage = language::input::LANG_SMTLIB_V2;
-        break;
-      } else if(!strcmp(optarg, "auto")) {
-        inputLanguage = language::input::LANG_AUTO;
-        break;
-      }
-
-      if(strcmp(optarg, "help")) {
-        throw OptionException(string("unknown language for --lang: `") +
-                              optarg + "'.  Try --lang help.");
-      }
-
-      languageHelp = true;
+      setInputLanguage(optarg);
       break;
 
     case OUTPUT_LANGUAGE:
-      if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
-        outputLanguage = language::output::LANG_CVC4;
-        break;
-      } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
-        outputLanguage = language::output::LANG_SMTLIB;
-        break;
-      } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) {
-        outputLanguage = language::output::LANG_SMTLIB_V2;
-        break;
-      } else if(!strcmp(optarg, "ast")) {
-        outputLanguage = language::output::LANG_AST;
-        break;
-      } else if(!strcmp(optarg, "auto")) {
-        outputLanguage = language::output::LANG_AUTO;
-        break;
-      }
-
-      if(strcmp(optarg, "help")) {
-        throw OptionException(string("unknown language for --output-lang: `") +
-                              optarg + "'.  Try --output-lang help.");
-      }
-
-      languageHelp = true;
+      setOutputLanguage(optarg);
       break;
 
     case 't':
@@ -842,12 +797,60 @@ throw(OptionException) {
     default:
       throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
     }
-
   }
 
   return optind;
 }
 
+void Options::setOutputLanguage(const char* str) throw(OptionException) {
+  if(!strcmp(str, "cvc4") || !strcmp(str, "pl")) {
+    outputLanguage = language::output::LANG_CVC4;
+    return;
+  } else if(!strcmp(str, "smtlib") || !strcmp(str, "smt")) {
+    outputLanguage = language::output::LANG_SMTLIB;
+    return;
+  } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
+    outputLanguage = language::output::LANG_SMTLIB_V2;
+    return;
+  } else if(!strcmp(str, "ast")) {
+    outputLanguage = language::output::LANG_AST;
+    return;
+  } else if(!strcmp(str, "auto")) {
+    outputLanguage = language::output::LANG_AUTO;
+    return;
+  }
+
+  if(strcmp(str, "help")) {
+    throw OptionException(string("unknown language for --output-lang: `") +
+                          str + "'.  Try --output-lang help.");
+  }
+
+  languageHelp = true;
+}
+
+void Options::setInputLanguage(const char* str) throw(OptionException) {
+  if(!strcmp(str, "cvc4") || !strcmp(str, "pl") || !strcmp(str, "presentation")) {
+    inputLanguage = language::input::LANG_CVC4;
+    return;
+  } else if(!strcmp(str, "smtlib") || !strcmp(str, "smt")) {
+    inputLanguage = language::input::LANG_SMTLIB;
+    return;
+  } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
+    inputLanguage = language::input::LANG_SMTLIB_V2;
+    return;
+  } else if(!strcmp(str, "auto")) {
+    inputLanguage = language::input::LANG_AUTO;
+    return;
+  }
+
+  if(strcmp(str, "help")) {
+    throw OptionException(string("unknown language for --lang: `") +
+                          str + "'.  Try --lang help.");
+  }
+
+  languageHelp = true;
+}
+
 std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) {
   switch(rule) {
   case Options::MINIMUM:

diff --git a/src/util/options.h b/src/util/options.h
index c4e115b085bc442290611c25ed1dce2f2846e084..7fc894d93805d8b4487f36cecfae17adfa0d208c 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -216,8 +216,18 @@ struct CVC4_PUBLIC Options {
   /**
    * Initialize the options based on the given command-line arguments.
    */
-  int parseOptions(int argc, char* argv[])
-    throw(OptionException);
+  int parseOptions(int argc, char* argv[]) throw(OptionException);
+
+  /**
+   * Set the output language based on the given string.
+   */
+  void setOutputLanguage(const char* str) throw(OptionException);
+
+  /**
+   * Set the input language based on the given string.
+   */
+  void setInputLanguage(const char* str) throw(OptionException);
+
 };/* struct Options */
 
 inline std::ostream& operator<<(std::ostream& out,