diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-07 20:45:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-07 20:45:13 +0000 |
commit | e568f34e1f4713c678336fbef1006e585128d466 (patch) | |
tree | a20636a5d50a84d22016f278e9f3a036436125dd /src/theory/logic_info.cpp | |
parent | d71827eef17c181d225f64ea59d26c34d76b9b1e (diff) |
LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.
ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 51 |
1 files changed, 49 insertions, 2 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index ba7119071..d0c1e4b6a 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -37,7 +37,9 @@ LogicInfo::LogicInfo() : d_sharingTheories(0), d_integers(true), d_reals(true), - d_linear(false) { + d_linear(false), + d_differenceLogic(false), + d_locked(false) { for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { d_theories[id] = false;// ensure it's cleared @@ -51,11 +53,16 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : d_sharingTheories(0), d_integers(false), d_reals(false), - d_linear(false) { + d_linear(false), + d_differenceLogic(false), + d_locked(false) { + setLogicString(logicString); + lock(); } std::string LogicInfo::getLogicString() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { size_t seen = 0; // make sure we support all the active theories @@ -108,6 +115,7 @@ std::string LogicInfo::getLogicString() const { } void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { d_theories[id] = false;// ensure it's cleared } @@ -124,6 +132,16 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc if(!strcmp(p, "QF_SAT") || *p == '\0') { // propositional logic only; we're done. p += 6; + } else if(!strcmp(p, "QF_ALL_SUPPORTED")) { + // the "all theories included" logic, no quantifiers + enableEverything(); + disableQuantifiers(); + p += 16; + } else if(!strcmp(p, "ALL_SUPPORTED")) { + // the "all theories included" logic, with quantifiers + enableEverything(); + enableQuantifiers(); + p += 13; } else { if(!strncmp(p, "QF_", 3)) { disableQuantifiers(); @@ -211,7 +229,18 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc d_logicString = logicString; } +void LogicInfo::enableEverything() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + *this = LogicInfo(); +} + +void LogicInfo::disableEverything() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + *this = LogicInfo(""); +} + void LogicInfo::enableTheory(theory::TheoryId theory) { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); if(!d_theories[theory]) { if(isTrueTheory(theory)) { ++d_sharingTheories; @@ -222,6 +251,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) { } void LogicInfo::disableTheory(theory::TheoryId theory) { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); if(d_theories[theory]) { if(isTrueTheory(theory)) { Assert(d_sharingTheories > 0); @@ -237,12 +267,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } void LogicInfo::enableIntegers() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_integers = true; } void LogicInfo::disableIntegers() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_integers = false; if(!d_reals) { @@ -251,12 +283,14 @@ void LogicInfo::disableIntegers() { } void LogicInfo::enableReals() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_reals = true; } void LogicInfo::disableReals() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_reals = false; if(!d_integers) { @@ -265,21 +299,34 @@ void LogicInfo::disableReals() { } void LogicInfo::arithOnlyDifference() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = true; } void LogicInfo::arithOnlyLinear() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = false; } void LogicInfo::arithNonLinear() { + Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = false; d_differenceLogic = false; } +LogicInfo LogicInfo::getUnlockedCopy() const { + if(d_locked) { + LogicInfo info = *this; + info.d_locked = false; + return info; + } else { + return *this; + } +} + }/* CVC4 namespace */ |