From: Tianyi Liang Date: Fri, 21 Feb 2014 00:31:27 +0000 (-0600) Subject: add more tests, and define int.to.str(NEGATIVE)="" X-Git-Tag: cvc5-1.0.0~7078 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be91d86dd0f7b33f7c373c4d9bd40e207af910d2;p=cvc5.git add more tests, and define int.to.str(NEGATIVE)="" --- 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().getNumerator().toUnsignedInt(); - std::string stmp = static_cast( &(std::ostringstream() << i) )->str(); - retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); + std::string stmp = node[0].getConst().getNumerator().toString(); + //std::string stmp = static_cast( &(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(); - 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= i 420)) -(assert (= x (int.to.str i))) -(assert (= x (str.++ y "0" z))) -(assert (not (= y ""))) -(assert (not (= z ""))) - - - -(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/strings/str2int.smt2 b/test/regress/regress0/strings/str2int.smt2 deleted file mode 100644 index b8f0ac5ae..000000000 --- a/test/regress/regress0/strings/str2int.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) -(set-option :strings-exp true) - -(declare-fun i () Int) -(declare-fun s () String) - -(assert (< 67 (str.to.int s))) -(assert (= (str.len s) 2)) -(assert (not (= s "68"))) - -(check-sat) 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/type002.smt2 b/test/regress/regress0/strings/type002.smt2 new file mode 100644 index 000000000..ac4d9ab8a --- /dev/null +++ b/test/regress/regress0/strings/type002.smt2 @@ -0,0 +1,18 @@ +(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun i () Int) + +(assert (>= i 420)) +(assert (= x (int.to.str i))) +(assert (= x (str.++ y "0" z))) +(assert (not (= y ""))) +(assert (not (= z ""))) + + + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/strings/type003.smt2 b/test/regress/regress0/strings/type003.smt2 new file mode 100644 index 000000000..b8f0ac5ae --- /dev/null +++ b/test/regress/regress0/strings/type003.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun i () Int) +(declare-fun s () String) + +(assert (< 67 (str.to.int s))) +(assert (= (str.len s) 2)) +(assert (not (= s "68"))) + +(check-sat)