diff options
-rw-r--r-- | examples/api/Makefile.am | 8 | ||||
-rw-r--r-- | examples/api/java/Makefile.am | 6 | ||||
-rw-r--r-- | examples/api/java/Strings.java | 67 | ||||
-rw-r--r-- | examples/api/strings.cpp | 101 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 102 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 20 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 10 | ||||
-rw-r--r-- | src/util/regexp.cpp | 52 | ||||
-rw-r--r-- | src/util/regexp.h | 26 |
11 files changed, 314 insertions, 87 deletions
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 <iostream>
+
+//#include <cvc4/cvc4.h> // 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<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]); 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<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()) { @@ -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<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) { @@ -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<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 ) { @@ -653,7 +665,7 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) 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; @@ -663,14 +675,14 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned> &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<unsigned> &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<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; } @@ -1109,13 +1121,13 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes } } -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 ) { @@ -1123,7 +1135,15 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) 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; @@ -1172,19 +1192,19 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &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<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; } @@ -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<Node> vr1, vr2; for( unsigned i=0; i<n.getNumChildren(); i++ ) { @@ -1291,11 +1306,12 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { } 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(); } } @@ -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<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); @@ -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<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()) { @@ -1781,7 +1799,7 @@ void RegExpOpr::disjunctRegExp(Node r, std::vector<Node> &vec_or) { 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; 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<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; @@ -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<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(); 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<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" ); 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<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) ); } } @@ -114,33 +114,33 @@ std::string String::toString() const { 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; } 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<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; } @@ -126,7 +126,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<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; } @@ -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<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; } @@ -146,7 +146,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<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; } @@ -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<unsigned int> &cset) const; + + void getCharSet(std::set<char> &cset) const; + + std::vector<unsigned int> getVec() const { + return d_str; + } };/* class String */ namespace strings { |