bug fix (caused by merge), move cardinality option to expert option

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 5ac86dcae844c35c749777e690f2a074a80e19a0..139eca6acc542e6c977782a9282c8c59d1b816e2 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -5,7 +5,7 @@
 
 module STRINGS "theory/strings/options.h" Strings theory
 
-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
+expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the cardinality of the characters used by the theory of strings, default 256
 
 option stringRegExpUnrollDepth strings-regexp-depth --strings-regexp-depth=N int16_t :default 10 :read-write

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 1f4e86846f038219516dd8f687ab805b45f3d18c..e608a0533ac43ebbfd0c8dfc74b8366aaf203a2b 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -702,7 +702,7 @@ void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes )
                                for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
                                        if(r[i].getKind() == kind::STRING_TO_REGEXP) {\r
                                                cc.push_back( r[i][0] );\r
-                                       } if(r[i].getKind() == kind::STRING_TO_REGEXP) {\r
+                                       } else if(r[i].getKind() == kind::REGEXP_EMPTY) {\r
                                                emptyflag = true;\r
                                                break;\r
                                        } else {\r

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 246f1624382b3d3246b967e3ecc6297c5fc80f55..684a480fb2631f26f0ae454becce433e39c89b95 100644 (file)
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -17,6 +17,7 @@
 \r
 #include "util/regexp.h"\r
 #include <iostream>\r
+#include <iomanip>\r
 \r
 using namespace std;\r
 \r
@@ -46,11 +47,10 @@ std::string String::toString() const {
                        case '\n': s = "\\n"; break;\r
                        case '\e': s = "\\e"; break;\r
                        default  : {\r
-                               std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();\r
-                               if(s2.size() == 1) {\r
-                                       s2 = "0" + s2;\r
-                               }\r
-                               s = "\\x" + s2;\r
+                               std::stringstream ss;\r
+                               ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);\r
+                               s = "\\x" + ss.str();\r
+                               //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();\r
                        }\r
                  }\r
                  str += s;\r

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 254df183ee840d65712f27a66c5b932ee5e61c96..f11ada1a1db7c8aaca0679f82bb49d049661fda9 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -21,6 +21,7 @@ MAKEFLAGS = -k
 TESTS =        \
   at001.smt2 \
   cardinality.smt2 \
+  escchar.smt2 \
   str001.smt2 \
   str002.smt2 \
   str003.smt2 \

diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2
index d64bc240e8fc33f1a3040d19fd9409e77c583c38..921991f741cfce822bed67cd9501ba2a31111566 100644 (file)
--- a/test/regress/regress0/strings/cardinality.smt2
+++ b/test/regress/regress0/strings/cardinality.smt2
@@ -1,6 +1,6 @@
 (set-logic QF_S)
 (set-info :status unsat)
-
+;this option for experts only
 (set-option :strings-alphabet-card 2)
 
 (declare-fun x () String)