summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.h
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-03-10 17:30:18 -0500
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-03-10 17:30:18 -0500
commit3ed865aa12a94e935038d70b130701045b84a8b8 (patch)
treedf4f45c6606c70eefd8ae35f9eb7de21fecc936a /src/theory/strings/theory_strings.h
parent48e6c3ff2e6f3feac0022b0e2ed8c3c78837dd81 (diff)
adds intro vars length cache
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r--src/theory/strings/theory_strings.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index cbfa481c3..c8a374893 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -156,6 +156,7 @@ private:
bool isNormalFormPair2( Node n1, Node n2 );
// loop ant
NodeSet d_loop_antec;
+ NodeSet d_length_intro_vars;
/////////////////////////////////////////////////////////////////////////////
// MODEL GENERATION
@@ -295,7 +296,7 @@ private:
// Regular Expression
private:
// regular expression memberships
- NodeList d_reg_exp_mem;
+ NodeList d_regexp_memberships;
NodeSet d_regexp_ucached;
NodeSet d_regexp_ccached;
// antecedant for why regexp membership must be true
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback