diff options
| -rw-r--r-- | src/theory/strings/options | 2 | ||||
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 2 | ||||
| -rw-r--r-- | src/util/regexp.cpp | 10 | ||||
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/cardinality.smt2 | 2 |
5 files changed, 9 insertions, 8 deletions
diff --git a/src/theory/strings/options b/src/theory/strings/options index 5ac86dcae..139eca6ac 100644 --- 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 1f4e86846..e608a0533 100644 --- 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) {
if(r[i].getKind() == kind::STRING_TO_REGEXP) {
cc.push_back( r[i][0] );
- } if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {
emptyflag = true;
break;
} else {
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 246f16243..684a480fb 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -17,6 +17,7 @@ #include "util/regexp.h"
#include <iostream>
+#include <iomanip>
using namespace std;
@@ -46,11 +47,10 @@ std::string String::toString() const { case '\n': s = "\\n"; break;
case '\e': s = "\\e"; break;
default : {
- std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
- if(s2.size() == 1) {
- s2 = "0" + s2;
- }
- s = "\\x" + s2;
+ std::stringstream ss;
+ ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);
+ s = "\\x" + ss.str();
+ //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
}
}
str += s;
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 254df183e..f11ada1a1 100644 --- 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 d64bc240e..921991f74 100644 --- 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) |