diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-17 16:03:23 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-17 16:03:36 -0500 |
| commit | 8975d286f5da01112bbb9f8f7f9e357a48953314 (patch) | |
| tree | 054723d77f5d59b389ce575ca6a150ae3870e6fa /src/theory/strings | |
| parent | 516409c5d03e8a3a5ac9ff346784d962ebe1c409 (diff) | |
Fix strings preprocessing for justification heuristic
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 8 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 1 |
2 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 2b0cedd07..b2fa3dcd3 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -378,11 +378,15 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { return retNode; } -void StringsPreprocess::simplify(std::vector< Node > &vec_node) { - std::vector< Node > new_nodes; +void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) { for( unsigned i=0; i<vec_node.size(); i++ ){ vec_node[i] = simplify( vec_node[i], new_nodes ); } +} + +void StringsPreprocess::simplify(std::vector< Node > &vec_node) { + std::vector< Node > new_nodes; + simplify(vec_node, new_nodes); vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() ); } diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 7aa0a2af8..c2d5d656a 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -39,6 +39,7 @@ private: void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ); Node simplify( Node t, std::vector< Node > &new_nodes ); public: + void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes); void simplify(std::vector< Node > &vec_node); StringsPreprocess(); }; |