diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /src/theory/logic_info.cpp | |
parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 9660986cf..c4ae81927 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -76,7 +76,7 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : } std::string LogicInfo::getLogicString() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "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 @@ -129,7 +129,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"); + CheckArgument(!d_locked, *this, "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 } @@ -244,17 +244,17 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } void LogicInfo::enableEverything() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(); } void LogicInfo::disableEverything() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "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"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(!d_theories[theory]) { if(isTrueTheory(theory)) { ++d_sharingTheories; @@ -265,7 +265,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) { } void LogicInfo::disableTheory(theory::TheoryId theory) { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(d_theories[theory]) { if(isTrueTheory(theory)) { Assert(d_sharingTheories > 0); @@ -281,14 +281,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } void LogicInfo::enableIntegers() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "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"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_integers = false; if(!d_reals) { @@ -297,14 +297,14 @@ void LogicInfo::disableIntegers() { } void LogicInfo::enableReals() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "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"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_reals = false; if(!d_integers) { @@ -313,21 +313,21 @@ void LogicInfo::disableReals() { } void LogicInfo::arithOnlyDifference() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "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"); + CheckArgument(!d_locked, *this, "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"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = false; d_differenceLogic = false; |