Importing Chris's recent changes to CVC3's ValidityChecker into the compatibility layer

2 files changed, 28 insertions, 4 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 25901f872..c8e9106a7 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1148,11 +1148,31 @@ Type ValidityChecker::importType(const Type& t) {
 }
 
 void ValidityChecker::cmdsFromString(const std::string& s, InputLanguage lang) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  std::stringstream ss(s, std::stringstream::in);
+  return loadFile(ss, lang, false);
 }
 
-Expr ValidityChecker::exprFromString(const std::string& e) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+Expr ValidityChecker::exprFromString(const std::string& s, InputLanguage lang) {
+  std::stringstream ss;
+
+  if( lang != PRESENTATION_LANG && lang != SMTLIB_V2_LANG ) {
+    ss << lang;
+    throw Exception("Unsupported language in exprFromString: " + ss.str());
+  }
+
+  CVC4::parser::Parser* p = CVC4::parser::ParserBuilder(d_em, "<internal>").withStringInput(s).withInputLanguage(lang).build();
+  Expr dummy = p->nextExpression();
+  if( dummy.isNull() ) {
+    throw CVC4::parser::ParserException("Parser result is null: '" + s + "'");
+  }
+  //DebugAssert(dummy.getKind() == RAW_LIST, "Expected list expression");
+  //DebugAssert(dummy.arity() == 2, "Expected two children");
+
+  Expr e = parseExpr(dummy[1]);
+
+  delete p;
+
+  return e;
 }
 
 Expr ValidityChecker::trueExpr() {
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 63df75a68..2798c5b3c 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -747,7 +747,11 @@ public:
                               InputLanguage lang = PRESENTATION_LANG);
 
   //! Parse an expression from a presentation language string
-  virtual Expr exprFromString(const std::string& e);
+  /*! Only PRESENTATION_LANG and SMTLIB_V2_LANG are supported. Any other
+   *  value for lang will raise an exception.
+   */
+  virtual Expr exprFromString(const std::string& e,
+                              InputLanguage lang = PRESENTATION_LANG);
 
   /*@}*/ // End of General Expr Methods