LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.

ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers.  In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 405e397b8..a3ddba013 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -457,6 +457,11 @@ public:
   /** Parse and return the next expression. */
   Expr nextExpression() throw(ParserException);
 
+  /** Issue a warning to the user. */
+  inline void warning(const std::string& msg) {
+    d_input->warning(msg);
+  }
+
   /** Raise a parse error with the given message. */
   inline void parseError(const std::string& msg) throw(ParserException) {
     d_input->parseError(msg);