diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3fa00baae..709ba087f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -17,6 +17,7 @@ **/ #include "expr/type.h" +#include "expr/command.h" #include "parser/parser.h" #include "parser/smt/smt.h" #include "parser/smt2/smt2.h" @@ -193,6 +194,16 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_REALS); break; + case Smt::ALL_SUPPORTED: + /* fall through */ + case Smt::QF_ALL_SUPPORTED: + addTheory(THEORY_ARRAYS); + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_BITVECTORS); + break; + case Smt::AUFLIA: case Smt::AUFLIRA: case Smt::AUFNIRA: @@ -211,5 +222,22 @@ void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { // TODO: ??? } +void Smt2::checkThatLogicIsSet() { + if( ! logicIsSet() ) { + if( strictModeEnabled() ) { + parseError("set-logic must appear before this point."); + } else { + warning("No set-logic command was given before this point."); + warning("CVC4 will assume the non-standard ALL_SUPPORTED logic."); + warning("Consider setting a stricter logic for (likely) better performance."); + warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED)."); + + setLogic("ALL_SUPPORTED"); + + preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED")); + } + } +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ |