diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-03 18:24:57 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-03 18:24:57 +0000 |
commit | 40253236078988fecc3becd2619dd5ccad5e3077 (patch) | |
tree | 76193586ff6093a68d158e869ff332d99f32e5b2 /src/compat/cvc3_compat.cpp | |
parent | 69e31c19cc566b6a536914e3a0360b54f6bd748a (diff) |
Importing Chris's recent changes to CVC3's ValidityChecker into the compatibility layer
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 26 |
1 files changed, 23 insertions, 3 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() { |