diff options
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 45 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 22 |
2 files changed, 31 insertions, 36 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 08146760f..35211a49a 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -16,30 +16,29 @@ #include "compat/cvc3_compat.h" -#include "expr/kind.h" -#include "expr/command.h" +#include <algorithm> +#include <cassert> +#include <iostream> +#include <iterator> +#include <sstream> +#include <string> -#include "util/rational.h" -#include "util/integer.h" +#include "base/output.h" +#include "expr/kind.h" +#include "expr/predicate.h" +#include "expr/sexpr.h" +#include "options/expr_options.h" +#include "options/parser_options.h" +#include "options/smt_options.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "smt_util/command.h" #include "util/bitvector.h" #include "util/hash.h" +#include "util/integer.h" +#include "util/rational.h" #include "util/subrange_bound.h" -#include "util/predicate.h" -#include "util/output.h" - -#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> -#include <algorithm> -#include <iterator> -#include <cassert> using namespace std; @@ -2498,8 +2497,8 @@ void ValidityChecker::loadFile(const std::string& fileName, 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")); + d_smt->setOption("input-language", CVC4::SExpr(langss.str())); + d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false)); CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts); CVC4::parser::Parser* p = parserBuilder.build(); p->useDeclarationsFrom(d_parserContext); @@ -2513,8 +2512,8 @@ void ValidityChecker::loadFile(std::istream& is, 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")); + d_smt->setOption("input-language", CVC4::SExpr(langss.str())); + d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false)); CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts); CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build(); d_parserContext = p; diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 0fa4a7ce5..5fefa6871 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -48,23 +48,19 @@ #define _cvc3__include__queryresult_h_ #define _cvc3__include__formula_value_h_ -#include "expr/expr_manager.h" +#include <stdlib.h> +#include <map> +#include <utility> + +#include "base/exception.h" #include "expr/expr.h" +#include "expr/expr_manager.h" #include "expr/type.h" - +#include "parser/parser.h" #include "smt/smt_engine.h" - -#include "util/rational.h" -#include "util/integer.h" - -#include "util/exception.h" #include "util/hash.h" - -#include "parser/parser.h" - -#include <stdlib.h> -#include <map> -#include <utility> +#include "util/integer.h" +#include "util/rational.h" //class CInterface; |