diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-11 11:23:19 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-11 18:15:18 -0400 |
commit | c3a959b3112af83492694b8f0919381b1c467fb8 (patch) | |
tree | 62ae7f49087bfb61a439161b5bc1cb5c8c691f21 /src/theory/logic_info.cpp | |
parent | f49c16dd1169d3de4bbfcdca22af1269bbd0a005 (diff) |
Theory of strings.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 008618342..d74f36069 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic + ** Minor contributors (to current version): Dejan Jovanovic, Tianyi Liang ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -105,6 +105,10 @@ std::string LogicInfo::getLogicString() const { ss << "DT"; ++seen; } + if(d_theories[THEORY_STRINGS]) { + ss << "S"; + ++seen; + } if(d_theories[THEORY_ARITH]) { if(isDifferenceLogic()) { ss << (areIntegersUsed() ? "I" : ""); @@ -177,6 +181,16 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc enableTheory(THEORY_ARRAY); ++p; } + if(*p == 'S') { + // Strings requires arith for length constraints, + // and UF for equality (?) + enableTheory(THEORY_STRINGS); + enableTheory(THEORY_UF); + enableTheory(THEORY_ARITH); + enableIntegers(); + arithOnlyLinear(); + ++p; + } if(!strncmp(p, "UF", 2)) { enableTheory(THEORY_UF); p += 2; |