diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-29 17:57:17 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-29 19:54:13 -0400 |
commit | 03c1daa126ecd86d1434c7512b73723687ea8ca0 (patch) | |
tree | 5c9f3fa488b6a8c63237ccc90598feb6265b14ab /src/parser/parser.h | |
parent | 138259870f2eb506ba8f9b57cf9f44db440e6940 (diff) |
Fix for --force-logic to extend its reach to the parser.
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index b6ba482b7..3f5e66492 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -164,6 +164,16 @@ class CVC4_PUBLIC Parser { */ bool d_canIncludeFile; + /** + * Whether the logic has been forced with --force-logic. + */ + bool d_logicIsForced; + + /** + * The logic, if d_logicIsForced == true. + */ + std::string d_forcedLogic; + /** The set of operators available in the current logic. */ std::set<Kind> d_logicOperators; @@ -262,6 +272,10 @@ public: void disallowIncludeFile() { d_canIncludeFile = false; } bool canIncludeFile() const { return d_canIncludeFile; } + void forceLogic(const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced = true; d_forcedLogic = logic; } + const std::string& getForcedLogic() const { return d_forcedLogic; } + bool logicIsForced() const { return d_logicIsForced; } + /** * Returns a variable, given a name. * |