summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp127
-rw-r--r--src/theory/strings/theory_strings.cpp3
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp122
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp17
-rw-r--r--src/util/regexp.h21
5 files changed, 241 insertions, 49 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 08568f8da..c1aff6f4b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -313,6 +313,12 @@ class SmtEnginePrivate : public NodeManagerListener {
Node d_ufSubstr;
/**
+ * Function symbol used to implement uninterpreted undefined string
+ * semantics. Needed to deal with partial str2int function.
+ */
+ Node d_ufS2I;
+
+ /**
* Function symbol used to implement uninterpreted division-by-zero
* semantics. Needed to deal with partial division function ("/").
*/
@@ -787,34 +793,6 @@ void SmtEngine::finalOptionsAreSet() {
return;
}
- // for strings
- if(options::stringExp()) {
- if( !d_logic.isQuantified() ) {
- d_logic = d_logic.getUnlockedCopy();
- d_logic.enableQuantifiers();
- Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl;
- }
- if(! options::finiteModelFind.wasSetByUser()) {
- options::finiteModelFind.set( true );
- Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
- }
- if(! options::fmfBoundInt.wasSetByUser()) {
- options::fmfBoundInt.set( true );
- Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
- }
- if(! options::rewriteDivk.wasSetByUser()) {
- options::rewriteDivk.set( true );
- Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
- }
-
- /*
- if(! options::stringFMF.wasSetByUser()) {
- options::stringFMF.set( true );
- Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
- }
- */
- }
-
if(options::bitvectorEagerBitblast()) {
// Eager solver should use the internal decision strategy
options::decisionMode.set(DECISION_STRATEGY_INTERNAL);
@@ -965,6 +943,35 @@ void SmtEngine::setLogicInternal() throw() {
}
}
+
+ // for strings
+ if(options::stringExp()) {
+ if( !d_logic.isQuantified() ) {
+ d_logic = d_logic.getUnlockedCopy();
+ d_logic.enableQuantifiers();
+ d_logic.lock();
+ Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl;
+ }
+ if(! options::finiteModelFind.wasSetByUser()) {
+ options::finiteModelFind.set( true );
+ Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
+ }
+ if(! options::fmfBoundInt.wasSetByUser()) {
+ options::fmfBoundInt.set( true );
+ Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
+ }
+ if(! options::rewriteDivk.wasSetByUser()) {
+ options::rewriteDivk.set( true );
+ Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
+ }
+
+ /*
+ if(! options::stringFMF.wasSetByUser()) {
+ options::stringFMF.set( true );
+ Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
+ }*/
+ }
+
// by default, symmetry breaker is on only for QF_UF
if(! options::ufSymmetryBreaker.wasSetByUser()) {
bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
@@ -1607,6 +1614,61 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
break;
}
+ case kind::STRING_STOI: {
+ if(d_ufS2I.isNull()) {
+ std::vector< TypeNode > argTypes;
+ argTypes.push_back(NodeManager::currentNM()->stringType());
+ d_ufS2I = NodeManager::currentNM()->mkSkolem("__ufS2I",
+ NodeManager::currentNM()->mkFunctionType(
+ argTypes, NodeManager::currentNM()->integerType()),
+ "uf str2int",
+ NodeManager::SKOLEM_EXACT_NAME);
+ }
+ Node cond;
+ if(n[0].isConst()) {
+ CVC4::String s = n[0].getConst<String>();
+ if(s.isNumber()) {
+ cond = NodeManager::currentNM()->mkConst( false );
+ } else {
+ cond = NodeManager::currentNM()->mkConst( true );
+ }
+ } else {
+ Node cc1 = n[0].eqNode(nm->mkConst(::CVC4::String("")));
+ Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+ Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+ Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
+ Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType());
+ Node z2 = NodeManager::currentNM()->mkBoundVar("z2", NodeManager::currentNM()->stringType());
+ Node z3 = NodeManager::currentNM()->mkBoundVar("z3", NodeManager::currentNM()->stringType());
+ Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1, z1, z2, z3);
+ std::vector< Node > vec_n;
+ Node g = NodeManager::currentNM()->mkNode(kind::GEQ, b1, zero);
+ vec_n.push_back(g);
+ g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]), b1);
+ vec_n.push_back(g);
+ g = b1.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z1) );
+ vec_n.push_back(g);
+ g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
+ vec_n.push_back(g);
+ g = n[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
+ vec_n.push_back(g);
+ for(unsigned i=0; i<=9; i++) {
+ char ch[2];
+ ch[0] = i + '0'; ch[1] = '\0';
+ std::string stmp(ch);
+ g = z2.eqNode( nm->mkConst(::CVC4::String(stmp)) ).negate();
+ vec_n.push_back(g);
+ }
+ Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
+ cc2 = NodeManager::currentNM()->mkNode(kind::EXISTS, b1v, cc2);
+ cond = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2));
+ }
+ Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_STOI_TOTAL, n[0]);
+ Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufS2I, n[0]);
+ node = NodeManager::currentNM()->mkNode( kind::ITE, cond, uf, totalf );
+
+ break;
+ }
case kind::DIVISION: {
// partial function: division
if(d_divByZero.isNull()) {
@@ -3123,18 +3185,11 @@ void SmtEnginePrivate::processAssertions() {
// Assertions ARE guaranteed to be rewritten by this point
if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
- dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
CVC4::theory::strings::StringsPreprocess sp;
- std::vector<Node> newNodes;
- newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]);
- sp.simplify( d_assertionsToPreprocess, newNodes );
- if(newNodes.size() > 1) {
- d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
- }
+ sp.simplify( d_assertionsToPreprocess );
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
}
- dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
}
if( d_smt.d_logic.isQuantified() ){
dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index cd583c144..056cd9eb5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -57,7 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
- //d_equalityEngine.addFunctionKind(kind::STRING_STOI_TOTAL);
+ d_equalityEngine.addFunctionKind(kind::STRING_STOI_TOTAL);
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -408,6 +408,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
case kind::STRING_CONCAT:
case kind::STRING_SUBSTR_TOTAL:
case kind::STRING_ITOS:
+ case kind::STRING_STOI_TOTAL:
d_equalityEngine.addTerm(n);
break;
//case kind::STRING_ITOS:
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index b2fa3dcd3..2b8aeddcc 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -249,11 +249,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$",
NodeManager::currentNM()->mkFunctionType(
argTypes, NodeManager::currentNM()->integerType()),
- "uf itos assist P");
+ "uf type conv P");
Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$",
NodeManager::currentNM()->mkFunctionType(
argTypes, NodeManager::currentNM()->integerType()),
- "uf itos assist M");
+ "uf type conv M");
new_nodes.push_back( num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero)) );
new_nodes.push_back( NodeManager::currentNM()->mkNode(kind::GT, lenp, d_zero) );
@@ -319,6 +319,114 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
} else {
throw LogicException("string int.to.str not supported in this release");
}
+ } else if( t.getKind() == kind::STRING_STOI_TOTAL ) {
+ if(options::stringExp()) {
+ Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+ Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
+ Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
+ std::vector< TypeNode > argTypes;
+ argTypes.push_back(NodeManager::currentNM()->integerType());
+ Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$",
+ NodeManager::currentNM()->mkFunctionType(
+ argTypes, NodeManager::currentNM()->integerType()),
+ "uf type conv P");
+ Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$",
+ NodeManager::currentNM()->mkFunctionType(
+ argTypes, NodeManager::currentNM()->integerType()),
+ "uf type conv M");
+
+ Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
+ new_nodes.push_back(t.eqNode(ufP0));
+ //cc1
+ Node cc1 = t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
+ cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(d_zero), cc1);
+ //cc2
+ Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
+ Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType());
+ Node z2 = NodeManager::currentNM()->mkBoundVar("z2", NodeManager::currentNM()->stringType());
+ Node z3 = NodeManager::currentNM()->mkBoundVar("z3", NodeManager::currentNM()->stringType());
+ Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1, z1, z2, z3);
+ std::vector< Node > vec_n;
+ Node g = NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero);
+ vec_n.push_back(g);
+ g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b1);
+ vec_n.push_back(g);
+ g = b1.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z1) );
+ vec_n.push_back(g);
+ g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
+ vec_n.push_back(g);
+ g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
+ vec_n.push_back(g);
+ for(unsigned i=0; i<=9; i++) {
+ char ch[2];
+ ch[0] = i + '0'; ch[1] = '\0';
+ std::string stmp(ch);
+ g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate();
+ vec_n.push_back(g);
+ }
+ Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
+ cc2 = NodeManager::currentNM()->mkNode(kind::EXISTS, b1v, cc2);
+ cc2 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(d_zero), cc2);
+ //cc3
+ Node b2 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->integerType());
+ Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
+ Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
+ NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
+ NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b2));
+ Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
+ Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
+ Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
+ Node w1 = NodeManager::currentNM()->mkBoundVar("w1", NodeManager::currentNM()->stringType());
+ Node w2 = NodeManager::currentNM()->mkBoundVar("w2", NodeManager::currentNM()->stringType());
+ Node b3v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, w1, w2);
+ Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero);
+ Node c3c1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS,
+ NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten),
+ NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one)) ));
+ c3c1 = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::GT, ufx, d_zero), c3c1);
+ c3c1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz, c3c1);
+ Node lstx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]).eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b2, one));
+ Node c3c2 = ufx.eqNode(ufMx);
+ c3c2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, c3c2);
+ Node c3c3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
+ Node c3c4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
+ Node rev = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, w1).eqNode(
+ NodeManager::currentNM()->mkNode(kind::MINUS, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]),
+ NodeManager::currentNM()->mkNode(kind::PLUS, b2, one)));
+ Node ch =
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("0")),
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("1")),
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("2")),
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("3")),
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("4")),
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("5")),
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("6")),
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("7")),
+ NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
+ NodeManager::currentNM()->mkConst(::CVC4::String("8")),
+ NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
+ Node c3c5 = t[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, w1, ch, w2));
+ c3c5 = NodeManager::currentNM()->mkNode(kind::AND, rev, c3c5);
+ c3c5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b3v, c3c5);
+ Node cc3 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, c3c1, c3c2, c3c3, c3c4, c3c5) );
+ cc3 = NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, cc3);
+ cc3 = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, cc3);
+ //conc
+ Node conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
+ new_nodes.push_back( conc );
+ d_cache[t] = t;
+ retNode = t;
+ } else {
+ throw LogicException("string int.to.str not supported in this release");
+ }
} else if( t.getKind() == kind::STRING_STRREPL ) {
if(options::stringExp()) {
Node x = t[0];
@@ -335,8 +443,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ),
skw.eqNode(x) ) );
new_nodes.push_back( rr );
- //rr = cond.negate();
- //new_nodes.push_back( rr );
d_cache[t] = skw;
retNode = skw;
@@ -378,15 +484,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
return retNode;
}
-void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) {
+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+ std::vector< Node > new_nodes;
for( unsigned i=0; i<vec_node.size(); i++ ){
vec_node[i] = simplify( vec_node[i], new_nodes );
}
-}
-
-void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
- std::vector< Node > new_nodes;
- simplify(vec_node, new_nodes);
vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
}
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 112f5eb4f..c3f63f803 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -451,8 +451,21 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) );
}
} else if(node.getKind() == kind::STRING_STOI_TOTAL) {
- //TODO
- Assert(false, "stoi not supported.");
+ if(node[0].isConst()) {
+ CVC4::String s = node[0].getConst<String>();
+ int rt = s.toNumber();
+ retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(rt));
+ } else if(node[0].getKind() == kind::STRING_CONCAT) {
+ for(unsigned i=0; i<node[0].getNumChildren(); ++i) {
+ if(node[0][i].isConst()) {
+ CVC4::String t = node[0][i].getConst<String>();
+ if(!t.isNumber()) {
+ retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(0));
+ break;
+ }
+ }
+ }
+ }
} else if(node.getKind() == kind::STRING_IN_REGEXP) {
retNode = rewriteMembership(node);
}
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 4c69592d4..4891998e5 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -354,6 +354,27 @@ public:
ret_vec.insert( ret_vec.end(), itr, itr + j );
return String(ret_vec);
}
+ bool isNumber() const {
+ for(unsigned int i=0; i<d_str.size(); ++i) {
+ char c = convertUnsignedIntToChar( d_str[i] );
+ if(c<'0' || c>'9') {
+ return false;
+ }
+ }
+ return true;
+ }
+ int toNumber() const {
+ if(isNumber()) {
+ int ret=0;
+ for(unsigned int i=0; i<d_str.size(); ++i) {
+ char c = convertUnsignedIntToChar( d_str[i] );
+ ret = ret * 10 + (int)c - (int)'0';
+ }
+ return ret;
+ } else {
+ return 0;
+ }
+ }
};/* class String */
namespace strings {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback