diff options
| author | Martin Brain <martin.brain@cs.ox.ac.uk> | 2014-12-03 21:29:43 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-03 21:58:28 -0500 |
| commit | cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7 (patch) | |
| tree | 582afecddf7d64953d8562ab57dd915db6cc852f /src/theory/logic_info.cpp | |
| parent | 2121eaac7e63875f1e6ba53076535d25fd561c04 (diff) | |
Floating point infrastructure.
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 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 4ea30d5c9..635262a1e 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -107,6 +107,10 @@ std::string LogicInfo::getLogicString() const { ss << "BV"; ++seen; } + if(d_theories[THEORY_FP]) { + ss << "FP"; + ++seen; + } if(d_theories[THEORY_DATATYPES]) { ss << "DT"; ++seen; @@ -206,6 +210,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc enableTheory(THEORY_BV); p += 2; } + if(!strncmp(p, "FP", 2)) { + enableTheory(THEORY_FP); + p += 2; + } if(!strncmp(p, "DT", 2)) { enableTheory(THEORY_DATATYPES); p += 2; |