+
+ void testStrIdOf()
+ {
+ Node a = d_nm->mkConst(String("A"));
+ Node empty = d_nm->mkConst(String(""));
+ Node one = d_nm->mkConst(Rational(1));
+ Node two = d_nm->mkConst(Rational(2));
+
+ std::vector<Node> args;
+ std::vector<Node> vals;
+ Evaluator eval;
+
+ {
+ Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, empty, one);
+ Node r = eval.eval(n, args, vals);
+ TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
+ }
+
+ {
+ Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, a, one);
+ Node r = eval.eval(n, args, vals);
+ TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
+ }
+
+ {
+ Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, empty, two);
+ Node r = eval.eval(n, args, vals);
+ TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
+ }
+
+ {
+ Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, a, two);
+ Node r = eval.eval(n, args, vals);
+ TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
+ }
+ }