From: Andrew Reynolds Date: Sun, 5 Nov 2017 17:44:21 +0000 (-0600) Subject: Make higher-order a flag in logic info. (#1318) X-Git-Tag: cvc5-1.0.0~5511 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bfeedc822f39875c7d54dac0a744a63c5dc838bd;p=cvc5.git 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 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 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 */