summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2019-12-10 17:17:00 -0300
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-12-10 14:17:00 -0600
commitd19c52821bb911413ff3dd4494c08a42a1db1e22 (patch)
treeaa91cb7bbc7aa66521b7bbfc528ab67394944616 /src/options
parentee5fed52332ec6baddc8ecd8f8e04a644990bf29 (diff)
Fix ufho issues (#3551)
Diffstat (limited to 'src/options')
-rw-r--r--src/options/options.h1
-rw-r--r--src/options/options_public_functions.cpp7
2 files changed, 6 insertions, 2 deletions
diff --git a/src/options/options.h b/src/options/options.h
index 3f758e392..c321b3499 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -197,6 +197,7 @@ public:
InputLanguage getInputLanguage() const;
InstFormatMode getInstFormatMode() const;
OutputLanguage getOutputLanguage() const;
+ bool getUfHo() const;
bool getCheckProofs() const;
bool getDumpInstantiations() const;
bool getDumpModels() const;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index a753c08de..d3906e24d 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -28,12 +28,13 @@
#include "options/base_options.h"
#include "options/language.h"
#include "options/main_options.h"
+#include "options/option_exception.h"
#include "options/parser_options.h"
#include "options/printer_modes.h"
#include "options/printer_options.h"
-#include "options/option_exception.h"
-#include "options/smt_options.h"
#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
namespace CVC4 {
@@ -50,6 +51,8 @@ OutputLanguage Options::getOutputLanguage() const {
return (*this)[options::outputLanguage];
}
+bool Options::getUfHo() const { return (*this)[options::ufHo]; }
+
bool Options::getCheckProofs() const{
return (*this)[options::checkProofs];
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback