From e43fe877d0800077ee493d926b15ce9bfc73f91e Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 27 Dec 2013 11:24:14 -0600 Subject: [PATCH] minor fix --- src/parser/smt2/Smt2.g | 4 ++-- src/theory/strings/theory_strings_preprocess.cpp | 9 ++++++--- src/theory/strings/theory_strings_type_rules.h | 14 +------------- 3 files changed, 9 insertions(+), 18 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index be8bddcb2..be20e9416 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1252,8 +1252,8 @@ builtinOp[CVC4::Kind& kind] | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } | STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; } -// | STRCTN_TOK { $kind = CVC4::kind::STRING_STRCTN; } -// | STRCAT_TOK { $kind = CVC4::kind::STRING_CHARAT; } + | STRCTN_TOK { $kind = CVC4::kind::STRING_STRCTN; } + | STRCAT_TOK { $kind = CVC4::kind::STRING_CHARAT; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 355b182c9..111c4f51d 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -144,18 +144,21 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { std::vector< Node > or_vec; or_vec.push_back( w.eqNode(y) ); Node x1 = NodeManager::currentNM()->mkBoundVar( t[0].getType() ); - Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND, + Node b1 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x1 ); + Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, b1, NodeManager::currentNM()->mkNode( kind::AND, x1.eqNode( emptyString ).negate(), w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x1, y ) ))); or_vec.push_back( c1 ); Node z2 = NodeManager::currentNM()->mkBoundVar( t[0].getType() ); - Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND, + Node b2 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, z2 ); + Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, b2, NodeManager::currentNM()->mkNode( kind::AND, z2.eqNode( emptyString ).negate(), w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, z2 ) ))); or_vec.push_back( c2 ); Node x3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() ); Node z3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() ); - Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND, + Node b3 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x3, z3 ); + Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, b3, NodeManager::currentNM()->mkNode( kind::AND, x3.eqNode( emptyString ).negate(), z3.eqNode( emptyString ).negate(), w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x3, y, z3 ) ))); or_vec.push_back( c3 ); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index df9d29f0f..9d3197517 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -57,9 +57,6 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ){ - if(n.getNumChildren() != 1) { - throw TypeCheckingExceptionPrivate(n, "expecting 1 term in string length"); - } TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length"); @@ -74,9 +71,6 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ){ - if(n.getNumChildren() != 3) { - throw TypeCheckingExceptionPrivate(n, "expecting 3 terms in substr"); - } TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr"); @@ -99,9 +93,6 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ){ - if(n.getNumChildren() != 2) { - throw TypeCheckingExceptionPrivate(n, "expecting 2 terms in string contain"); - } TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain"); @@ -111,7 +102,7 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain"); } } - return nodeManager->stringType(); + return nodeManager->booleanType(); } }; @@ -120,9 +111,6 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ){ - if(n.getNumChildren() != 2) { - throw TypeCheckingExceptionPrivate(n, "expecting 2 terms in string char at"); - } TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at"); -- 2.30.2