Make higher-order a flag in logic info. (#1318)

* Make higher-order a flag in logic info.

* Format

* Minor

* Format

1 files changed, 29 insertions, 6 deletions

diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index a502041f5..dc88cc9f4 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -47,12 +47,18 @@ class CVC4_PUBLIC LogicInfo {
   std::vector<bool> d_theories; /**< set of active theories */
   size_t d_sharingTheories; /**< count of theories that need sharing */
 
-  // for arithmetic
-  bool d_integers; /**< are integers used in this logic? */
-  bool d_reals; /**< are reals used in this logic? */
-  bool d_linear; /**< linear-only arithmetic in this logic? */
-  bool d_differenceLogic; /**< difference-only arithmetic in this logic? */
-  bool d_cardinalityConstraints; /**< cardinality constraints in this logic? */
+  /** are integers used in this logic? */
+  bool d_integers;
+  /** are reals used in this logic? */
+  bool d_reals;
+  /** linear-only arithmetic in this logic? */
+  bool d_linear;
+  /** difference-only arithmetic in this logic? */
+  bool d_differenceLogic;
+  /** cardinality constraints in this logic? */
+  bool d_cardinalityConstraints;
+  /** higher-order constraints in this logic? */
+  bool d_higherOrder;
 
   bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
 
@@ -141,6 +147,9 @@ public:
   /** Does this logic allow cardinality constraints? */
   bool hasCardinalityConstraints() const;
 
+  /** Is this a higher order logic? */
+  bool isHigherOrder() const;
+
   // MUTATORS
 
   /**
@@ -204,6 +213,20 @@ public:
   /** Permit nonlinear arithmetic in this logic. */
   void arithNonLinear();
 
+  // for cardinality constraints
+
+  /** Enable the use of cardinality constraints in this logic. */
+  void enableCardinalityConstraints();
+  /** Disable the use of cardinality constraints in this logic. */
+  void disableCardinalityConstraints();
+
+  // for higher-order
+
+  /** Enable the use of higher-order in this logic. */
+  void enableHigherOrder();
+  /** Disable the use of higher-order in this logic. */
+  void disableHigherOrder();
+
   // LOCKING FUNCTIONALITY
 
   /** Lock this LogicInfo, disabling further mutation and allowing queries */