diff options
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 53 |
1 files changed, 29 insertions, 24 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 15e0d8001..afac925e2 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -31,6 +31,10 @@ #include "parser/parser.h" #include "parser/parser_builder.h" +#include "parser/options.h" +#include "smt/options.h" +#include "expr/options.h" + #include <iostream> #include <string> #include <sstream> @@ -707,21 +711,20 @@ void CLFlags::setFlag(const std::string& name, 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()); + d_smt->setOption("incremental", string("true")); + d_smt->setOption("produce-models", string("true")); + + d_smt->setOption("statistics", string(clflags["stats"].getBool() ? "true" : "false")); + d_smt->setOption("random-seed", int2string(clflags["seed"].getInt())); + d_smt->setOption("interactive-mode", string(clflags["interactive"].getBool() ? "true" : "false")); + d_smt->setOption("parse-only", string(clflags["parse-only"].getBool() ? "true" : "false")); + d_smt->setOption("input-language", clflags["lang"].getString()); if(clflags["output-lang"].getString() == "") { - options.outputLanguage = CVC4::language::toOutputLanguage(options.inputLanguage); + stringstream langss; + langss << CVC4::language::toOutputLanguage(options[CVC4::options::inputLanguage]); + d_smt->setOption("output-language", langss.str()); } else { - options.setOutputLanguage(clflags["output-lang"].getString().c_str()); + d_smt->setOption("output-language", clflags["output-lang"].getString()); } } @@ -1290,7 +1293,7 @@ void ValidityChecker::printExpr(const Expr& e) { void ValidityChecker::printExpr(const Expr& e, std::ostream& os) { Expr::setdepth::Scope sd(os, -1); Expr::printtypes::Scope pt(os, false); - Expr::setlanguage::Scope sl(os, d_em->getOptions()->outputLanguage); + Expr::setlanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]); os << e; } @@ -2133,8 +2136,8 @@ void ValidityChecker::logAnnotation(const Expr& annot) { static void doCommands(CVC4::parser::Parser* parser, CVC4::SmtEngine* smt, CVC4::Options& opts) { while(CVC4::Command* cmd = parser->nextCommand()) { - if(opts.verbosity >= 0) { - cmd->invoke(smt, *opts.out); + if(opts[CVC4::options::verbosity] >= 0) { + cmd->invoke(smt, *opts[CVC4::options::out]); } else { cmd->invoke(smt); } @@ -2146,10 +2149,11 @@ void ValidityChecker::loadFile(const std::string& fileName, InputLanguage lang, bool interactive, bool calledFromParser) { - CVC4::Options opts = *d_em->getOptions(); - opts.inputLanguage = lang; - opts.interactive = interactive; - opts.interactiveSetByUser = true; + CVC4::Options opts = d_em->getOptions(); + stringstream langss; + langss << lang; + d_smt->setOption("input-language", langss.str()); + d_smt->setOption("interactive-mode", string(interactive ? "true" : "false")); CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts); CVC4::parser::Parser* p = parserBuilder.build(); p->useDeclarationsFrom(d_parserContext); @@ -2160,10 +2164,11 @@ void ValidityChecker::loadFile(const std::string& fileName, void ValidityChecker::loadFile(std::istream& is, InputLanguage lang, bool interactive) { - CVC4::Options opts = *d_em->getOptions(); - opts.inputLanguage = lang; - opts.interactive = interactive; - opts.interactiveSetByUser = true; + CVC4::Options opts = d_em->getOptions(); + stringstream langss; + langss << lang; + d_smt->setOption("input-language", langss.str()); + d_smt->setOption("interactive-mode", string(interactive ? "true" : "false")); CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts); CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build(); d_parserContext = p; |