From 86afc869b79b76739b400824d8478039717ab88c Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Sat, 6 Dec 2014 13:24:01 -0600 Subject: Added C++/Java api examples; Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input. --- examples/api/Makefile.am | 8 +- examples/api/java/Makefile.am | 6 +- examples/api/java/Strings.java | 67 ++++++++++++++++ examples/api/strings.cpp | 101 ++++++++++++++++++++++++ src/printer/smt2/smt2_printer.cpp | 2 +- src/theory/strings/regexp_operation.cpp | 102 +++++++++++++++---------- src/theory/strings/regexp_operation.h | 20 +++-- src/theory/strings/theory_strings.cpp | 7 +- src/theory/strings/theory_strings_rewriter.cpp | 10 +++ src/util/regexp.cpp | 52 ++++++------- src/util/regexp.h | 26 +++++-- 11 files changed, 314 insertions(+), 87 deletions(-) create mode 100644 examples/api/java/Strings.java create mode 100644 examples/api/strings.cpp diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am index a1455d168..1b3e0b086 100644 --- a/examples/api/Makefile.am +++ b/examples/api/Makefile.am @@ -12,7 +12,8 @@ noinst_PROGRAMS = \ datatypes \ helloworld \ linear_arith \ - sets + sets \ + strings noinst_DATA = @@ -53,6 +54,11 @@ sets_SOURCES = \ 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) diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am index 7216d758e..d12f2877e 100644 --- a/examples/api/java/Makefile.am +++ b/examples/api/java/Makefile.am @@ -9,7 +9,8 @@ noinst_DATA += \ HelloWorld.class \ LinearArith.class \ Datatypes.class \ - PipedInput.class + PipedInput.class \ + Strings.class endif %.class: %.java @@ -23,7 +24,8 @@ EXTRA_DIST = \ HelloWorld.java \ LinearArith.java \ Datatypes.java \ - PipedInput.java + PipedInput.java \ + Strings.java # for installation examplesdir = $(docdir)/$(subdir) diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java new file mode 100644 index 000000000..293118d62 --- /dev/null +++ b/examples/api/java/Strings.java @@ -0,0 +1,67 @@ +/********************* */ +/*! \file Strings.java + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Reasoning about strings with CVC4 via Java API. + ** + ** A simple demonstration of reasoning about strings with CVC4 via Jave API. + **/ + +import edu.nyu.acsys.CVC4.*; + +public class Strings { + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + // Set the logic + smt.setLogic("S"); + + // Produce models + smt.setOption("produce-models", new SExpr(true)); + // The option strings-exp is needed + smt.setOption("strings-exp", new SExpr(true)); + // output-language + smt.setOption("output-language", new SExpr("smt2")); + + // String type + Type string = em.stringType(); + + // Variables + Expr x = em.mkVar("x", string); + Expr y = em.mkVar("y", string); + Expr z = em.mkVar("z", string); + + // String concatenation: x.y + Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, y); + // String concatenation: z.z + Expr rhs = em.mkExpr(Kind.STRING_CONCAT, z, z);; + // x.y = z.z + Expr formula1 = em.mkExpr(Kind.EQUAL, lhs, rhs); + + // Length of y: |y| + Expr leny = em.mkExpr(Kind.STRING_LENGTH, y); + // |y| >= 1 + Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(1))); + + // Make a query + Expr q = em.mkExpr(Kind.AND, + formula1, + formula2); + + // check sat + Result result = smt.checkSat(q); + System.out.println("CVC4 reports: " + q + " is " + result + "."); + + System.out.println(" x = " + smt.getValue(x)); + } +} diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp new file mode 100644 index 000000000..a424c654a --- /dev/null +++ b/examples/api/strings.cpp @@ -0,0 +1,101 @@ +/********************* */ +/*! \file sets.cpp + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Reasoning about strings with CVC4 via C++ API. + ** + ** A simple demonstration of reasoning about strings with CVC4 via C++ API. + **/ + +#include + +//#include // use this after CVC4 is properly installed +#include "smt/smt_engine.h" + +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + + // Set the logic + smt.setLogic("S"); + + // Produce models + smt.setOption("produce-models", true); + + // The option strings-exp is needed + smt.setOption("strings-exp", true); + + // Set output language to SMTLIB2 + std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + + // String type + Type string = em.stringType(); + + // std::string + std::string std_str_ab("ab"); + // CVC4::String + CVC4::String cvc4_str_ab(std_str_ab); + CVC4::String cvc4_str_abc("abc"); + // String constants + Expr ab = em.mkConst(cvc4_str_ab); + Expr abc = em.mkConst(CVC4::String("abc")); + // String variables + Expr x = em.mkVar("x", string); + Expr y = em.mkVar("y", string); + Expr z = em.mkVar("z", string); + + // String concatenation: x.ab.y + Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y); + // String concatenation: abc.z + Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z); + // x.ab.y = abc.z + Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs); + + // Length of y: |y| + Expr leny = em.mkExpr(kind::STRING_LENGTH, y); + // |y| >= 0 + Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0))); + + // Regular expression: (ab[c-e]*f)|g|h + Expr r = em.mkExpr(kind::REGEXP_UNION, + em.mkExpr(kind::REGEXP_CONCAT, + em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))), + em.mkExpr(kind::REGEXP_STAR, + em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))), + em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))), + em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))), + em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("h")))); + + // String variables + Expr s1 = em.mkVar("s1", string); + Expr s2 = em.mkVar("s2", string); + // String concatenation: s1.s2 + Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2); + + // s1.s2 in (ab[c-e]*f)|g|h + Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r); + + // Make a query + Expr q = em.mkExpr(kind::AND, + formula1, + formula2, + formula3); + + // check sat + Result result = smt.checkSat(q); + std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + + if(result == Result::SAT) { + std::cout << " x = " << smt.getValue(x) << std::endl; + std::cout << " s1.s2 = " << smt.getValue(s) << std::endl; + } +} diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b3b548450..2197cd648 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -215,7 +215,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } case kind::CONST_STRING: { - const String& s = n.getConst(); + const std::vector& s = n.getConst().getVec(); out << '"'; for(size_t i = 0; i < s.size(); ++i) { char c = String::convertUnsignedIntToChar(s[i]); diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 2347af3e6..9d83b91a8 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -22,7 +22,7 @@ namespace theory { namespace strings { RegExpOpr::RegExpOpr() - : d_card( 256 ), + : d_lastchar( '\xff' ), RMAXINT( LONG_MAX ) { d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); @@ -240,6 +240,12 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { retNode = d_emptySingleton; break; } + case kind::REGEXP_RANGE: { + CVC4::String a = r[0].getConst(); + CVC4::String b = r[1].getConst(); + retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp; + break; + } case kind::STRING_TO_REGEXP: { Node tmp = Rewriter::rewrite(r[0]); if(tmp.isConst()) { @@ -450,6 +456,12 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ); break; } + case kind::REGEXP_RANGE: { + CVC4::String a = r[0].getConst(); + CVC4::String b = r[1].getConst(); + retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp; + break; + } case kind::STRING_TO_REGEXP: { if(r[0].isConst()) { if(r[0] == d_emptyString) { @@ -556,7 +568,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { 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(); } } @@ -639,13 +651,13 @@ bool RegExpOpr::guessLength( Node r, int &co ) { } } -void RegExpOpr::firstChars( Node r, std::set &pcset, SetNodes &pvset ) { - std::map< Node, std::pair< std::set, SetNodes > >::const_iterator itr = d_fset_cache.find(r); +void RegExpOpr::firstChars( Node r, std::set &pcset, SetNodes &pvset ) { + std::map< Node, std::pair< std::set, 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 cset; + std::set cset; SetNodes vset; int k = r.getKind(); switch( k ) { @@ -653,7 +665,7 @@ void RegExpOpr::firstChars( Node r, std::set &pcset, SetNodes &pvset ) break; } case kind::REGEXP_SIGMA: { - for(unsigned i=0; i &pcset, SetNodes &pvset ) 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] ); } @@ -707,23 +719,23 @@ void RegExpOpr::firstChars( Node r, std::set &pcset, SetNodes &pvset ) 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, SetNodes > p(cset, vset); + std::pair< std::set, SetNodes > p(cset, vset); d_fset_cache[r] = p; if(Trace.isOn("regexp-fset")) { Trace("regexp-fset") << "FSET(" << mkString(r) << ") = {"; - for(std::set::const_iterator itr = cset.begin(); + for(std::set::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; } @@ -1109,13 +1121,13 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes } } -void RegExpOpr::getCharSet( Node r, std::set &pcset, SetNodes &pvset ) { - std::map< Node, std::pair< std::set, SetNodes > >::const_iterator itr = d_cset_cache.find(r); +void RegExpOpr::getCharSet( Node r, std::set &pcset, SetNodes &pvset ) { + std::map< Node, std::pair< std::set, 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 cset; + std::set cset; SetNodes vset; int k = r.getKind(); switch( k ) { @@ -1123,7 +1135,15 @@ void RegExpOpr::getCharSet( Node r, std::set &pcset, SetNodes &pvset ) break; } case kind::REGEXP_SIGMA: { - for(unsigned i=0; i().getFirstChar(); + char b = r[1].getConst().getFirstChar(); + for(char i=a; i<=b; i++) { cset.insert(i); } break; @@ -1172,19 +1192,19 @@ void RegExpOpr::getCharSet( Node r, std::set &pcset, SetNodes &pvset ) 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, SetNodes > p(cset, vset); + std::pair< std::set, SetNodes > p(cset, vset); d_cset_cache[r] = p; Trace("regexp-cset") << "CSET( " << mkString(r) << " ) = { "; - for(std::set::const_iterator itr = cset.begin(); + for(std::set::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; } @@ -1251,11 +1271,6 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { 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 vr1, vr2; for( unsigned i=0; imkNode(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(); } } @@ -1318,7 +1334,7 @@ bool RegExpOpr::testNoRV(Node r) { } 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; @@ -1358,8 +1374,8 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > 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); @@ -1379,20 +1395,20 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > } if(Trace.isOn("regexp-int-debug")) { Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {"; - for(std::vector::const_iterator itr = cset.begin(); + for(std::vector::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::const_iterator itr = cset.begin(); + for(std::vector::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); @@ -1502,8 +1518,10 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { 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(); @@ -1525,12 +1543,12 @@ Node RegExpOpr::complement(Node r, int &ret) { //TODO: var to be extended ret = 0; } else { - std::set cset; + std::set cset; SetNodes vset; firstChars(r, cset, vset); std::vector< Node > vec_nodes; - for(unsigned i=0; imkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)); Node r2; if(cset.find(i) == cset.end()) { @@ -1781,7 +1799,7 @@ void RegExpOpr::disjunctRegExp(Node r, std::vector &vec_or) { std::string RegExpOpr::niceChar(Node r) { if(r.isConst()) { std::string s = r.getConst().toString() ; - return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s ); + return s == "" ? "{E}" : ( s == " " ? "{ }" : s ); } else { std::string ss = "$" + r.toString(); return ss; diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index a522161fb..d170bd17a 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -39,7 +39,7 @@ class RegExpOpr { typedef std::pair< Node, Node > PairNodes; private: - unsigned d_card; + const char d_lastchar; Node d_emptyString; Node d_true; Node d_false; @@ -61,8 +61,8 @@ private: 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, std::set > > d_cset_cache; - std::map< Node, std::pair< std::set, std::set > > d_fset_cache; + std::map< Node, std::pair< std::set, std::set > > d_cset_cache; + std::map< Node, std::pair< std::set, std::set > > 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; @@ -75,18 +75,28 @@ private: Node mkAllExceptOne( char c ); bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2); - void getCharSet( Node r, std::set &pcset, SetNodes &pvset ); + void getCharSet( Node r, std::set &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 &pcset, SetNodes &pvset ); + void firstChars( Node r, std::set &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(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 384d4567b..f394047fa 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -472,12 +472,15 @@ void TheoryStrings::preRegisterTerm(TNode n) { 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() ) { diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 6fcbdfff3..56f6a2ef0 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -358,6 +358,16 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i return false; } } + case kind::REGEXP_RANGE: { + if(s.size() == index_start + 1) { + char a = r[0].getConst().getFirstChar(); + char b = r[1].getConst().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" ); diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index b1b454cfa..1c672d4b9 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -91,10 +91,10 @@ void String::toInternal(const std::string &s) { } } -void String::getCharSet(std::set &cset) const { +void String::getCharSet(std::set &cset) const { for(std::vector::const_iterator itr = d_str.begin(); itr != d_str.end(); itr++) { - cset.insert( *itr ); + cset.insert( convertUnsignedIntToChar(*itr) ); } } @@ -114,33 +114,33 @@ std::string String::toString() const { std::string str; for(unsigned int i=0; i( &(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() << (int)c) )->str(); + } } str += s; } diff --git a/src/util/regexp.h b/src/util/regexp.h index 2b7bfa303..26d468a30 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -116,7 +116,7 @@ public: if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size(); else { for(unsigned int i=0; i y.d_str.size(); else { for(unsigned int i=0; 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; } @@ -136,7 +136,7 @@ public: if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size(); else { for(unsigned int i=0; i y.d_str.size(); else { for(unsigned int i=0; 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; } @@ -188,10 +188,10 @@ public: 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 */ @@ -205,6 +205,11 @@ public: 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]; @@ -307,7 +312,12 @@ public: return -1; } } - void getCharSet(std::set &cset) const; + + void getCharSet(std::set &cset) const; + + std::vector getVec() const { + return d_str; + } };/* class String */ namespace strings { -- cgit v1.2.3