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.h | |
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.h')
-rw-r--r-- | src/theory/logic_info.h | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 36b71e931..8cd326039 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -105,25 +105,25 @@ public: /** Is sharing enabled for this logic? */ bool isSharingEnabled() 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"); return d_sharingTheories > 1; } /** Is the given theory module active in this logic? */ bool isTheoryEnabled(theory::TheoryId theory) 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"); return d_theories[theory]; } /** Is this a quantified logic? */ bool isQuantified() 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"); return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES); } /** Is this the all-inclusive logic? */ bool hasEverything() 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"); LogicInfo everything; everything.lock(); return *this == everything; @@ -131,7 +131,7 @@ public: /** Is this the all-exclusive logic? (Here, that means propositional logic) */ bool hasNothing() 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"); LogicInfo nothing(""); nothing.lock(); return *this == nothing; @@ -143,7 +143,7 @@ public: * use "isPure(theory) && !isQuantified()". */ bool isPure(theory::TheoryId theory) 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"); // the third and fourth conjucts are really just to rule out the misleading // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA return isTheoryEnabled(theory) && !isSharingEnabled() && @@ -155,22 +155,22 @@ public: /** Are integers in this logic? */ bool areIntegersUsed() 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"); return d_integers; } /** Are reals in this logic? */ bool areRealsUsed() 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"); return d_reals; } /** Does this logic only linear arithmetic? */ bool isLinear() 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"); return d_linear || d_differenceLogic; } /** Does this logic only permit difference reasoning? (implies linear) */ bool isDifferenceLogic() 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"); return d_differenceLogic; } @@ -252,13 +252,13 @@ public: /** Are these two LogicInfos equal? */ bool operator==(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried"); for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { if(d_theories[id] != other.d_theories[id]) { return false; } } - Assert(d_sharingTheories == other.d_sharingTheories, "LogicInfo internal inconsistency"); + CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); if(isTheoryEnabled(theory::THEORY_ARITH)) { return d_integers == other.d_integers && @@ -283,13 +283,13 @@ public: } /** Is this LogicInfo "less than or equal" the other? */ bool operator<=(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried"); for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { if(d_theories[id] && !other.d_theories[id]) { return false; } } - Assert(d_sharingTheories <= other.d_sharingTheories, "LogicInfo internal inconsistency"); + CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { return (!d_integers || other.d_integers) && @@ -302,13 +302,13 @@ public: } /** Is this LogicInfo "greater than or equal" the other? */ bool operator>=(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried"); for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { if(!d_theories[id] && other.d_theories[id]) { return false; } } - Assert(d_sharingTheories >= other.d_sharingTheories, "LogicInfo internal inconsistency"); + CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { return (d_integers || !other.d_integers) && |