From 735bf7daa07b016aa7964cabdcef27a918d4a96a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 28 May 2013 13:29:59 -0400 Subject: [PATCH] Standardize SMT-LIBv2 set of logics to use LogicInfo. Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2. This led to inconsistencies---such as nonstandard logics like "QF_LIRA" being accepted in set-logic but not providing the "Real" sort. Now, the LogicInfo is used and queried, so nonstandard logics should work fine and declare the correct symbols. SMT-LIB v1.2, unfortunately, can't take advantage of this fully since symbols like "Array" have substantially different meanings in different logics. --- src/parser/smt2/smt2.cpp | 132 ++++------------------------ src/parser/smt2/smt2.h | 3 +- src/theory/logic_info.h | 4 + test/unit/theory/logic_info_white.h | 16 ++-- 4 files changed, 30 insertions(+), 125 deletions(-) diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a7f7796cd..a4623bdfc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -138,135 +138,35 @@ bool Smt2::logicIsSet() { void Smt2::setLogic(const std::string& name) { d_logicSet = true; - d_logic = Smt1::toLogic(name); + d_logic = name; // Core theory belongs to every logic addTheory(THEORY_CORE); - switch(d_logic) { - case Smt1::QF_SAT: - /* No extra symbols necessary */ - break; - - case Smt1::QF_AX: - addTheory(THEORY_ARRAYS); - break; - - case Smt1::QF_IDL: - case Smt1::QF_LIA: - case Smt1::QF_NIA: - addTheory(THEORY_INTS); - break; - - case Smt1::QF_RDL: - case Smt1::QF_LRA: - case Smt1::QF_NRA: - addTheory(THEORY_REALS); - break; - - case Smt1::QF_UF: - addOperator(kind::APPLY_UF); - break; - - case Smt1::QF_UFIDL: - case Smt1::QF_UFLIA: - case Smt1::QF_UFNIA:// nonstandard logic - addTheory(THEORY_INTS); - addOperator(kind::APPLY_UF); - break; - - case Smt1::QF_UFLRA: - case Smt1::QF_UFNRA: - addTheory(THEORY_REALS); - addOperator(kind::APPLY_UF); - break; - - case Smt1::QF_UFLIRA:// nonstandard logic - case Smt1::QF_UFNIRA:// nonstandard logic - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - break; - - case Smt1::QF_BV: - addTheory(THEORY_BITVECTORS); - break; - - case Smt1::QF_ABV: - addTheory(THEORY_ARRAYS); - addTheory(THEORY_BITVECTORS); - break; - - case Smt1::QF_UFBV: - addOperator(kind::APPLY_UF); - addTheory(THEORY_BITVECTORS); - break; - - case Smt1::QF_AUFBV: + if(d_logic.isTheoryEnabled(theory::THEORY_UF)) { addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS); - addTheory(THEORY_BITVECTORS); - break; - - case Smt1::QF_AUFBVLIA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS); - addTheory(THEORY_BITVECTORS); - addTheory(THEORY_INTS); - break; + } - case Smt1::QF_AUFBVLRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS); - addTheory(THEORY_BITVECTORS); - addTheory(THEORY_REALS); - break; + if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { + if(d_logic.areIntegersUsed()) { + addTheory(THEORY_INTS); + } - case Smt1::QF_AUFLIA: - addTheory(THEORY_ARRAYS); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - break; + if(d_logic.areRealsUsed()) { + addTheory(THEORY_REALS); + } + } - case Smt1::QF_AUFLIRA: + if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) { addTheory(THEORY_ARRAYS); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - break; + } - case Smt1::ALL_SUPPORTED: - addTheory(THEORY_QUANTIFIERS); - /* fall through */ - case Smt1::QF_ALL_SUPPORTED: - addTheory(THEORY_ARRAYS); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); + if(d_logic.isTheoryEnabled(theory::THEORY_BV)) { addTheory(THEORY_BITVECTORS); - break; + } - case Smt1::AUFLIA: - case Smt1::AUFLIRA: - case Smt1::AUFNIRA: - case Smt1::LRA: - case Smt1::UFNIA: - case Smt1::UFNIRA: - case Smt1::UFLRA: - if(d_logic != Smt1::AUFLIA && d_logic != Smt1::UFNIA) { - addTheory(THEORY_REALS); - } - if(d_logic != Smt1::LRA) { - addOperator(kind::APPLY_UF); - if(d_logic != Smt1::UFLRA) { - addTheory(THEORY_INTS); - if(d_logic != Smt1::UFNIA && d_logic != Smt1::UFNIRA) { - addTheory(THEORY_ARRAYS); - } - } - } + if(d_logic.isQuantified()) { addTheory(THEORY_QUANTIFIERS); - break; } }/* Smt2::setLogic() */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 5762ff5f9..7a464c773 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -21,6 +21,7 @@ #include "parser/parser.h" #include "parser/smt1/smt1.h" +#include "theory/logic_info.h" #include "util/abstract_value.h" #include @@ -47,7 +48,7 @@ public: private: bool d_logicSet; - Smt1::Logic d_logic; + LogicInfo d_logic; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index c7b5c58f9..2448898c0 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -155,21 +155,25 @@ public: /** Are integers in this logic? */ bool areIntegersUsed() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used"); return d_integers; } /** Are reals in this logic? */ bool areRealsUsed() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used"); return d_reals; } /** Does this logic only linear arithmetic? */ bool isLinear() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear"); return d_linear || d_differenceLogic; } /** Does this logic only permit difference reasoning? (implies linear) */ bool isDifferenceLogic() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); return d_differenceLogic; } diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index a0d415296..39d8aadb1 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -555,10 +555,10 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areRealsUsed() ); + TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException ); // check copy is unchanged info = info.getUnlockedCopy(); @@ -574,10 +574,10 @@ public: TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areRealsUsed() ); + TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException ); + TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException ); // check all-included logic info = info.getUnlockedCopy(); -- 2.30.2