diff options
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 18 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 18 | ||||
-rw-r--r-- | test/regress/regress0/strings/type001.smt2 | 21 | ||||
-rw-r--r-- | test/regress/regress0/strings/type002.smt2 (renamed from test/regress/regress0/strings/int2str.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress0/strings/type003.smt2 (renamed from test/regress/regress0/strings/str2int.smt2) | 0 |
5 files changed, 45 insertions, 12 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 1df79ccff..ca4a4e75e 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -235,14 +235,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero), // t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0]))); Node num = t[0]; - Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); + Node pret = t;//NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); - /*Node lem = NodeManager::currentNM()->mkNode(kind::IFF, - t.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))), - t[0].eqNode(d_zero)); - new_nodes.push_back(lem);*/ + Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero); + Node lem = NodeManager::currentNM()->mkNode(kind::ITE, nonneg, + NodeManager::currentNM()->mkNode(kind::GT, lenp, d_zero), + t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero) + ); + new_nodes.push_back(lem); + //non-neg Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType()); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ), @@ -262,8 +265,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { argTypes, NodeManager::currentNM()->integerType()), "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) ); + lem = num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero)); + new_nodes.push_back( lem ); Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1); Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)); @@ -318,6 +321,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) ); conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); + conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, nonneg, conc ); new_nodes.push_back( conc ); /*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES, diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 660b7aafe..c459d7d7e 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -446,15 +446,23 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } else if(node.getKind() == kind::STRING_ITOS) { if(node[0].isConst()) { - int i = node[0].getConst<Rational>().getNumerator().toUnsignedInt(); - std::string stmp = static_cast<std::ostringstream*>( &(std::ostringstream() << i) )->str(); - retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); + std::string stmp = node[0].getConst<Rational>().getNumerator().toString(); + //std::string stmp = static_cast<std::ostringstream*>( &(std::ostringstream() << node[0]) )->str(); + if(stmp[0] == '-') { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + } else { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); + } } } else if(node.getKind() == kind::STRING_STOI) { if(node[0].isConst()) { CVC4::String s = node[0].getConst<String>(); - int rt = s.toNumber(); - retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(rt)); + if(s.isNumber()) { + std::string stmp = s.toString(); + retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(stmp.c_str())); + } else { + retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1)); + } } else if(node[0].getKind() == kind::STRING_CONCAT) { for(unsigned i=0; i<node[0].getNumChildren(); ++i) { if(node[0][i].isConst()) { diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2 new file mode 100644 index 000000000..ca93b00e5 --- /dev/null +++ b/test/regress/regress0/strings/type001.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun z () String)
+
+;big num test
+(assert (= x (int.to.str 4785582390527685649)))
+;should be ""
+(assert (= y (int.to.str (- 9))))
+
+;big num
+(assert (= i (str.to.int "783914785582390527685649")))
+;should be -1
+(assert (= j (str.to.int "-783914785582390527685649")))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/int2str.smt2 b/test/regress/regress0/strings/type002.smt2 index ac4d9ab8a..ac4d9ab8a 100644 --- a/test/regress/regress0/strings/int2str.smt2 +++ b/test/regress/regress0/strings/type002.smt2 diff --git a/test/regress/regress0/strings/str2int.smt2 b/test/regress/regress0/strings/type003.smt2 index b8f0ac5ae..b8f0ac5ae 100644 --- a/test/regress/regress0/strings/str2int.smt2 +++ b/test/regress/regress0/strings/type003.smt2 |