diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-04 10:39:27 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-04 10:39:38 +0100 |
commit | 74f1358ca108f3ae4bc8b2d01a2c14e0c20bcc9b (patch) | |
tree | ffcd22bc1205e4619e05af2eac79918287af2374 /src/theory/theory_engine.h | |
parent | f6833bca76627f970d3c61ee163a32869ffa1b10 (diff) |
More work on arithmetic single invocation synthesis conjectures.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4f1a5163e..0dd8b5f71 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -753,6 +753,10 @@ public: return d_theoryTable[theoryId]; } + inline bool isTheoryEnabled(theory::TheoryId theoryId) const { + return d_logicInfo.isTheoryEnabled(theoryId); + } + /** * Returns the equality status of the two terms, from the theory * that owns the domain type. The types of a and b must be the same. |