Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.
datatypes \
helloworld \
linear_arith \
- sets
+ sets \
+ strings
noinst_DATA =
sets_LDADD = \
@builddir@/../../src/libcvc4.la
+strings_SOURCES = \
+ strings.cpp
+strings_LDADD = \
+ @builddir@/../../src/libcvc4.la
+
# for installation
examplesdir = $(docdir)/$(subdir)
examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
HelloWorld.class \
LinearArith.class \
Datatypes.class \
- PipedInput.class
+ PipedInput.class \
+ Strings.class
endif
%.class: %.java
HelloWorld.java \
LinearArith.java \
Datatypes.java \
- PipedInput.java
+ PipedInput.java \
+ Strings.java
# for installation
examplesdir = $(docdir)/$(subdir)
--- /dev/null
+/********************* */\r
+/*! \file Strings.java\r
+ ** \verbatim\r
+ ** Original author: Tianyi Liang\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Reasoning about strings with CVC4 via Java API.\r
+ **\r
+ ** A simple demonstration of reasoning about strings with CVC4 via Jave API.\r
+ **/\r
+\r
+import edu.nyu.acsys.CVC4.*;\r
+\r
+public class Strings {\r
+ public static void main(String[] args) {\r
+ System.loadLibrary("cvc4jni");\r
+\r
+ ExprManager em = new ExprManager();\r
+ SmtEngine smt = new SmtEngine(em);\r
+\r
+ // Set the logic\r
+ smt.setLogic("S");\r
+\r
+ // Produce models\r
+ smt.setOption("produce-models", new SExpr(true));\r
+ // The option strings-exp is needed\r
+ smt.setOption("strings-exp", new SExpr(true));\r
+ // output-language\r
+ smt.setOption("output-language", new SExpr("smt2"));\r
+\r
+ // String type\r
+ Type string = em.stringType();\r
+\r
+ // Variables\r
+ Expr x = em.mkVar("x", string);\r
+ Expr y = em.mkVar("y", string);\r
+ Expr z = em.mkVar("z", string);\r
+\r
+ // String concatenation: x.y\r
+ Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, y);\r
+ // String concatenation: z.z\r
+ Expr rhs = em.mkExpr(Kind.STRING_CONCAT, z, z);;\r
+ // x.y = z.z\r
+ Expr formula1 = em.mkExpr(Kind.EQUAL, lhs, rhs);\r
+\r
+ // Length of y: |y|\r
+ Expr leny = em.mkExpr(Kind.STRING_LENGTH, y);\r
+ // |y| >= 1\r
+ Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(1)));\r
+\r
+ // Make a query\r
+ Expr q = em.mkExpr(Kind.AND,\r
+ formula1,\r
+ formula2);\r
+\r
+ // check sat\r
+ Result result = smt.checkSat(q);\r
+ System.out.println("CVC4 reports: " + q + " is " + result + ".");\r
+\r
+ System.out.println(" x = " + smt.getValue(x));\r
+ }\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file sets.cpp\r
+ ** \verbatim\r
+ ** Original author: Tianyi Liang\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Reasoning about strings with CVC4 via C++ API.\r
+ **\r
+ ** A simple demonstration of reasoning about strings with CVC4 via C++ API.\r
+ **/\r
+\r
+#include <iostream>\r
+\r
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed\r
+#include "smt/smt_engine.h"\r
+\r
+using namespace CVC4;\r
+\r
+int main() {\r
+ ExprManager em;\r
+ SmtEngine smt(&em);\r
+\r
+ // Set the logic\r
+ smt.setLogic("S");\r
+\r
+ // Produce models\r
+ smt.setOption("produce-models", true);\r
+\r
+ // The option strings-exp is needed\r
+ smt.setOption("strings-exp", true);\r
+\r
+ // Set output language to SMTLIB2\r
+ std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);\r
+ \r
+ // String type\r
+ Type string = em.stringType();\r
+\r
+ // std::string\r
+ std::string std_str_ab("ab");\r
+ // CVC4::String\r
+ CVC4::String cvc4_str_ab(std_str_ab);\r
+ CVC4::String cvc4_str_abc("abc");\r
+ // String constants\r
+ Expr ab = em.mkConst(cvc4_str_ab);\r
+ Expr abc = em.mkConst(CVC4::String("abc"));\r
+ // String variables\r
+ Expr x = em.mkVar("x", string);\r
+ Expr y = em.mkVar("y", string);\r
+ Expr z = em.mkVar("z", string);\r
+\r
+ // String concatenation: x.ab.y\r
+ Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y);\r
+ // String concatenation: abc.z\r
+ Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z);\r
+ // x.ab.y = abc.z\r
+ Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs);\r
+\r
+ // Length of y: |y|\r
+ Expr leny = em.mkExpr(kind::STRING_LENGTH, y);\r
+ // |y| >= 0\r
+ Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0)));\r
+\r
+ // Regular expression: (ab[c-e]*f)|g|h\r
+ Expr r = em.mkExpr(kind::REGEXP_UNION,\r
+ em.mkExpr(kind::REGEXP_CONCAT,\r
+ em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))),\r
+ em.mkExpr(kind::REGEXP_STAR,\r
+ em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))),\r
+ em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))),\r
+ em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))),\r
+ em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("h"))));\r
+\r
+ // String variables\r
+ Expr s1 = em.mkVar("s1", string);\r
+ Expr s2 = em.mkVar("s2", string);\r
+ // String concatenation: s1.s2\r
+ Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2);\r
+\r
+ // s1.s2 in (ab[c-e]*f)|g|h\r
+ Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r);\r
+\r
+ // Make a query\r
+ Expr q = em.mkExpr(kind::AND,\r
+ formula1,\r
+ formula2,\r
+ formula3);\r
+\r
+ // check sat\r
+ Result result = smt.checkSat(q);\r
+ std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;\r
+\r
+ if(result == Result::SAT) {\r
+ std::cout << " x = " << smt.getValue(x) << std::endl;\r
+ std::cout << " s1.s2 = " << smt.getValue(s) << std::endl;\r
+ }\r
+}\r
}
case kind::CONST_STRING: {
- const String& s = n.getConst<String>();
+ const std::vector<unsigned int>& s = n.getConst<String>().getVec();
out << '"';
for(size_t i = 0; i < s.size(); ++i) {
char c = String::convertUnsignedIntToChar(s[i]);
namespace strings {
RegExpOpr::RegExpOpr()
- : d_card( 256 ),
+ : d_lastchar( '\xff' ),
RMAXINT( LONG_MAX )
{
d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
retNode = d_emptySingleton;
break;
}
+ case kind::REGEXP_RANGE: {
+ CVC4::String a = r[0].getConst<String>();
+ CVC4::String b = r[1].getConst<String>();
+ retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp;
+ break;
+ }
case kind::STRING_TO_REGEXP: {
Node tmp = Rewriter::rewrite(r[0]);
if(tmp.isConst()) {
retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
break;
}
+ case kind::REGEXP_RANGE: {
+ CVC4::String a = r[0].getConst<String>();
+ CVC4::String b = r[1].getConst<String>();
+ retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp;
+ break;
+ }
case kind::STRING_TO_REGEXP: {
if(r[0].isConst()) {
if(r[0] == d_emptyString) {
default: {
//TODO: special sym: sigma, none, all
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;
- Assert( false, "Unsupported Term" );
+ Unreachable();
//return Node::null();
}
}
}
}
-void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) {
- std::map< Node, std::pair< std::set<unsigned>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
+void RegExpOpr::firstChars( Node r, std::set<char> &pcset, SetNodes &pvset ) {
+ std::map< Node, std::pair< std::set<char>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
if(itr != d_fset_cache.end()) {
pcset.insert((itr->second).first.begin(), (itr->second).first.end());
pvset.insert((itr->second).second.begin(), (itr->second).second.end());
} else {
- std::set<unsigned> cset;
+ std::set<char> cset;
SetNodes vset;
int k = r.getKind();
switch( k ) {
break;
}
case kind::REGEXP_SIGMA: {
- for(unsigned i=0; i<d_card; i++) {
+ for(char i='\0'; i<=d_lastchar; i++) {
cset.insert(i);
}
break;
if(st.isConst()) {
CVC4::String s = st.getConst< CVC4::String >();
if(s.size() != 0) {
- cset.insert(s[0]);
+ cset.insert(s.getFirstChar());
}
} else if(st.getKind() == kind::VARIABLE) {
vset.insert( st );
} else {
if(st[0].isConst()) {
CVC4::String s = st[0].getConst< CVC4::String >();
- cset.insert(s[0]);
+ cset.insert(s.getFirstChar());
} else {
vset.insert( st[0] );
}
break;
}
default: {
- Trace("strings-regexp") << "Unsupported term: " << r << " in getCharSet." << std::endl;
- Assert( false, "Unsupported Term" );
+ //Trace("regexp-error") << "Unsupported term: " << r << " in firstChars." << std::endl;
+ Unreachable();
}
}
pcset.insert(cset.begin(), cset.end());
pvset.insert(vset.begin(), vset.end());
- std::pair< std::set<unsigned>, SetNodes > p(cset, vset);
+ std::pair< std::set<char>, SetNodes > p(cset, vset);
d_fset_cache[r] = p;
if(Trace.isOn("regexp-fset")) {
Trace("regexp-fset") << "FSET(" << mkString(r) << ") = {";
- for(std::set<unsigned>::const_iterator itr = cset.begin();
+ for(std::set<char>::const_iterator itr = cset.begin();
itr != cset.end(); itr++) {
if(itr != cset.begin()) {
Trace("regexp-fset") << ",";
}
- Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr);
+ Trace("regexp-fset") << (*itr);
}
Trace("regexp-fset") << "}" << std::endl;
}
}
}
-void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) {
- std::map< Node, std::pair< std::set<unsigned>, SetNodes > >::const_iterator itr = d_cset_cache.find(r);
+void RegExpOpr::getCharSet( Node r, std::set<char> &pcset, SetNodes &pvset ) {
+ std::map< Node, std::pair< std::set<char>, SetNodes > >::const_iterator itr = d_cset_cache.find(r);
if(itr != d_cset_cache.end()) {
pcset.insert((itr->second).first.begin(), (itr->second).first.end());
pvset.insert((itr->second).second.begin(), (itr->second).second.end());
} else {
- std::set<unsigned> cset;
+ std::set<char> cset;
SetNodes vset;
int k = r.getKind();
switch( k ) {
break;
}
case kind::REGEXP_SIGMA: {
- for(unsigned i=0; i<d_card; i++) {
+ for(char i='\0'; i<=d_lastchar; i++) {
+ cset.insert(i);
+ }
+ break;
+ }
+ case kind::REGEXP_RANGE: {
+ char a = r[0].getConst<String>().getFirstChar();
+ char b = r[1].getConst<String>().getFirstChar();
+ for(char i=a; i<=b; i++) {
cset.insert(i);
}
break;
break;
}
default: {
- Trace("strings-regexp") << "Unsupported term: " << r << " in getCharSet." << std::endl;
- Assert( false, "Unsupported Term" );
+ //Trace("strings-error") << "Unsupported term: " << r << " in getCharSet." << std::endl;
+ Unreachable();
}
}
pcset.insert(cset.begin(), cset.end());
pvset.insert(vset.begin(), vset.end());
- std::pair< std::set<unsigned>, SetNodes > p(cset, vset);
+ std::pair< std::set<char>, SetNodes > p(cset, vset);
d_cset_cache[r] = p;
Trace("regexp-cset") << "CSET( " << mkString(r) << " ) = { ";
- for(std::set<unsigned>::const_iterator itr = cset.begin();
+ for(std::set<char>::const_iterator itr = cset.begin();
itr != cset.end(); itr++) {
- Trace("regexp-cset") << CVC4::String::convertUnsignedIntToChar(*itr) << ",";
+ Trace("regexp-cset") << (*itr) << ",";
}
Trace("regexp-cset") << " }" << std::endl;
}
r2 = n;
}
} else if(n.getKind() == kind::REGEXP_CONCAT) {
- //TODO
- //convert2 x (r@(Seq l r1))
- // | contains x r1 = let (r2,r3) = convert2 x r1
- // in (Seq l r2, r3)
- // | otherwise = (Empty, r)
bool flag = true;
std::vector<Node> vr1, vr2;
for( unsigned i=0; i<n.getNumChildren(); i++ ) {
}
r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr1);
r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr2);
- } else if(n.getKind() == kind::STRING_TO_REGEXP) {
+ } else if(n.getKind() == kind::STRING_TO_REGEXP || n.getKind() == kind::REGEXP_SIGMA || n.getKind() == kind::REGEXP_RANGE) {
r1 = d_emptySingleton;
r2 = n;
} else {
//is it possible?
+ Unreachable();
}
}
}
Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt ) {
- //(checkConstRegExp(r1) && checkConstRegExp(r2))
+ //Assert(checkConstRegExp(r1) && checkConstRegExp(r2));
if(r1 > r2) {
TNode tmpNode = r1;
r1 = r2;
if(itrcache != cache.end()) {
rNode = itrcache->second;
} else {
- std::vector< unsigned > cset;
- std::set< unsigned > cset1, cset2;
+ std::vector< char > cset;
+ std::set< char > cset1, cset2;
std::set< Node > vset1, vset2;
firstChars(r1, cset1, vset1);
firstChars(r2, cset2, vset2);
}
if(Trace.isOn("regexp-int-debug")) {
Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {";
- for(std::vector<unsigned>::const_iterator itr = cset.begin();
+ for(std::vector<char>::const_iterator itr = cset.begin();
itr != cset.end(); itr++) {
- CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
+ //CVC4::String c( *itr );
if(itr != cset.begin()) {
Trace("regexp-int-debug") << ", ";
}
- Trace("regexp-int-debug") << c;
+ Trace("regexp-int-debug") << ( *itr );
}
Trace("regexp-int-debug") << std::endl;
}
std::map< PairNodes, Node > cacheX;
- for(std::vector<unsigned>::const_iterator itr = cset.begin();
+ for(std::vector<char>::const_iterator itr = cset.begin();
itr != cset.end(); itr++) {
- CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
+ CVC4::String c( *itr );
Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl;
Node r1l = derivativeSingle(r1, c);
Node r2l = derivativeSingle(r2, c);
Node rr1 = removeIntersection(r1);
Node rr2 = removeIntersection(r2);
std::map< PairNodes, Node > cache;
- //std::map< PairNodes, Node > inter_cache;
- return intersectInternal(rr1, rr2, cache, 1);
+ Trace("regexp-intersect") << "Start INTERSECTION(\n\t" << mkString(r1) << ",\n\t"<< mkString(r2) << ")" << std::endl;
+ Node retNode = intersectInternal(rr1, rr2, cache, 1);
+ Trace("regexp-intersect") << "End INTERSECTION(\n\t" << mkString(r1) << ",\n\t"<< mkString(r2) << ") =\n\t" << mkString(retNode) << std::endl;
+ return retNode;
} else {
spflag = true;
return Node::null();
//TODO: var to be extended
ret = 0;
} else {
- std::set<unsigned> cset;
+ std::set<char> cset;
SetNodes vset;
firstChars(r, cset, vset);
std::vector< Node > vec_nodes;
- for(unsigned i=0; i<d_card; i++) {
- CVC4::String c = CVC4::String::convertUnsignedIntToChar(i);
+ for(char i=0; i<=d_lastchar; i++) {
+ CVC4::String c(i);
Node n = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c));
Node r2;
if(cset.find(i) == cset.end()) {
std::string RegExpOpr::niceChar(Node r) {
if(r.isConst()) {
std::string s = r.getConst<CVC4::String>().toString() ;
- return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s );
+ return s == "" ? "{E}" : ( s == " " ? "{ }" : s );
} else {
std::string ss = "$" + r.toString();
return ss;
typedef std::pair< Node, Node > PairNodes;
private:
- unsigned d_card;
+ const char d_lastchar;
Node d_emptyString;
Node d_true;
Node d_false;
std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;
std::map< Node, std::pair< Node, int > > d_compl_cache;
std::map< Node, bool > d_cstre_cache;
- std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;
- std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;
+ std::map< Node, std::pair< std::set<char>, std::set<Node> > > d_cset_cache;
+ std::map< Node, std::pair< std::set<char>, std::set<Node> > > d_fset_cache;
std::map< PairNodes, Node > d_inter_cache;
std::map< Node, Node > d_rm_inter_cache;
std::map< Node, bool > d_norv_cache;
Node mkAllExceptOne( char c );
bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2);
- void getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
+ void getCharSet( Node r, std::set<char> &pcset, SetNodes &pvset );
bool containC2(unsigned cnt, Node n);
Node convert1(unsigned cnt, Node n);
void convert2(unsigned cnt, Node n, Node &r1, Node &r2);
bool testNoRV(Node r);
Node intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt );
Node removeIntersection(Node r);
- void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
+ void firstChars( Node r, std::set<char> &pcset, SetNodes &pvset );
//TODO: for intersection
bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );
+ /*class CState {
+ public:
+ Node r1;
+ Node r2;
+ unsigned cnt;
+ Node head;
+ CState(Node rr1, Node rr2, Node rcnt, Node rhead)
+ : r1(rr1), r2(rr2), cnt(rcnt), head(rhead) {}
+ };*/
+
public:
RegExpOpr();
void TheoryStrings::preRegisterTerm(TNode n) {
if( d_registed_terms_cache.find(n) == d_registed_terms_cache.end() ) {
switch( n.getKind() ) {
- case kind::EQUAL:
+ case kind::EQUAL: {
d_equalityEngine.addTriggerEquality(n);
break;
- case kind::STRING_IN_REGEXP:
+ }
+ case kind::STRING_IN_REGEXP: {
+ d_out->requirePhase(n, true);
d_equalityEngine.addTriggerPredicate(n);
break;
+ }
//case kind::STRING_SUBSTR_TOTAL:
default: {
if( n.getType().isString() ) {
return false;
}
}
+ case kind::REGEXP_RANGE: {
+ if(s.size() == index_start + 1) {
+ char a = r[0].getConst<String>().getFirstChar();
+ char b = r[1].getConst<String>().getFirstChar();
+ char c = s.getLastChar();
+ return (a <= c && c <= b);
+ } else {
+ return false;
+ }
+ }
default: {
Trace("strings-error") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl;
Assert( false, "Unsupported Term" );
}
}
-void String::getCharSet(std::set<unsigned int> &cset) const {
+void String::getCharSet(std::set<char> &cset) const {
for(std::vector<unsigned int>::const_iterator itr = d_str.begin();
itr != d_str.end(); itr++) {
- cset.insert( *itr );
+ cset.insert( convertUnsignedIntToChar(*itr) );
}
}
std::string str;
for(unsigned int i=0; i<d_str.size(); ++i) {
char c = convertUnsignedIntToChar( d_str[i] );
- if(isprint( c )) {
- if(c == '\\') {
- str += "\\\\";
- } else if(c == '\"') {
- str += "\\\"";
- } else {
- str += c;
- }
+ if(isprint( c )) {
+ if(c == '\\') {
+ str += "\\\\";
+ } else if(c == '\"') {
+ str += "\\\"";
+ } else {
+ str += c;
+ }
} else {
std::string s;
switch(c) {
- case '\a': s = "\\a"; break;
- case '\b': s = "\\b"; break;
- case '\t': s = "\\t"; break;
- case '\r': s = "\\r"; break;
- case '\v': s = "\\v"; break;
- case '\f': s = "\\f"; break;
- case '\n': s = "\\n"; break;
- case '\e': s = "\\e"; break;
- default : {
- std::stringstream ss;
- ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);
- std::string t = ss.str();
- t = t.substr(t.size()-2, 2);
- s = "\\x" + t;
- //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
- }
+ case '\a': s = "\\a"; break;
+ case '\b': s = "\\b"; break;
+ case '\t': s = "\\t"; break;
+ case '\r': s = "\\r"; break;
+ case '\v': s = "\\v"; break;
+ case '\f': s = "\\f"; break;
+ case '\n': s = "\\n"; break;
+ case '\e': s = "\\e"; break;
+ default : {
+ std::stringstream ss;
+ ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);
+ std::string t = ss.str();
+ t = t.substr(t.size()-2, 2);
+ s = "\\x" + t;
+ //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
+ }
}
str += s;
}
if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
else {
for(unsigned int i=0; i<d_str.size(); ++i)
- if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+ if(d_str[i] != y.d_str[i]) return convertUnsignedIntToChar(d_str[i]) < convertUnsignedIntToChar(y.d_str[i]);
return false;
}
if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
else {
for(unsigned int i=0; i<d_str.size(); ++i)
- if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+ if(d_str[i] != y.d_str[i]) return convertUnsignedIntToChar(d_str[i]) > convertUnsignedIntToChar(y.d_str[i]);
return false;
}
if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size();
else {
for(unsigned int i=0; i<d_str.size(); ++i)
- if(d_str[i] != y.d_str[i]) return d_str[i] < y.d_str[i];
+ if(d_str[i] != y.d_str[i]) return convertUnsignedIntToChar(d_str[i]) < convertUnsignedIntToChar(y.d_str[i]);
return true;
}
if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size();
else {
for(unsigned int i=0; i<d_str.size(); ++i)
- if(d_str[i] != y.d_str[i]) return d_str[i] > y.d_str[i];
+ if(d_str[i] != y.d_str[i]) return convertUnsignedIntToChar(d_str[i]) > convertUnsignedIntToChar(y.d_str[i]);
return true;
}
return ( d_str.size() == 0 );
}
- unsigned int operator[] (const std::size_t i) const {
+ /*char operator[] (const std::size_t i) const {
assert( i < d_str.size() );
- return d_str[i];
- }
+ return convertUnsignedIntToChar(d_str[i]);
+ }*/
/*
* Convenience functions
*/
return convertUnsignedIntToChar( d_str[0] );
}
+ char getLastChar() const {
+ assert(d_str.size() != 0);
+ return convertUnsignedIntToChar( d_str[d_str.size() - 1] );
+ }
+
bool isRepeated() const {
if(d_str.size() > 1) {
unsigned int f = d_str[0];
return -1;
}
}
- void getCharSet(std::set<unsigned int> &cset) const;
+
+ void getCharSet(std::set<char> &cset) const;
+
+ std::vector<unsigned int> getVec() const {
+ return d_str;
+ }
};/* class String */
namespace strings {
projects / cvc5.git / commitdiff