Generate code for options with modes. (#3561)

This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.

1 files changed, 10 insertions, 3 deletions

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 83a7e3bff..4ad8c8785 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -14,10 +14,12 @@
  ** Implementation of Valuation class.
  **/
 
-#include "expr/node.h"
 #include "theory/valuation.h"
-#include "theory/theory_engine.h"
+
+#include "expr/node.h"
+#include "options/theory_options.h"
 #include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -123,7 +125,12 @@ unsigned Valuation::getAssertionLevel() const{
   return d_engine->getPropEngine()->getAssertionLevel();
 }
 
-std::pair<bool, Node> Valuation::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params, theory::EntailmentCheckSideEffects* out) {
+std::pair<bool, Node> Valuation::entailmentCheck(
+    options::TheoryOfMode mode,
+    TNode lit,
+    const theory::EntailmentCheckParameters* params,
+    theory::EntailmentCheckSideEffects* out)
+{
   return d_engine->entailmentCheck(mode, lit, params, out);
 }