diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7a1fdf174..db242d101 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -86,6 +86,12 @@ void Smt2::addBitvectorOperators() { addOperator(kind::BITVECTOR_ROTATE_RIGHT); } +void Smt2::addStringOperators() { + addOperator(kind::STRING_CONCAT); + addOperator(kind::STRING_LENGTH); + //addOperator(kind::STRING_IN_REGEXP); +} + void Smt2::addTheory(Theory theory) { switch(theory) { case THEORY_CORE: @@ -135,6 +141,11 @@ void Smt2::addTheory(Theory theory) { addBitvectorOperators(); break; + case THEORY_STRINGS: + defineType("String", getExprManager()->stringType()); + addStringOperators(); + break; + case THEORY_QUANTIFIERS: break; @@ -180,6 +191,10 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); } + if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { + addTheory(THEORY_STRINGS); + } + if(d_logic.isQuantified()) { addTheory(THEORY_QUANTIFIERS); } |