summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/smt1/smt1.cpp7
-rw-r--r--src/parser/smt1/smt1.h4
-rw-r--r--src/parser/smt2/Smt2.g40
-rw-r--r--src/parser/smt2/smt2.cpp15
-rw-r--r--src/parser/smt2/smt2.h3
5 files changed, 65 insertions, 4 deletions
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 41b0523bd..c9bbd3860 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -3,7 +3,7 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Clark Barrett
+ ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Clark Barrett, Tianyi Liang
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
@@ -39,6 +39,7 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne
logicMap["QF_NIA"] = QF_NIA;
logicMap["QF_NRA"] = QF_NRA;
logicMap["QF_RDL"] = QF_RDL;
+ logicMap["QF_S"] = QF_S;
logicMap["QF_SAT"] = QF_SAT;
logicMap["QF_UF"] = QF_UF;
logicMap["QF_UFIDL"] = QF_UFIDL;
@@ -180,6 +181,10 @@ void Smt1::setLogic(const std::string& name) {
d_logic = toLogic(name);
switch(d_logic) {
+ case QF_S:
+ throw ParserException("Strings theory unsupported in SMT-LIBv1 front-end; try SMT-LIBv2.");
+ break;
+
case QF_AX:
addTheory(THEORY_ARRAYS_EX);
break;
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index d6961371a..f96a4e810 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -3,7 +3,7 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Clark Barrett
+ ** Minor contributors (to current version): Clark Barrett, Tianyi Liang
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
@@ -52,6 +52,7 @@ public:
QF_NIA,
QF_NRA,
QF_RDL,
+ QF_S, // nonstandard (for string theory)
QF_SAT,
QF_UF,
QF_UFIDL,
@@ -82,6 +83,7 @@ public:
THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX,
THEORY_REALS,
THEORY_REALS_INTS,
+ THEORY_STRINGS,
THEORY_QUANTIFIERS
};
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a6a2aa58c..74434f499 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -3,7 +3,7 @@
** \verbatim
** Original author: Christopher L. Conway
** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds, Francois Bobot
+ ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds, Francois Bobot, Tianyi Liang
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
@@ -452,7 +452,7 @@ extendedCommand[CVC4::Command*& cmd]
: DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{ /* open a scope to keep the UnresolvedTypes contained */
PARSER_STATE->pushScope(true); }
- LPAREN_TOK /* parametric sorts */
+ LPAREN_TOK /* parametric sorts */
( symbol[name,CHECK_UNDECLARED,SYM_SORT] {
sorts.push_back( PARSER_STATE->mkSort(name) ); }
)*
@@ -697,6 +697,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
@declarations {
CVC4::Kind k;
std::string s;
+ std::vector<unsigned int> s_vec;
}
: INTEGER_LITERAL
{ sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
@@ -704,6 +705,13 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
{ sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
| str[s]
{ sexpr = SExpr(s); }
+// | LPAREN_TOK STRCST_TOK
+// ( INTEGER_LITERAL {
+// s_vec.push_back( atoi( AntlrInput::tokenText($INTEGER_LITERAL) ) + 65 );
+// } )* RPAREN_TOK
+// {
+// sexpr = SExpr( MK_CONST( ::CVC4::String(s_vec) ) );
+// }
| symbol[s,CHECK_NONE,SYM_SORT]
{ sexpr = SExpr(SExpr::Keyword(s)); }
| tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
@@ -757,6 +765,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
std::hash_set<std::string, StringHashFunction> names;
std::vector< std::pair<std::string, Expr> > binders;
Type type;
+ std::string s;
}
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
@@ -1011,6 +1020,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
expr = MK_CONST( BitVector(binString, 2) ); }
+ | str[s]
+ { expr = MK_CONST( ::CVC4::String(s) ); }
+
// NOTE: Theory constants go here
;
@@ -1222,6 +1234,17 @@ builtinOp[CVC4::Kind& kind]
| BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; }
| BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; }
+ | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; }
+ | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; }
+ | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; }
+ | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; }
+ | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; }
+ | REOR_TOK { $kind = CVC4::kind::REGEXP_OR; }
+ | REINTER_TOK { $kind = CVC4::kind::REGEXP_INTER; }
+ | RESTAR_TOK { $kind = CVC4::kind::REGEXP_STAR; }
+ | REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; }
+ | REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; }
+
// NOTE: Theory operators go here
;
@@ -1579,6 +1602,19 @@ BVSLE_TOK : 'bvsle';
BVSGT_TOK : 'bvsgt';
BVSGE_TOK : 'bvsge';
+//STRING
+STRCST_TOK : 'str.const';
+STRCON_TOK : 'str.++';
+STRLEN_TOK : 'str.len';
+STRINRE_TOK : 'str.in.re';
+STRTORE_TOK : 'str.to.re';
+RECON_TOK : 're.++';
+REOR_TOK : 're.or';
+REINTER_TOK : 're.inter';
+RESTAR_TOK : 're.*';
+REPLUS_TOK : 're.+';
+REOPT_TOK : 're.opt';
+
/**
* A sequence of printable ASCII characters (except backslash) that starts
* and ends with | and does not otherwise contain |.
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7a1fdf174..db242d101 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -86,6 +86,12 @@ void Smt2::addBitvectorOperators() {
addOperator(kind::BITVECTOR_ROTATE_RIGHT);
}
+void Smt2::addStringOperators() {
+ addOperator(kind::STRING_CONCAT);
+ addOperator(kind::STRING_LENGTH);
+ //addOperator(kind::STRING_IN_REGEXP);
+}
+
void Smt2::addTheory(Theory theory) {
switch(theory) {
case THEORY_CORE:
@@ -135,6 +141,11 @@ void Smt2::addTheory(Theory theory) {
addBitvectorOperators();
break;
+ case THEORY_STRINGS:
+ defineType("String", getExprManager()->stringType());
+ addStringOperators();
+ break;
+
case THEORY_QUANTIFIERS:
break;
@@ -180,6 +191,10 @@ void Smt2::setLogic(const std::string& name) {
addTheory(THEORY_BITVECTORS);
}
+ if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
+ addTheory(THEORY_STRINGS);
+ }
+
if(d_logic.isQuantified()) {
addTheory(THEORY_QUANTIFIERS);
}
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 3f1d3b087..cc46efe07 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -44,6 +44,7 @@ public:
THEORY_REALS,
THEORY_REALS_INTS,
THEORY_QUANTIFIERS,
+ THEORY_STRINGS
};
private:
@@ -127,6 +128,8 @@ private:
void addBitvectorOperators();
+ void addStringOperators();
+
};/* class Smt2 */
}/* CVC4::parser namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback