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.h | |
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.h')
-rw-r--r-- | src/theory/logic_info.h | 55 |
1 files changed, 49 insertions, 6 deletions
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index d5b8be58d..33a059bb9 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -54,6 +54,8 @@ class LogicInfo { bool d_linear; /**< linear-only arithmetic in this logic? */ bool d_differenceLogic; /**< difference-only arithmetic in this logic? */ + bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */ + /** * Returns true iff this is a "true" theory (one that must be worried * about for sharing @@ -95,12 +97,19 @@ public: std::string getLogicString() const; /** Is sharing enabled for this logic? */ - bool isSharingEnabled() const { return d_sharingTheories > 1; } + bool isSharingEnabled() const { + Assert(d_locked, "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 { return d_theories[theory]; } + bool isTheoryEnabled(theory::TheoryId theory) const { + Assert(d_locked, "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"); return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES); } @@ -110,6 +119,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"); // 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() && @@ -120,13 +130,25 @@ public: // these are for arithmetic /** Are integers in this logic? */ - bool areIntegersUsed() const { return d_integers; } + bool areIntegersUsed() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_integers; + } /** Are reals in this logic? */ - bool areRealsUsed() const { return d_reals; } + bool areRealsUsed() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_reals; + } /** Does this logic only linear arithmetic? */ - bool isLinear() const { return d_linear || d_differenceLogic; } + bool isLinear() const { + Assert(d_locked, "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 { return d_differenceLogic; } + bool isDifferenceLogic() const { + Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_differenceLogic; + } // MUTATORS @@ -138,6 +160,18 @@ public: void setLogicString(std::string logicString) throw(IllegalArgumentException); /** + * Enable all functionality. All theories, plus quantifiers, will be + * enabled. + */ + void enableEverything(); + + /** + * Disable all functionality. The result will be a LogicInfo with + * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT"). + */ + void disableEverything(); + + /** * Enable the given theory module. */ void enableTheory(theory::TheoryId theory); @@ -181,6 +215,15 @@ public: /** Permit nonlinear arithmetic in this logic. */ void arithNonLinear(); + // LOCKING FUNCTIONALITY + + /** Lock this LogicInfo, disabling further mutation and allowing queries */ + void lock() { d_locked = true; } + /** Check whether this LogicInfo is locked, disallowing further mutation */ + bool isLocked() const { return d_locked; } + /** Get a copy of this LogicInfo that is identical, but unlocked */ + LogicInfo getUnlockedCopy() const; + };/* class LogicInfo */ }/* CVC4 namespace */ |