diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-27 11:24:14 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-27 11:24:41 -0600 |
commit | e43fe877d0800077ee493d926b15ce9bfc73f91e (patch) | |
tree | 7985eb2203b474ab70e47b132c9172f04990b216 /src/theory/strings | |
parent | 76897e049175f7c42c36ddc6375fc52d8dcdf54d (diff) |
minor fix
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 9 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 14 |
2 files changed, 7 insertions, 16 deletions
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"); |