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

* Make higher-order a flag in logic info.

* Format

* Minor

* Format

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 0fc3678c713ff0fd9f5283e320636d5b814b0358..a72b0ac6e4b350d047e48fe51ecf771536b8c30d 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -381,14 +381,16 @@ void Smt2::setLogic(std::string name) {
   } else {
     d_logic = name;
   }
-  
-  // if sygus is enabled, we must enable UF, datatypes and integer arithmetic
+
+  // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
+  // higher-order
   if(sygus()) {
     // get unlocked copy, modify, copy and relock
     LogicInfo log(d_logic.getUnlockedCopy());
     log.enableTheory(theory::THEORY_UF);
     log.enableTheory(theory::THEORY_DATATYPES);
     log.enableIntegers();
+    log.enableHigherOrder();
     d_logic = log;
     d_logic.lock();
   }

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 335a8750168b4cc4c4c223d893bd08250aae5730..bf1a9bf6524e17186c5ad9d0926196a34b5e3551 100644 (file)
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -30,48 +30,51 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-LogicInfo::LogicInfo() :
-  d_logicString(""),
-  d_theories(THEORY_LAST, false),
-  d_sharingTheories(0),
-  d_integers(true),
-  d_reals(true),
-  d_linear(false),
-  d_differenceLogic(false),
-  d_cardinalityConstraints(false),
-  d_locked(false) {
-
+LogicInfo::LogicInfo()
+    : d_logicString(""),
+      d_theories(THEORY_LAST, false),
+      d_sharingTheories(0),
+      d_integers(true),
+      d_reals(true),
+      d_linear(false),
+      d_differenceLogic(false),
+      d_cardinalityConstraints(false),
+      d_higherOrder(true),
+      d_locked(false)
+{
   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
     enableTheory(id);
   }
 }
 
-LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
-  d_logicString(""),
-  d_theories(THEORY_LAST, false),
-  d_sharingTheories(0),
-  d_integers(false),
-  d_reals(false),
-  d_linear(false),
-  d_differenceLogic(false),
-  d_cardinalityConstraints(false),
-  d_locked(false) {
-
+LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException)
+    : d_logicString(""),
+      d_theories(THEORY_LAST, false),
+      d_sharingTheories(0),
+      d_integers(false),
+      d_reals(false),
+      d_linear(false),
+      d_differenceLogic(false),
+      d_cardinalityConstraints(false),
+      d_higherOrder(false),
+      d_locked(false)
+{
   setLogicString(logicString);
   lock();
 }
 
-LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) :
-  d_logicString(""),
-  d_theories(THEORY_LAST, false),
-  d_sharingTheories(0),
-  d_integers(false),
-  d_reals(false),
-  d_linear(false),
-  d_differenceLogic(false),
-  d_cardinalityConstraints(false),
-  d_locked(false) {
-
+LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException)
+    : d_logicString(""),
+      d_theories(THEORY_LAST, false),
+      d_sharingTheories(0),
+      d_integers(false),
+      d_reals(false),
+      d_linear(false),
+      d_differenceLogic(false),
+      d_cardinalityConstraints(false),
+      d_higherOrder(false),
+      d_locked(false)
+{
   setLogicString(logicString);
   lock();
 }
@@ -98,6 +101,15 @@ bool LogicInfo::isQuantified() const {
   return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
 }
 
+/** Is this a higher-order logic? */
+bool LogicInfo::isHigherOrder() const
+{
+  PrettyCheckArgument(d_locked,
+                      *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  return d_higherOrder;
+}
+
 /** Is this the all-inclusive logic? */
 bool LogicInfo::hasEverything() const {
   PrettyCheckArgument(d_locked, *this,
@@ -571,6 +583,38 @@ void LogicInfo::arithNonLinear() {
   d_differenceLogic = false;
 }
 
+void LogicInfo::enableCardinalityConstraints()
+{
+  PrettyCheckArgument(
+      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  d_logicString = "";
+  d_cardinalityConstraints = true;
+}
+
+void LogicInfo::disableCardinalityConstraints()
+{
+  PrettyCheckArgument(
+      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  d_logicString = "";
+  d_cardinalityConstraints = false;
+}
+
+void LogicInfo::enableHigherOrder()
+{
+  PrettyCheckArgument(
+      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  d_logicString = "";
+  d_higherOrder = true;
+}
+
+void LogicInfo::disableHigherOrder()
+{
+  PrettyCheckArgument(
+      !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  d_logicString = "";
+  d_higherOrder = false;
+}
+
 LogicInfo LogicInfo::getUnlockedCopy() const {
   if(d_locked) {
     LogicInfo info = *this;

diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index a502041f520077792025e45a9a678f8fe817d8d3..dc88cc9f4a5eda6a736f2a1ebb15f939767b7753 100644 (file)
--- 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 */