diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 20:29:17 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 20:29:17 +0000 |
commit | 8d691eac8e478576ebceb6406a8e372db5e3f7f1 (patch) | |
tree | cd808cd26804490fd5a2e938bf24fdec85918004 /src/parser/smt2/smt2_input.cpp | |
parent | 05d29aa0de4c2d4d773a81375fb14584221595ea (diff) |
true and false are only defined if the core theory is loaded in SMT v2 strict mode
Diffstat (limited to 'src/parser/smt2/smt2_input.cpp')
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index bcefe166b..6d7a04800 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -20,6 +20,7 @@ #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" +#include "parser/smt2/smt2.h" #include "parser/smt2/generated/Smt2Lexer.h" #include "parser/smt2/generated/Smt2Parser.h" @@ -64,5 +65,12 @@ Expr Smt2Input::parseExpr() throw (ParserException) { return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } +void Smt2Input::setParser(Parser& parser) { + super::setParser(parser); + if( !parser.strictModeEnabled() ) { + Smt2::addTheory(parser,Smt2::THEORY_CORE); + } +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ |