diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
commit | d01d291be3213368985f28d0072905c4f033d5ff (patch) | |
tree | 8524a2b6a00c012221ecca9266c3ab9fb11989ed /src/parser | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt/Smt.g | 8 | ||||
-rw-r--r-- | src/parser/smt/smt.cpp | 15 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 1 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 12 |
4 files changed, 33 insertions, 3 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 5a80083b3..6dd4e78f3 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -511,7 +511,13 @@ sortSymbol returns [CVC4::parser::smt::myType t] { $t = PARSER_STATE->getSort(name); } | BITVECTOR_TOK '[' NUMERAL_TOK ']' { $t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK)); - } + } + /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in + * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */ + | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' { + $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)), + EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2))); + } ; /** diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 508bfe352..58495c650 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -44,6 +44,9 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL logicMap["QF_UFLIRA"] = QF_UFLIRA; logicMap["QF_UFNIA"] = QF_UFNIA; logicMap["QF_UFNIRA"] = QF_UFNIRA; + logicMap["QF_ABV"] = QF_ABV; + logicMap["QF_AUFBV"] = QF_AUFBV; + logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; return logicMap; @@ -188,6 +191,17 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; + case QF_ABV: + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + break; + + case QF_AUFBV: + addUf(); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + break; + case QF_AUFLIA: addTheory(THEORY_ARRAYS_EX); addUf(); @@ -206,7 +220,6 @@ void Smt::setLogic(const std::string& name) { case AUFNIRA: case LRA: case UFNIA: - case QF_AUFBV: Unhandled(name); } } diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 62bb24336..3a089641f 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -40,6 +40,7 @@ public: AUFLIRA, AUFNIRA, LRA, + QF_ABV, QF_AUFBV, QF_AUFLIA, QF_AUFLIRA, diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 39eaf5b95..a4b8647a9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -149,6 +149,17 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; + case Smt::QF_ABV: + addTheory(THEORY_ARRAYS); + addTheory(THEORY_BITVECTORS); + break; + + case Smt::QF_AUFBV: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS); + addTheory(THEORY_BITVECTORS); + break; + case Smt::QF_AUFLIA: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); @@ -167,7 +178,6 @@ void Smt2::setLogic(const std::string& name) { case Smt::AUFNIRA: case Smt::LRA: case Smt::UFNIA: - case Smt::QF_AUFBV: Unhandled(name); } } |