diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 13:03:03 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 13:03:03 -0400 |
commit | 79052f8209cb871e6159d148b0586c562948a2fd (patch) | |
tree | d2c7ba8c1688addfaeb284eebf85b922a8eb91b6 /src/parser | |
parent | fbc81b67ac1cfeb3afe37f3299180177faaa1ca6 (diff) | |
parent | e6dc2c46fced4d8121d6d7bdd739d977f32d0462 (diff) |
Merge branch '1.2.x'
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 139 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 3 |
2 files changed, 23 insertions, 119 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a7f7796cd..c042c3992 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -36,7 +36,6 @@ void Smt2::addArithmeticOperators() { addOperator(kind::MINUS); addOperator(kind::UMINUS); addOperator(kind::MULT); - addOperator(kind::DIVISION); addOperator(kind::LT); addOperator(kind::LEQ); addOperator(kind::GT); @@ -106,16 +105,20 @@ void Smt2::addTheory(Theory theory) { case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); - // falling-through on purpose, to add Ints part of RealsInts + addOperator(kind::DIVISION); + // falling through on purpose, to add Ints part of Reals_Ints case THEORY_INTS: defineType("Int", getExprManager()->integerType()); addArithmeticOperators(); + addOperator(kind::INTS_DIVISION); + addOperator(kind::INTS_MODULUS); break; case THEORY_REALS: defineType("Real", getExprManager()->realType()); addArithmeticOperators(); + addOperator(kind::DIVISION); break; case THEORY_BITVECTORS: @@ -138,135 +141,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); |