diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-28 13:29:59 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-28 16:30:14 -0400 |
commit | 735bf7daa07b016aa7964cabdcef27a918d4a96a (patch) | |
tree | 2b322d405693ceea219b70ddcf3dc3e14e47b283 /src | |
parent | 7709fff002e3345bd727eaef2677e28830efb84d (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 132 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 3 | ||||
-rw-r--r-- | src/theory/logic_info.h | 4 |
3 files changed, 22 insertions, 117 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 <sstream> @@ -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; } |