projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
efd933d
)
Add support for charat in native language, minor cleanup.
author
ajreynol
<andrew.j.reynolds@gmail.com>
Sat, 29 Jul 2017 09:33:27 +0000
(
04:33
-0500)
committer
ajreynol
<andrew.j.reynolds@gmail.com>
Sat, 29 Jul 2017 09:33:27 +0000
(
04:33
-0500)
src/parser/cvc/Cvc.g
patch
|
blob
|
history
src/theory/strings/theory_strings.cpp
patch
|
blob
|
history
src/theory/strings/theory_strings.h
patch
|
blob
|
history
test/regress/regress0/strings/Makefile.am
patch
|
blob
|
history
test/regress/regress0/strings/strings-charat.cvc
[new file with mode: 0644]
patch
|
blob
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); }
{ 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
| 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_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),
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 );
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;
// 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 \
bug768.smt2 \
username_checker_min.smt2 \
repl-empty-sem.smt2 \
- bug799-min.smt2
+ bug799-min.smt2 \
+ strings-charat.cvc
FAILING_TESTS =
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;