From c3a959b3112af83492694b8f0919381b1c467fb8 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 11 Sep 2013 11:23:19 -0400 Subject: Theory of strings. Signed-off-by: Morgan Deters --- src/parser/smt2/Smt2.g | 40 ++++++++++++++++++++++++++++++++++++++-- src/parser/smt2/smt2.cpp | 15 +++++++++++++++ src/parser/smt2/smt2.h | 3 +++ 3 files changed, 56 insertions(+), 2 deletions(-) (limited to 'src/parser/smt2') 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 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 names; std::vector< std::pair > 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 */ -- cgit v1.2.3