summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/smt2/smt2.cpp6
-rw-r--r--src/theory/logic_info.cpp110
-rw-r--r--src/theory/logic_info.h35
3 files changed, 110 insertions, 41 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 0fc3678c7..a72b0ac6e 100644
--- 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 335a87501..bf1a9bf65 100644
--- 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 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback