diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-11 18:47:18 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-11 19:08:20 -0400 |
| commit | aef9f4e13ddcf2fa48226d98a2a14f9141a761f7 (patch) | |
| tree | 1408033093d6baf363bcf4760262d1daf3d7f506 /src/theory/logic_info.h | |
| parent | 21c71dd206b2b131ee12c811bd7b0997de07adfa (diff) | |
Fix for rewriterules build breakage.
Diffstat (limited to 'src/theory/logic_info.h')
| -rw-r--r-- | src/theory/logic_info.h | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 2448898c0..a0777ae70 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -64,7 +64,6 @@ class CVC4_PUBLIC LogicInfo { case theory::THEORY_BUILTIN: case theory::THEORY_BOOL: case theory::THEORY_QUANTIFIERS: - case theory::THEORY_REWRITERULES: return false; default: return true; @@ -117,7 +116,7 @@ public: /** Is this a quantified logic? */ bool isQuantified() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES); + return isTheoryEnabled(theory::THEORY_QUANTIFIERS); } /** Is this the all-inclusive logic? */ @@ -214,7 +213,6 @@ public: */ void enableQuantifiers() { enableTheory(theory::THEORY_QUANTIFIERS); - enableTheory(theory::THEORY_REWRITERULES); } /** @@ -222,7 +220,6 @@ public: */ void disableQuantifiers() { disableTheory(theory::THEORY_QUANTIFIERS); - disableTheory(theory::THEORY_REWRITERULES); } // these are for arithmetic |