Add support for charat in native language, minor cleanup.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index a2e9e6f4739f61541d396970dfbcd48d5d374247..a137cece3f05f773b4a0f39c18d57007b7d919b3 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1997,6 +1997,8 @@ stringTerm[CVC4::Expr& f]
     { f = MK_EXPR(CVC4::kind::STRING_STRCTN, f, f2); }
   | STRING_SUBSTR_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_SUBSTR, f, f2, f3); }
+  | STRING_CHARAT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_CHARAT, f, f2); }
   | STRING_INDEXOF_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_STRIDOF, f, f2, f3); }
   | STRING_REPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 15700decf6cbb0db991ad9d058eb743b9c8aea4c..24358182f4b2e4f54876fe6cfcba44f75fbd65d7 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -68,7 +68,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
       d_infer(c),
       d_infer_exp(c),
       d_nf_pairs(c),
-      d_loop_antec(u),
       d_pregistered_terms_cache(u),
       d_registered_terms_cache(u),
       d_length_lemma_terms_cache(u),

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 9c59f9c71f40613dba7b1816c06492557ba7eb7c..0bdaf7ab5205cf499d0077c1e7d5883818229f3c 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -172,8 +172,6 @@ private:
   void addNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair2( Node n1, Node n2 );
-  // loop ant
-  NodeSet d_loop_antec;
   // preReg cache
   NodeSet d_pregistered_terms_cache;
   NodeSet d_registered_terms_cache;

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 5c89c847265a97a94b4fabced35db8a976679aac..c47c10de0c930d7f993bc68b82783733c92f69e6 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -88,7 +88,8 @@ TESTS = \
   bug768.smt2 \
   username_checker_min.smt2 \
   repl-empty-sem.smt2 \
-  bug799-min.smt2
+  bug799-min.smt2 \
+  strings-charat.cvc
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/strings-charat.cvc b/test/regress/regress0/strings/strings-charat.cvc
new file mode 100644 (file)
index 0000000..71114d3
--- /dev/null
+++ b/test/regress/regress0/strings/strings-charat.cvc
@@ -0,0 +1,9 @@
+% EXPECT: unsat
+
+x : STRING;
+y : STRING;
+
+ASSERT x = CONCAT( "abcd", y );
+ASSERT CHARAT(x,0) = CHARAT(x,2);
+
+CHECKSAT;